gaussian_factorization_append_irreducible

Exact expanded first-order arithmetic statement

forall z u b c l p w. (((exists gr_inverse_factor_append_oldunit. (exists ge_first_rp_factor_append_oldunitidentity ge_first_rn_factor_append_oldunitidentity ge_first_ip_factor_append_oldunitidentity ge_first_in_factor_append_oldunitidentity ge_second_rp_factor_append_oldunitidentity ge_second_rn_factor_append_oldunitidentity ge_second_ip_factor_append_oldunitidentity ge_second_in_factor_append_oldunitidentity. ((exists ge_representation_real_code_factor_append_oldunitidentityfirst ge_representation_imaginary_code_factor_append_oldunitidentityfirst. (((u) = ((ge_representation_real_code_factor_append_oldunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldunitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldunitidentityfirstreal ge_balance_negative_factor_append_oldunitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldunitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldunitidentityfirst) = 2 * ge_signed_half_factor_append_oldunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityfirstreal) = S ge_signed_half_factor_append_oldunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentityfirstreal = (ge_first_rn_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldunitidentityfirstimaginary ge_balance_negative_factor_append_oldunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldunitidentityfirst) = 2 * ge_signed_half_factor_append_oldunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityfirstimaginary) = S ge_signed_half_factor_append_oldunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentityfirstimaginary = (ge_first_in_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldunitidentitysecond ge_representation_imaginary_code_factor_append_oldunitidentitysecond. (((gr_inverse_factor_append_oldunit) = ((ge_representation_real_code_factor_append_oldunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldunitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldunitidentitysecondreal ge_balance_negative_factor_append_oldunitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldunitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldunitidentitysecond) = 2 * ge_signed_half_factor_append_oldunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldunitidentitysecondreal) = S ge_signed_half_factor_append_oldunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentitysecondreal = (ge_second_rn_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldunitidentitysecondimaginary ge_balance_negative_factor_append_oldunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldunitidentitysecond) = 2 * ge_signed_half_factor_append_oldunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldunitidentitysecondimaginary) = S ge_signed_half_factor_append_oldunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentitysecondimaginary = (ge_second_in_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldunitidentityoutput ge_representation_imaginary_code_factor_append_oldunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldunitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldunitidentityoutputreal ge_balance_negative_factor_append_oldunitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldunitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldunitidentityoutput) = 2 * ge_signed_half_factor_append_oldunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityoutputreal) = S ge_signed_half_factor_append_oldunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))))))) + ge_balance_negative_factor_append_oldunitidentityoutputreal = (((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))))))) + ge_balance_positive_factor_append_oldunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldunitidentityoutputimaginary ge_balance_negative_factor_append_oldunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldunitidentityoutput) = 2 * ge_signed_half_factor_append_oldunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityoutputimaginary) = S ge_signed_half_factor_append_oldunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))))))) + ge_balance_negative_factor_append_oldunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))))))) + ge_balance_positive_factor_append_oldunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factor_append_oldirreducible gr_factor_value_factor_append_oldirreducible. (exists ge_gap_factor_append_oldirreducibleindex. ge_gap_factor_append_oldirreducibleindex + S (gr_factor_index_factor_append_oldirreducible) = (l)) -> (((exists ff_h_gprod_factor_append_oldirreducibleentry. ff_h_gprod_factor_append_oldirreducibleentry + S (gr_factor_value_factor_append_oldirreducible) = S ((S (gr_factor_index_factor_append_oldirreducible)) * c)) /\ exists ff_q_gprod_factor_append_oldirreducibleentry. b = ff_q_gprod_factor_append_oldirreducibleentry * S ((S (gr_factor_index_factor_append_oldirreducible)) * c) + (gr_factor_value_factor_append_oldirreducible))) -> (((exists ge_real_positive_factor_append_oldirreducibleirreduciblecarrier ge_real_negative_factor_append_oldirreducibleirreduciblecarrier ge_imaginary_positive_factor_append_oldirreducibleirreduciblecarrier ge_imaginary_negative_factor_append_oldirreducibleirreduciblecarrier. (exists ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode. (((gr_factor_value_factor_append_oldirreducible) = ((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factor_append_oldirreducibleirreduciblecarrier) /\ (ge_real_negative_factor_append_oldirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factor_append_oldirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factor_append_oldirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factor_append_oldirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factor_append_oldirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_append_oldirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factor_append_oldirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factor_append_oldirreducible)=0)) /\ ((~(exists gr_inverse_factor_append_oldirreducibleirreduciblenonunit. (exists ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factor_append_oldirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factor_append_oldirreducibleirreduciblenonunit) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_append_oldirreducibleirreducible gr_second_factor_factor_append_oldirreducibleirreducible. (exists ge_first_rp_factor_append_oldirreducibleirreduciblefactorization ge_first_rn_factor_append_oldirreducibleirreduciblefactorization ge_first_ip_factor_append_oldirreducibleirreduciblefactorization ge_first_in_factor_append_oldirreducibleirreduciblefactorization ge_second_rp_factor_append_oldirreducibleirreduciblefactorization ge_second_rn_factor_append_oldirreducibleirreduciblefactorization ge_second_ip_factor_append_oldirreducibleirreduciblefactorization ge_second_in_factor_append_oldirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factor_append_oldirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_append_oldirreducibleirreduciblefirst_unit. (exists ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factor_append_oldirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_append_oldirreducibleirreduciblesecond_unit. (exists ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factor_append_oldirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factor_append_old. ((exists gr_product_trace_factor_append_oldtrace gr_product_scale_factor_append_oldtrace. ((((exists ff_h_gprod_factor_append_oldtracestart. ff_h_gprod_factor_append_oldtracestart + S (6) = S ((S (0)) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtracestart. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtracestart * S ((S (0)) * gr_product_scale_factor_append_oldtrace) + (6))) /\ ((((exists ff_h_gprod_factor_append_oldtraceend. ff_h_gprod_factor_append_oldtraceend + S (gr_factor_product_factor_append_old) = S ((S (l)) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtraceend. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtraceend * S ((S (l)) * gr_product_scale_factor_append_oldtrace) + (gr_factor_product_factor_append_old))) /\ (forall gr_product_index_factor_append_oldtracesteps. (exists ge_gap_factor_append_oldtracestepsindex_bound. ge_gap_factor_append_oldtracestepsindex_bound + S (gr_product_index_factor_append_oldtracesteps) = (l)) -> exists gr_product_factor_factor_append_oldtracesteps gr_product_before_factor_append_oldtracesteps gr_product_after_factor_append_oldtracesteps. ((((exists ff_h_gprod_factor_append_oldtracestepsfactor. ff_h_gprod_factor_append_oldtracestepsfactor + S (gr_product_factor_factor_append_oldtracesteps) = S ((S (gr_product_index_factor_append_oldtracesteps)) * c)) /\ exists ff_q_gprod_factor_append_oldtracestepsfactor. b = ff_q_gprod_factor_append_oldtracestepsfactor * S ((S (gr_product_index_factor_append_oldtracesteps)) * c) + (gr_product_factor_factor_append_oldtracesteps))) /\ ((((exists ff_h_gprod_factor_append_oldtracestepsbefore. ff_h_gprod_factor_append_oldtracestepsbefore + S (gr_product_before_factor_append_oldtracesteps) = S ((S (gr_product_index_factor_append_oldtracesteps)) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtracestepsbefore. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtracestepsbefore * S ((S (gr_product_index_factor_append_oldtracesteps)) * gr_product_scale_factor_append_oldtrace) + (gr_product_before_factor_append_oldtracesteps))) /\ ((((exists ff_h_gprod_factor_append_oldtracestepsafter. ff_h_gprod_factor_append_oldtracestepsafter + S (gr_product_after_factor_append_oldtracesteps) = S ((S (S (gr_product_index_factor_append_oldtracesteps))) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtracestepsafter. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtracestepsafter * S ((S (S (gr_product_index_factor_append_oldtracesteps))) * gr_product_scale_factor_append_oldtrace) + (gr_product_after_factor_append_oldtracesteps))) /\ (exists ge_first_rp_factor_append_oldtracestepsmultiply ge_first_rn_factor_append_oldtracestepsmultiply ge_first_ip_factor_append_oldtracestepsmultiply ge_first_in_factor_append_oldtracestepsmultiply ge_second_rp_factor_append_oldtracestepsmultiply ge_second_rn_factor_append_oldtracestepsmultiply ge_second_ip_factor_append_oldtracestepsmultiply ge_second_in_factor_append_oldtracestepsmultiply. ((exists ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst. (((gr_product_before_factor_append_oldtracesteps) = ((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst)) * S ((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal. (((((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal) = S ge_signed_half_factor_append_oldtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal = (ge_first_rn_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary) = S ge_signed_half_factor_append_oldtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary = (ge_first_in_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldtracestepsmultiplysecond ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond. (((gr_product_factor_factor_append_oldtracesteps) = ((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond)) * S ((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal. (((((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal) = S ge_signed_half_factor_append_oldtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal = (ge_second_rn_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary) = S ge_signed_half_factor_append_oldtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary = (ge_second_in_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput. (((gr_product_after_factor_append_oldtracesteps) = ((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput)) * S ((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal. (((((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal) = S ge_signed_half_factor_append_oldtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))))))) + ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal = (((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))))))) + ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary) = S ge_signed_half_factor_append_oldtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))))))) + ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))))))) + ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factor_append_oldreconstruct ge_first_rn_factor_append_oldreconstruct ge_first_ip_factor_append_oldreconstruct ge_first_in_factor_append_oldreconstruct ge_second_rp_factor_append_oldreconstruct ge_second_rn_factor_append_oldreconstruct ge_second_ip_factor_append_oldreconstruct ge_second_in_factor_append_oldreconstruct. ((exists ge_representation_real_code_factor_append_oldreconstructfirst ge_representation_imaginary_code_factor_append_oldreconstructfirst. (((u) = ((ge_representation_real_code_factor_append_oldreconstructfirst) + (ge_representation_imaginary_code_factor_append_oldreconstructfirst)) * S ((ge_representation_real_code_factor_append_oldreconstructfirst) + (ge_representation_imaginary_code_factor_append_oldreconstructfirst)) + ((ge_representation_imaginary_code_factor_append_oldreconstructfirst) + (ge_representation_imaginary_code_factor_append_oldreconstructfirst))) /\ ((exists ge_balance_positive_factor_append_oldreconstructfirstreal ge_balance_negative_factor_append_oldreconstructfirstreal. (((((ge_representation_real_code_factor_append_oldreconstructfirst) = 2 * (ge_balance_positive_factor_append_oldreconstructfirstreal) /\ (ge_balance_negative_factor_append_oldreconstructfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldreconstructfirstrealdecode. (((ge_representation_real_code_factor_append_oldreconstructfirst) = 2 * ge_signed_half_factor_append_oldreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldreconstructfirstreal) = S ge_signed_half_factor_append_oldreconstructfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructfirstreal = (ge_first_rn_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructfirstreal))) /\ (exists ge_balance_positive_factor_append_oldreconstructfirstimaginary ge_balance_negative_factor_append_oldreconstructfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldreconstructfirst) = 2 * (ge_balance_positive_factor_append_oldreconstructfirstimaginary) /\ (ge_balance_negative_factor_append_oldreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldreconstructfirst) = 2 * ge_signed_half_factor_append_oldreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldreconstructfirstimaginary) = S ge_signed_half_factor_append_oldreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructfirstimaginary = (ge_first_in_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldreconstructsecond ge_representation_imaginary_code_factor_append_oldreconstructsecond. (((gr_factor_product_factor_append_old) = ((ge_representation_real_code_factor_append_oldreconstructsecond) + (ge_representation_imaginary_code_factor_append_oldreconstructsecond)) * S ((ge_representation_real_code_factor_append_oldreconstructsecond) + (ge_representation_imaginary_code_factor_append_oldreconstructsecond)) + ((ge_representation_imaginary_code_factor_append_oldreconstructsecond) + (ge_representation_imaginary_code_factor_append_oldreconstructsecond))) /\ ((exists ge_balance_positive_factor_append_oldreconstructsecondreal ge_balance_negative_factor_append_oldreconstructsecondreal. (((((ge_representation_real_code_factor_append_oldreconstructsecond) = 2 * (ge_balance_positive_factor_append_oldreconstructsecondreal) /\ (ge_balance_negative_factor_append_oldreconstructsecondreal) = 0) \/ exists ge_signed_half_factor_append_oldreconstructsecondrealdecode. (((ge_representation_real_code_factor_append_oldreconstructsecond) = 2 * ge_signed_half_factor_append_oldreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructsecondreal) = 0) /\ (ge_balance_negative_factor_append_oldreconstructsecondreal) = S ge_signed_half_factor_append_oldreconstructsecondrealdecode))) /\ ((ge_second_rp_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructsecondreal = (ge_second_rn_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructsecondreal))) /\ (exists ge_balance_positive_factor_append_oldreconstructsecondimaginary ge_balance_negative_factor_append_oldreconstructsecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldreconstructsecond) = 2 * (ge_balance_positive_factor_append_oldreconstructsecondimaginary) /\ (ge_balance_negative_factor_append_oldreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldreconstructsecond) = 2 * ge_signed_half_factor_append_oldreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldreconstructsecondimaginary) = S ge_signed_half_factor_append_oldreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructsecondimaginary = (ge_second_in_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldreconstructoutput ge_representation_imaginary_code_factor_append_oldreconstructoutput. (((z) = ((ge_representation_real_code_factor_append_oldreconstructoutput) + (ge_representation_imaginary_code_factor_append_oldreconstructoutput)) * S ((ge_representation_real_code_factor_append_oldreconstructoutput) + (ge_representation_imaginary_code_factor_append_oldreconstructoutput)) + ((ge_representation_imaginary_code_factor_append_oldreconstructoutput) + (ge_representation_imaginary_code_factor_append_oldreconstructoutput))) /\ ((exists ge_balance_positive_factor_append_oldreconstructoutputreal ge_balance_negative_factor_append_oldreconstructoutputreal. (((((ge_representation_real_code_factor_append_oldreconstructoutput) = 2 * (ge_balance_positive_factor_append_oldreconstructoutputreal) /\ (ge_balance_negative_factor_append_oldreconstructoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldreconstructoutputrealdecode. (((ge_representation_real_code_factor_append_oldreconstructoutput) = 2 * ge_signed_half_factor_append_oldreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldreconstructoutputreal) = S ge_signed_half_factor_append_oldreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))))))) + ge_balance_negative_factor_append_oldreconstructoutputreal = (((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))))))) + ge_balance_positive_factor_append_oldreconstructoutputreal))) /\ (exists ge_balance_positive_factor_append_oldreconstructoutputimaginary ge_balance_negative_factor_append_oldreconstructoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldreconstructoutput) = 2 * (ge_balance_positive_factor_append_oldreconstructoutputimaginary) /\ (ge_balance_negative_factor_append_oldreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldreconstructoutput) = 2 * ge_signed_half_factor_append_oldreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldreconstructoutputimaginary) = S ge_signed_half_factor_append_oldreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))))))) + ge_balance_negative_factor_append_oldreconstructoutputimaginary = (((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))))))) + ge_balance_positive_factor_append_oldreconstructoutputimaginary)))))))))))))) -> (((exists ge_real_positive_factor_append_primecarrier ge_real_negative_factor_append_primecarrier ge_imaginary_positive_factor_append_primecarrier ge_imaginary_negative_factor_append_primecarrier. (exists ge_real_code_factor_append_primecarrierdecode ge_imaginary_code_factor_append_primecarrierdecode. (((p) = ((ge_real_code_factor_append_primecarrierdecode) + (ge_imaginary_code_factor_append_primecarrierdecode)) * S ((ge_real_code_factor_append_primecarrierdecode) + (ge_imaginary_code_factor_append_primecarrierdecode)) + ((ge_imaginary_code_factor_append_primecarrierdecode) + (ge_imaginary_code_factor_append_primecarrierdecode))) /\ (((((ge_real_code_factor_append_primecarrierdecode) = 2 * (ge_real_positive_factor_append_primecarrier) /\ (ge_real_negative_factor_append_primecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_primecarrierdecode_real. (((ge_real_code_factor_append_primecarrierdecode) = 2 * ge_signed_half_ge_factor_append_primecarrierdecode_real + 1 /\ (ge_real_positive_factor_append_primecarrier) = 0) /\ (ge_real_negative_factor_append_primecarrier) = S ge_signed_half_ge_factor_append_primecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_append_primecarrierdecode) = 2 * (ge_imaginary_positive_factor_append_primecarrier) /\ (ge_imaginary_negative_factor_append_primecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_primecarrierdecode_imaginary. (((ge_imaginary_code_factor_append_primecarrierdecode) = 2 * ge_signed_half_ge_factor_append_primecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_append_primecarrier) = 0) /\ (ge_imaginary_negative_factor_append_primecarrier) = S ge_signed_half_ge_factor_append_primecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_factor_append_primenonunit. (exists ge_first_rp_factor_append_primenonunitidentity ge_first_rn_factor_append_primenonunitidentity ge_first_ip_factor_append_primenonunitidentity ge_first_in_factor_append_primenonunitidentity ge_second_rp_factor_append_primenonunitidentity ge_second_rn_factor_append_primenonunitidentity ge_second_ip_factor_append_primenonunitidentity ge_second_in_factor_append_primenonunitidentity. ((exists ge_representation_real_code_factor_append_primenonunitidentityfirst ge_representation_imaginary_code_factor_append_primenonunitidentityfirst. (((p) = ((ge_representation_real_code_factor_append_primenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_primenonunitidentityfirst)) * S ((ge_representation_real_code_factor_append_primenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_primenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_primenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_primenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_primenonunitidentityfirstreal ge_balance_negative_factor_append_primenonunitidentityfirstreal. (((((ge_representation_real_code_factor_append_primenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_primenonunitidentityfirstreal) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_primenonunitidentityfirst) = 2 * ge_signed_half_factor_append_primenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstreal) = S ge_signed_half_factor_append_primenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentityfirstreal = (ge_first_rn_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_primenonunitidentityfirstimaginary ge_balance_negative_factor_append_primenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_primenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primenonunitidentityfirst) = 2 * ge_signed_half_factor_append_primenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstimaginary) = S ge_signed_half_factor_append_primenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentityfirstimaginary = (ge_first_in_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primenonunitidentitysecond ge_representation_imaginary_code_factor_append_primenonunitidentitysecond. (((gr_inverse_factor_append_primenonunit) = ((ge_representation_real_code_factor_append_primenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_primenonunitidentitysecond)) * S ((ge_representation_real_code_factor_append_primenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_primenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_primenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_primenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_primenonunitidentitysecondreal ge_balance_negative_factor_append_primenonunitidentitysecondreal. (((((ge_representation_real_code_factor_append_primenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_primenonunitidentitysecondreal) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_primenonunitidentitysecond) = 2 * ge_signed_half_factor_append_primenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondreal) = S ge_signed_half_factor_append_primenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentitysecondreal = (ge_second_rn_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_primenonunitidentitysecondimaginary ge_balance_negative_factor_append_primenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_primenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_primenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primenonunitidentitysecond) = 2 * ge_signed_half_factor_append_primenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondimaginary) = S ge_signed_half_factor_append_primenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentitysecondimaginary = (ge_second_in_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primenonunitidentityoutput ge_representation_imaginary_code_factor_append_primenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_primenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_primenonunitidentityoutput)) * S ((ge_representation_real_code_factor_append_primenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_primenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_primenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_primenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_primenonunitidentityoutputreal ge_balance_negative_factor_append_primenonunitidentityoutputreal. (((((ge_representation_real_code_factor_append_primenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_primenonunitidentityoutputreal) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_primenonunitidentityoutput) = 2 * ge_signed_half_factor_append_primenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputreal) = S ge_signed_half_factor_append_primenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))))))) + ge_balance_negative_factor_append_primenonunitidentityoutputreal = (((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))))))) + ge_balance_positive_factor_append_primenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_primenonunitidentityoutputimaginary ge_balance_negative_factor_append_primenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_primenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primenonunitidentityoutput) = 2 * ge_signed_half_factor_append_primenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputimaginary) = S ge_signed_half_factor_append_primenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))))))) + ge_balance_negative_factor_append_primenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))))))) + ge_balance_positive_factor_append_primenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_append_prime gr_second_factor_factor_append_prime. (exists ge_first_rp_factor_append_primefactorization ge_first_rn_factor_append_primefactorization ge_first_ip_factor_append_primefactorization ge_first_in_factor_append_primefactorization ge_second_rp_factor_append_primefactorization ge_second_rn_factor_append_primefactorization ge_second_ip_factor_append_primefactorization ge_second_in_factor_append_primefactorization. ((exists ge_representation_real_code_factor_append_primefactorizationfirst ge_representation_imaginary_code_factor_append_primefactorizationfirst. (((gr_first_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primefactorizationfirst) + (ge_representation_imaginary_code_factor_append_primefactorizationfirst)) * S ((ge_representation_real_code_factor_append_primefactorizationfirst) + (ge_representation_imaginary_code_factor_append_primefactorizationfirst)) + ((ge_representation_imaginary_code_factor_append_primefactorizationfirst) + (ge_representation_imaginary_code_factor_append_primefactorizationfirst))) /\ ((exists ge_balance_positive_factor_append_primefactorizationfirstreal ge_balance_negative_factor_append_primefactorizationfirstreal. (((((ge_representation_real_code_factor_append_primefactorizationfirst) = 2 * (ge_balance_positive_factor_append_primefactorizationfirstreal) /\ (ge_balance_negative_factor_append_primefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_append_primefactorizationfirstrealdecode. (((ge_representation_real_code_factor_append_primefactorizationfirst) = 2 * ge_signed_half_factor_append_primefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_append_primefactorizationfirstreal) = S ge_signed_half_factor_append_primefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationfirstreal = (ge_first_rn_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_append_primefactorizationfirstimaginary ge_balance_negative_factor_append_primefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primefactorizationfirst) = 2 * (ge_balance_positive_factor_append_primefactorizationfirstimaginary) /\ (ge_balance_negative_factor_append_primefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefactorizationfirst) = 2 * ge_signed_half_factor_append_primefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primefactorizationfirstimaginary) = S ge_signed_half_factor_append_primefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationfirstimaginary = (ge_first_in_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primefactorizationsecond ge_representation_imaginary_code_factor_append_primefactorizationsecond. (((gr_second_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primefactorizationsecond) + (ge_representation_imaginary_code_factor_append_primefactorizationsecond)) * S ((ge_representation_real_code_factor_append_primefactorizationsecond) + (ge_representation_imaginary_code_factor_append_primefactorizationsecond)) + ((ge_representation_imaginary_code_factor_append_primefactorizationsecond) + (ge_representation_imaginary_code_factor_append_primefactorizationsecond))) /\ ((exists ge_balance_positive_factor_append_primefactorizationsecondreal ge_balance_negative_factor_append_primefactorizationsecondreal. (((((ge_representation_real_code_factor_append_primefactorizationsecond) = 2 * (ge_balance_positive_factor_append_primefactorizationsecondreal) /\ (ge_balance_negative_factor_append_primefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_append_primefactorizationsecondrealdecode. (((ge_representation_real_code_factor_append_primefactorizationsecond) = 2 * ge_signed_half_factor_append_primefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_append_primefactorizationsecondreal) = S ge_signed_half_factor_append_primefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationsecondreal = (ge_second_rn_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_append_primefactorizationsecondimaginary ge_balance_negative_factor_append_primefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_primefactorizationsecond) = 2 * (ge_balance_positive_factor_append_primefactorizationsecondimaginary) /\ (ge_balance_negative_factor_append_primefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefactorizationsecond) = 2 * ge_signed_half_factor_append_primefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primefactorizationsecondimaginary) = S ge_signed_half_factor_append_primefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationsecondimaginary = (ge_second_in_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primefactorizationoutput ge_representation_imaginary_code_factor_append_primefactorizationoutput. (((p) = ((ge_representation_real_code_factor_append_primefactorizationoutput) + (ge_representation_imaginary_code_factor_append_primefactorizationoutput)) * S ((ge_representation_real_code_factor_append_primefactorizationoutput) + (ge_representation_imaginary_code_factor_append_primefactorizationoutput)) + ((ge_representation_imaginary_code_factor_append_primefactorizationoutput) + (ge_representation_imaginary_code_factor_append_primefactorizationoutput))) /\ ((exists ge_balance_positive_factor_append_primefactorizationoutputreal ge_balance_negative_factor_append_primefactorizationoutputreal. (((((ge_representation_real_code_factor_append_primefactorizationoutput) = 2 * (ge_balance_positive_factor_append_primefactorizationoutputreal) /\ (ge_balance_negative_factor_append_primefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_append_primefactorizationoutputrealdecode. (((ge_representation_real_code_factor_append_primefactorizationoutput) = 2 * ge_signed_half_factor_append_primefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_append_primefactorizationoutputreal) = S ge_signed_half_factor_append_primefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))))))) + ge_balance_negative_factor_append_primefactorizationoutputreal = (((((((ge_first_rp_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))))))) + ge_balance_positive_factor_append_primefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_append_primefactorizationoutputimaginary ge_balance_negative_factor_append_primefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primefactorizationoutput) = 2 * (ge_balance_positive_factor_append_primefactorizationoutputimaginary) /\ (ge_balance_negative_factor_append_primefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefactorizationoutput) = 2 * ge_signed_half_factor_append_primefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primefactorizationoutputimaginary) = S ge_signed_half_factor_append_primefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))))))) + ge_balance_negative_factor_append_primefactorizationoutputimaginary = (((((((ge_first_rp_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))))))) + ge_balance_positive_factor_append_primefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_append_primefirst_unit. (exists ge_first_rp_factor_append_primefirst_unitidentity ge_first_rn_factor_append_primefirst_unitidentity ge_first_ip_factor_append_primefirst_unitidentity ge_first_in_factor_append_primefirst_unitidentity ge_second_rp_factor_append_primefirst_unitidentity ge_second_rn_factor_append_primefirst_unitidentity ge_second_ip_factor_append_primefirst_unitidentity ge_second_in_factor_append_primefirst_unitidentity. ((exists ge_representation_real_code_factor_append_primefirst_unitidentityfirst ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst. (((gr_first_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_primefirst_unitidentityfirstreal ge_balance_negative_factor_append_primefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_primefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstreal) = S ge_signed_half_factor_append_primefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentityfirstreal = (ge_first_rn_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_primefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_append_primefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary = (ge_first_in_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primefirst_unitidentitysecond ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond. (((gr_inverse_factor_append_primefirst_unit) = ((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_primefirst_unitidentitysecondreal ge_balance_negative_factor_append_primefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_primefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondreal) = S ge_signed_half_factor_append_primefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentitysecondreal = (ge_second_rn_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_primefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_append_primefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary = (ge_second_in_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primefirst_unitidentityoutput ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_primefirst_unitidentityoutputreal ge_balance_negative_factor_append_primefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_primefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputreal) = S ge_signed_half_factor_append_primefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))))))) + ge_balance_negative_factor_append_primefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))))))) + ge_balance_positive_factor_append_primefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_primefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_append_primefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))))))) + ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))))))) + ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_append_primesecond_unit. (exists ge_first_rp_factor_append_primesecond_unitidentity ge_first_rn_factor_append_primesecond_unitidentity ge_first_ip_factor_append_primesecond_unitidentity ge_first_in_factor_append_primesecond_unitidentity ge_second_rp_factor_append_primesecond_unitidentity ge_second_rn_factor_append_primesecond_unitidentity ge_second_ip_factor_append_primesecond_unitidentity ge_second_in_factor_append_primesecond_unitidentity. ((exists ge_representation_real_code_factor_append_primesecond_unitidentityfirst ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst. (((gr_second_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_primesecond_unitidentityfirstreal ge_balance_negative_factor_append_primesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_primesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstreal) = S ge_signed_half_factor_append_primesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentityfirstreal = (ge_first_rn_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_primesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_append_primesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary = (ge_first_in_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primesecond_unitidentitysecond ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond. (((gr_inverse_factor_append_primesecond_unit) = ((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_primesecond_unitidentitysecondreal ge_balance_negative_factor_append_primesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_primesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondreal) = S ge_signed_half_factor_append_primesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentitysecondreal = (ge_second_rn_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_primesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_append_primesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary = (ge_second_in_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primesecond_unitidentityoutput ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_primesecond_unitidentityoutputreal ge_balance_negative_factor_append_primesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_primesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputreal) = S ge_signed_half_factor_append_primesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))))))) + ge_balance_negative_factor_append_primesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))))))) + ge_balance_positive_factor_append_primesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_primesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_append_primesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))))))) + ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))))))) + ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary))))))))))))))) -> (exists ge_first_rp_factor_append_equation ge_first_rn_factor_append_equation ge_first_ip_factor_append_equation ge_first_in_factor_append_equation ge_second_rp_factor_append_equation ge_second_rn_factor_append_equation ge_second_ip_factor_append_equation ge_second_in_factor_append_equation. ((exists ge_representation_real_code_factor_append_equationfirst ge_representation_imaginary_code_factor_append_equationfirst. (((z) = ((ge_representation_real_code_factor_append_equationfirst) + (ge_representation_imaginary_code_factor_append_equationfirst)) * S ((ge_representation_real_code_factor_append_equationfirst) + (ge_representation_imaginary_code_factor_append_equationfirst)) + ((ge_representation_imaginary_code_factor_append_equationfirst) + (ge_representation_imaginary_code_factor_append_equationfirst))) /\ ((exists ge_balance_positive_factor_append_equationfirstreal ge_balance_negative_factor_append_equationfirstreal. (((((ge_representation_real_code_factor_append_equationfirst) = 2 * (ge_balance_positive_factor_append_equationfirstreal) /\ (ge_balance_negative_factor_append_equationfirstreal) = 0) \/ exists ge_signed_half_factor_append_equationfirstrealdecode. (((ge_representation_real_code_factor_append_equationfirst) = 2 * ge_signed_half_factor_append_equationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_equationfirstreal) = 0) /\ (ge_balance_negative_factor_append_equationfirstreal) = S ge_signed_half_factor_append_equationfirstrealdecode))) /\ ((ge_first_rp_factor_append_equation) + ge_balance_negative_factor_append_equationfirstreal = (ge_first_rn_factor_append_equation) + ge_balance_positive_factor_append_equationfirstreal))) /\ (exists ge_balance_positive_factor_append_equationfirstimaginary ge_balance_negative_factor_append_equationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_equationfirst) = 2 * (ge_balance_positive_factor_append_equationfirstimaginary) /\ (ge_balance_negative_factor_append_equationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_equationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_equationfirst) = 2 * ge_signed_half_factor_append_equationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_equationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_equationfirstimaginary) = S ge_signed_half_factor_append_equationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_equation) + ge_balance_negative_factor_append_equationfirstimaginary = (ge_first_in_factor_append_equation) + ge_balance_positive_factor_append_equationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_equationsecond ge_representation_imaginary_code_factor_append_equationsecond. (((p) = ((ge_representation_real_code_factor_append_equationsecond) + (ge_representation_imaginary_code_factor_append_equationsecond)) * S ((ge_representation_real_code_factor_append_equationsecond) + (ge_representation_imaginary_code_factor_append_equationsecond)) + ((ge_representation_imaginary_code_factor_append_equationsecond) + (ge_representation_imaginary_code_factor_append_equationsecond))) /\ ((exists ge_balance_positive_factor_append_equationsecondreal ge_balance_negative_factor_append_equationsecondreal. (((((ge_representation_real_code_factor_append_equationsecond) = 2 * (ge_balance_positive_factor_append_equationsecondreal) /\ (ge_balance_negative_factor_append_equationsecondreal) = 0) \/ exists ge_signed_half_factor_append_equationsecondrealdecode. (((ge_representation_real_code_factor_append_equationsecond) = 2 * ge_signed_half_factor_append_equationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_equationsecondreal) = 0) /\ (ge_balance_negative_factor_append_equationsecondreal) = S ge_signed_half_factor_append_equationsecondrealdecode))) /\ ((ge_second_rp_factor_append_equation) + ge_balance_negative_factor_append_equationsecondreal = (ge_second_rn_factor_append_equation) + ge_balance_positive_factor_append_equationsecondreal))) /\ (exists ge_balance_positive_factor_append_equationsecondimaginary ge_balance_negative_factor_append_equationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_equationsecond) = 2 * (ge_balance_positive_factor_append_equationsecondimaginary) /\ (ge_balance_negative_factor_append_equationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_equationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_equationsecond) = 2 * ge_signed_half_factor_append_equationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_equationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_equationsecondimaginary) = S ge_signed_half_factor_append_equationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_equation) + ge_balance_negative_factor_append_equationsecondimaginary = (ge_second_in_factor_append_equation) + ge_balance_positive_factor_append_equationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_equationoutput ge_representation_imaginary_code_factor_append_equationoutput. (((w) = ((ge_representation_real_code_factor_append_equationoutput) + (ge_representation_imaginary_code_factor_append_equationoutput)) * S ((ge_representation_real_code_factor_append_equationoutput) + (ge_representation_imaginary_code_factor_append_equationoutput)) + ((ge_representation_imaginary_code_factor_append_equationoutput) + (ge_representation_imaginary_code_factor_append_equationoutput))) /\ ((exists ge_balance_positive_factor_append_equationoutputreal ge_balance_negative_factor_append_equationoutputreal. (((((ge_representation_real_code_factor_append_equationoutput) = 2 * (ge_balance_positive_factor_append_equationoutputreal) /\ (ge_balance_negative_factor_append_equationoutputreal) = 0) \/ exists ge_signed_half_factor_append_equationoutputrealdecode. (((ge_representation_real_code_factor_append_equationoutput) = 2 * ge_signed_half_factor_append_equationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_equationoutputreal) = 0) /\ (ge_balance_negative_factor_append_equationoutputreal) = S ge_signed_half_factor_append_equationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_equation) * (ge_second_rp_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_rn_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_in_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_ip_factor_append_equation))))))) + ge_balance_negative_factor_append_equationoutputreal = (((((((ge_first_rp_factor_append_equation) * (ge_second_rn_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_rp_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_ip_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_in_factor_append_equation))))))) + ge_balance_positive_factor_append_equationoutputreal))) /\ (exists ge_balance_positive_factor_append_equationoutputimaginary ge_balance_negative_factor_append_equationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_equationoutput) = 2 * (ge_balance_positive_factor_append_equationoutputimaginary) /\ (ge_balance_negative_factor_append_equationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_equationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_equationoutput) = 2 * ge_signed_half_factor_append_equationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_equationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_equationoutputimaginary) = S ge_signed_half_factor_append_equationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_equation) * (ge_second_ip_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_in_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_rp_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_rn_factor_append_equation))))))) + ge_balance_negative_factor_append_equationoutputimaginary = (((((((ge_first_rp_factor_append_equation) * (ge_second_in_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_ip_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_rn_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_rp_factor_append_equation))))))) + ge_balance_positive_factor_append_equationoutputimaginary))))))))) -> exists d e. (((exists gr_inverse_factor_append_newunit. (exists ge_first_rp_factor_append_newunitidentity ge_first_rn_factor_append_newunitidentity ge_first_ip_factor_append_newunitidentity ge_first_in_factor_append_newunitidentity ge_second_rp_factor_append_newunitidentity ge_second_rn_factor_append_newunitidentity ge_second_ip_factor_append_newunitidentity ge_second_in_factor_append_newunitidentity. ((exists ge_representation_real_code_factor_append_newunitidentityfirst ge_representation_imaginary_code_factor_append_newunitidentityfirst. (((u) = ((ge_representation_real_code_factor_append_newunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newunitidentityfirst)) * S ((ge_representation_real_code_factor_append_newunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newunitidentityfirstreal ge_balance_negative_factor_append_newunitidentityfirstreal. (((((ge_representation_real_code_factor_append_newunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newunitidentityfirstreal) /\ (ge_balance_negative_factor_append_newunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newunitidentityfirst) = 2 * ge_signed_half_factor_append_newunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newunitidentityfirstreal) = S ge_signed_half_factor_append_newunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentityfirstreal = (ge_first_rn_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newunitidentityfirstimaginary ge_balance_negative_factor_append_newunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newunitidentityfirst) = 2 * ge_signed_half_factor_append_newunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newunitidentityfirstimaginary) = S ge_signed_half_factor_append_newunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentityfirstimaginary = (ge_first_in_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newunitidentitysecond ge_representation_imaginary_code_factor_append_newunitidentitysecond. (((gr_inverse_factor_append_newunit) = ((ge_representation_real_code_factor_append_newunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newunitidentitysecond)) * S ((ge_representation_real_code_factor_append_newunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newunitidentitysecondreal ge_balance_negative_factor_append_newunitidentitysecondreal. (((((ge_representation_real_code_factor_append_newunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newunitidentitysecondreal) /\ (ge_balance_negative_factor_append_newunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newunitidentitysecond) = 2 * ge_signed_half_factor_append_newunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newunitidentitysecondreal) = S ge_signed_half_factor_append_newunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentitysecondreal = (ge_second_rn_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newunitidentitysecondimaginary ge_balance_negative_factor_append_newunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newunitidentitysecond) = 2 * ge_signed_half_factor_append_newunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newunitidentitysecondimaginary) = S ge_signed_half_factor_append_newunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentitysecondimaginary = (ge_second_in_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newunitidentityoutput ge_representation_imaginary_code_factor_append_newunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newunitidentityoutput)) * S ((ge_representation_real_code_factor_append_newunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newunitidentityoutputreal ge_balance_negative_factor_append_newunitidentityoutputreal. (((((ge_representation_real_code_factor_append_newunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newunitidentityoutputreal) /\ (ge_balance_negative_factor_append_newunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newunitidentityoutput) = 2 * ge_signed_half_factor_append_newunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newunitidentityoutputreal) = S ge_signed_half_factor_append_newunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))))))) + ge_balance_negative_factor_append_newunitidentityoutputreal = (((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))))))) + ge_balance_positive_factor_append_newunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newunitidentityoutputimaginary ge_balance_negative_factor_append_newunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newunitidentityoutput) = 2 * ge_signed_half_factor_append_newunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newunitidentityoutputimaginary) = S ge_signed_half_factor_append_newunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))))))) + ge_balance_negative_factor_append_newunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))))))) + ge_balance_positive_factor_append_newunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factor_append_newirreducible gr_factor_value_factor_append_newirreducible. (exists ge_gap_factor_append_newirreducibleindex. ge_gap_factor_append_newirreducibleindex + S (gr_factor_index_factor_append_newirreducible) = (S l)) -> (((exists ff_h_gprod_factor_append_newirreducibleentry. ff_h_gprod_factor_append_newirreducibleentry + S (gr_factor_value_factor_append_newirreducible) = S ((S (gr_factor_index_factor_append_newirreducible)) * e)) /\ exists ff_q_gprod_factor_append_newirreducibleentry. d = ff_q_gprod_factor_append_newirreducibleentry * S ((S (gr_factor_index_factor_append_newirreducible)) * e) + (gr_factor_value_factor_append_newirreducible))) -> (((exists ge_real_positive_factor_append_newirreducibleirreduciblecarrier ge_real_negative_factor_append_newirreducibleirreduciblecarrier ge_imaginary_positive_factor_append_newirreducibleirreduciblecarrier ge_imaginary_negative_factor_append_newirreducibleirreduciblecarrier. (exists ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode. (((gr_factor_value_factor_append_newirreducible) = ((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factor_append_newirreducibleirreduciblecarrier) /\ (ge_real_negative_factor_append_newirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factor_append_newirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factor_append_newirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factor_append_newirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factor_append_newirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_append_newirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factor_append_newirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factor_append_newirreducible)=0)) /\ ((~(exists gr_inverse_factor_append_newirreducibleirreduciblenonunit. (exists ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factor_append_newirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factor_append_newirreducibleirreduciblenonunit) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_append_newirreducibleirreducible gr_second_factor_factor_append_newirreducibleirreducible. (exists ge_first_rp_factor_append_newirreducibleirreduciblefactorization ge_first_rn_factor_append_newirreducibleirreduciblefactorization ge_first_ip_factor_append_newirreducibleirreduciblefactorization ge_first_in_factor_append_newirreducibleirreduciblefactorization ge_second_rp_factor_append_newirreducibleirreduciblefactorization ge_second_rn_factor_append_newirreducibleirreduciblefactorization ge_second_ip_factor_append_newirreducibleirreduciblefactorization ge_second_in_factor_append_newirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factor_append_newirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_append_newirreducibleirreduciblefirst_unit. (exists ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factor_append_newirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_append_newirreducibleirreduciblesecond_unit. (exists ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factor_append_newirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factor_append_new. ((exists gr_product_trace_factor_append_newtrace gr_product_scale_factor_append_newtrace. ((((exists ff_h_gprod_factor_append_newtracestart. ff_h_gprod_factor_append_newtracestart + S (6) = S ((S (0)) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtracestart. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtracestart * S ((S (0)) * gr_product_scale_factor_append_newtrace) + (6))) /\ ((((exists ff_h_gprod_factor_append_newtraceend. ff_h_gprod_factor_append_newtraceend + S (gr_factor_product_factor_append_new) = S ((S (S l)) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtraceend. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtraceend * S ((S (S l)) * gr_product_scale_factor_append_newtrace) + (gr_factor_product_factor_append_new))) /\ (forall gr_product_index_factor_append_newtracesteps. (exists ge_gap_factor_append_newtracestepsindex_bound. ge_gap_factor_append_newtracestepsindex_bound + S (gr_product_index_factor_append_newtracesteps) = (S l)) -> exists gr_product_factor_factor_append_newtracesteps gr_product_before_factor_append_newtracesteps gr_product_after_factor_append_newtracesteps. ((((exists ff_h_gprod_factor_append_newtracestepsfactor. ff_h_gprod_factor_append_newtracestepsfactor + S (gr_product_factor_factor_append_newtracesteps) = S ((S (gr_product_index_factor_append_newtracesteps)) * e)) /\ exists ff_q_gprod_factor_append_newtracestepsfactor. d = ff_q_gprod_factor_append_newtracestepsfactor * S ((S (gr_product_index_factor_append_newtracesteps)) * e) + (gr_product_factor_factor_append_newtracesteps))) /\ ((((exists ff_h_gprod_factor_append_newtracestepsbefore. ff_h_gprod_factor_append_newtracestepsbefore + S (gr_product_before_factor_append_newtracesteps) = S ((S (gr_product_index_factor_append_newtracesteps)) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtracestepsbefore. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtracestepsbefore * S ((S (gr_product_index_factor_append_newtracesteps)) * gr_product_scale_factor_append_newtrace) + (gr_product_before_factor_append_newtracesteps))) /\ ((((exists ff_h_gprod_factor_append_newtracestepsafter. ff_h_gprod_factor_append_newtracestepsafter + S (gr_product_after_factor_append_newtracesteps) = S ((S (S (gr_product_index_factor_append_newtracesteps))) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtracestepsafter. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtracestepsafter * S ((S (S (gr_product_index_factor_append_newtracesteps))) * gr_product_scale_factor_append_newtrace) + (gr_product_after_factor_append_newtracesteps))) /\ (exists ge_first_rp_factor_append_newtracestepsmultiply ge_first_rn_factor_append_newtracestepsmultiply ge_first_ip_factor_append_newtracestepsmultiply ge_first_in_factor_append_newtracestepsmultiply ge_second_rp_factor_append_newtracestepsmultiply ge_second_rn_factor_append_newtracestepsmultiply ge_second_ip_factor_append_newtracestepsmultiply ge_second_in_factor_append_newtracestepsmultiply. ((exists ge_representation_real_code_factor_append_newtracestepsmultiplyfirst ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst. (((gr_product_before_factor_append_newtracesteps) = ((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst)) * S ((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal. (((((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal) = S ge_signed_half_factor_append_newtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal = (ge_first_rn_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary) = S ge_signed_half_factor_append_newtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary = (ge_first_in_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newtracestepsmultiplysecond ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond. (((gr_product_factor_factor_append_newtracesteps) = ((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond)) * S ((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factor_append_newtracestepsmultiplysecondreal ge_balance_negative_factor_append_newtracestepsmultiplysecondreal. (((((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplysecondreal) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_newtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondreal) = S ge_signed_half_factor_append_newtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplysecondreal = (ge_second_rn_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_newtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary) = S ge_signed_half_factor_append_newtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary = (ge_second_in_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newtracestepsmultiplyoutput ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput. (((gr_product_after_factor_append_newtracesteps) = ((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput)) * S ((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal. (((((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal) = S ge_signed_half_factor_append_newtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))))))) + ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal = (((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))))))) + ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary) = S ge_signed_half_factor_append_newtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))))))) + ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))))))) + ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factor_append_newreconstruct ge_first_rn_factor_append_newreconstruct ge_first_ip_factor_append_newreconstruct ge_first_in_factor_append_newreconstruct ge_second_rp_factor_append_newreconstruct ge_second_rn_factor_append_newreconstruct ge_second_ip_factor_append_newreconstruct ge_second_in_factor_append_newreconstruct. ((exists ge_representation_real_code_factor_append_newreconstructfirst ge_representation_imaginary_code_factor_append_newreconstructfirst. (((u) = ((ge_representation_real_code_factor_append_newreconstructfirst) + (ge_representation_imaginary_code_factor_append_newreconstructfirst)) * S ((ge_representation_real_code_factor_append_newreconstructfirst) + (ge_representation_imaginary_code_factor_append_newreconstructfirst)) + ((ge_representation_imaginary_code_factor_append_newreconstructfirst) + (ge_representation_imaginary_code_factor_append_newreconstructfirst))) /\ ((exists ge_balance_positive_factor_append_newreconstructfirstreal ge_balance_negative_factor_append_newreconstructfirstreal. (((((ge_representation_real_code_factor_append_newreconstructfirst) = 2 * (ge_balance_positive_factor_append_newreconstructfirstreal) /\ (ge_balance_negative_factor_append_newreconstructfirstreal) = 0) \/ exists ge_signed_half_factor_append_newreconstructfirstrealdecode. (((ge_representation_real_code_factor_append_newreconstructfirst) = 2 * ge_signed_half_factor_append_newreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newreconstructfirstreal) = 0) /\ (ge_balance_negative_factor_append_newreconstructfirstreal) = S ge_signed_half_factor_append_newreconstructfirstrealdecode))) /\ ((ge_first_rp_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructfirstreal = (ge_first_rn_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructfirstreal))) /\ (exists ge_balance_positive_factor_append_newreconstructfirstimaginary ge_balance_negative_factor_append_newreconstructfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newreconstructfirst) = 2 * (ge_balance_positive_factor_append_newreconstructfirstimaginary) /\ (ge_balance_negative_factor_append_newreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newreconstructfirst) = 2 * ge_signed_half_factor_append_newreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newreconstructfirstimaginary) = S ge_signed_half_factor_append_newreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructfirstimaginary = (ge_first_in_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newreconstructsecond ge_representation_imaginary_code_factor_append_newreconstructsecond. (((gr_factor_product_factor_append_new) = ((ge_representation_real_code_factor_append_newreconstructsecond) + (ge_representation_imaginary_code_factor_append_newreconstructsecond)) * S ((ge_representation_real_code_factor_append_newreconstructsecond) + (ge_representation_imaginary_code_factor_append_newreconstructsecond)) + ((ge_representation_imaginary_code_factor_append_newreconstructsecond) + (ge_representation_imaginary_code_factor_append_newreconstructsecond))) /\ ((exists ge_balance_positive_factor_append_newreconstructsecondreal ge_balance_negative_factor_append_newreconstructsecondreal. (((((ge_representation_real_code_factor_append_newreconstructsecond) = 2 * (ge_balance_positive_factor_append_newreconstructsecondreal) /\ (ge_balance_negative_factor_append_newreconstructsecondreal) = 0) \/ exists ge_signed_half_factor_append_newreconstructsecondrealdecode. (((ge_representation_real_code_factor_append_newreconstructsecond) = 2 * ge_signed_half_factor_append_newreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newreconstructsecondreal) = 0) /\ (ge_balance_negative_factor_append_newreconstructsecondreal) = S ge_signed_half_factor_append_newreconstructsecondrealdecode))) /\ ((ge_second_rp_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructsecondreal = (ge_second_rn_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructsecondreal))) /\ (exists ge_balance_positive_factor_append_newreconstructsecondimaginary ge_balance_negative_factor_append_newreconstructsecondimaginary. (((((ge_representation_imaginary_code_factor_append_newreconstructsecond) = 2 * (ge_balance_positive_factor_append_newreconstructsecondimaginary) /\ (ge_balance_negative_factor_append_newreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newreconstructsecond) = 2 * ge_signed_half_factor_append_newreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newreconstructsecondimaginary) = S ge_signed_half_factor_append_newreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructsecondimaginary = (ge_second_in_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newreconstructoutput ge_representation_imaginary_code_factor_append_newreconstructoutput. (((w) = ((ge_representation_real_code_factor_append_newreconstructoutput) + (ge_representation_imaginary_code_factor_append_newreconstructoutput)) * S ((ge_representation_real_code_factor_append_newreconstructoutput) + (ge_representation_imaginary_code_factor_append_newreconstructoutput)) + ((ge_representation_imaginary_code_factor_append_newreconstructoutput) + (ge_representation_imaginary_code_factor_append_newreconstructoutput))) /\ ((exists ge_balance_positive_factor_append_newreconstructoutputreal ge_balance_negative_factor_append_newreconstructoutputreal. (((((ge_representation_real_code_factor_append_newreconstructoutput) = 2 * (ge_balance_positive_factor_append_newreconstructoutputreal) /\ (ge_balance_negative_factor_append_newreconstructoutputreal) = 0) \/ exists ge_signed_half_factor_append_newreconstructoutputrealdecode. (((ge_representation_real_code_factor_append_newreconstructoutput) = 2 * ge_signed_half_factor_append_newreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newreconstructoutputreal) = 0) /\ (ge_balance_negative_factor_append_newreconstructoutputreal) = S ge_signed_half_factor_append_newreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))))))) + ge_balance_negative_factor_append_newreconstructoutputreal = (((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))))))) + ge_balance_positive_factor_append_newreconstructoutputreal))) /\ (exists ge_balance_positive_factor_append_newreconstructoutputimaginary ge_balance_negative_factor_append_newreconstructoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newreconstructoutput) = 2 * (ge_balance_positive_factor_append_newreconstructoutputimaginary) /\ (ge_balance_negative_factor_append_newreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newreconstructoutput) = 2 * ge_signed_half_factor_append_newreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newreconstructoutputimaginary) = S ge_signed_half_factor_append_newreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))))))) + ge_balance_negative_factor_append_newreconstructoutputimaginary = (((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))))))) + ge_balance_positive_factor_append_newreconstructoutputimaginary))))))))))))))