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
∀ b. ∀ c. ∀ l. ∀ m. l = m → GAllIrreducible(b,c,l) → GAllIrreducible(b,c,m)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall b c l m. l=m -> (forall gr_factor_index_irreducible_length_old gr_factor_value_irreducible_length_old. (exists ge_gap_irreducible_length_oldindex. ge_gap_irreducible_length_oldindex + S (gr_factor_index_irreducible_length_old) = (l)) -> (((exists ff_h_gprod_irreducible_length_oldentry. ff_h_gprod_irreducible_length_oldentry + S (gr_factor_value_irreducible_length_old) = S ((S (gr_factor_index_irreducible_length_old)) * c)) /\ exists ff_q_gprod_irreducible_length_oldentry. b = ff_q_gprod_irreducible_length_oldentry * S ((S (gr_factor_index_irreducible_length_old)) * c) + (gr_factor_value_irreducible_length_old))) -> (((exists ge_real_positive_irreducible_length_oldirreduciblecarrier ge_real_negative_irreducible_length_oldirreduciblecarrier ge_imaginary_positive_irreducible_length_oldirreduciblecarrier ge_imaginary_negative_irreducible_length_oldirreduciblecarrier. (exists ge_real_code_irreducible_length_oldirreduciblecarrierdecode ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode. (((gr_factor_value_irreducible_length_old) = ((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_length_oldirreduciblecarrier) /\ (ge_real_negative_irreducible_length_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_real. (((ge_real_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_length_oldirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_length_oldirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_length_oldirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_length_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_length_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_length_oldirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_length_oldirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_oldirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_length_old)=0)) /\ ((~(exists gr_inverse_irreducible_length_oldirreduciblenonunit. (exists ge_first_rp_irreducible_length_oldirreduciblenonunitidentity ge_first_rn_irreducible_length_oldirreduciblenonunitidentity ge_first_ip_irreducible_length_oldirreduciblenonunitidentity ge_first_in_irreducible_length_oldirreduciblenonunitidentity ge_second_rp_irreducible_length_oldirreduciblenonunitidentity ge_second_rn_irreducible_length_oldirreduciblenonunitidentity ge_second_ip_irreducible_length_oldirreduciblenonunitidentity ge_second_in_irreducible_length_oldirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_length_old) = ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_length_oldirreduciblenonunit) = ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_length_oldirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_in_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_oldirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_oldirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_length_oldirreducible gr_second_factor_irreducible_length_oldirreducible. (exists ge_first_rp_irreducible_length_oldirreduciblefactorization ge_first_rn_irreducible_length_oldirreduciblefactorization ge_first_ip_irreducible_length_oldirreduciblefactorization ge_first_in_irreducible_length_oldirreduciblefactorization ge_second_rp_irreducible_length_oldirreduciblefactorization ge_second_rn_irreducible_length_oldirreduciblefactorization ge_second_ip_irreducible_length_oldirreduciblefactorization ge_second_in_irreducible_length_oldirreduciblefactorization. ((exists ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst. (((gr_first_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond. (((gr_second_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblefactorization) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_length_oldirreduciblefactorization) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput. (((gr_factor_value_irreducible_length_old) = ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_oldirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblefactorization) * (ge_second_in_irreducible_length_oldirreduciblefactorization))) + (((ge_first_rn_irreducible_length_oldirreduciblefactorization) * (ge_second_ip_irreducible_length_oldirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefactorization) * (ge_second_rn_irreducible_length_oldirreduciblefactorization))) + (((ge_first_in_irreducible_length_oldirreduciblefactorization) * (ge_second_rp_irreducible_length_oldirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_oldirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_length_oldirreduciblefirst_unit. (exists ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_length_oldirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_length_oldirreduciblesecond_unit. (exists ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_length_oldirreducible) = ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_length_oldirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_oldirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_oldirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_oldirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (forall gr_factor_index_irreducible_length_new gr_factor_value_irreducible_length_new. (exists ge_gap_irreducible_length_newindex. ge_gap_irreducible_length_newindex + S (gr_factor_index_irreducible_length_new) = (m)) -> (((exists ff_h_gprod_irreducible_length_newentry. ff_h_gprod_irreducible_length_newentry + S (gr_factor_value_irreducible_length_new) = S ((S (gr_factor_index_irreducible_length_new)) * c)) /\ exists ff_q_gprod_irreducible_length_newentry. b = ff_q_gprod_irreducible_length_newentry * S ((S (gr_factor_index_irreducible_length_new)) * c) + (gr_factor_value_irreducible_length_new))) -> (((exists ge_real_positive_irreducible_length_newirreduciblecarrier ge_real_negative_irreducible_length_newirreduciblecarrier ge_imaginary_positive_irreducible_length_newirreduciblecarrier ge_imaginary_negative_irreducible_length_newirreduciblecarrier. (exists ge_real_code_irreducible_length_newirreduciblecarrierdecode ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode. (((gr_factor_value_irreducible_length_new) = ((ge_real_code_irreducible_length_newirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_length_newirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_length_newirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_length_newirreduciblecarrier) /\ (ge_real_negative_irreducible_length_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_real. (((ge_real_code_irreducible_length_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_length_newirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_length_newirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_length_newirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_length_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_length_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_length_newirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_length_newirreduciblecarrier) = S ge_signed_half_ge_irreducible_length_newirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_length_new)=0)) /\ ((~(exists gr_inverse_irreducible_length_newirreduciblenonunit. (exists ge_first_rp_irreducible_length_newirreduciblenonunitidentity ge_first_rn_irreducible_length_newirreduciblenonunitidentity ge_first_ip_irreducible_length_newirreduciblenonunitidentity ge_first_in_irreducible_length_newirreduciblenonunitidentity ge_second_rp_irreducible_length_newirreduciblenonunitidentity ge_second_rn_irreducible_length_newirreduciblenonunitidentity ge_second_ip_irreducible_length_newirreduciblenonunitidentity ge_second_in_irreducible_length_newirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_length_new) = ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_length_newirreduciblenonunit) = ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblenonunitidentity) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_length_newirreduciblenonunitidentity) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblenonunitidentity) * (ge_second_in_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblenonunitidentity) * (ge_second_ip_irreducible_length_newirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rn_irreducible_length_newirreduciblenonunitidentity))) + (((ge_first_in_irreducible_length_newirreduciblenonunitidentity) * (ge_second_rp_irreducible_length_newirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_length_newirreducible gr_second_factor_irreducible_length_newirreducible. (exists ge_first_rp_irreducible_length_newirreduciblefactorization ge_first_rn_irreducible_length_newirreduciblefactorization ge_first_ip_irreducible_length_newirreduciblefactorization ge_first_in_irreducible_length_newirreduciblefactorization ge_second_rp_irreducible_length_newirreduciblefactorization ge_second_rn_irreducible_length_newirreduciblefactorization ge_second_ip_irreducible_length_newirreduciblefactorization ge_second_in_irreducible_length_newirreduciblefactorization. ((exists ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst. (((gr_first_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_length_newirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond. (((gr_second_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_length_newirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblefactorization) + ge_balance_negative_irreducible_length_newirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_length_newirreduciblefactorization) + ge_balance_positive_irreducible_length_newirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput. (((gr_factor_value_irreducible_length_new) = ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_length_newirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))))))) + ge_balance_negative_irreducible_length_newirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblefactorization) * (ge_second_in_irreducible_length_newirreduciblefactorization))) + (((ge_first_rn_irreducible_length_newirreduciblefactorization) * (ge_second_ip_irreducible_length_newirreduciblefactorization))))) + (((((ge_first_ip_irreducible_length_newirreduciblefactorization) * (ge_second_rn_irreducible_length_newirreduciblefactorization))) + (((ge_first_in_irreducible_length_newirreduciblefactorization) * (ge_second_rp_irreducible_length_newirreduciblefactorization))))))) + ge_balance_positive_irreducible_length_newirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_length_newirreduciblefirst_unit. (exists ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity ge_first_in_irreducible_length_newirreduciblefirst_unitidentity ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity ge_second_in_irreducible_length_newirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_length_newirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_in_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_length_newirreduciblesecond_unit. (exists ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity ge_first_in_irreducible_length_newirreduciblesecond_unitidentity ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity ge_second_in_irreducible_length_newirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_length_newirreducible) = ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_length_newirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_length_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_length_newirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_in_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_length_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_length_newirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_length_newirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_length_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_length_newirreduciblesecond_unitidentityoutputimaginary))))))))))))))))Complete tactic proof in conservative notation
All 8 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
8 script commands · 3 reading checkpoints · 0 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.
01Fix variables and assumptionsL1–6
02Calculate and transport equalitiesL7–7
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L7
rewrite heq at h
03Use earlier factsL8–8
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L8
exact h