Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded first-order arithmetic statement
forall z u b c l. (((exists gr_inverse_factor_valid_givenunit. (exists ge_first_rp_factor_valid_givenunitidentity ge_first_rn_factor_valid_givenunitidentity ge_first_ip_factor_valid_givenunitidentity ge_first_in_factor_valid_givenunitidentity ge_second_rp_factor_valid_givenunitidentity ge_second_rn_factor_valid_givenunitidentity ge_second_ip_factor_valid_givenunitidentity ge_second_in_factor_valid_givenunitidentity. ((exists ge_representation_real_code_factor_valid_givenunitidentityfirst ge_representation_imaginary_code_factor_valid_givenunitidentityfirst. (((u) = ((ge_representation_real_code_factor_valid_givenunitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenunitidentityfirst)) * S ((ge_representation_real_code_factor_valid_givenunitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenunitidentityfirst)) + ((ge_representation_imaginary_code_factor_valid_givenunitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenunitidentityfirst))) /\ ((exists ge_balance_positive_factor_valid_givenunitidentityfirstreal ge_balance_negative_factor_valid_givenunitidentityfirstreal. (((((ge_representation_real_code_factor_valid_givenunitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenunitidentityfirstreal) /\ (ge_balance_negative_factor_valid_givenunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_valid_givenunitidentityfirstrealdecode. (((ge_representation_real_code_factor_valid_givenunitidentityfirst) = 2 * ge_signed_half_factor_valid_givenunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_valid_givenunitidentityfirstreal) = S ge_signed_half_factor_valid_givenunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_valid_givenunitidentity) + ge_balance_negative_factor_valid_givenunitidentityfirstreal = (ge_first_rn_factor_valid_givenunitidentity) + ge_balance_positive_factor_valid_givenunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_valid_givenunitidentityfirstimaginary ge_balance_negative_factor_valid_givenunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_givenunitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenunitidentityfirstimaginary) /\ (ge_balance_negative_factor_valid_givenunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenunitidentityfirst) = 2 * ge_signed_half_factor_valid_givenunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenunitidentityfirstimaginary) = S ge_signed_half_factor_valid_givenunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_givenunitidentity) + ge_balance_negative_factor_valid_givenunitidentityfirstimaginary = (ge_first_in_factor_valid_givenunitidentity) + ge_balance_positive_factor_valid_givenunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_givenunitidentitysecond ge_representation_imaginary_code_factor_valid_givenunitidentitysecond. (((gr_inverse_factor_valid_givenunit) = ((ge_representation_real_code_factor_valid_givenunitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenunitidentitysecond)) * S ((ge_representation_real_code_factor_valid_givenunitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenunitidentitysecond)) + ((ge_representation_imaginary_code_factor_valid_givenunitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenunitidentitysecond))) /\ ((exists ge_balance_positive_factor_valid_givenunitidentitysecondreal ge_balance_negative_factor_valid_givenunitidentitysecondreal. (((((ge_representation_real_code_factor_valid_givenunitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenunitidentitysecondreal) /\ (ge_balance_negative_factor_valid_givenunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_valid_givenunitidentitysecondrealdecode. (((ge_representation_real_code_factor_valid_givenunitidentitysecond) = 2 * ge_signed_half_factor_valid_givenunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_valid_givenunitidentitysecondreal) = S ge_signed_half_factor_valid_givenunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_valid_givenunitidentity) + ge_balance_negative_factor_valid_givenunitidentitysecondreal = (ge_second_rn_factor_valid_givenunitidentity) + ge_balance_positive_factor_valid_givenunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_valid_givenunitidentitysecondimaginary ge_balance_negative_factor_valid_givenunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_valid_givenunitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenunitidentitysecondimaginary) /\ (ge_balance_negative_factor_valid_givenunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenunitidentitysecond) = 2 * ge_signed_half_factor_valid_givenunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenunitidentitysecondimaginary) = S ge_signed_half_factor_valid_givenunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_givenunitidentity) + ge_balance_negative_factor_valid_givenunitidentitysecondimaginary = (ge_second_in_factor_valid_givenunitidentity) + ge_balance_positive_factor_valid_givenunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_givenunitidentityoutput ge_representation_imaginary_code_factor_valid_givenunitidentityoutput. (((6) = ((ge_representation_real_code_factor_valid_givenunitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenunitidentityoutput)) * S ((ge_representation_real_code_factor_valid_givenunitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenunitidentityoutput)) + ((ge_representation_imaginary_code_factor_valid_givenunitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenunitidentityoutput))) /\ ((exists ge_balance_positive_factor_valid_givenunitidentityoutputreal ge_balance_negative_factor_valid_givenunitidentityoutputreal. (((((ge_representation_real_code_factor_valid_givenunitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenunitidentityoutputreal) /\ (ge_balance_negative_factor_valid_givenunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_valid_givenunitidentityoutputrealdecode. (((ge_representation_real_code_factor_valid_givenunitidentityoutput) = 2 * ge_signed_half_factor_valid_givenunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_valid_givenunitidentityoutputreal) = S ge_signed_half_factor_valid_givenunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_givenunitidentity) * (ge_second_rp_factor_valid_givenunitidentity))) + (((ge_first_rn_factor_valid_givenunitidentity) * (ge_second_rn_factor_valid_givenunitidentity))))) + (((((ge_first_ip_factor_valid_givenunitidentity) * (ge_second_in_factor_valid_givenunitidentity))) + (((ge_first_in_factor_valid_givenunitidentity) * (ge_second_ip_factor_valid_givenunitidentity))))))) + ge_balance_negative_factor_valid_givenunitidentityoutputreal = (((((((ge_first_rp_factor_valid_givenunitidentity) * (ge_second_rn_factor_valid_givenunitidentity))) + (((ge_first_rn_factor_valid_givenunitidentity) * (ge_second_rp_factor_valid_givenunitidentity))))) + (((((ge_first_ip_factor_valid_givenunitidentity) * (ge_second_ip_factor_valid_givenunitidentity))) + (((ge_first_in_factor_valid_givenunitidentity) * (ge_second_in_factor_valid_givenunitidentity))))))) + ge_balance_positive_factor_valid_givenunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_valid_givenunitidentityoutputimaginary ge_balance_negative_factor_valid_givenunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_givenunitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenunitidentityoutputimaginary) /\ (ge_balance_negative_factor_valid_givenunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenunitidentityoutput) = 2 * ge_signed_half_factor_valid_givenunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenunitidentityoutputimaginary) = S ge_signed_half_factor_valid_givenunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_givenunitidentity) * (ge_second_ip_factor_valid_givenunitidentity))) + (((ge_first_rn_factor_valid_givenunitidentity) * (ge_second_in_factor_valid_givenunitidentity))))) + (((((ge_first_ip_factor_valid_givenunitidentity) * (ge_second_rp_factor_valid_givenunitidentity))) + (((ge_first_in_factor_valid_givenunitidentity) * (ge_second_rn_factor_valid_givenunitidentity))))))) + ge_balance_negative_factor_valid_givenunitidentityoutputimaginary = (((((((ge_first_rp_factor_valid_givenunitidentity) * (ge_second_in_factor_valid_givenunitidentity))) + (((ge_first_rn_factor_valid_givenunitidentity) * (ge_second_ip_factor_valid_givenunitidentity))))) + (((((ge_first_ip_factor_valid_givenunitidentity) * (ge_second_rn_factor_valid_givenunitidentity))) + (((ge_first_in_factor_valid_givenunitidentity) * (ge_second_rp_factor_valid_givenunitidentity))))))) + ge_balance_positive_factor_valid_givenunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factor_valid_givenirreducible gr_factor_value_factor_valid_givenirreducible. (exists ge_gap_factor_valid_givenirreducibleindex. ge_gap_factor_valid_givenirreducibleindex + S (gr_factor_index_factor_valid_givenirreducible) = (l)) -> (((exists ff_h_gprod_factor_valid_givenirreducibleentry. ff_h_gprod_factor_valid_givenirreducibleentry + S (gr_factor_value_factor_valid_givenirreducible) = S ((S (gr_factor_index_factor_valid_givenirreducible)) * c)) /\ exists ff_q_gprod_factor_valid_givenirreducibleentry. b = ff_q_gprod_factor_valid_givenirreducibleentry * S ((S (gr_factor_index_factor_valid_givenirreducible)) * c) + (gr_factor_value_factor_valid_givenirreducible))) -> (((exists ge_real_positive_factor_valid_givenirreducibleirreduciblecarrier ge_real_negative_factor_valid_givenirreducibleirreduciblecarrier ge_imaginary_positive_factor_valid_givenirreducibleirreduciblecarrier ge_imaginary_negative_factor_valid_givenirreducibleirreduciblecarrier. (exists ge_real_code_factor_valid_givenirreducibleirreduciblecarrierdecode ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode. (((gr_factor_value_factor_valid_givenirreducible) = ((ge_real_code_factor_valid_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factor_valid_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factor_valid_givenirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factor_valid_givenirreducibleirreduciblecarrier) /\ (ge_real_negative_factor_valid_givenirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_valid_givenirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factor_valid_givenirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_valid_givenirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factor_valid_givenirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factor_valid_givenirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_valid_givenirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factor_valid_givenirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factor_valid_givenirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_valid_givenirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factor_valid_givenirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_valid_givenirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_valid_givenirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factor_valid_givenirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_valid_givenirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factor_valid_givenirreducible)=0)) /\ ((~(exists gr_inverse_factor_valid_givenirreducibleirreduciblenonunit. (exists ge_first_rp_factor_valid_givenirreducibleirreduciblenonunitidentity ge_first_rn_factor_valid_givenirreducibleirreduciblenonunitidentity ge_first_ip_factor_valid_givenirreducibleirreduciblenonunitidentity ge_first_in_factor_valid_givenirreducibleirreduciblenonunitidentity ge_second_rp_factor_valid_givenirreducibleirreduciblenonunitidentity ge_second_rn_factor_valid_givenirreducibleirreduciblenonunitidentity ge_second_ip_factor_valid_givenirreducibleirreduciblenonunitidentity ge_second_in_factor_valid_givenirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factor_valid_givenirreducible) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factor_valid_givenirreducibleirreduciblenonunit) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factor_valid_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_valid_givenirreducibleirreducible gr_second_factor_factor_valid_givenirreducibleirreducible. (exists ge_first_rp_factor_valid_givenirreducibleirreduciblefactorization ge_first_rn_factor_valid_givenirreducibleirreduciblefactorization ge_first_ip_factor_valid_givenirreducibleirreduciblefactorization ge_first_in_factor_valid_givenirreducibleirreduciblefactorization ge_second_rp_factor_valid_givenirreducibleirreduciblefactorization ge_second_rn_factor_valid_givenirreducibleirreduciblefactorization ge_second_ip_factor_valid_givenirreducibleirreduciblefactorization ge_second_in_factor_valid_givenirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factor_valid_givenirreducibleirreducible) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factor_valid_givenirreducibleirreducible) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factor_valid_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factor_valid_givenirreducible) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_valid_givenirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_valid_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_valid_givenirreducibleirreduciblefirst_unit. (exists ge_first_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_first_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_first_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_first_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_second_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_second_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_second_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity ge_second_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factor_valid_givenirreducibleirreducible) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factor_valid_givenirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_valid_givenirreducibleirreduciblesecond_unit. (exists ge_first_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_first_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_first_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_first_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_second_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_second_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_second_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity ge_second_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factor_valid_givenirreducibleirreducible) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factor_valid_givenirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_valid_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_valid_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_valid_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_valid_givenirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factor_valid_given. ((exists gr_product_trace_factor_valid_giventrace gr_product_scale_factor_valid_giventrace. ((((exists ff_h_gprod_factor_valid_giventracestart. ff_h_gprod_factor_valid_giventracestart + S (6) = S ((S (0)) * gr_product_scale_factor_valid_giventrace)) /\ exists ff_q_gprod_factor_valid_giventracestart. gr_product_trace_factor_valid_giventrace = ff_q_gprod_factor_valid_giventracestart * S ((S (0)) * gr_product_scale_factor_valid_giventrace) + (6))) /\ ((((exists ff_h_gprod_factor_valid_giventraceend. ff_h_gprod_factor_valid_giventraceend + S (gr_factor_product_factor_valid_given) = S ((S (l)) * gr_product_scale_factor_valid_giventrace)) /\ exists ff_q_gprod_factor_valid_giventraceend. gr_product_trace_factor_valid_giventrace = ff_q_gprod_factor_valid_giventraceend * S ((S (l)) * gr_product_scale_factor_valid_giventrace) + (gr_factor_product_factor_valid_given))) /\ (forall gr_product_index_factor_valid_giventracesteps. (exists ge_gap_factor_valid_giventracestepsindex_bound. ge_gap_factor_valid_giventracestepsindex_bound + S (gr_product_index_factor_valid_giventracesteps) = (l)) -> exists gr_product_factor_factor_valid_giventracesteps gr_product_before_factor_valid_giventracesteps gr_product_after_factor_valid_giventracesteps. ((((exists ff_h_gprod_factor_valid_giventracestepsfactor. ff_h_gprod_factor_valid_giventracestepsfactor + S (gr_product_factor_factor_valid_giventracesteps) = S ((S (gr_product_index_factor_valid_giventracesteps)) * c)) /\ exists ff_q_gprod_factor_valid_giventracestepsfactor. b = ff_q_gprod_factor_valid_giventracestepsfactor * S ((S (gr_product_index_factor_valid_giventracesteps)) * c) + (gr_product_factor_factor_valid_giventracesteps))) /\ ((((exists ff_h_gprod_factor_valid_giventracestepsbefore. ff_h_gprod_factor_valid_giventracestepsbefore + S (gr_product_before_factor_valid_giventracesteps) = S ((S (gr_product_index_factor_valid_giventracesteps)) * gr_product_scale_factor_valid_giventrace)) /\ exists ff_q_gprod_factor_valid_giventracestepsbefore. gr_product_trace_factor_valid_giventrace = ff_q_gprod_factor_valid_giventracestepsbefore * S ((S (gr_product_index_factor_valid_giventracesteps)) * gr_product_scale_factor_valid_giventrace) + (gr_product_before_factor_valid_giventracesteps))) /\ ((((exists ff_h_gprod_factor_valid_giventracestepsafter. ff_h_gprod_factor_valid_giventracestepsafter + S (gr_product_after_factor_valid_giventracesteps) = S ((S (S (gr_product_index_factor_valid_giventracesteps))) * gr_product_scale_factor_valid_giventrace)) /\ exists ff_q_gprod_factor_valid_giventracestepsafter. gr_product_trace_factor_valid_giventrace = ff_q_gprod_factor_valid_giventracestepsafter * S ((S (S (gr_product_index_factor_valid_giventracesteps))) * gr_product_scale_factor_valid_giventrace) + (gr_product_after_factor_valid_giventracesteps))) /\ (exists ge_first_rp_factor_valid_giventracestepsmultiply ge_first_rn_factor_valid_giventracestepsmultiply ge_first_ip_factor_valid_giventracestepsmultiply ge_first_in_factor_valid_giventracestepsmultiply ge_second_rp_factor_valid_giventracestepsmultiply ge_second_rn_factor_valid_giventracestepsmultiply ge_second_ip_factor_valid_giventracestepsmultiply ge_second_in_factor_valid_giventracestepsmultiply. ((exists ge_representation_real_code_factor_valid_giventracestepsmultiplyfirst ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst. (((gr_product_before_factor_valid_giventracesteps) = ((ge_representation_real_code_factor_valid_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst)) * S ((ge_representation_real_code_factor_valid_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factor_valid_giventracestepsmultiplyfirstreal ge_balance_negative_factor_valid_giventracestepsmultiplyfirstreal. (((((ge_representation_real_code_factor_valid_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_valid_giventracestepsmultiplyfirstreal) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factor_valid_giventracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factor_valid_giventracestepsmultiplyfirst) = 2 * ge_signed_half_factor_valid_giventracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_giventracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyfirstreal) = S ge_signed_half_factor_valid_giventracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factor_valid_giventracestepsmultiply) + ge_balance_negative_factor_valid_giventracestepsmultiplyfirstreal = (ge_first_rn_factor_valid_giventracestepsmultiply) + ge_balance_positive_factor_valid_giventracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factor_valid_giventracestepsmultiplyfirstimaginary ge_balance_negative_factor_valid_giventracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_valid_giventracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_giventracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyfirst) = 2 * ge_signed_half_factor_valid_giventracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_giventracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyfirstimaginary) = S ge_signed_half_factor_valid_giventracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_giventracestepsmultiply) + ge_balance_negative_factor_valid_giventracestepsmultiplyfirstimaginary = (ge_first_in_factor_valid_giventracestepsmultiply) + ge_balance_positive_factor_valid_giventracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_giventracestepsmultiplysecond ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond. (((gr_product_factor_factor_valid_giventracesteps) = ((ge_representation_real_code_factor_valid_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond)) * S ((ge_representation_real_code_factor_valid_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factor_valid_giventracestepsmultiplysecondreal ge_balance_negative_factor_valid_giventracestepsmultiplysecondreal. (((((ge_representation_real_code_factor_valid_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_valid_giventracestepsmultiplysecondreal) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factor_valid_giventracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factor_valid_giventracestepsmultiplysecond) = 2 * ge_signed_half_factor_valid_giventracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_giventracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplysecondreal) = S ge_signed_half_factor_valid_giventracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factor_valid_giventracestepsmultiply) + ge_balance_negative_factor_valid_giventracestepsmultiplysecondreal = (ge_second_rn_factor_valid_giventracestepsmultiply) + ge_balance_positive_factor_valid_giventracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factor_valid_giventracestepsmultiplysecondimaginary ge_balance_negative_factor_valid_giventracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_valid_giventracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_giventracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplysecond) = 2 * ge_signed_half_factor_valid_giventracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_giventracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplysecondimaginary) = S ge_signed_half_factor_valid_giventracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_giventracestepsmultiply) + ge_balance_negative_factor_valid_giventracestepsmultiplysecondimaginary = (ge_second_in_factor_valid_giventracestepsmultiply) + ge_balance_positive_factor_valid_giventracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_giventracestepsmultiplyoutput ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput. (((gr_product_after_factor_valid_giventracesteps) = ((ge_representation_real_code_factor_valid_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput)) * S ((ge_representation_real_code_factor_valid_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factor_valid_giventracestepsmultiplyoutputreal ge_balance_negative_factor_valid_giventracestepsmultiplyoutputreal. (((((ge_representation_real_code_factor_valid_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_valid_giventracestepsmultiplyoutputreal) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factor_valid_giventracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factor_valid_giventracestepsmultiplyoutput) = 2 * ge_signed_half_factor_valid_giventracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_giventracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyoutputreal) = S ge_signed_half_factor_valid_giventracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_giventracestepsmultiply) * (ge_second_rp_factor_valid_giventracestepsmultiply))) + (((ge_first_rn_factor_valid_giventracestepsmultiply) * (ge_second_rn_factor_valid_giventracestepsmultiply))))) + (((((ge_first_ip_factor_valid_giventracestepsmultiply) * (ge_second_in_factor_valid_giventracestepsmultiply))) + (((ge_first_in_factor_valid_giventracestepsmultiply) * (ge_second_ip_factor_valid_giventracestepsmultiply))))))) + ge_balance_negative_factor_valid_giventracestepsmultiplyoutputreal = (((((((ge_first_rp_factor_valid_giventracestepsmultiply) * (ge_second_rn_factor_valid_giventracestepsmultiply))) + (((ge_first_rn_factor_valid_giventracestepsmultiply) * (ge_second_rp_factor_valid_giventracestepsmultiply))))) + (((((ge_first_ip_factor_valid_giventracestepsmultiply) * (ge_second_ip_factor_valid_giventracestepsmultiply))) + (((ge_first_in_factor_valid_giventracestepsmultiply) * (ge_second_in_factor_valid_giventracestepsmultiply))))))) + ge_balance_positive_factor_valid_giventracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factor_valid_giventracestepsmultiplyoutputimaginary ge_balance_negative_factor_valid_giventracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_valid_giventracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_giventracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_giventracestepsmultiplyoutput) = 2 * ge_signed_half_factor_valid_giventracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_giventracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_giventracestepsmultiplyoutputimaginary) = S ge_signed_half_factor_valid_giventracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_giventracestepsmultiply) * (ge_second_ip_factor_valid_giventracestepsmultiply))) + (((ge_first_rn_factor_valid_giventracestepsmultiply) * (ge_second_in_factor_valid_giventracestepsmultiply))))) + (((((ge_first_ip_factor_valid_giventracestepsmultiply) * (ge_second_rp_factor_valid_giventracestepsmultiply))) + (((ge_first_in_factor_valid_giventracestepsmultiply) * (ge_second_rn_factor_valid_giventracestepsmultiply))))))) + ge_balance_negative_factor_valid_giventracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factor_valid_giventracestepsmultiply) * (ge_second_in_factor_valid_giventracestepsmultiply))) + (((ge_first_rn_factor_valid_giventracestepsmultiply) * (ge_second_ip_factor_valid_giventracestepsmultiply))))) + (((((ge_first_ip_factor_valid_giventracestepsmultiply) * (ge_second_rn_factor_valid_giventracestepsmultiply))) + (((ge_first_in_factor_valid_giventracestepsmultiply) * (ge_second_rp_factor_valid_giventracestepsmultiply))))))) + ge_balance_positive_factor_valid_giventracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factor_valid_givenreconstruct ge_first_rn_factor_valid_givenreconstruct ge_first_ip_factor_valid_givenreconstruct ge_first_in_factor_valid_givenreconstruct ge_second_rp_factor_valid_givenreconstruct ge_second_rn_factor_valid_givenreconstruct ge_second_ip_factor_valid_givenreconstruct ge_second_in_factor_valid_givenreconstruct. ((exists ge_representation_real_code_factor_valid_givenreconstructfirst ge_representation_imaginary_code_factor_valid_givenreconstructfirst. (((u) = ((ge_representation_real_code_factor_valid_givenreconstructfirst) + (ge_representation_imaginary_code_factor_valid_givenreconstructfirst)) * S ((ge_representation_real_code_factor_valid_givenreconstructfirst) + (ge_representation_imaginary_code_factor_valid_givenreconstructfirst)) + ((ge_representation_imaginary_code_factor_valid_givenreconstructfirst) + (ge_representation_imaginary_code_factor_valid_givenreconstructfirst))) /\ ((exists ge_balance_positive_factor_valid_givenreconstructfirstreal ge_balance_negative_factor_valid_givenreconstructfirstreal. (((((ge_representation_real_code_factor_valid_givenreconstructfirst) = 2 * (ge_balance_positive_factor_valid_givenreconstructfirstreal) /\ (ge_balance_negative_factor_valid_givenreconstructfirstreal) = 0) \/ exists ge_signed_half_factor_valid_givenreconstructfirstrealdecode. (((ge_representation_real_code_factor_valid_givenreconstructfirst) = 2 * ge_signed_half_factor_valid_givenreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenreconstructfirstreal) = 0) /\ (ge_balance_negative_factor_valid_givenreconstructfirstreal) = S ge_signed_half_factor_valid_givenreconstructfirstrealdecode))) /\ ((ge_first_rp_factor_valid_givenreconstruct) + ge_balance_negative_factor_valid_givenreconstructfirstreal = (ge_first_rn_factor_valid_givenreconstruct) + ge_balance_positive_factor_valid_givenreconstructfirstreal))) /\ (exists ge_balance_positive_factor_valid_givenreconstructfirstimaginary ge_balance_negative_factor_valid_givenreconstructfirstimaginary. (((((ge_representation_imaginary_code_factor_valid_givenreconstructfirst) = 2 * (ge_balance_positive_factor_valid_givenreconstructfirstimaginary) /\ (ge_balance_negative_factor_valid_givenreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenreconstructfirst) = 2 * ge_signed_half_factor_valid_givenreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenreconstructfirstimaginary) = S ge_signed_half_factor_valid_givenreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factor_valid_givenreconstruct) + ge_balance_negative_factor_valid_givenreconstructfirstimaginary = (ge_first_in_factor_valid_givenreconstruct) + ge_balance_positive_factor_valid_givenreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_valid_givenreconstructsecond ge_representation_imaginary_code_factor_valid_givenreconstructsecond. (((gr_factor_product_factor_valid_given) = ((ge_representation_real_code_factor_valid_givenreconstructsecond) + (ge_representation_imaginary_code_factor_valid_givenreconstructsecond)) * S ((ge_representation_real_code_factor_valid_givenreconstructsecond) + (ge_representation_imaginary_code_factor_valid_givenreconstructsecond)) + ((ge_representation_imaginary_code_factor_valid_givenreconstructsecond) + (ge_representation_imaginary_code_factor_valid_givenreconstructsecond))) /\ ((exists ge_balance_positive_factor_valid_givenreconstructsecondreal ge_balance_negative_factor_valid_givenreconstructsecondreal. (((((ge_representation_real_code_factor_valid_givenreconstructsecond) = 2 * (ge_balance_positive_factor_valid_givenreconstructsecondreal) /\ (ge_balance_negative_factor_valid_givenreconstructsecondreal) = 0) \/ exists ge_signed_half_factor_valid_givenreconstructsecondrealdecode. (((ge_representation_real_code_factor_valid_givenreconstructsecond) = 2 * ge_signed_half_factor_valid_givenreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenreconstructsecondreal) = 0) /\ (ge_balance_negative_factor_valid_givenreconstructsecondreal) = S ge_signed_half_factor_valid_givenreconstructsecondrealdecode))) /\ ((ge_second_rp_factor_valid_givenreconstruct) + ge_balance_negative_factor_valid_givenreconstructsecondreal = (ge_second_rn_factor_valid_givenreconstruct) + ge_balance_positive_factor_valid_givenreconstructsecondreal))) /\ (exists ge_balance_positive_factor_valid_givenreconstructsecondimaginary ge_balance_negative_factor_valid_givenreconstructsecondimaginary. (((((ge_representation_imaginary_code_factor_valid_givenreconstructsecond) = 2 * (ge_balance_positive_factor_valid_givenreconstructsecondimaginary) /\ (ge_balance_negative_factor_valid_givenreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenreconstructsecond) = 2 * ge_signed_half_factor_valid_givenreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenreconstructsecondimaginary) = S ge_signed_half_factor_valid_givenreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factor_valid_givenreconstruct) + ge_balance_negative_factor_valid_givenreconstructsecondimaginary = (ge_second_in_factor_valid_givenreconstruct) + ge_balance_positive_factor_valid_givenreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_valid_givenreconstructoutput ge_representation_imaginary_code_factor_valid_givenreconstructoutput. (((z) = ((ge_representation_real_code_factor_valid_givenreconstructoutput) + (ge_representation_imaginary_code_factor_valid_givenreconstructoutput)) * S ((ge_representation_real_code_factor_valid_givenreconstructoutput) + (ge_representation_imaginary_code_factor_valid_givenreconstructoutput)) + ((ge_representation_imaginary_code_factor_valid_givenreconstructoutput) + (ge_representation_imaginary_code_factor_valid_givenreconstructoutput))) /\ ((exists ge_balance_positive_factor_valid_givenreconstructoutputreal ge_balance_negative_factor_valid_givenreconstructoutputreal. (((((ge_representation_real_code_factor_valid_givenreconstructoutput) = 2 * (ge_balance_positive_factor_valid_givenreconstructoutputreal) /\ (ge_balance_negative_factor_valid_givenreconstructoutputreal) = 0) \/ exists ge_signed_half_factor_valid_givenreconstructoutputrealdecode. (((ge_representation_real_code_factor_valid_givenreconstructoutput) = 2 * ge_signed_half_factor_valid_givenreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factor_valid_givenreconstructoutputreal) = 0) /\ (ge_balance_negative_factor_valid_givenreconstructoutputreal) = S ge_signed_half_factor_valid_givenreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factor_valid_givenreconstruct) * (ge_second_rp_factor_valid_givenreconstruct))) + (((ge_first_rn_factor_valid_givenreconstruct) * (ge_second_rn_factor_valid_givenreconstruct))))) + (((((ge_first_ip_factor_valid_givenreconstruct) * (ge_second_in_factor_valid_givenreconstruct))) + (((ge_first_in_factor_valid_givenreconstruct) * (ge_second_ip_factor_valid_givenreconstruct))))))) + ge_balance_negative_factor_valid_givenreconstructoutputreal = (((((((ge_first_rp_factor_valid_givenreconstruct) * (ge_second_rn_factor_valid_givenreconstruct))) + (((ge_first_rn_factor_valid_givenreconstruct) * (ge_second_rp_factor_valid_givenreconstruct))))) + (((((ge_first_ip_factor_valid_givenreconstruct) * (ge_second_ip_factor_valid_givenreconstruct))) + (((ge_first_in_factor_valid_givenreconstruct) * (ge_second_in_factor_valid_givenreconstruct))))))) + ge_balance_positive_factor_valid_givenreconstructoutputreal))) /\ (exists ge_balance_positive_factor_valid_givenreconstructoutputimaginary ge_balance_negative_factor_valid_givenreconstructoutputimaginary. (((((ge_representation_imaginary_code_factor_valid_givenreconstructoutput) = 2 * (ge_balance_positive_factor_valid_givenreconstructoutputimaginary) /\ (ge_balance_negative_factor_valid_givenreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factor_valid_givenreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factor_valid_givenreconstructoutput) = 2 * ge_signed_half_factor_valid_givenreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_valid_givenreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factor_valid_givenreconstructoutputimaginary) = S ge_signed_half_factor_valid_givenreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_valid_givenreconstruct) * (ge_second_ip_factor_valid_givenreconstruct))) + (((ge_first_rn_factor_valid_givenreconstruct) * (ge_second_in_factor_valid_givenreconstruct))))) + (((((ge_first_ip_factor_valid_givenreconstruct) * (ge_second_rp_factor_valid_givenreconstruct))) + (((ge_first_in_factor_valid_givenreconstruct) * (ge_second_rn_factor_valid_givenreconstruct))))))) + ge_balance_negative_factor_valid_givenreconstructoutputimaginary = (((((((ge_first_rp_factor_valid_givenreconstruct) * (ge_second_in_factor_valid_givenreconstruct))) + (((ge_first_rn_factor_valid_givenreconstruct) * (ge_second_ip_factor_valid_givenreconstruct))))) + (((((ge_first_ip_factor_valid_givenreconstruct) * (ge_second_rn_factor_valid_givenreconstruct))) + (((ge_first_in_factor_valid_givenreconstruct) * (ge_second_rp_factor_valid_givenreconstruct))))))) + ge_balance_positive_factor_valid_givenreconstructoutputimaginary)))))))))))))) -> (exists ge_real_positive_factor_valid_value ge_real_negative_factor_valid_value ge_imaginary_positive_factor_valid_value ge_imaginary_negative_factor_valid_value. (exists ge_real_code_factor_valid_valuedecode ge_imaginary_code_factor_valid_valuedecode. (((z) = ((ge_real_code_factor_valid_valuedecode) + (ge_imaginary_code_factor_valid_valuedecode)) * S ((ge_real_code_factor_valid_valuedecode) + (ge_imaginary_code_factor_valid_valuedecode)) + ((ge_imaginary_code_factor_valid_valuedecode) + (ge_imaginary_code_factor_valid_valuedecode))) /\ (((((ge_real_code_factor_valid_valuedecode) = 2 * (ge_real_positive_factor_valid_value) /\ (ge_real_negative_factor_valid_value) = 0) \/ exists ge_signed_half_ge_factor_valid_valuedecode_real. (((ge_real_code_factor_valid_valuedecode) = 2 * ge_signed_half_ge_factor_valid_valuedecode_real + 1 /\ (ge_real_positive_factor_valid_value) = 0) /\ (ge_real_negative_factor_valid_value) = S ge_signed_half_ge_factor_valid_valuedecode_real))) /\ ((((ge_imaginary_code_factor_valid_valuedecode) = 2 * (ge_imaginary_positive_factor_valid_value) /\ (ge_imaginary_negative_factor_valid_value) = 0) \/ exists ge_signed_half_ge_factor_valid_valuedecode_imaginary. (((ge_imaginary_code_factor_valid_valuedecode) = 2 * ge_signed_half_ge_factor_valid_valuedecode_imaginary + 1 /\ (ge_imaginary_positive_factor_valid_value) = 0) /\ (ge_imaginary_negative_factor_valid_value) = S ge_signed_half_ge_factor_valid_valuedecode_imaginary)))))))Constructive proof overview
Generated structural guide
Every actual Gaussian factorization reconstructs a value in the genuine canonical carrier.
The unchanged tactic script uses 1 declared prerequisite and contains 15 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
none
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–10
03Use earlier factsL11–15
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 15 lines
- 0001
intro z - 0002
intro u - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro hf - 0007
cases hf - 0008
cases hf_right - 0009
cases hf_right_right - 0010
cases hf_right_right_witness - 0011
specialize gaussian_multiply_output_valid (u) - 0012
specialize gaussian_multiply_output_valid (x) - 0013
specialize gaussian_multiply_output_valid (z) - 0014
apply gaussian_multiply_output_valid - 0015
exact hf_right_right_witness_right