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.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ z. ∀ u. ∀ b. ∀ c. ∀ l. GIrreducibleFactorization(z,u,b,c,l) → ¬z = 0Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall z u b c l. (((exists gr_inverse_factor_nonzero_givenunit. (exists ge_first_rp_factor_nonzero_givenunitidentity ge_first_rn_factor_nonzero_givenunitidentity ge_first_ip_factor_nonzero_givenunitidentity ge_first_in_factor_nonzero_givenunitidentity ge_second_rp_factor_nonzero_givenunitidentity ge_second_rn_factor_nonzero_givenunitidentity ge_second_ip_factor_nonzero_givenunitidentity ge_second_in_factor_nonzero_givenunitidentity. ((exists ge_representation_real_code_factor_nonzero_givenunitidentityfirst ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst. (((u) = ((ge_representation_real_code_factor_nonzero_givenunitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst)) * S ((ge_representation_real_code_factor_nonzero_givenunitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst)) + ((ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst))) /\ ((exists ge_balance_positive_factor_nonzero_givenunitidentityfirstreal ge_balance_negative_factor_nonzero_givenunitidentityfirstreal. (((((ge_representation_real_code_factor_nonzero_givenunitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenunitidentityfirstreal) /\ (ge_balance_negative_factor_nonzero_givenunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenunitidentityfirstrealdecode. (((ge_representation_real_code_factor_nonzero_givenunitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenunitidentityfirstreal) = S ge_signed_half_factor_nonzero_givenunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_givenunitidentity) + ge_balance_negative_factor_nonzero_givenunitidentityfirstreal = (ge_first_rn_factor_nonzero_givenunitidentity) + ge_balance_positive_factor_nonzero_givenunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_givenunitidentityfirstimaginary ge_balance_negative_factor_nonzero_givenunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenunitidentityfirstimaginary) /\ (ge_balance_negative_factor_nonzero_givenunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenunitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenunitidentityfirstimaginary) = S ge_signed_half_factor_nonzero_givenunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_givenunitidentity) + ge_balance_negative_factor_nonzero_givenunitidentityfirstimaginary = (ge_first_in_factor_nonzero_givenunitidentity) + ge_balance_positive_factor_nonzero_givenunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_givenunitidentitysecond ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond. (((gr_inverse_factor_nonzero_givenunit) = ((ge_representation_real_code_factor_nonzero_givenunitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond)) * S ((ge_representation_real_code_factor_nonzero_givenunitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond)) + ((ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond))) /\ ((exists ge_balance_positive_factor_nonzero_givenunitidentitysecondreal ge_balance_negative_factor_nonzero_givenunitidentitysecondreal. (((((ge_representation_real_code_factor_nonzero_givenunitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenunitidentitysecondreal) /\ (ge_balance_negative_factor_nonzero_givenunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenunitidentitysecondrealdecode. (((ge_representation_real_code_factor_nonzero_givenunitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenunitidentitysecondreal) = S ge_signed_half_factor_nonzero_givenunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_givenunitidentity) + ge_balance_negative_factor_nonzero_givenunitidentitysecondreal = (ge_second_rn_factor_nonzero_givenunitidentity) + ge_balance_positive_factor_nonzero_givenunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_nonzero_givenunitidentitysecondimaginary ge_balance_negative_factor_nonzero_givenunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenunitidentitysecondimaginary) /\ (ge_balance_negative_factor_nonzero_givenunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenunitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenunitidentitysecondimaginary) = S ge_signed_half_factor_nonzero_givenunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_givenunitidentity) + ge_balance_negative_factor_nonzero_givenunitidentitysecondimaginary = (ge_second_in_factor_nonzero_givenunitidentity) + ge_balance_positive_factor_nonzero_givenunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_givenunitidentityoutput ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput. (((6) = ((ge_representation_real_code_factor_nonzero_givenunitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput)) * S ((ge_representation_real_code_factor_nonzero_givenunitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput)) + ((ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput))) /\ ((exists ge_balance_positive_factor_nonzero_givenunitidentityoutputreal ge_balance_negative_factor_nonzero_givenunitidentityoutputreal. (((((ge_representation_real_code_factor_nonzero_givenunitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenunitidentityoutputreal) /\ (ge_balance_negative_factor_nonzero_givenunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenunitidentityoutputrealdecode. (((ge_representation_real_code_factor_nonzero_givenunitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenunitidentityoutputreal) = S ge_signed_half_factor_nonzero_givenunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenunitidentity) * (ge_second_rp_factor_nonzero_givenunitidentity))) + (((ge_first_rn_factor_nonzero_givenunitidentity) * (ge_second_rn_factor_nonzero_givenunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenunitidentity) * (ge_second_in_factor_nonzero_givenunitidentity))) + (((ge_first_in_factor_nonzero_givenunitidentity) * (ge_second_ip_factor_nonzero_givenunitidentity))))))) + ge_balance_negative_factor_nonzero_givenunitidentityoutputreal = (((((((ge_first_rp_factor_nonzero_givenunitidentity) * (ge_second_rn_factor_nonzero_givenunitidentity))) + (((ge_first_rn_factor_nonzero_givenunitidentity) * (ge_second_rp_factor_nonzero_givenunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenunitidentity) * (ge_second_ip_factor_nonzero_givenunitidentity))) + (((ge_first_in_factor_nonzero_givenunitidentity) * (ge_second_in_factor_nonzero_givenunitidentity))))))) + ge_balance_positive_factor_nonzero_givenunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_givenunitidentityoutputimaginary ge_balance_negative_factor_nonzero_givenunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenunitidentityoutputimaginary) /\ (ge_balance_negative_factor_nonzero_givenunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenunitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenunitidentityoutputimaginary) = S ge_signed_half_factor_nonzero_givenunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenunitidentity) * (ge_second_ip_factor_nonzero_givenunitidentity))) + (((ge_first_rn_factor_nonzero_givenunitidentity) * (ge_second_in_factor_nonzero_givenunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenunitidentity) * (ge_second_rp_factor_nonzero_givenunitidentity))) + (((ge_first_in_factor_nonzero_givenunitidentity) * (ge_second_rn_factor_nonzero_givenunitidentity))))))) + ge_balance_negative_factor_nonzero_givenunitidentityoutputimaginary = (((((((ge_first_rp_factor_nonzero_givenunitidentity) * (ge_second_in_factor_nonzero_givenunitidentity))) + (((ge_first_rn_factor_nonzero_givenunitidentity) * (ge_second_ip_factor_nonzero_givenunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenunitidentity) * (ge_second_rn_factor_nonzero_givenunitidentity))) + (((ge_first_in_factor_nonzero_givenunitidentity) * (ge_second_rp_factor_nonzero_givenunitidentity))))))) + ge_balance_positive_factor_nonzero_givenunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factor_nonzero_givenirreducible gr_factor_value_factor_nonzero_givenirreducible. (exists ge_gap_factor_nonzero_givenirreducibleindex. ge_gap_factor_nonzero_givenirreducibleindex + S (gr_factor_index_factor_nonzero_givenirreducible) = (l)) -> (((exists ff_h_gprod_factor_nonzero_givenirreducibleentry. ff_h_gprod_factor_nonzero_givenirreducibleentry + S (gr_factor_value_factor_nonzero_givenirreducible) = S ((S (gr_factor_index_factor_nonzero_givenirreducible)) * c)) /\ exists ff_q_gprod_factor_nonzero_givenirreducibleentry. b = ff_q_gprod_factor_nonzero_givenirreducibleentry * S ((S (gr_factor_index_factor_nonzero_givenirreducible)) * c) + (gr_factor_value_factor_nonzero_givenirreducible))) -> (((exists ge_real_positive_factor_nonzero_givenirreducibleirreduciblecarrier ge_real_negative_factor_nonzero_givenirreducibleirreduciblecarrier ge_imaginary_positive_factor_nonzero_givenirreducibleirreduciblecarrier ge_imaginary_negative_factor_nonzero_givenirreducibleirreduciblecarrier. (exists ge_real_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode. (((gr_factor_value_factor_nonzero_givenirreducible) = ((ge_real_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factor_nonzero_givenirreducibleirreduciblecarrier) /\ (ge_real_negative_factor_nonzero_givenirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_nonzero_givenirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_nonzero_givenirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factor_nonzero_givenirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factor_nonzero_givenirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_nonzero_givenirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factor_nonzero_givenirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factor_nonzero_givenirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_nonzero_givenirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factor_nonzero_givenirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_nonzero_givenirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_nonzero_givenirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factor_nonzero_givenirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_nonzero_givenirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factor_nonzero_givenirreducible)=0)) /\ ((~(exists gr_inverse_factor_nonzero_givenirreducibleirreduciblenonunit. (exists ge_first_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_first_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_first_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_first_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_second_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_second_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_second_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity ge_second_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factor_nonzero_givenirreducible) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factor_nonzero_givenirreducibleirreduciblenonunit) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_nonzero_givenirreducibleirreducible gr_second_factor_factor_nonzero_givenirreducibleirreducible. (exists ge_first_rp_factor_nonzero_givenirreducibleirreduciblefactorization ge_first_rn_factor_nonzero_givenirreducibleirreduciblefactorization ge_first_ip_factor_nonzero_givenirreducibleirreduciblefactorization ge_first_in_factor_nonzero_givenirreducibleirreduciblefactorization ge_second_rp_factor_nonzero_givenirreducibleirreduciblefactorization ge_second_rn_factor_nonzero_givenirreducibleirreduciblefactorization ge_second_ip_factor_nonzero_givenirreducibleirreduciblefactorization ge_second_in_factor_nonzero_givenirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factor_nonzero_givenirreducibleirreducible) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factor_nonzero_givenirreducibleirreducible) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factor_nonzero_givenirreducibleirreduciblefactorization) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factor_nonzero_givenirreducible) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefactorization))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefactorization) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_nonzero_givenirreducibleirreduciblefirst_unit. (exists ge_first_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_first_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_first_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_first_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_second_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_second_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_second_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity ge_second_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factor_nonzero_givenirreducibleirreducible) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factor_nonzero_givenirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_nonzero_givenirreducibleirreduciblesecond_unit. (exists ge_first_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_first_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_first_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_first_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_second_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_second_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_second_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity ge_second_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factor_nonzero_givenirreducibleirreducible) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factor_nonzero_givenirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_nonzero_givenirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_nonzero_givenirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factor_nonzero_given. ((exists gr_product_trace_factor_nonzero_giventrace gr_product_scale_factor_nonzero_giventrace. ((((exists ff_h_gprod_factor_nonzero_giventracestart. ff_h_gprod_factor_nonzero_giventracestart + S (6) = S ((S (0)) * gr_product_scale_factor_nonzero_giventrace)) /\ exists ff_q_gprod_factor_nonzero_giventracestart. gr_product_trace_factor_nonzero_giventrace = ff_q_gprod_factor_nonzero_giventracestart * S ((S (0)) * gr_product_scale_factor_nonzero_giventrace) + (6))) /\ ((((exists ff_h_gprod_factor_nonzero_giventraceend. ff_h_gprod_factor_nonzero_giventraceend + S (gr_factor_product_factor_nonzero_given) = S ((S (l)) * gr_product_scale_factor_nonzero_giventrace)) /\ exists ff_q_gprod_factor_nonzero_giventraceend. gr_product_trace_factor_nonzero_giventrace = ff_q_gprod_factor_nonzero_giventraceend * S ((S (l)) * gr_product_scale_factor_nonzero_giventrace) + (gr_factor_product_factor_nonzero_given))) /\ (forall gr_product_index_factor_nonzero_giventracesteps. (exists ge_gap_factor_nonzero_giventracestepsindex_bound. ge_gap_factor_nonzero_giventracestepsindex_bound + S (gr_product_index_factor_nonzero_giventracesteps) = (l)) -> exists gr_product_factor_factor_nonzero_giventracesteps gr_product_before_factor_nonzero_giventracesteps gr_product_after_factor_nonzero_giventracesteps. ((((exists ff_h_gprod_factor_nonzero_giventracestepsfactor. ff_h_gprod_factor_nonzero_giventracestepsfactor + S (gr_product_factor_factor_nonzero_giventracesteps) = S ((S (gr_product_index_factor_nonzero_giventracesteps)) * c)) /\ exists ff_q_gprod_factor_nonzero_giventracestepsfactor. b = ff_q_gprod_factor_nonzero_giventracestepsfactor * S ((S (gr_product_index_factor_nonzero_giventracesteps)) * c) + (gr_product_factor_factor_nonzero_giventracesteps))) /\ ((((exists ff_h_gprod_factor_nonzero_giventracestepsbefore. ff_h_gprod_factor_nonzero_giventracestepsbefore + S (gr_product_before_factor_nonzero_giventracesteps) = S ((S (gr_product_index_factor_nonzero_giventracesteps)) * gr_product_scale_factor_nonzero_giventrace)) /\ exists ff_q_gprod_factor_nonzero_giventracestepsbefore. gr_product_trace_factor_nonzero_giventrace = ff_q_gprod_factor_nonzero_giventracestepsbefore * S ((S (gr_product_index_factor_nonzero_giventracesteps)) * gr_product_scale_factor_nonzero_giventrace) + (gr_product_before_factor_nonzero_giventracesteps))) /\ ((((exists ff_h_gprod_factor_nonzero_giventracestepsafter. ff_h_gprod_factor_nonzero_giventracestepsafter + S (gr_product_after_factor_nonzero_giventracesteps) = S ((S (S (gr_product_index_factor_nonzero_giventracesteps))) * gr_product_scale_factor_nonzero_giventrace)) /\ exists ff_q_gprod_factor_nonzero_giventracestepsafter. gr_product_trace_factor_nonzero_giventrace = ff_q_gprod_factor_nonzero_giventracestepsafter * S ((S (S (gr_product_index_factor_nonzero_giventracesteps))) * gr_product_scale_factor_nonzero_giventrace) + (gr_product_after_factor_nonzero_giventracesteps))) /\ (exists ge_first_rp_factor_nonzero_giventracestepsmultiply ge_first_rn_factor_nonzero_giventracestepsmultiply ge_first_ip_factor_nonzero_giventracestepsmultiply ge_first_in_factor_nonzero_giventracestepsmultiply ge_second_rp_factor_nonzero_giventracestepsmultiply ge_second_rn_factor_nonzero_giventracestepsmultiply ge_second_ip_factor_nonzero_giventracestepsmultiply ge_second_in_factor_nonzero_giventracestepsmultiply. ((exists ge_representation_real_code_factor_nonzero_giventracestepsmultiplyfirst ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst. (((gr_product_before_factor_nonzero_giventracesteps) = ((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst)) * S ((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstreal ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstreal. (((((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstreal) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_giventracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyfirst) = 2 * ge_signed_half_factor_nonzero_giventracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstreal) = S ge_signed_half_factor_nonzero_giventracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_giventracestepsmultiply) + ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstreal = (ge_first_rn_factor_nonzero_giventracestepsmultiply) + ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstimaginary ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_giventracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyfirst) = 2 * ge_signed_half_factor_nonzero_giventracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstimaginary) = S ge_signed_half_factor_nonzero_giventracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_giventracestepsmultiply) + ge_balance_negative_factor_nonzero_giventracestepsmultiplyfirstimaginary = (ge_first_in_factor_nonzero_giventracestepsmultiply) + ge_balance_positive_factor_nonzero_giventracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_giventracestepsmultiplysecond ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond. (((gr_product_factor_factor_nonzero_giventracesteps) = ((ge_representation_real_code_factor_nonzero_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond)) * S ((ge_representation_real_code_factor_nonzero_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondreal ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondreal. (((((ge_representation_real_code_factor_nonzero_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondreal) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_giventracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factor_nonzero_giventracestepsmultiplysecond) = 2 * ge_signed_half_factor_nonzero_giventracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondreal) = S ge_signed_half_factor_nonzero_giventracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_giventracestepsmultiply) + ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondreal = (ge_second_rn_factor_nonzero_giventracestepsmultiply) + ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondimaginary ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_giventracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplysecond) = 2 * ge_signed_half_factor_nonzero_giventracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondimaginary) = S ge_signed_half_factor_nonzero_giventracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_giventracestepsmultiply) + ge_balance_negative_factor_nonzero_giventracestepsmultiplysecondimaginary = (ge_second_in_factor_nonzero_giventracestepsmultiply) + ge_balance_positive_factor_nonzero_giventracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_giventracestepsmultiplyoutput ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput. (((gr_product_after_factor_nonzero_giventracesteps) = ((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput)) * S ((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputreal ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputreal. (((((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputreal) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_giventracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factor_nonzero_giventracestepsmultiplyoutput) = 2 * ge_signed_half_factor_nonzero_giventracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputreal) = S ge_signed_half_factor_nonzero_giventracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_giventracestepsmultiply) * (ge_second_rp_factor_nonzero_giventracestepsmultiply))) + (((ge_first_rn_factor_nonzero_giventracestepsmultiply) * (ge_second_rn_factor_nonzero_giventracestepsmultiply))))) + (((((ge_first_ip_factor_nonzero_giventracestepsmultiply) * (ge_second_in_factor_nonzero_giventracestepsmultiply))) + (((ge_first_in_factor_nonzero_giventracestepsmultiply) * (ge_second_ip_factor_nonzero_giventracestepsmultiply))))))) + ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputreal = (((((((ge_first_rp_factor_nonzero_giventracestepsmultiply) * (ge_second_rn_factor_nonzero_giventracestepsmultiply))) + (((ge_first_rn_factor_nonzero_giventracestepsmultiply) * (ge_second_rp_factor_nonzero_giventracestepsmultiply))))) + (((((ge_first_ip_factor_nonzero_giventracestepsmultiply) * (ge_second_ip_factor_nonzero_giventracestepsmultiply))) + (((ge_first_in_factor_nonzero_giventracestepsmultiply) * (ge_second_in_factor_nonzero_giventracestepsmultiply))))))) + ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputimaginary ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_giventracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_giventracestepsmultiplyoutput) = 2 * ge_signed_half_factor_nonzero_giventracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputimaginary) = S ge_signed_half_factor_nonzero_giventracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_giventracestepsmultiply) * (ge_second_ip_factor_nonzero_giventracestepsmultiply))) + (((ge_first_rn_factor_nonzero_giventracestepsmultiply) * (ge_second_in_factor_nonzero_giventracestepsmultiply))))) + (((((ge_first_ip_factor_nonzero_giventracestepsmultiply) * (ge_second_rp_factor_nonzero_giventracestepsmultiply))) + (((ge_first_in_factor_nonzero_giventracestepsmultiply) * (ge_second_rn_factor_nonzero_giventracestepsmultiply))))))) + ge_balance_negative_factor_nonzero_giventracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factor_nonzero_giventracestepsmultiply) * (ge_second_in_factor_nonzero_giventracestepsmultiply))) + (((ge_first_rn_factor_nonzero_giventracestepsmultiply) * (ge_second_ip_factor_nonzero_giventracestepsmultiply))))) + (((((ge_first_ip_factor_nonzero_giventracestepsmultiply) * (ge_second_rn_factor_nonzero_giventracestepsmultiply))) + (((ge_first_in_factor_nonzero_giventracestepsmultiply) * (ge_second_rp_factor_nonzero_giventracestepsmultiply))))))) + ge_balance_positive_factor_nonzero_giventracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factor_nonzero_givenreconstruct ge_first_rn_factor_nonzero_givenreconstruct ge_first_ip_factor_nonzero_givenreconstruct ge_first_in_factor_nonzero_givenreconstruct ge_second_rp_factor_nonzero_givenreconstruct ge_second_rn_factor_nonzero_givenreconstruct ge_second_ip_factor_nonzero_givenreconstruct ge_second_in_factor_nonzero_givenreconstruct. ((exists ge_representation_real_code_factor_nonzero_givenreconstructfirst ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst. (((u) = ((ge_representation_real_code_factor_nonzero_givenreconstructfirst) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst)) * S ((ge_representation_real_code_factor_nonzero_givenreconstructfirst) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst)) + ((ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst))) /\ ((exists ge_balance_positive_factor_nonzero_givenreconstructfirstreal ge_balance_negative_factor_nonzero_givenreconstructfirstreal. (((((ge_representation_real_code_factor_nonzero_givenreconstructfirst) = 2 * (ge_balance_positive_factor_nonzero_givenreconstructfirstreal) /\ (ge_balance_negative_factor_nonzero_givenreconstructfirstreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenreconstructfirstrealdecode. (((ge_representation_real_code_factor_nonzero_givenreconstructfirst) = 2 * ge_signed_half_factor_nonzero_givenreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenreconstructfirstreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenreconstructfirstreal) = S ge_signed_half_factor_nonzero_givenreconstructfirstrealdecode))) /\ ((ge_first_rp_factor_nonzero_givenreconstruct) + ge_balance_negative_factor_nonzero_givenreconstructfirstreal = (ge_first_rn_factor_nonzero_givenreconstruct) + ge_balance_positive_factor_nonzero_givenreconstructfirstreal))) /\ (exists ge_balance_positive_factor_nonzero_givenreconstructfirstimaginary ge_balance_negative_factor_nonzero_givenreconstructfirstimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst) = 2 * (ge_balance_positive_factor_nonzero_givenreconstructfirstimaginary) /\ (ge_balance_negative_factor_nonzero_givenreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenreconstructfirst) = 2 * ge_signed_half_factor_nonzero_givenreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenreconstructfirstimaginary) = S ge_signed_half_factor_nonzero_givenreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factor_nonzero_givenreconstruct) + ge_balance_negative_factor_nonzero_givenreconstructfirstimaginary = (ge_first_in_factor_nonzero_givenreconstruct) + ge_balance_positive_factor_nonzero_givenreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_nonzero_givenreconstructsecond ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond. (((gr_factor_product_factor_nonzero_given) = ((ge_representation_real_code_factor_nonzero_givenreconstructsecond) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond)) * S ((ge_representation_real_code_factor_nonzero_givenreconstructsecond) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond)) + ((ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond))) /\ ((exists ge_balance_positive_factor_nonzero_givenreconstructsecondreal ge_balance_negative_factor_nonzero_givenreconstructsecondreal. (((((ge_representation_real_code_factor_nonzero_givenreconstructsecond) = 2 * (ge_balance_positive_factor_nonzero_givenreconstructsecondreal) /\ (ge_balance_negative_factor_nonzero_givenreconstructsecondreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenreconstructsecondrealdecode. (((ge_representation_real_code_factor_nonzero_givenreconstructsecond) = 2 * ge_signed_half_factor_nonzero_givenreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenreconstructsecondreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenreconstructsecondreal) = S ge_signed_half_factor_nonzero_givenreconstructsecondrealdecode))) /\ ((ge_second_rp_factor_nonzero_givenreconstruct) + ge_balance_negative_factor_nonzero_givenreconstructsecondreal = (ge_second_rn_factor_nonzero_givenreconstruct) + ge_balance_positive_factor_nonzero_givenreconstructsecondreal))) /\ (exists ge_balance_positive_factor_nonzero_givenreconstructsecondimaginary ge_balance_negative_factor_nonzero_givenreconstructsecondimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond) = 2 * (ge_balance_positive_factor_nonzero_givenreconstructsecondimaginary) /\ (ge_balance_negative_factor_nonzero_givenreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenreconstructsecond) = 2 * ge_signed_half_factor_nonzero_givenreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenreconstructsecondimaginary) = S ge_signed_half_factor_nonzero_givenreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factor_nonzero_givenreconstruct) + ge_balance_negative_factor_nonzero_givenreconstructsecondimaginary = (ge_second_in_factor_nonzero_givenreconstruct) + ge_balance_positive_factor_nonzero_givenreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_nonzero_givenreconstructoutput ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput. (((z) = ((ge_representation_real_code_factor_nonzero_givenreconstructoutput) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput)) * S ((ge_representation_real_code_factor_nonzero_givenreconstructoutput) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput)) + ((ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput) + (ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput))) /\ ((exists ge_balance_positive_factor_nonzero_givenreconstructoutputreal ge_balance_negative_factor_nonzero_givenreconstructoutputreal. (((((ge_representation_real_code_factor_nonzero_givenreconstructoutput) = 2 * (ge_balance_positive_factor_nonzero_givenreconstructoutputreal) /\ (ge_balance_negative_factor_nonzero_givenreconstructoutputreal) = 0) \/ exists ge_signed_half_factor_nonzero_givenreconstructoutputrealdecode. (((ge_representation_real_code_factor_nonzero_givenreconstructoutput) = 2 * ge_signed_half_factor_nonzero_givenreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factor_nonzero_givenreconstructoutputreal) = 0) /\ (ge_balance_negative_factor_nonzero_givenreconstructoutputreal) = S ge_signed_half_factor_nonzero_givenreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenreconstruct) * (ge_second_rp_factor_nonzero_givenreconstruct))) + (((ge_first_rn_factor_nonzero_givenreconstruct) * (ge_second_rn_factor_nonzero_givenreconstruct))))) + (((((ge_first_ip_factor_nonzero_givenreconstruct) * (ge_second_in_factor_nonzero_givenreconstruct))) + (((ge_first_in_factor_nonzero_givenreconstruct) * (ge_second_ip_factor_nonzero_givenreconstruct))))))) + ge_balance_negative_factor_nonzero_givenreconstructoutputreal = (((((((ge_first_rp_factor_nonzero_givenreconstruct) * (ge_second_rn_factor_nonzero_givenreconstruct))) + (((ge_first_rn_factor_nonzero_givenreconstruct) * (ge_second_rp_factor_nonzero_givenreconstruct))))) + (((((ge_first_ip_factor_nonzero_givenreconstruct) * (ge_second_ip_factor_nonzero_givenreconstruct))) + (((ge_first_in_factor_nonzero_givenreconstruct) * (ge_second_in_factor_nonzero_givenreconstruct))))))) + ge_balance_positive_factor_nonzero_givenreconstructoutputreal))) /\ (exists ge_balance_positive_factor_nonzero_givenreconstructoutputimaginary ge_balance_negative_factor_nonzero_givenreconstructoutputimaginary. (((((ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput) = 2 * (ge_balance_positive_factor_nonzero_givenreconstructoutputimaginary) /\ (ge_balance_negative_factor_nonzero_givenreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factor_nonzero_givenreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factor_nonzero_givenreconstructoutput) = 2 * ge_signed_half_factor_nonzero_givenreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_nonzero_givenreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factor_nonzero_givenreconstructoutputimaginary) = S ge_signed_half_factor_nonzero_givenreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_nonzero_givenreconstruct) * (ge_second_ip_factor_nonzero_givenreconstruct))) + (((ge_first_rn_factor_nonzero_givenreconstruct) * (ge_second_in_factor_nonzero_givenreconstruct))))) + (((((ge_first_ip_factor_nonzero_givenreconstruct) * (ge_second_rp_factor_nonzero_givenreconstruct))) + (((ge_first_in_factor_nonzero_givenreconstruct) * (ge_second_rn_factor_nonzero_givenreconstruct))))))) + ge_balance_negative_factor_nonzero_givenreconstructoutputimaginary = (((((((ge_first_rp_factor_nonzero_givenreconstruct) * (ge_second_in_factor_nonzero_givenreconstruct))) + (((ge_first_rn_factor_nonzero_givenreconstruct) * (ge_second_ip_factor_nonzero_givenreconstruct))))) + (((((ge_first_ip_factor_nonzero_givenreconstruct) * (ge_second_rn_factor_nonzero_givenreconstruct))) + (((ge_first_in_factor_nonzero_givenreconstruct) * (ge_second_rp_factor_nonzero_givenreconstruct))))))) + ge_balance_positive_factor_nonzero_givenreconstructoutputimaginary)))))))))))))) -> ~(z=0)Complete tactic proof in conservative notation
All 30 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
30 script commands · 6 reading checkpoints · 1 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (3)
01Fix variables and assumptionsL1–7
02Separate the logical casesL8–11
03Establish hcasesL12–17
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply zero implies zero factor.
04Separate the logical casesL18–18
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L18
cases hcases
05Use earlier factsL19–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
specialize gaussian_unit_nonzero (u) - L20
apply gaussian_unit_nonzero - L21
exact hf_left - L22
exact hcases_left - L23
specialize gaussian_all_irreducible_product_nonzero (l) - L24
specialize gaussian_all_irreducible_product_nonzero (b) - L25
specialize gaussian_all_irreducible_product_nonzero (c) - L26
specialize gaussian_all_irreducible_product_nonzero (x) - L27
apply gaussian_all_irreducible_product_nonzero - L28
exact hf_right_left
Original defined command ledger · 30 lines
- 0001
intro z - 0002
intro u - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro hf - 0007
intro hz - 0008
cases hf - 0009
cases hf_right - 0010
cases hf_right_right - 0011
cases hf_right_right_witness - 0012
have hcases : u=0 \/ x=0 - 0013
specialize gaussian_multiply_zero_implies_zero_factor (u) - 0014
specialize gaussian_multiply_zero_implies_zero_factor (x) - 0015
apply gaussian_multiply_zero_implies_zero_factor - 0016
rewrite hz at hf_right_right_witness_right - 0017
exact hf_right_right_witness_right - 0018
cases hcases - 0019
specialize gaussian_unit_nonzero (u) - 0020
apply gaussian_unit_nonzero - 0021
exact hf_left - 0022
exact hcases_left - 0023
specialize gaussian_all_irreducible_product_nonzero (l) - 0024
specialize gaussian_all_irreducible_product_nonzero (b) - 0025
specialize gaussian_all_irreducible_product_nonzero (c) - 0026
specialize gaussian_all_irreducible_product_nonzero (x) - 0027
apply gaussian_all_irreducible_product_nonzero - 0028
exact hf_right_left - 0029
exact hf_right_right_witness_left - 0030
exact hcases_right