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. GAllIrreducible(b,c,S l) → GAllIrreducible(b,c,l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
lt_of_lt_of_le · checked external prerequisitele_succ_self · checked external prerequisite
Original expanded first-order statement
forall b c l. (forall gr_factor_index_irreducible_full gr_factor_value_irreducible_full. (exists ge_gap_irreducible_fullindex. ge_gap_irreducible_fullindex + S (gr_factor_index_irreducible_full) = (S l)) -> (((exists ff_h_gprod_irreducible_fullentry. ff_h_gprod_irreducible_fullentry + S (gr_factor_value_irreducible_full) = S ((S (gr_factor_index_irreducible_full)) * c)) /\ exists ff_q_gprod_irreducible_fullentry. b = ff_q_gprod_irreducible_fullentry * S ((S (gr_factor_index_irreducible_full)) * c) + (gr_factor_value_irreducible_full))) -> (((exists ge_real_positive_irreducible_fullirreduciblecarrier ge_real_negative_irreducible_fullirreduciblecarrier ge_imaginary_positive_irreducible_fullirreduciblecarrier ge_imaginary_negative_irreducible_fullirreduciblecarrier. (exists ge_real_code_irreducible_fullirreduciblecarrierdecode ge_imaginary_code_irreducible_fullirreduciblecarrierdecode. (((gr_factor_value_irreducible_full) = ((ge_real_code_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_fullirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_fullirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_fullirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_fullirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_fullirreduciblecarrier) /\ (ge_real_negative_irreducible_fullirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_fullirreduciblecarrierdecode_real. (((ge_real_code_irreducible_fullirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_fullirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_fullirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_fullirreduciblecarrier) = S ge_signed_half_ge_irreducible_fullirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_fullirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_fullirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_fullirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_fullirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_fullirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_fullirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_fullirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_fullirreduciblecarrier) = S ge_signed_half_ge_irreducible_fullirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_full)=0)) /\ ((~(exists gr_inverse_irreducible_fullirreduciblenonunit. (exists ge_first_rp_irreducible_fullirreduciblenonunitidentity ge_first_rn_irreducible_fullirreduciblenonunitidentity ge_first_ip_irreducible_fullirreduciblenonunitidentity ge_first_in_irreducible_fullirreduciblenonunitidentity ge_second_rp_irreducible_fullirreduciblenonunitidentity ge_second_rn_irreducible_fullirreduciblenonunitidentity ge_second_ip_irreducible_fullirreduciblenonunitidentity ge_second_in_irreducible_fullirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_fullirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_full) = ((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_fullirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_fullirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_irreducible_fullirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_irreducible_fullirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_fullirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_fullirreduciblenonunit) = ((ge_representation_real_code_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_fullirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_fullirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_fullirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_irreducible_fullirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_irreducible_fullirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_fullirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_fullirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_fullirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_fullirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_fullirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_fullirreducible gr_second_factor_irreducible_fullirreducible. (exists ge_first_rp_irreducible_fullirreduciblefactorization ge_first_rn_irreducible_fullirreduciblefactorization ge_first_ip_irreducible_fullirreduciblefactorization ge_first_in_irreducible_fullirreduciblefactorization ge_second_rp_irreducible_fullirreduciblefactorization ge_second_rn_irreducible_fullirreduciblefactorization ge_second_ip_irreducible_fullirreduciblefactorization ge_second_in_irreducible_fullirreduciblefactorization. ((exists ge_representation_real_code_irreducible_fullirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst. (((gr_first_factor_irreducible_fullirreducible) = ((ge_representation_real_code_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblefactorizationfirstreal ge_balance_negative_irreducible_fullirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_fullirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_fullirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_fullirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_fullirreduciblefactorization) + ge_balance_negative_irreducible_fullirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_fullirreduciblefactorization) + ge_balance_positive_irreducible_fullirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_fullirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_fullirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_fullirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_fullirreduciblefactorization) + ge_balance_negative_irreducible_fullirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_fullirreduciblefactorization) + ge_balance_positive_irreducible_fullirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_fullirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond. (((gr_second_factor_irreducible_fullirreducible) = ((ge_representation_real_code_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblefactorizationsecondreal ge_balance_negative_irreducible_fullirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_fullirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_fullirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_fullirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_fullirreduciblefactorization) + ge_balance_negative_irreducible_fullirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_fullirreduciblefactorization) + ge_balance_positive_irreducible_fullirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_fullirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_fullirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_fullirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_fullirreduciblefactorization) + ge_balance_negative_irreducible_fullirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_fullirreduciblefactorization) + ge_balance_positive_irreducible_fullirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_fullirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput. (((gr_factor_value_irreducible_full) = ((ge_representation_real_code_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblefactorizationoutputreal ge_balance_negative_irreducible_fullirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_fullirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_fullirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_fullirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblefactorization) * (ge_second_rp_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_irreducible_fullirreduciblefactorization) * (ge_second_rn_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_irreducible_fullirreduciblefactorization) * (ge_second_in_irreducible_fullirreduciblefactorization))) + (((ge_first_in_irreducible_fullirreduciblefactorization) * (ge_second_ip_irreducible_fullirreduciblefactorization))))))) + ge_balance_negative_irreducible_fullirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_fullirreduciblefactorization) * (ge_second_rn_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_irreducible_fullirreduciblefactorization) * (ge_second_rp_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_irreducible_fullirreduciblefactorization) * (ge_second_ip_irreducible_fullirreduciblefactorization))) + (((ge_first_in_irreducible_fullirreduciblefactorization) * (ge_second_in_irreducible_fullirreduciblefactorization))))))) + ge_balance_positive_irreducible_fullirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_fullirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_fullirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_fullirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblefactorization) * (ge_second_ip_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_irreducible_fullirreduciblefactorization) * (ge_second_in_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_irreducible_fullirreduciblefactorization) * (ge_second_rp_irreducible_fullirreduciblefactorization))) + (((ge_first_in_irreducible_fullirreduciblefactorization) * (ge_second_rn_irreducible_fullirreduciblefactorization))))))) + ge_balance_negative_irreducible_fullirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_fullirreduciblefactorization) * (ge_second_in_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_irreducible_fullirreduciblefactorization) * (ge_second_ip_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_irreducible_fullirreduciblefactorization) * (ge_second_rn_irreducible_fullirreduciblefactorization))) + (((ge_first_in_irreducible_fullirreduciblefactorization) * (ge_second_rp_irreducible_fullirreduciblefactorization))))))) + ge_balance_positive_irreducible_fullirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_fullirreduciblefirst_unit. (exists ge_first_rp_irreducible_fullirreduciblefirst_unitidentity ge_first_rn_irreducible_fullirreduciblefirst_unitidentity ge_first_ip_irreducible_fullirreduciblefirst_unitidentity ge_first_in_irreducible_fullirreduciblefirst_unitidentity ge_second_rp_irreducible_fullirreduciblefirst_unitidentity ge_second_rn_irreducible_fullirreduciblefirst_unitidentity ge_second_ip_irreducible_fullirreduciblefirst_unitidentity ge_second_in_irreducible_fullirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_fullirreducible) = ((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_fullirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_fullirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_fullirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_fullirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_fullirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_fullirreduciblesecond_unit. (exists ge_first_rp_irreducible_fullirreduciblesecond_unitidentity ge_first_rn_irreducible_fullirreduciblesecond_unitidentity ge_first_ip_irreducible_fullirreduciblesecond_unitidentity ge_first_in_irreducible_fullirreduciblesecond_unitidentity ge_second_rp_irreducible_fullirreduciblesecond_unitidentity ge_second_rn_irreducible_fullirreduciblesecond_unitidentity ge_second_ip_irreducible_fullirreduciblesecond_unitidentity ge_second_in_irreducible_fullirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_fullirreducible) = ((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_fullirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_fullirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_fullirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_fullirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_fullirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (forall gr_factor_index_irreducible_prefix gr_factor_value_irreducible_prefix. (exists ge_gap_irreducible_prefixindex. ge_gap_irreducible_prefixindex + S (gr_factor_index_irreducible_prefix) = (l)) -> (((exists ff_h_gprod_irreducible_prefixentry. ff_h_gprod_irreducible_prefixentry + S (gr_factor_value_irreducible_prefix) = S ((S (gr_factor_index_irreducible_prefix)) * c)) /\ exists ff_q_gprod_irreducible_prefixentry. b = ff_q_gprod_irreducible_prefixentry * S ((S (gr_factor_index_irreducible_prefix)) * c) + (gr_factor_value_irreducible_prefix))) -> (((exists ge_real_positive_irreducible_prefixirreduciblecarrier ge_real_negative_irreducible_prefixirreduciblecarrier ge_imaginary_positive_irreducible_prefixirreduciblecarrier ge_imaginary_negative_irreducible_prefixirreduciblecarrier. (exists ge_real_code_irreducible_prefixirreduciblecarrierdecode ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode. (((gr_factor_value_irreducible_prefix) = ((ge_real_code_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_prefixirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_prefixirreduciblecarrier) /\ (ge_real_negative_irreducible_prefixirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prefixirreduciblecarrierdecode_real. (((ge_real_code_irreducible_prefixirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_prefixirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_prefixirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_prefixirreduciblecarrier) = S ge_signed_half_ge_irreducible_prefixirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_prefixirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_prefixirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prefixirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_prefixirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_prefixirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_prefixirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_prefixirreduciblecarrier) = S ge_signed_half_ge_irreducible_prefixirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_irreducible_prefix)=0)) /\ ((~(exists gr_inverse_irreducible_prefixirreduciblenonunit. (exists ge_first_rp_irreducible_prefixirreduciblenonunitidentity ge_first_rn_irreducible_prefixirreduciblenonunitidentity ge_first_ip_irreducible_prefixirreduciblenonunitidentity ge_first_in_irreducible_prefixirreduciblenonunitidentity ge_second_rp_irreducible_prefixirreduciblenonunitidentity ge_second_rn_irreducible_prefixirreduciblenonunitidentity ge_second_ip_irreducible_prefixirreduciblenonunitidentity ge_second_in_irreducible_prefixirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst. (((gr_factor_value_irreducible_prefix) = ((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_prefixirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_irreducible_prefixirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_irreducible_prefixirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prefixirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_prefixirreduciblenonunit) = ((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_prefixirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_prefixirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_irreducible_prefixirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_irreducible_prefixirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_prefixirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_prefixirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_prefixirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_prefixirreducible gr_second_factor_irreducible_prefixirreducible. (exists ge_first_rp_irreducible_prefixirreduciblefactorization ge_first_rn_irreducible_prefixirreduciblefactorization ge_first_ip_irreducible_prefixirreduciblefactorization ge_first_in_irreducible_prefixirreduciblefactorization ge_second_rp_irreducible_prefixirreduciblefactorization ge_second_rn_irreducible_prefixirreduciblefactorization ge_second_ip_irreducible_prefixirreduciblefactorization ge_second_in_irreducible_prefixirreduciblefactorization. ((exists ge_representation_real_code_irreducible_prefixirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst. (((gr_first_factor_irreducible_prefixirreducible) = ((ge_representation_real_code_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstreal ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_prefixirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_prefixirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_prefixirreduciblefactorization) + ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_prefixirreduciblefactorization) + ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_prefixirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prefixirreduciblefactorization) + ge_balance_negative_irreducible_prefixirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_prefixirreduciblefactorization) + ge_balance_positive_irreducible_prefixirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prefixirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond. (((gr_second_factor_irreducible_prefixirreducible) = ((ge_representation_real_code_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondreal ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_prefixirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_prefixirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_prefixirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_prefixirreduciblefactorization) + ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_prefixirreduciblefactorization) + ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_prefixirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_prefixirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prefixirreduciblefactorization) + ge_balance_negative_irreducible_prefixirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_prefixirreduciblefactorization) + ge_balance_positive_irreducible_prefixirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prefixirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput. (((gr_factor_value_irreducible_prefix) = ((ge_representation_real_code_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputreal ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_prefixirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_prefixirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblefactorization) * (ge_second_rp_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_irreducible_prefixirreduciblefactorization) * (ge_second_rn_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_irreducible_prefixirreduciblefactorization) * (ge_second_in_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_irreducible_prefixirreduciblefactorization) * (ge_second_ip_irreducible_prefixirreduciblefactorization))))))) + ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_prefixirreduciblefactorization) * (ge_second_rn_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_irreducible_prefixirreduciblefactorization) * (ge_second_rp_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_irreducible_prefixirreduciblefactorization) * (ge_second_ip_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_irreducible_prefixirreduciblefactorization) * (ge_second_in_irreducible_prefixirreduciblefactorization))))))) + ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_prefixirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblefactorization) * (ge_second_ip_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_irreducible_prefixirreduciblefactorization) * (ge_second_in_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_irreducible_prefixirreduciblefactorization) * (ge_second_rp_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_irreducible_prefixirreduciblefactorization) * (ge_second_rn_irreducible_prefixirreduciblefactorization))))))) + ge_balance_negative_irreducible_prefixirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_prefixirreduciblefactorization) * (ge_second_in_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_irreducible_prefixirreduciblefactorization) * (ge_second_ip_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_irreducible_prefixirreduciblefactorization) * (ge_second_rn_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_irreducible_prefixirreduciblefactorization) * (ge_second_rp_irreducible_prefixirreduciblefactorization))))))) + ge_balance_positive_irreducible_prefixirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_prefixirreduciblefirst_unit. (exists ge_first_rp_irreducible_prefixirreduciblefirst_unitidentity ge_first_rn_irreducible_prefixirreduciblefirst_unitidentity ge_first_ip_irreducible_prefixirreduciblefirst_unitidentity ge_first_in_irreducible_prefixirreduciblefirst_unitidentity ge_second_rp_irreducible_prefixirreduciblefirst_unitidentity ge_second_rn_irreducible_prefixirreduciblefirst_unitidentity ge_second_ip_irreducible_prefixirreduciblefirst_unitidentity ge_second_in_irreducible_prefixirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_prefixirreducible) = ((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_prefixirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_prefixirreduciblesecond_unit. (exists ge_first_rp_irreducible_prefixirreduciblesecond_unitidentity ge_first_rn_irreducible_prefixirreduciblesecond_unitidentity ge_first_ip_irreducible_prefixirreduciblesecond_unitidentity ge_first_in_irreducible_prefixirreduciblesecond_unitidentity ge_second_rp_irreducible_prefixirreduciblesecond_unitidentity ge_second_rn_irreducible_prefixirreduciblesecond_unitidentity ge_second_ip_irreducible_prefixirreduciblesecond_unitidentity ge_second_in_irreducible_prefixirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_prefixirreducible) = ((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_prefixirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary))))))))))))))))Complete tactic proof in conservative notation
All 19 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
19 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–8
02Use earlier factsL9–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
03Use earlier factsL19–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
exact hp
Original defined command ledger · 19 lines
- 0001
intro b - 0002
intro c - 0003
intro l - 0004
intro h - 0005
intro i - 0006
intro p - 0007
intro hi - 0008
intro hp - 0009
specialize h (i) - 0010
specialize h (p) - 0011
apply h - 0012
specialize lt_of_lt_of_le (i) - 0013
specialize lt_of_lt_of_le (l) - 0014
specialize lt_of_lt_of_le (S l) - 0015
apply lt_of_lt_of_le - 0016
exact hi - 0017
specialize le_succ_self (l) - 0018
apply le_succ_self - 0019
exact hp