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. ∀ d. ∀ e. ∀ l. ∀ p. GAllIrreducible(b,c,l) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)) → BetaAt(d,e,l,p) → GIrreducible(p) → GAllIrreducible(d,e,S l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisitegaussian_product_beta_index_transportgaussian_irreducible_code_transportfactor_permutation_prefix_reflect · checked external prerequisite
Original expanded first-order statement
forall b c d e l p. (forall gr_factor_index_append_irreducible_prefix gr_factor_value_append_irreducible_prefix. (exists ge_gap_append_irreducible_prefixindex. ge_gap_append_irreducible_prefixindex + S (gr_factor_index_append_irreducible_prefix) = (l)) -> (((exists ff_h_gprod_append_irreducible_prefixentry. ff_h_gprod_append_irreducible_prefixentry + S (gr_factor_value_append_irreducible_prefix) = S ((S (gr_factor_index_append_irreducible_prefix)) * c)) /\ exists ff_q_gprod_append_irreducible_prefixentry. b = ff_q_gprod_append_irreducible_prefixentry * S ((S (gr_factor_index_append_irreducible_prefix)) * c) + (gr_factor_value_append_irreducible_prefix))) -> (((exists ge_real_positive_append_irreducible_prefixirreduciblecarrier ge_real_negative_append_irreducible_prefixirreduciblecarrier ge_imaginary_positive_append_irreducible_prefixirreduciblecarrier ge_imaginary_negative_append_irreducible_prefixirreduciblecarrier. (exists ge_real_code_append_irreducible_prefixirreduciblecarrierdecode ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode. (((gr_factor_value_append_irreducible_prefix) = ((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode)) * S ((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode)) + ((ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode))) /\ (((((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * (ge_real_positive_append_irreducible_prefixirreduciblecarrier) /\ (ge_real_negative_append_irreducible_prefixirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_real. (((ge_real_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_append_irreducible_prefixirreduciblecarrier) = 0) /\ (ge_real_negative_append_irreducible_prefixirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_append_irreducible_prefixirreduciblecarrier) /\ (ge_imaginary_negative_append_irreducible_prefixirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_append_irreducible_prefixirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_append_irreducible_prefixirreduciblecarrier) = 0) /\ (ge_imaginary_negative_append_irreducible_prefixirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_prefixirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_append_irreducible_prefix)=0)) /\ ((~(exists gr_inverse_append_irreducible_prefixirreduciblenonunit. (exists ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity ge_first_in_append_irreducible_prefixirreduciblenonunitidentity ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity ge_second_in_append_irreducible_prefixirreduciblenonunitidentity. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst. (((gr_factor_value_append_irreducible_prefix) = ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond. (((gr_inverse_append_irreducible_prefixirreduciblenonunit) = ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondreal = (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_in_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_append_irreducible_prefixirreducible gr_second_factor_append_irreducible_prefixirreducible. (exists ge_first_rp_append_irreducible_prefixirreduciblefactorization ge_first_rn_append_irreducible_prefixirreduciblefactorization ge_first_ip_append_irreducible_prefixirreduciblefactorization ge_first_in_append_irreducible_prefixirreduciblefactorization ge_second_rp_append_irreducible_prefixirreduciblefactorization ge_second_rn_append_irreducible_prefixirreduciblefactorization ge_second_ip_append_irreducible_prefixirreduciblefactorization ge_second_in_append_irreducible_prefixirreduciblefactorization. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst. (((gr_first_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond. (((gr_second_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondreal = (ge_second_rn_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblefactorization) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationsecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblefactorization) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput. (((gr_factor_value_append_irreducible_prefix) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblefactorization) * (ge_second_in_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_rn_append_irreducible_prefixirreduciblefactorization) * (ge_second_ip_append_irreducible_prefixirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefactorization) * (ge_second_rn_append_irreducible_prefixirreduciblefactorization))) + (((ge_first_in_append_irreducible_prefixirreduciblefactorization) * (ge_second_rp_append_irreducible_prefixirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_append_irreducible_prefixirreduciblefirst_unit. (exists ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst. (((gr_first_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond. (((gr_inverse_append_irreducible_prefixirreduciblefirst_unit) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal = (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_append_irreducible_prefixirreduciblesecond_unit. (exists ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity. ((exists ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst. (((gr_second_factor_append_irreducible_prefixirreducible) = ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal = (ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond. (((gr_inverse_append_irreducible_prefixirreduciblesecond_unit) = ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal = (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_prefixirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_prefixirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_prefixirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_prefixirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_prefixirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_prefixirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (forall pfp_i_append_irreducible_preserve pfp_a_append_irreducible_preserve. (exists pfp_gap_append_irreducible_preservebound. pfp_gap_append_irreducible_preservebound + S (pfp_i_append_irreducible_preserve) = (l)) -> (((exists ff_h_pfp_append_irreducible_preserveold. ff_h_pfp_append_irreducible_preserveold + S (pfp_a_append_irreducible_preserve) = S ((S (pfp_i_append_irreducible_preserve)) * c)) /\ exists ff_q_pfp_append_irreducible_preserveold. b = ff_q_pfp_append_irreducible_preserveold * S ((S (pfp_i_append_irreducible_preserve)) * c) + (pfp_a_append_irreducible_preserve))) -> (((exists ff_h_pfp_append_irreducible_preservenew. ff_h_pfp_append_irreducible_preservenew + S (pfp_a_append_irreducible_preserve) = S ((S (pfp_i_append_irreducible_preserve)) * e)) /\ exists ff_q_pfp_append_irreducible_preservenew. d = ff_q_pfp_append_irreducible_preservenew * S ((S (pfp_i_append_irreducible_preserve)) * e) + (pfp_a_append_irreducible_preserve)))) -> (((exists ff_h_gprod_append_irreducible_last. ff_h_gprod_append_irreducible_last + S (p) = S ((S (l)) * e)) /\ exists ff_q_gprod_append_irreducible_last. d = ff_q_gprod_append_irreducible_last * S ((S (l)) * e) + (p))) -> (((exists ge_real_positive_append_irreducible_factorcarrier ge_real_negative_append_irreducible_factorcarrier ge_imaginary_positive_append_irreducible_factorcarrier ge_imaginary_negative_append_irreducible_factorcarrier. (exists ge_real_code_append_irreducible_factorcarrierdecode ge_imaginary_code_append_irreducible_factorcarrierdecode. (((p) = ((ge_real_code_append_irreducible_factorcarrierdecode) + (ge_imaginary_code_append_irreducible_factorcarrierdecode)) * S ((ge_real_code_append_irreducible_factorcarrierdecode) + (ge_imaginary_code_append_irreducible_factorcarrierdecode)) + ((ge_imaginary_code_append_irreducible_factorcarrierdecode) + (ge_imaginary_code_append_irreducible_factorcarrierdecode))) /\ (((((ge_real_code_append_irreducible_factorcarrierdecode) = 2 * (ge_real_positive_append_irreducible_factorcarrier) /\ (ge_real_negative_append_irreducible_factorcarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_factorcarrierdecode_real. (((ge_real_code_append_irreducible_factorcarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_factorcarrierdecode_real + 1 /\ (ge_real_positive_append_irreducible_factorcarrier) = 0) /\ (ge_real_negative_append_irreducible_factorcarrier) = S ge_signed_half_ge_append_irreducible_factorcarrierdecode_real))) /\ ((((ge_imaginary_code_append_irreducible_factorcarrierdecode) = 2 * (ge_imaginary_positive_append_irreducible_factorcarrier) /\ (ge_imaginary_negative_append_irreducible_factorcarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_factorcarrierdecode_imaginary. (((ge_imaginary_code_append_irreducible_factorcarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_factorcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_append_irreducible_factorcarrier) = 0) /\ (ge_imaginary_negative_append_irreducible_factorcarrier) = S ge_signed_half_ge_append_irreducible_factorcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_append_irreducible_factornonunit. (exists ge_first_rp_append_irreducible_factornonunitidentity ge_first_rn_append_irreducible_factornonunitidentity ge_first_ip_append_irreducible_factornonunitidentity ge_first_in_append_irreducible_factornonunitidentity ge_second_rp_append_irreducible_factornonunitidentity ge_second_rn_append_irreducible_factornonunitidentity ge_second_ip_append_irreducible_factornonunitidentity ge_second_in_append_irreducible_factornonunitidentity. ((exists ge_representation_real_code_append_irreducible_factornonunitidentityfirst ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst. (((p) = ((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_factornonunitidentityfirstreal ge_balance_negative_append_irreducible_factornonunitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_factornonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_factornonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstreal) = S ge_signed_half_append_irreducible_factornonunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentityfirstreal = (ge_first_rn_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factornonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_factornonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary) = S ge_signed_half_append_irreducible_factornonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentityfirstimaginary = (ge_first_in_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factornonunitidentitysecond ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond. (((gr_inverse_append_irreducible_factornonunit) = ((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_factornonunitidentitysecondreal ge_balance_negative_append_irreducible_factornonunitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_factornonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_factornonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondreal) = S ge_signed_half_append_irreducible_factornonunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentitysecondreal = (ge_second_rn_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factornonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_factornonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary) = S ge_signed_half_append_irreducible_factornonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factornonunitidentity) + ge_balance_negative_append_irreducible_factornonunitidentitysecondimaginary = (ge_second_in_append_irreducible_factornonunitidentity) + ge_balance_positive_append_irreducible_factornonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factornonunitidentityoutput ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_factornonunitidentityoutputreal ge_balance_negative_append_irreducible_factornonunitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_factornonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_factornonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputreal) = S ge_signed_half_append_irreducible_factornonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))))))) + ge_balance_negative_append_irreducible_factornonunitidentityoutputreal = (((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))))))) + ge_balance_positive_append_irreducible_factornonunitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factornonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factornonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_factornonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary) = S ge_signed_half_append_irreducible_factornonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))))))) + ge_balance_negative_append_irreducible_factornonunitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_factornonunitidentity) * (ge_second_in_append_irreducible_factornonunitidentity))) + (((ge_first_rn_append_irreducible_factornonunitidentity) * (ge_second_ip_append_irreducible_factornonunitidentity))))) + (((((ge_first_ip_append_irreducible_factornonunitidentity) * (ge_second_rn_append_irreducible_factornonunitidentity))) + (((ge_first_in_append_irreducible_factornonunitidentity) * (ge_second_rp_append_irreducible_factornonunitidentity))))))) + ge_balance_positive_append_irreducible_factornonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_append_irreducible_factor gr_second_factor_append_irreducible_factor. (exists ge_first_rp_append_irreducible_factorfactorization ge_first_rn_append_irreducible_factorfactorization ge_first_ip_append_irreducible_factorfactorization ge_first_in_append_irreducible_factorfactorization ge_second_rp_append_irreducible_factorfactorization ge_second_rn_append_irreducible_factorfactorization ge_second_ip_append_irreducible_factorfactorization ge_second_in_append_irreducible_factorfactorization. ((exists ge_representation_real_code_append_irreducible_factorfactorizationfirst ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst. (((gr_first_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorfactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst)) * S ((ge_representation_real_code_append_irreducible_factorfactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst)) + ((ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst))) /\ ((exists ge_balance_positive_append_irreducible_factorfactorizationfirstreal ge_balance_negative_append_irreducible_factorfactorizationfirstreal. (((((ge_representation_real_code_append_irreducible_factorfactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationfirstreal) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationfirstrealdecode. (((ge_representation_real_code_append_irreducible_factorfactorizationfirst) = 2 * ge_signed_half_append_irreducible_factorfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstreal) = S ge_signed_half_append_irreducible_factorfactorizationfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationfirstreal = (ge_first_rn_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfactorizationfirst) = 2 * ge_signed_half_append_irreducible_factorfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary) = S ge_signed_half_append_irreducible_factorfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationfirstimaginary = (ge_first_in_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factorfactorizationsecond ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond. (((gr_second_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorfactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond)) * S ((ge_representation_real_code_append_irreducible_factorfactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond)) + ((ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond))) /\ ((exists ge_balance_positive_append_irreducible_factorfactorizationsecondreal ge_balance_negative_append_irreducible_factorfactorizationsecondreal. (((((ge_representation_real_code_append_irreducible_factorfactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationsecondreal) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationsecondrealdecode. (((ge_representation_real_code_append_irreducible_factorfactorizationsecond) = 2 * ge_signed_half_append_irreducible_factorfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationsecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondreal) = S ge_signed_half_append_irreducible_factorfactorizationsecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationsecondreal = (ge_second_rn_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationsecondreal))) /\ (exists ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfactorizationsecond) = 2 * ge_signed_half_append_irreducible_factorfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary) = S ge_signed_half_append_irreducible_factorfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factorfactorization) + ge_balance_negative_append_irreducible_factorfactorizationsecondimaginary = (ge_second_in_append_irreducible_factorfactorization) + ge_balance_positive_append_irreducible_factorfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factorfactorizationoutput ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput. (((p) = ((ge_representation_real_code_append_irreducible_factorfactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput)) * S ((ge_representation_real_code_append_irreducible_factorfactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput)) + ((ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput))) /\ ((exists ge_balance_positive_append_irreducible_factorfactorizationoutputreal ge_balance_negative_append_irreducible_factorfactorizationoutputreal. (((((ge_representation_real_code_append_irreducible_factorfactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationoutputreal) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationoutputrealdecode. (((ge_representation_real_code_append_irreducible_factorfactorizationoutput) = 2 * ge_signed_half_append_irreducible_factorfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputreal) = S ge_signed_half_append_irreducible_factorfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))))))) + ge_balance_negative_append_irreducible_factorfactorizationoutputreal = (((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))))))) + ge_balance_positive_append_irreducible_factorfactorizationoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfactorizationoutput) = 2 * ge_signed_half_append_irreducible_factorfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary) = S ge_signed_half_append_irreducible_factorfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))))))) + ge_balance_negative_append_irreducible_factorfactorizationoutputimaginary = (((((((ge_first_rp_append_irreducible_factorfactorization) * (ge_second_in_append_irreducible_factorfactorization))) + (((ge_first_rn_append_irreducible_factorfactorization) * (ge_second_ip_append_irreducible_factorfactorization))))) + (((((ge_first_ip_append_irreducible_factorfactorization) * (ge_second_rn_append_irreducible_factorfactorization))) + (((ge_first_in_append_irreducible_factorfactorization) * (ge_second_rp_append_irreducible_factorfactorization))))))) + ge_balance_positive_append_irreducible_factorfactorizationoutputimaginary))))))))) -> (exists gr_inverse_append_irreducible_factorfirst_unit. (exists ge_first_rp_append_irreducible_factorfirst_unitidentity ge_first_rn_append_irreducible_factorfirst_unitidentity ge_first_ip_append_irreducible_factorfirst_unitidentity ge_first_in_append_irreducible_factorfirst_unitidentity ge_second_rp_append_irreducible_factorfirst_unitidentity ge_second_rn_append_irreducible_factorfirst_unitidentity ge_second_ip_append_irreducible_factorfirst_unitidentity ge_second_in_append_irreducible_factorfirst_unitidentity. ((exists ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst. (((gr_first_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal) = S ge_signed_half_append_irreducible_factorfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstreal = (ge_first_rn_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_factorfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentityfirstimaginary = (ge_first_in_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond. (((gr_inverse_append_irreducible_factorfirst_unit) = ((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal) = S ge_signed_half_append_irreducible_factorfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondreal = (ge_second_rn_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_factorfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factorfirst_unitidentity) + ge_balance_negative_append_irreducible_factorfirst_unitidentitysecondimaginary = (ge_second_in_append_irreducible_factorfirst_unitidentity) + ge_balance_positive_append_irreducible_factorfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal) = S ge_signed_half_append_irreducible_factorfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorfirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_factorfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_negative_append_irreducible_factorfirst_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_factorfirst_unitidentity) * (ge_second_in_append_irreducible_factorfirst_unitidentity))) + (((ge_first_rn_append_irreducible_factorfirst_unitidentity) * (ge_second_ip_append_irreducible_factorfirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorfirst_unitidentity) * (ge_second_rn_append_irreducible_factorfirst_unitidentity))) + (((ge_first_in_append_irreducible_factorfirst_unitidentity) * (ge_second_rp_append_irreducible_factorfirst_unitidentity))))))) + ge_balance_positive_append_irreducible_factorfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_append_irreducible_factorsecond_unit. (exists ge_first_rp_append_irreducible_factorsecond_unitidentity ge_first_rn_append_irreducible_factorsecond_unitidentity ge_first_ip_append_irreducible_factorsecond_unitidentity ge_first_in_append_irreducible_factorsecond_unitidentity ge_second_rp_append_irreducible_factorsecond_unitidentity ge_second_rn_append_irreducible_factorsecond_unitidentity ge_second_ip_append_irreducible_factorsecond_unitidentity ge_second_in_append_irreducible_factorsecond_unitidentity. ((exists ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst. (((gr_second_factor_append_irreducible_factor) = ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal) = S ge_signed_half_append_irreducible_factorsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstreal = (ge_first_rn_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_factorsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentityfirstimaginary = (ge_first_in_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond. (((gr_inverse_append_irreducible_factorsecond_unit) = ((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal) = S ge_signed_half_append_irreducible_factorsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondreal = (ge_second_rn_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_factorsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_factorsecond_unitidentity) + ge_balance_negative_append_irreducible_factorsecond_unitidentitysecondimaginary = (ge_second_in_append_irreducible_factorsecond_unitidentity) + ge_balance_positive_append_irreducible_factorsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal) = S ge_signed_half_append_irreducible_factorsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_factorsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_factorsecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_factorsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_factorsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_negative_append_irreducible_factorsecond_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_factorsecond_unitidentity) * (ge_second_in_append_irreducible_factorsecond_unitidentity))) + (((ge_first_rn_append_irreducible_factorsecond_unitidentity) * (ge_second_ip_append_irreducible_factorsecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_factorsecond_unitidentity) * (ge_second_rn_append_irreducible_factorsecond_unitidentity))) + (((ge_first_in_append_irreducible_factorsecond_unitidentity) * (ge_second_rp_append_irreducible_factorsecond_unitidentity))))))) + ge_balance_positive_append_irreducible_factorsecond_unitidentityoutputimaginary))))))))))))))) -> (forall gr_factor_index_append_irreducible_full gr_factor_value_append_irreducible_full. (exists ge_gap_append_irreducible_fullindex. ge_gap_append_irreducible_fullindex + S (gr_factor_index_append_irreducible_full) = (S l)) -> (((exists ff_h_gprod_append_irreducible_fullentry. ff_h_gprod_append_irreducible_fullentry + S (gr_factor_value_append_irreducible_full) = S ((S (gr_factor_index_append_irreducible_full)) * e)) /\ exists ff_q_gprod_append_irreducible_fullentry. d = ff_q_gprod_append_irreducible_fullentry * S ((S (gr_factor_index_append_irreducible_full)) * e) + (gr_factor_value_append_irreducible_full))) -> (((exists ge_real_positive_append_irreducible_fullirreduciblecarrier ge_real_negative_append_irreducible_fullirreduciblecarrier ge_imaginary_positive_append_irreducible_fullirreduciblecarrier ge_imaginary_negative_append_irreducible_fullirreduciblecarrier. (exists ge_real_code_append_irreducible_fullirreduciblecarrierdecode ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode. (((gr_factor_value_append_irreducible_full) = ((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode)) * S ((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode)) + ((ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode) + (ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode))) /\ (((((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * (ge_real_positive_append_irreducible_fullirreduciblecarrier) /\ (ge_real_negative_append_irreducible_fullirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_real. (((ge_real_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_append_irreducible_fullirreduciblecarrier) = 0) /\ (ge_real_negative_append_irreducible_fullirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_append_irreducible_fullirreduciblecarrier) /\ (ge_imaginary_negative_append_irreducible_fullirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_append_irreducible_fullirreduciblecarrierdecode) = 2 * ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_append_irreducible_fullirreduciblecarrier) = 0) /\ (ge_imaginary_negative_append_irreducible_fullirreduciblecarrier) = S ge_signed_half_ge_append_irreducible_fullirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_append_irreducible_full)=0)) /\ ((~(exists gr_inverse_append_irreducible_fullirreduciblenonunit. (exists ge_first_rp_append_irreducible_fullirreduciblenonunitidentity ge_first_rn_append_irreducible_fullirreduciblenonunitidentity ge_first_ip_append_irreducible_fullirreduciblenonunitidentity ge_first_in_append_irreducible_fullirreduciblenonunitidentity ge_second_rp_append_irreducible_fullirreduciblenonunitidentity ge_second_rn_append_irreducible_fullirreduciblenonunitidentity ge_second_ip_append_irreducible_fullirreduciblenonunitidentity ge_second_in_append_irreducible_fullirreduciblenonunitidentity. ((exists ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst. (((gr_factor_value_append_irreducible_full) = ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstreal = (ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond. (((gr_inverse_append_irreducible_fullirreduciblenonunit) = ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondreal = (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentitysecondimaginary = (ge_second_in_append_irreducible_fullirreduciblenonunitidentity) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblenonunitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_in_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_ip_append_irreducible_fullirreduciblenonunitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rn_append_irreducible_fullirreduciblenonunitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblenonunitidentity) * (ge_second_rp_append_irreducible_fullirreduciblenonunitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_append_irreducible_fullirreducible gr_second_factor_append_irreducible_fullirreducible. (exists ge_first_rp_append_irreducible_fullirreduciblefactorization ge_first_rn_append_irreducible_fullirreduciblefactorization ge_first_ip_append_irreducible_fullirreduciblefactorization ge_first_in_append_irreducible_fullirreduciblefactorization ge_second_rp_append_irreducible_fullirreduciblefactorization ge_second_rn_append_irreducible_fullirreduciblefactorization ge_second_ip_append_irreducible_fullirreduciblefactorization ge_second_in_append_irreducible_fullirreduciblefactorization. ((exists ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst. (((gr_first_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstreal = (ge_first_rn_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond. (((gr_second_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondreal = (ge_second_rn_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationsecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblefactorization) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationsecondimaginary = (ge_second_in_append_irreducible_fullirreduciblefactorization) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput. (((gr_factor_value_append_irreducible_full) = ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefactorizationoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_negative_append_irreducible_fullirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblefactorization) * (ge_second_in_append_irreducible_fullirreduciblefactorization))) + (((ge_first_rn_append_irreducible_fullirreduciblefactorization) * (ge_second_ip_append_irreducible_fullirreduciblefactorization))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefactorization) * (ge_second_rn_append_irreducible_fullirreduciblefactorization))) + (((ge_first_in_append_irreducible_fullirreduciblefactorization) * (ge_second_rp_append_irreducible_fullirreduciblefactorization))))))) + ge_balance_positive_append_irreducible_fullirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_append_irreducible_fullirreduciblefirst_unit. (exists ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity. ((exists ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst. (((gr_first_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstreal = (ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond. (((gr_inverse_append_irreducible_fullirreduciblefirst_unit) = ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondreal = (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblefirst_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblefirst_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblefirst_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblefirst_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_append_irreducible_fullirreduciblesecond_unit. (exists ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity. ((exists ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst. (((gr_second_factor_append_irreducible_fullirreducible) = ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstreal = (ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond. (((gr_inverse_append_irreducible_fullirreduciblesecond_unit) = ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondreal = (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_irreducible_fullirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_negative_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_in_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_rn_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_ip_append_irreducible_fullirreduciblesecond_unitidentity))))) + (((((ge_first_ip_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rn_append_irreducible_fullirreduciblesecond_unitidentity))) + (((ge_first_in_append_irreducible_fullirreduciblesecond_unitidentity) * (ge_second_rp_append_irreducible_fullirreduciblesecond_unitidentity))))))) + ge_balance_positive_append_irreducible_fullirreduciblesecond_unitidentityoutputimaginary))))))))))))))))Complete tactic proof in conservative notation
All 56 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
56 script commands · 8 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Establish hcL15–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
04Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
cases hc
05Establish heqL21–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
- L21
have heq : p=q - L22
specialize beta_at_unique (d) - L23
specialize beta_at_unique (e) - L24
specialize beta_at_unique (l) - L25
specialize beta_at_unique (p) - L26
specialize beta_at_unique (q) - L27
apply beta_at_unique - L28
exact hlast - L29
specialize gaussian_product_beta_index_transport (d) - L30
specialize gaussian_product_beta_index_transport (e)
06Use earlier factsL31–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
specialize gaussian_product_beta_index_transport (i) - L32
specialize gaussian_product_beta_index_transport (l) - L33
specialize gaussian_product_beta_index_transport (q) - L34
apply gaussian_product_beta_index_transport - L35
exact hc_left - L36
exact hq - L37
specialize gaussian_irreducible_code_transport (p) - L38
specialize gaussian_irreducible_code_transport (q) - L39
apply gaussian_irreducible_code_transport - L40
exact heq
07Use earlier factsL41–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L41
exact hp - L42
specialize hall (i) - L43
specialize hall (q) - L44
apply hall - L45
exact hc_right - L46
specialize factor_permutation_prefix_reflect (b) - L47
specialize factor_permutation_prefix_reflect (c) - L48
specialize factor_permutation_prefix_reflect (d) - L49
specialize factor_permutation_prefix_reflect (e) - L50
specialize factor_permutation_prefix_reflect (l)
Original defined command ledger · 56 lines
- 0001
intro b - 0002
intro c - 0003
intro d - 0004
intro e - 0005
intro l - 0006
intro p - 0007
intro hall - 0008
intro hpreserve - 0009
intro hlast - 0010
intro hp - 0011
intro i - 0012
intro q - 0013
intro hi - 0014
intro hq - 0015
have hc : i = l ∨ Lt(i,l) - 0016
specialize finite_lt_succ_eq_or_lt (l) - 0017
specialize finite_lt_succ_eq_or_lt (i) - 0018
apply finite_lt_succ_eq_or_lt - 0019
exact hi - 0020
cases hc - 0021
have heq : p=q - 0022
specialize beta_at_unique (d) - 0023
specialize beta_at_unique (e) - 0024
specialize beta_at_unique (l) - 0025
specialize beta_at_unique (p) - 0026
specialize beta_at_unique (q) - 0027
apply beta_at_unique - 0028
exact hlast - 0029
specialize gaussian_product_beta_index_transport (d) - 0030
specialize gaussian_product_beta_index_transport (e) - 0031
specialize gaussian_product_beta_index_transport (i) - 0032
specialize gaussian_product_beta_index_transport (l) - 0033
specialize gaussian_product_beta_index_transport (q) - 0034
apply gaussian_product_beta_index_transport - 0035
exact hc_left - 0036
exact hq - 0037
specialize gaussian_irreducible_code_transport (p) - 0038
specialize gaussian_irreducible_code_transport (q) - 0039
apply gaussian_irreducible_code_transport - 0040
exact heq - 0041
exact hp - 0042
specialize hall (i) - 0043
specialize hall (q) - 0044
apply hall - 0045
exact hc_right - 0046
specialize factor_permutation_prefix_reflect (b) - 0047
specialize factor_permutation_prefix_reflect (c) - 0048
specialize factor_permutation_prefix_reflect (d) - 0049
specialize factor_permutation_prefix_reflect (e) - 0050
specialize factor_permutation_prefix_reflect (l) - 0051
specialize factor_permutation_prefix_reflect (i) - 0052
specialize factor_permutation_prefix_reflect (q) - 0053
apply factor_permutation_prefix_reflect - 0054
exact hpreserve - 0055
exact hc_right - 0056
exact hq