gaussian_all_irreducible_append

Exact expanded first-order arithmetic statement

forall b c d e l p. (forall gr_factor_index_append_irreducible_prefix gr_factor_value_append_irreducible_prefix. (exists ge_gap_append_irreducible_prefixindex. ge_gap_append_irreducible_prefixindex + S (gr_factor_index_append_irreducible_prefix) = (l)) -> (((exists ff_h_gprod_append_irreducible_prefixentry. ff_h_gprod_append_irreducible_prefixentry + S (gr_factor_value_append_irreducible_prefix) = S ((S (gr_factor_index_append_irreducible_prefix)) * c)) /\ exists ff_q_gprod_append_irreducible_prefixentry. b = ff_q_gprod_append_irreducible_prefixentry * S ((S (gr_factor_index_append_irreducible_prefix)) * c) + (gr_factor_value_append_irreducible_prefix))) -> (((exists ge_real_positive_append_irreducible_prefixirreduciblecarrier ge_real_negative_append_irreducible_prefixirreduciblecarrier ge_imaginary_positive_append_irreducible_prefixirreduciblecarrier ge_imaginary_negative_append_irreducible_prefixirreduciblecarrier. (exists ge_real_code_append_irreducible_prefixirreduciblecarrierdecode ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode. (((gr_factor_value_append_irreducible_prefix) = ((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode)) * S ((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode)) + ((ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode))) /\ (((((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * (ge_real_positive_append_irreducible_prefixirreduciblecarrier) /\ (ge_real_negative_append_irreducible_prefixirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_real. (((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_append_irreducible_prefixirreduciblecarrier) = 0) /\ (ge_real_negative_append_irreducible_prefixirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_append_irreducible_prefixirreduciblecarrier) /\ (ge_imaginary_negative_append_irreducible_prefixirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_append_irreducible_prefixirreduciblecarrier) = 0) /\ (ge_imaginary_negative_append_irreducible_prefixirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_append_irreducible_prefix)=0)) /\ ((~(exists gr_inverse_append_irreducible_prefixirreduciblenonunit. (exists ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity ge_first_in_append_irreducible_prefixirreduciblenonunitidentity ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity ge_second_in_append_irreducible_prefixirreduciblenonunitidentity. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst. (((gr_factor_value_append_irreducible_prefix) = ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond. (((gr_inverse_append_irreducible_prefixirreduciblenonunit) = ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal = (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_append_irreducible_prefixirreducible gr_second_factor_append_irreducible_prefixirreducible. (exists ge_first_rp_append_irreducible_prefixirreduciblefactorization ge_first_rn_append_irreducible_prefixirreduciblefactorization ge_first_ip_append_irreducible_prefixirreduciblefactorization ge_first_in_append_irreducible_prefixirreduciblefactorization ge_second_rp_append_irreducible_prefixirreduciblefactorization ge_second_rn_append_irreducible_prefixirreduciblefactorization ge_second_ip_append_irreducible_prefixirreduciblefactorization ge_second_in_append_irreducible_prefixirreduciblefactorization. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst. (((gr_first_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond. (((gr_second_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal = (ge_second_rn_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput. (((gr_factor_value_append_irreducible_prefix) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_append_irreducible_prefixirreduciblefirst_unit. (exists ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst. (((gr_first_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond. (((gr_inverse_append_irreducible_prefixirreduciblefirst_unit) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal = (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_append_irreducible_prefixirreduciblesecond_unit. (exists ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst. (((gr_second_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond. (((gr_inverse_append_irreducible_prefixirreduciblesecond_unit) = ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal = (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (forall pfp_i_append_irreducible_preserve pfp_a_append_irreducible_preserve. (exists pfp_gap_append_irreducible_preservebound. pfp_gap_append_irreducible_preservebound + S (pfp_i_append_irreducible_preserve) = (l)) -> (((exists ff_h_pfp_append_irreducible_preserveold. ff_h_pfp_append_irreducible_preserveold + S (pfp_a_append_irreducible_preserve) = S ((S (pfp_i_append_irreducible_preserve)) * c)) /\ exists ff_q_pfp_append_irreducible_preserveold. b = ff_q_pfp_append_irreducible_preserveold * S ((S (pfp_i_append_irreducible_preserve)) * c) + (pfp_a_append_irreducible_preserve))) -> (((exists ff_h_pfp_append_irreducible_preservenew. ff_h_pfp_append_irreducible_preservenew + S (pfp_a_append_irreducible_preserve) = S ((S (pfp_i_append_irreducible_preserve)) * e)) /\ exists ff_q_pfp_append_irreducible_preservenew. d = ff_q_pfp_append_irreducible_preservenew * S ((S (pfp_i_append_irreducible_preserve)) * e) + (pfp_a_append_irreducible_preserve)))) -> (((exists ff_h_gprod_append_irreducible_last. ff_h_gprod_append_irreducible_last + S (p) = S ((S (l)) * e)) /\ exists ff_q_gprod_append_irreducible_last. d = ff_q_gprod_append_irreducible_last * S ((S (l)) * e) + (p))) -> (((exists ge_real_positive_append_irreducible_factorcarrier ge_real_negative_append_irreducible_factorcarrier ge_imaginary_positive_append_irreducible_factorcarrier ge_imaginary_negative_append_irreducible_factorcarrier. (exists ge_real_code_append_irreducible_factorcarrierdecode ge_imaginary_code_append_irreducible_factorcarrierdecode. (((p) = ((ge_real_code_append_irreducible_factorcarrierdecode) + (ge_imaginary_code_append_irreducible_factorcarrierdecode)) * S ((ge_real_code_append_irreducible_factorcarrierdecode) + (ge_imaginary_code_append_irreducible_factorcarrierdecode)) + ((ge_imaginary_code_append_irreducible_factorcarrierdecode) + (ge_imaginary_code_append_irreducible_factorcarrierdecode))) /\ (((((ge_real_code_append_irreducible_factorcarrierdecode) = 2 * (ge_real_positive_append_irreducible_factorcarrier) /\ (ge_real_negative_append_irreducible_factorcarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_factorcarrierdecode_real. (((ge_real_code_append_irreducible_factorcarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_factorcarrierdecode_real + 1 /\ (ge_real_positive_append_irreducible_factorcarrier) = 0) /\ (ge_real_negative_append_irreducible_factorcarrier) = S ge_signed_half_ge_append_irreducible_factorcarrierdecode_real))) /\ ((((ge_imaginary_code_append_irreducible_factorcarrierdecode) = 2 * (ge_imaginary_positive_append_irreducible_factorcarrier) /\ (ge_imaginary_negative_append_irreducible_factorcarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_factorcarrierdecode_imaginary. (((ge_imaginary_code_append_irreducible_factorcarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_factorcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_append_irreducible_factorcarrier) = 0) /\ (ge_imaginary_negative_append_irreducible_factorcarrier) = S ge_signed_half_ge_append_irreducible_factorcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_append_irreducible_factornonunit. (exists ge_first_rp_append_irreducible_factornonunitidentity ge_first_rn_append_irreducible_factornonunitidentity ge_first_ip_append_irreducible_factornonunitidentity ge_first_in_append_irreducible_factornonunitidentity ge_second_rp_append_irreducible_factornonunitidentity ge_second_rn_append_irreducible_factornonunitidentity ge_second_ip_append_irreducible_factornonunitidentity ge_second_in_append_irreducible_factornonunitidentity. ((exists ge_representation_real_code_append_irreducible_factornonunitidentityfirst ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst. (((p) = ((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_factornonunitidentityfirstreal ge_balance_negative_append_irreducible_factornonunitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_factornonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstreal) = S ge_signed_half_append_irreducible_factornonunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentityfirstreal = (ge_first_rn_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_factornonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary) = S ge_signed_half_append_irreducible_factornonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary = (ge_first_in_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factornonunitidentitysecond ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond. (((gr_inverse_append_irreducible_factornonunit) = ((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_factornonunitidentitysecondreal ge_balance_negative_append_irreducible_factornonunitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_factornonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondreal) = S ge_signed_half_append_irreducible_factornonunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentitysecondreal = (ge_second_rn_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_factornonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary) = S ge_signed_half_append_irreducible_factornonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary = (ge_second_in_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factornonunitidentityoutput ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_factornonunitidentityoutputreal ge_balance_negative_append_irreducible_factornonunitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_factornonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputreal) = S ge_signed_half_append_irreducible_factornonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))))))) + ge_balance_negative_append_irreducible_factornonunitidentityoutputreal = (((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))))))) + ge_balance_positive_append_irreducible_factornonunitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_factornonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary) = S ge_signed_half_append_irreducible_factornonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))))))) + ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))))))) + ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_append_irreducible_factor gr_second_factor_append_irreducible_factor. (exists ge_first_rp_append_irreducible_factorfactorization ge_first_rn_append_irreducible_factorfactorization ge_first_ip_append_irreducible_factorfactorization ge_first_in_append_irreducible_factorfactorization ge_second_rp_append_irreducible_factorfactorization ge_second_rn_append_irreducible_factorfactorization ge_second_ip_append_irreducible_factorfactorization ge_second_in_append_irreducible_factorfactorization. ((exists ge_representation_real_code_append_irreducible_factorfactorizationfirst ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst. (((gr_first_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorfactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst)) * S ((ge_representation_real_code_append_irreducible_factorfactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst)) + ((ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst))) /\ ((exists ge_balance_positive_append_irreducible_factorfactorizationfirstreal ge_balance_negative_append_irreducible_factorfactorizationfirstreal. (((((ge_representation_real_code_append_irreducible_factorfactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationfirstreal) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationfirstrealdecode. (((ge_representation_real_code_append_irreducible_factorfactorizationfirst) = 2 * ge_signed_half_append_irreducible_factorfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstreal) = S ge_signed_half_append_irreducible_factorfactorizationfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationfirstreal = (ge_first_rn_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst) = 2 * ge_signed_half_append_irreducible_factorfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary) = S ge_signed_half_append_irreducible_factorfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary = (ge_first_in_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factorfactorizationsecond ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond. (((gr_second_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorfactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond)) * S ((ge_representation_real_code_append_irreducible_factorfactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond)) + ((ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond))) /\ ((exists ge_balance_positive_append_irreducible_factorfactorizationsecondreal ge_balance_negative_append_irreducible_factorfactorizationsecondreal. (((((ge_representation_real_code_append_irreducible_factorfactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationsecondreal) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationsecondrealdecode. (((ge_representation_real_code_append_irreducible_factorfactorizationsecond) = 2 * ge_signed_half_append_irreducible_factorfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationsecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondreal) = S ge_signed_half_append_irreducible_factorfactorizationsecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationsecondreal = (ge_second_rn_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationsecondreal))) /\ (exists ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond) = 2 * ge_signed_half_append_irreducible_factorfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary) = S ge_signed_half_append_irreducible_factorfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary = (ge_second_in_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factorfactorizationoutput ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput. (((p) = ((ge_representation_real_code_append_irreducible_factorfactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput)) * S ((ge_representation_real_code_append_irreducible_factorfactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput)) + ((ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput))) /\ ((exists ge_balance_positive_append_irreducible_factorfactorizationoutputreal ge_balance_negative_append_irreducible_factorfactorizationoutputreal. (((((ge_representation_real_code_append_irreducible_factorfactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationoutputreal) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationoutputrealdecode. (((ge_representation_real_code_append_irreducible_factorfactorizationoutput) = 2 * ge_signed_half_append_irreducible_factorfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputreal) = S ge_signed_half_append_irreducible_factorfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))))))) + ge_balance_negative_append_irreducible_factorfactorizationoutputreal = (((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))))))) + ge_balance_positive_append_irreducible_factorfactorizationoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput) = 2 * ge_signed_half_append_irreducible_factorfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary) = S ge_signed_half_append_irreducible_factorfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))))))) + ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary = (((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))))))) + ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary))))))))) -> (exists gr_inverse_append_irreducible_factorfirst_unit. (exists ge_first_rp_append_irreducible_factorfirst_unitidentity ge_first_rn_append_irreducible_factorfirst_unitidentity ge_first_ip_append_irreducible_factorfirst_unitidentity ge_first_in_append_irreducible_factorfirst_unitidentity ge_second_rp_append_irreducible_factorfirst_unitidentity ge_second_rn_append_irreducible_factorfirst_unitidentity ge_second_ip_append_irreducible_factorfirst_unitidentity ge_second_in_append_irreducible_factorfirst_unitidentity. ((exists ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst. (((gr_first_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal) = S ge_signed_half_append_irreducible_factorfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal = (ge_first_rn_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_factorfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary = (ge_first_in_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond. (((gr_inverse_append_irreducible_factorfirst_unit) = ((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal) = S ge_signed_half_append_irreducible_factorfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal = (ge_second_rn_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_factorfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary = (ge_second_in_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal) = S ge_signed_half_append_irreducible_factorfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_factorfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_append_irreducible_factorsecond_unit. (exists ge_first_rp_append_irreducible_factorsecond_unitidentity ge_first_rn_append_irreducible_factorsecond_unitidentity ge_first_ip_append_irreducible_factorsecond_unitidentity ge_first_in_append_irreducible_factorsecond_unitidentity ge_second_rp_append_irreducible_factorsecond_unitidentity ge_second_rn_append_irreducible_factorsecond_unitidentity ge_second_ip_append_irreducible_factorsecond_unitidentity ge_second_in_append_irreducible_factorsecond_unitidentity. ((exists ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst. (((gr_second_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal) = S ge_signed_half_append_irreducible_factorsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal = (ge_first_rn_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_factorsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary = (ge_first_in_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond. (((gr_inverse_append_irreducible_factorsecond_unit) = ((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal) = S ge_signed_half_append_irreducible_factorsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal = (ge_second_rn_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_factorsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary = (ge_second_in_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal) = S ge_signed_half_append_irreducible_factorsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_factorsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary))))))))))))))) -> (forall gr_factor_index_append_irreducible_full gr_factor_value_append_irreducible_full. (exists ge_gap_append_irreducible_fullindex. ge_gap_append_irreducible_fullindex + S (gr_factor_index_append_irreducible_full) = (S l)) -> (((exists ff_h_gprod_append_irreducible_fullentry. ff_h_gprod_append_irreducible_fullentry + S (gr_factor_value_append_irreducible_full) = S ((S (gr_factor_index_append_irreducible_full)) * e)) /\ exists ff_q_gprod_append_irreducible_fullentry. d = ff_q_gprod_append_irreducible_fullentry * S ((S (gr_factor_index_append_irreducible_full)) * e) + (gr_factor_value_append_irreducible_full))) -> (((exists ge_real_positive_append_irreducible_fullirreduciblecarrier ge_real_negative_append_irreducible_fullirreduciblecarrier ge_imaginary_positive_append_irreducible_fullirreduciblecarrier ge_imaginary_negative_append_irreducible_fullirreduciblecarrier. (exists ge_real_code_append_irreducible_fullirreduciblecarrierdecode ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode. (((gr_factor_value_append_irreducible_full) = ((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode)) * S ((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode)) + ((ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode))) /\ (((((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * (ge_real_positive_append_irreducible_fullirreduciblecarrier) /\ (ge_real_negative_append_irreducible_fullirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_real. (((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_append_irreducible_fullirreduciblecarrier) = 0) /\ (ge_real_negative_append_irreducible_fullirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_append_irreducible_fullirreduciblecarrier) /\ (ge_imaginary_negative_append_irreducible_fullirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_append_irreducible_fullirreduciblecarrier) = 0) /\ (ge_imaginary_negative_append_irreducible_fullirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_append_irreducible_full)=0)) /\ ((~(exists gr_inverse_append_irreducible_fullirreduciblenonunit. (exists ge_first_rp_append_irreducible_fullirreduciblenonunitidentity ge_first_rn_append_irreducible_fullirreduciblenonunitidentity ge_first_ip_append_irreducible_fullirreduciblenonunitidentity ge_first_in_append_irreducible_fullirreduciblenonunitidentity ge_second_rp_append_irreducible_fullirreduciblenonunitidentity ge_second_rn_append_irreducible_fullirreduciblenonunitidentity ge_second_ip_append_irreducible_fullirreduciblenonunitidentity ge_second_in_append_irreducible_fullirreduciblenonunitidentity. ((exists ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst. (((gr_factor_value_append_irreducible_full) = ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal = (ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond. (((gr_inverse_append_irreducible_fullirreduciblenonunit) = ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal = (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary = (ge_second_in_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_append_irreducible_fullirreducible gr_second_factor_append_irreducible_fullirreducible. (exists ge_first_rp_append_irreducible_fullirreduciblefactorization ge_first_rn_append_irreducible_fullirreduciblefactorization ge_first_ip_append_irreducible_fullirreduciblefactorization ge_first_in_append_irreducible_fullirreduciblefactorization ge_second_rp_append_irreducible_fullirreduciblefactorization ge_second_rn_append_irreducible_fullirreduciblefactorization ge_second_ip_append_irreducible_fullirreduciblefactorization ge_second_in_append_irreducible_fullirreduciblefactorization. ((exists ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst. (((gr_first_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal = (ge_first_rn_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond. (((gr_second_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal = (ge_second_rn_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary = (ge_second_in_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput. (((gr_factor_value_append_irreducible_full) = ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_append_irreducible_fullirreduciblefirst_unit. (exists ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity. ((exists ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst. (((gr_first_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal = (ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond. (((gr_inverse_append_irreducible_fullirreduciblefirst_unit) = ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal = (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_append_irreducible_fullirreduciblesecond_unit. (exists ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity. ((exists ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst. (((gr_second_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal = (ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond. (((gr_inverse_append_irreducible_fullirreduciblesecond_unit) = ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal = (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary))))))))))))))))