GF00AF — gaussian_irreducible_products_associate_unique

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

∀ l. ∀ b. ∀ c. ∀ P. ∀ m. ∀ d. ∀ e. ∀ Q. GAllIrreducible(b,c,l) → GProduct(b,c,l,P) → GAllIrreducible(d,e,m) → GProduct(d,e,m,Q) → GAssociate(P,Q) → l = m ∧ (∃ x. ∃ y. GMatchedFactors(b,c,d,e,x,y,l))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GMul(a,b,c) · 3 GDvd(d,z) · 1 GUnit(z) · 1 GAssociate(a,b) · 4 GIrreducible(z) · 1 GProduct(b,c,l,P) · 7 GAllIrreducible(b,c,l) · 4 GMatchedFactors(b,c,d,e,u,v,l) · 4 Lt(a,b) · 4 BetaAt(b,c,i,x) · 13

Actual proof prerequisites

gaussian_product_empty_value gaussian_factor_associate_unit gaussian_one_unit gaussian_all_irreducible_product_unit_length_zero gaussian_factor_empty_matching gaussian_product_successor_decomposele_refl · checked external prerequisitegaussian_divides_transitive gaussian_multiply_commutative gaussian_associate_divides gaussian_irreducible_divisor_product_memberzero_or_succ · checked external prerequisitegaussian_search_no_index_below_zero gaussian_product_length_transport gaussian_all_irreducible_length_transportfinite_lt_succ_eq_or_lt · checked external prerequisitegaussian_product_beta_index_transport gaussian_product_decompose_at_last gaussian_factor_associate_cancel_products gaussian_all_irreducible_prefix gaussian_factor_matched_append gaussian_factor_swapped_product_exists gaussian_factor_matched_unswap_exists gaussian_factor_swap_length_transport

Original expanded first-order statement

forall l b c P m d e Q. (forall gr_factor_index_unique_source_irreducible gr_factor_value_unique_source_irreducible. (exists ge_gap_unique_source_irreducibleindex. ge_gap_unique_source_irreducibleindex + S (gr_factor_index_unique_source_irreducible) = (l)) -> (((exists ff_h_gprod_unique_source_irreducibleentry. ff_h_gprod_unique_source_irreducibleentry + S (gr_factor_value_unique_source_irreducible) = S ((S (gr_factor_index_unique_source_irreducible)) * c)) /\ exists ff_q_gprod_unique_source_irreducibleentry. b = ff_q_gprod_unique_source_irreducibleentry * S ((S (gr_factor_index_unique_source_irreducible)) * c) + (gr_factor_value_unique_source_irreducible))) -> (((exists ge_real_positive_unique_source_irreducibleirreduciblecarrier ge_real_negative_unique_source_irreducibleirreduciblecarrier ge_imaginary_positive_unique_source_irreducibleirreduciblecarrier ge_imaginary_negative_unique_source_irreducibleirreduciblecarrier. (exists ge_real_code_unique_source_irreducibleirreduciblecarrierdecode ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode. (((gr_factor_value_unique_source_irreducible) = ((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unique_source_irreducibleirreduciblecarrier) /\ (ge_real_negative_unique_source_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_real. (((ge_real_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unique_source_irreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unique_source_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unique_source_irreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unique_source_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unique_source_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_source_irreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unique_source_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_source_irreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unique_source_irreducible)=0)) /\ ((~(exists gr_inverse_unique_source_irreducibleirreduciblenonunit. (exists ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity ge_first_in_unique_source_irreducibleirreduciblenonunitidentity ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity ge_second_in_unique_source_irreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unique_source_irreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unique_source_irreducibleirreduciblenonunit) = ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_source_irreducibleirreducible gr_second_factor_unique_source_irreducibleirreducible. (exists ge_first_rp_unique_source_irreducibleirreduciblefactorization ge_first_rn_unique_source_irreducibleirreduciblefactorization ge_first_ip_unique_source_irreducibleirreduciblefactorization ge_first_in_unique_source_irreducibleirreduciblefactorization ge_second_rp_unique_source_irreducibleirreduciblefactorization ge_second_rn_unique_source_irreducibleirreduciblefactorization ge_second_ip_unique_source_irreducibleirreduciblefactorization ge_second_in_unique_source_irreducibleirreduciblefactorization. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst. (((gr_first_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond. (((gr_second_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblefactorization) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblefactorization) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput. (((gr_factor_value_unique_source_irreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblefactorization) * (ge_second_in_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_source_irreducibleirreduciblefactorization) * (ge_second_ip_unique_source_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefactorization) * (ge_second_rn_unique_source_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_source_irreducibleirreduciblefactorization) * (ge_second_rp_unique_source_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unique_source_irreducibleirreduciblefirst_unit. (exists ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unique_source_irreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unique_source_irreducibleirreduciblesecond_unit. (exists ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unique_source_irreducibleirreducible) = ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unique_source_irreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_source_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_source_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_source_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_source_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_source_irreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_unique_source_product gr_product_scale_unique_source_product. ((((exists ff_h_gprod_unique_source_productstart. ff_h_gprod_unique_source_productstart + S (6) = S ((S (0)) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productstart. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productstart * S ((S (0)) * gr_product_scale_unique_source_product) + (6))) /\ ((((exists ff_h_gprod_unique_source_productend. ff_h_gprod_unique_source_productend + S (P) = S ((S (l)) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productend. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productend * S ((S (l)) * gr_product_scale_unique_source_product) + (P))) /\ (forall gr_product_index_unique_source_productsteps. (exists ge_gap_unique_source_productstepsindex_bound. ge_gap_unique_source_productstepsindex_bound + S (gr_product_index_unique_source_productsteps) = (l)) -> exists gr_product_factor_unique_source_productsteps gr_product_before_unique_source_productsteps gr_product_after_unique_source_productsteps. ((((exists ff_h_gprod_unique_source_productstepsfactor. ff_h_gprod_unique_source_productstepsfactor + S (gr_product_factor_unique_source_productsteps) = S ((S (gr_product_index_unique_source_productsteps)) * c)) /\ exists ff_q_gprod_unique_source_productstepsfactor. b = ff_q_gprod_unique_source_productstepsfactor * S ((S (gr_product_index_unique_source_productsteps)) * c) + (gr_product_factor_unique_source_productsteps))) /\ ((((exists ff_h_gprod_unique_source_productstepsbefore. ff_h_gprod_unique_source_productstepsbefore + S (gr_product_before_unique_source_productsteps) = S ((S (gr_product_index_unique_source_productsteps)) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productstepsbefore. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productstepsbefore * S ((S (gr_product_index_unique_source_productsteps)) * gr_product_scale_unique_source_product) + (gr_product_before_unique_source_productsteps))) /\ ((((exists ff_h_gprod_unique_source_productstepsafter. ff_h_gprod_unique_source_productstepsafter + S (gr_product_after_unique_source_productsteps) = S ((S (S (gr_product_index_unique_source_productsteps))) * gr_product_scale_unique_source_product)) /\ exists ff_q_gprod_unique_source_productstepsafter. gr_product_trace_unique_source_product = ff_q_gprod_unique_source_productstepsafter * S ((S (S (gr_product_index_unique_source_productsteps))) * gr_product_scale_unique_source_product) + (gr_product_after_unique_source_productsteps))) /\ (exists ge_first_rp_unique_source_productstepsmultiply ge_first_rn_unique_source_productstepsmultiply ge_first_ip_unique_source_productstepsmultiply ge_first_in_unique_source_productstepsmultiply ge_second_rp_unique_source_productstepsmultiply ge_second_rn_unique_source_productstepsmultiply ge_second_ip_unique_source_productstepsmultiply ge_second_in_unique_source_productstepsmultiply. ((exists ge_representation_real_code_unique_source_productstepsmultiplyfirst ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst. (((gr_product_before_unique_source_productsteps) = ((ge_representation_real_code_unique_source_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst)) * S ((ge_representation_real_code_unique_source_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_source_productstepsmultiplyfirstreal ge_balance_negative_unique_source_productstepsmultiplyfirstreal. (((((ge_representation_real_code_unique_source_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyfirstreal) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_source_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_source_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstreal) = S ge_signed_half_unique_source_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplyfirstreal = (ge_first_rn_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_source_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_source_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary) = S ge_signed_half_unique_source_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplyfirstimaginary = (ge_first_in_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_source_productstepsmultiplysecond ge_representation_imaginary_code_unique_source_productstepsmultiplysecond. (((gr_product_factor_unique_source_productsteps) = ((ge_representation_real_code_unique_source_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_source_productstepsmultiplysecond)) * S ((ge_representation_real_code_unique_source_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_source_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_source_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_source_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_source_productstepsmultiplysecondreal ge_balance_negative_unique_source_productstepsmultiplysecondreal. (((((ge_representation_real_code_unique_source_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_source_productstepsmultiplysecondreal) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_source_productstepsmultiplysecond) = 2 * ge_signed_half_unique_source_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondreal) = S ge_signed_half_unique_source_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplysecondreal = (ge_second_rn_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_source_productstepsmultiplysecondimaginary ge_balance_negative_unique_source_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_source_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_source_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_source_productstepsmultiplysecond) = 2 * ge_signed_half_unique_source_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplysecondimaginary) = S ge_signed_half_unique_source_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_source_productstepsmultiply) + ge_balance_negative_unique_source_productstepsmultiplysecondimaginary = (ge_second_in_unique_source_productstepsmultiply) + ge_balance_positive_unique_source_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_source_productstepsmultiplyoutput ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput. (((gr_product_after_unique_source_productsteps) = ((ge_representation_real_code_unique_source_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput)) * S ((ge_representation_real_code_unique_source_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_source_productstepsmultiplyoutputreal ge_balance_negative_unique_source_productstepsmultiplyoutputreal. (((((ge_representation_real_code_unique_source_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyoutputreal) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_source_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_source_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputreal) = S ge_signed_half_unique_source_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))))))) + ge_balance_negative_unique_source_productstepsmultiplyoutputreal = (((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))))))) + ge_balance_positive_unique_source_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_source_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_source_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_source_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary) = S ge_signed_half_unique_source_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))))))) + ge_balance_negative_unique_source_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_source_productstepsmultiply) * (ge_second_in_unique_source_productstepsmultiply))) + (((ge_first_rn_unique_source_productstepsmultiply) * (ge_second_ip_unique_source_productstepsmultiply))))) + (((((ge_first_ip_unique_source_productstepsmultiply) * (ge_second_rn_unique_source_productstepsmultiply))) + (((ge_first_in_unique_source_productstepsmultiply) * (ge_second_rp_unique_source_productstepsmultiply))))))) + ge_balance_positive_unique_source_productstepsmultiplyoutputimaginary)))))))))))))))) -> (forall gr_factor_index_unique_target_irreducible gr_factor_value_unique_target_irreducible. (exists ge_gap_unique_target_irreducibleindex. ge_gap_unique_target_irreducibleindex + S (gr_factor_index_unique_target_irreducible) = (m)) -> (((exists ff_h_gprod_unique_target_irreducibleentry. ff_h_gprod_unique_target_irreducibleentry + S (gr_factor_value_unique_target_irreducible) = S ((S (gr_factor_index_unique_target_irreducible)) * e)) /\ exists ff_q_gprod_unique_target_irreducibleentry. d = ff_q_gprod_unique_target_irreducibleentry * S ((S (gr_factor_index_unique_target_irreducible)) * e) + (gr_factor_value_unique_target_irreducible))) -> (((exists ge_real_positive_unique_target_irreducibleirreduciblecarrier ge_real_negative_unique_target_irreducibleirreduciblecarrier ge_imaginary_positive_unique_target_irreducibleirreduciblecarrier ge_imaginary_negative_unique_target_irreducibleirreduciblecarrier. (exists ge_real_code_unique_target_irreducibleirreduciblecarrierdecode ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode. (((gr_factor_value_unique_target_irreducible) = ((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unique_target_irreducibleirreduciblecarrier) /\ (ge_real_negative_unique_target_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_real. (((ge_real_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unique_target_irreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unique_target_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unique_target_irreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unique_target_irreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unique_target_irreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unique_target_irreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unique_target_irreducibleirreduciblecarrier) = S ge_signed_half_ge_unique_target_irreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unique_target_irreducible)=0)) /\ ((~(exists gr_inverse_unique_target_irreducibleirreduciblenonunit. (exists ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity ge_first_in_unique_target_irreducibleirreduciblenonunitidentity ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity ge_second_in_unique_target_irreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unique_target_irreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unique_target_irreducibleirreduciblenonunit) = ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_in_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblenonunitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblenonunitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unique_target_irreducibleirreducible gr_second_factor_unique_target_irreducibleirreducible. (exists ge_first_rp_unique_target_irreducibleirreduciblefactorization ge_first_rn_unique_target_irreducibleirreduciblefactorization ge_first_ip_unique_target_irreducibleirreduciblefactorization ge_first_in_unique_target_irreducibleirreduciblefactorization ge_second_rp_unique_target_irreducibleirreduciblefactorization ge_second_rn_unique_target_irreducibleirreduciblefactorization ge_second_ip_unique_target_irreducibleirreduciblefactorization ge_second_in_unique_target_irreducibleirreduciblefactorization. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst. (((gr_first_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond. (((gr_second_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblefactorization) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblefactorization) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput. (((gr_factor_value_unique_target_irreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblefactorization) * (ge_second_in_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_rn_unique_target_irreducibleirreduciblefactorization) * (ge_second_ip_unique_target_irreducibleirreduciblefactorization))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefactorization) * (ge_second_rn_unique_target_irreducibleirreduciblefactorization))) + (((ge_first_in_unique_target_irreducibleirreduciblefactorization) * (ge_second_rp_unique_target_irreducibleirreduciblefactorization))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unique_target_irreducibleirreduciblefirst_unit. (exists ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unique_target_irreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unique_target_irreducibleirreduciblesecond_unit. (exists ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unique_target_irreducibleirreducible) = ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unique_target_irreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_irreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_in_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unique_target_irreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unique_target_irreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unique_target_irreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unique_target_irreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unique_target_irreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_unique_target_product gr_product_scale_unique_target_product. ((((exists ff_h_gprod_unique_target_productstart. ff_h_gprod_unique_target_productstart + S (6) = S ((S (0)) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productstart. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productstart * S ((S (0)) * gr_product_scale_unique_target_product) + (6))) /\ ((((exists ff_h_gprod_unique_target_productend. ff_h_gprod_unique_target_productend + S (Q) = S ((S (m)) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productend. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productend * S ((S (m)) * gr_product_scale_unique_target_product) + (Q))) /\ (forall gr_product_index_unique_target_productsteps. (exists ge_gap_unique_target_productstepsindex_bound. ge_gap_unique_target_productstepsindex_bound + S (gr_product_index_unique_target_productsteps) = (m)) -> exists gr_product_factor_unique_target_productsteps gr_product_before_unique_target_productsteps gr_product_after_unique_target_productsteps. ((((exists ff_h_gprod_unique_target_productstepsfactor. ff_h_gprod_unique_target_productstepsfactor + S (gr_product_factor_unique_target_productsteps) = S ((S (gr_product_index_unique_target_productsteps)) * e)) /\ exists ff_q_gprod_unique_target_productstepsfactor. d = ff_q_gprod_unique_target_productstepsfactor * S ((S (gr_product_index_unique_target_productsteps)) * e) + (gr_product_factor_unique_target_productsteps))) /\ ((((exists ff_h_gprod_unique_target_productstepsbefore. ff_h_gprod_unique_target_productstepsbefore + S (gr_product_before_unique_target_productsteps) = S ((S (gr_product_index_unique_target_productsteps)) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productstepsbefore. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productstepsbefore * S ((S (gr_product_index_unique_target_productsteps)) * gr_product_scale_unique_target_product) + (gr_product_before_unique_target_productsteps))) /\ ((((exists ff_h_gprod_unique_target_productstepsafter. ff_h_gprod_unique_target_productstepsafter + S (gr_product_after_unique_target_productsteps) = S ((S (S (gr_product_index_unique_target_productsteps))) * gr_product_scale_unique_target_product)) /\ exists ff_q_gprod_unique_target_productstepsafter. gr_product_trace_unique_target_product = ff_q_gprod_unique_target_productstepsafter * S ((S (S (gr_product_index_unique_target_productsteps))) * gr_product_scale_unique_target_product) + (gr_product_after_unique_target_productsteps))) /\ (exists ge_first_rp_unique_target_productstepsmultiply ge_first_rn_unique_target_productstepsmultiply ge_first_ip_unique_target_productstepsmultiply ge_first_in_unique_target_productstepsmultiply ge_second_rp_unique_target_productstepsmultiply ge_second_rn_unique_target_productstepsmultiply ge_second_ip_unique_target_productstepsmultiply ge_second_in_unique_target_productstepsmultiply. ((exists ge_representation_real_code_unique_target_productstepsmultiplyfirst ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst. (((gr_product_before_unique_target_productsteps) = ((ge_representation_real_code_unique_target_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst)) * S ((ge_representation_real_code_unique_target_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst)) + ((ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst))) /\ ((exists ge_balance_positive_unique_target_productstepsmultiplyfirstreal ge_balance_negative_unique_target_productstepsmultiplyfirstreal. (((((ge_representation_real_code_unique_target_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyfirstreal) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyfirstrealdecode. (((ge_representation_real_code_unique_target_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_target_productstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstreal) = S ge_signed_half_unique_target_productstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplyfirstreal = (ge_first_rn_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unique_target_productstepsmultiplyfirst) = 2 * ge_signed_half_unique_target_productstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary) = S ge_signed_half_unique_target_productstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplyfirstimaginary = (ge_first_in_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_target_productstepsmultiplysecond ge_representation_imaginary_code_unique_target_productstepsmultiplysecond. (((gr_product_factor_unique_target_productsteps) = ((ge_representation_real_code_unique_target_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_target_productstepsmultiplysecond)) * S ((ge_representation_real_code_unique_target_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_target_productstepsmultiplysecond)) + ((ge_representation_imaginary_code_unique_target_productstepsmultiplysecond) + (ge_representation_imaginary_code_unique_target_productstepsmultiplysecond))) /\ ((exists ge_balance_positive_unique_target_productstepsmultiplysecondreal ge_balance_negative_unique_target_productstepsmultiplysecondreal. (((((ge_representation_real_code_unique_target_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_target_productstepsmultiplysecondreal) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplysecondrealdecode. (((ge_representation_real_code_unique_target_productstepsmultiplysecond) = 2 * ge_signed_half_unique_target_productstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondreal) = S ge_signed_half_unique_target_productstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplysecondreal = (ge_second_rn_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplysecondreal))) /\ (exists ge_balance_positive_unique_target_productstepsmultiplysecondimaginary ge_balance_negative_unique_target_productstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unique_target_productstepsmultiplysecond) = 2 * (ge_balance_positive_unique_target_productstepsmultiplysecondimaginary) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unique_target_productstepsmultiplysecond) = 2 * ge_signed_half_unique_target_productstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplysecondimaginary) = S ge_signed_half_unique_target_productstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unique_target_productstepsmultiply) + ge_balance_negative_unique_target_productstepsmultiplysecondimaginary = (ge_second_in_unique_target_productstepsmultiply) + ge_balance_positive_unique_target_productstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_target_productstepsmultiplyoutput ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput. (((gr_product_after_unique_target_productsteps) = ((ge_representation_real_code_unique_target_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput)) * S ((ge_representation_real_code_unique_target_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput)) + ((ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput) + (ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput))) /\ ((exists ge_balance_positive_unique_target_productstepsmultiplyoutputreal ge_balance_negative_unique_target_productstepsmultiplyoutputreal. (((((ge_representation_real_code_unique_target_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyoutputreal) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyoutputrealdecode. (((ge_representation_real_code_unique_target_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_target_productstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputreal) = S ge_signed_half_unique_target_productstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))))))) + ge_balance_negative_unique_target_productstepsmultiplyoutputreal = (((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))))))) + ge_balance_positive_unique_target_productstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput) = 2 * (ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unique_target_productstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unique_target_productstepsmultiplyoutput) = 2 * ge_signed_half_unique_target_productstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary) = S ge_signed_half_unique_target_productstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))))))) + ge_balance_negative_unique_target_productstepsmultiplyoutputimaginary = (((((((ge_first_rp_unique_target_productstepsmultiply) * (ge_second_in_unique_target_productstepsmultiply))) + (((ge_first_rn_unique_target_productstepsmultiply) * (ge_second_ip_unique_target_productstepsmultiply))))) + (((((ge_first_ip_unique_target_productstepsmultiply) * (ge_second_rn_unique_target_productstepsmultiply))) + (((ge_first_in_unique_target_productstepsmultiply) * (ge_second_rp_unique_target_productstepsmultiply))))))) + ge_balance_positive_unique_target_productstepsmultiplyoutputimaginary)))))))))))))))) -> (exists gr_unit_unique_products_associate. ((exists gr_inverse_unique_products_associateunit. (exists ge_first_rp_unique_products_associateunitidentity ge_first_rn_unique_products_associateunitidentity ge_first_ip_unique_products_associateunitidentity ge_first_in_unique_products_associateunitidentity ge_second_rp_unique_products_associateunitidentity ge_second_rn_unique_products_associateunitidentity ge_second_ip_unique_products_associateunitidentity ge_second_in_unique_products_associateunitidentity. ((exists ge_representation_real_code_unique_products_associateunitidentityfirst ge_representation_imaginary_code_unique_products_associateunitidentityfirst. (((gr_unit_unique_products_associate) = ((ge_representation_real_code_unique_products_associateunitidentityfirst) + (ge_representation_imaginary_code_unique_products_associateunitidentityfirst)) * S ((ge_representation_real_code_unique_products_associateunitidentityfirst) + (ge_representation_imaginary_code_unique_products_associateunitidentityfirst)) + ((ge_representation_imaginary_code_unique_products_associateunitidentityfirst) + (ge_representation_imaginary_code_unique_products_associateunitidentityfirst))) /\ ((exists ge_balance_positive_unique_products_associateunitidentityfirstreal ge_balance_negative_unique_products_associateunitidentityfirstreal. (((((ge_representation_real_code_unique_products_associateunitidentityfirst) = 2 * (ge_balance_positive_unique_products_associateunitidentityfirstreal) /\ (ge_balance_negative_unique_products_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityfirstrealdecode. (((ge_representation_real_code_unique_products_associateunitidentityfirst) = 2 * ge_signed_half_unique_products_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityfirstreal) = S ge_signed_half_unique_products_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentityfirstreal = (ge_first_rn_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_unique_products_associateunitidentityfirstimaginary ge_balance_negative_unique_products_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unique_products_associateunitidentityfirst) = 2 * (ge_balance_positive_unique_products_associateunitidentityfirstimaginary) /\ (ge_balance_negative_unique_products_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unique_products_associateunitidentityfirst) = 2 * ge_signed_half_unique_products_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityfirstimaginary) = S ge_signed_half_unique_products_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentityfirstimaginary = (ge_first_in_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_products_associateunitidentitysecond ge_representation_imaginary_code_unique_products_associateunitidentitysecond. (((gr_inverse_unique_products_associateunit) = ((ge_representation_real_code_unique_products_associateunitidentitysecond) + (ge_representation_imaginary_code_unique_products_associateunitidentitysecond)) * S ((ge_representation_real_code_unique_products_associateunitidentitysecond) + (ge_representation_imaginary_code_unique_products_associateunitidentitysecond)) + ((ge_representation_imaginary_code_unique_products_associateunitidentitysecond) + (ge_representation_imaginary_code_unique_products_associateunitidentitysecond))) /\ ((exists ge_balance_positive_unique_products_associateunitidentitysecondreal ge_balance_negative_unique_products_associateunitidentitysecondreal. (((((ge_representation_real_code_unique_products_associateunitidentitysecond) = 2 * (ge_balance_positive_unique_products_associateunitidentitysecondreal) /\ (ge_balance_negative_unique_products_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_unique_products_associateunitidentitysecondrealdecode. (((ge_representation_real_code_unique_products_associateunitidentitysecond) = 2 * ge_signed_half_unique_products_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_unique_products_associateunitidentitysecondreal) = S ge_signed_half_unique_products_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentitysecondreal = (ge_second_rn_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_unique_products_associateunitidentitysecondimaginary ge_balance_negative_unique_products_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unique_products_associateunitidentitysecond) = 2 * (ge_balance_positive_unique_products_associateunitidentitysecondimaginary) /\ (ge_balance_negative_unique_products_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unique_products_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unique_products_associateunitidentitysecond) = 2 * ge_signed_half_unique_products_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unique_products_associateunitidentitysecondimaginary) = S ge_signed_half_unique_products_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unique_products_associateunitidentity) + ge_balance_negative_unique_products_associateunitidentitysecondimaginary = (ge_second_in_unique_products_associateunitidentity) + ge_balance_positive_unique_products_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unique_products_associateunitidentityoutput ge_representation_imaginary_code_unique_products_associateunitidentityoutput. (((6) = ((ge_representation_real_code_unique_products_associateunitidentityoutput) + (ge_representation_imaginary_code_unique_products_associateunitidentityoutput)) * S ((ge_representation_real_code_unique_products_associateunitidentityoutput) + (ge_representation_imaginary_code_unique_products_associateunitidentityoutput)) + ((ge_representation_imaginary_code_unique_products_associateunitidentityoutput) + (ge_representation_imaginary_code_unique_products_associateunitidentityoutput))) /\ ((exists ge_balance_positive_unique_products_associateunitidentityoutputreal ge_balance_negative_unique_products_associateunitidentityoutputreal. (((((ge_representation_real_code_unique_products_associateunitidentityoutput) = 2 * (ge_balance_positive_unique_products_associateunitidentityoutputreal) /\ (ge_balance_negative_unique_products_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityoutputrealdecode. (((ge_representation_real_code_unique_products_associateunitidentityoutput) = 2 * ge_signed_half_unique_products_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityoutputreal) = S ge_signed_half_unique_products_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))))))) + ge_balance_negative_unique_products_associateunitidentityoutputreal = (((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))))))) + ge_balance_positive_unique_products_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_unique_products_associateunitidentityoutputimaginary ge_balance_negative_unique_products_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unique_products_associateunitidentityoutput) = 2 * (ge_balance_positive_unique_products_associateunitidentityoutputimaginary) /\ (ge_balance_negative_unique_products_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unique_products_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unique_products_associateunitidentityoutput) = 2 * ge_signed_half_unique_products_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unique_products_associateunitidentityoutputimaginary) = S ge_signed_half_unique_products_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))))))) + ge_balance_negative_unique_products_associateunitidentityoutputimaginary = (((((((ge_first_rp_unique_products_associateunitidentity) * (ge_second_in_unique_products_associateunitidentity))) + (((ge_first_rn_unique_products_associateunitidentity) * (ge_second_ip_unique_products_associateunitidentity))))) + (((((ge_first_ip_unique_products_associateunitidentity) * (ge_second_rn_unique_products_associateunitidentity))) + (((ge_first_in_unique_products_associateunitidentity) * (ge_second_rp_unique_products_associateunitidentity))))))) + ge_balance_positive_unique_products_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unique_products_associatetransport ge_first_rn_unique_products_associatetransport ge_first_ip_unique_products_associatetransport ge_first_in_unique_products_associatetransport ge_second_rp_unique_products_associatetransport ge_second_rn_unique_products_associatetransport ge_second_ip_unique_products_associatetransport ge_second_in_unique_products_associatetransport. ((exists ge_representation_real_code_unique_products_associatetransportfirst ge_representation_imaginary_code_unique_products_associatetransportfirst. (((gr_unit_unique_products_associate) = ((ge_representation_real_code_unique_products_associatetransportfirst) + (ge_representation_imaginary_code_unique_products_associatetransportfirst)) * S ((ge_representation_real_code_unique_products_associatetransportfirst) + (ge_representation_imaginary_code_unique_products_associatetransportfirst)) + ((ge_representation_imaginary_code_unique_products_associatetransportfirst) + (ge_representation_imaginary_code_unique_products_associatetransportfirst))) /\ ((exists ge_balance_positive_unique_products_associatetransportfirstreal ge_balance_negative_unique_products_associatetransportfirstreal. (((((ge_representation_real_code_unique_products_associatetransportfirst) = 2 * (ge_balance_positive_unique_products_associatetransportfirstreal) /\ (ge_balance_negative_unique_products_associatetransportfirstreal) = 0) \/ exists ge_signed_half_unique_products_associatetransportfirstrealdecode. (((ge_representation_real_code_unique_products_associatetransportfirst) = 2 * ge_signed_half_unique_products_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_unique_products_associatetransportfirstreal) = 0) /\ (ge_balance_negative_unique_products_associatetransportfirstreal) = S ge_signed_half_unique_products_associatetransportfirstrealdecode))) /\ ((ge_first_rp_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportfirstreal = (ge_first_rn_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportfirstreal))) /\ (exists ge_balance_positive_unique_products_associatetransportfirstimaginary ge_balance_negative_unique_products_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_unique_products_associatetransportfirst) = 2 * (ge_balance_positive_unique_products_associatetransportfirstimaginary) /\ (ge_balance_negative_unique_products_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_unique_products_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_unique_products_associatetransportfirst) = 2 * ge_signed_half_unique_products_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_unique_products_associatetransportfirstimaginary) = S ge_signed_half_unique_products_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportfirstimaginary = (ge_first_in_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unique_products_associatetransportsecond ge_representation_imaginary_code_unique_products_associatetransportsecond. (((P) = ((ge_representation_real_code_unique_products_associatetransportsecond) + (ge_representation_imaginary_code_unique_products_associatetransportsecond)) * S ((ge_representation_real_code_unique_products_associatetransportsecond) + (ge_representation_imaginary_code_unique_products_associatetransportsecond)) + ((ge_representation_imaginary_code_unique_products_associatetransportsecond) + (ge_representation_imaginary_code_unique_products_associatetransportsecond))) /\ ((exists ge_balance_positive_unique_products_associatetransportsecondreal ge_balance_negative_unique_products_associatetransportsecondreal. (((((ge_representation_real_code_unique_products_associatetransportsecond) = 2 * (ge_balance_positive_unique_products_associatetransportsecondreal) /\ (ge_balance_negative_unique_products_associatetransportsecondreal) = 0) \/ exists ge_signed_half_unique_products_associatetransportsecondrealdecode. (((ge_representation_real_code_unique_products_associatetransportsecond) = 2 * ge_signed_half_unique_products_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_unique_products_associatetransportsecondreal) = 0) /\ (ge_balance_negative_unique_products_associatetransportsecondreal) = S ge_signed_half_unique_products_associatetransportsecondrealdecode))) /\ ((ge_second_rp_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportsecondreal = (ge_second_rn_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportsecondreal))) /\ (exists ge_balance_positive_unique_products_associatetransportsecondimaginary ge_balance_negative_unique_products_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_unique_products_associatetransportsecond) = 2 * (ge_balance_positive_unique_products_associatetransportsecondimaginary) /\ (ge_balance_negative_unique_products_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_unique_products_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_unique_products_associatetransportsecond) = 2 * ge_signed_half_unique_products_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_unique_products_associatetransportsecondimaginary) = S ge_signed_half_unique_products_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_unique_products_associatetransport) + ge_balance_negative_unique_products_associatetransportsecondimaginary = (ge_second_in_unique_products_associatetransport) + ge_balance_positive_unique_products_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unique_products_associatetransportoutput ge_representation_imaginary_code_unique_products_associatetransportoutput. (((Q) = ((ge_representation_real_code_unique_products_associatetransportoutput) + (ge_representation_imaginary_code_unique_products_associatetransportoutput)) * S ((ge_representation_real_code_unique_products_associatetransportoutput) + (ge_representation_imaginary_code_unique_products_associatetransportoutput)) + ((ge_representation_imaginary_code_unique_products_associatetransportoutput) + (ge_representation_imaginary_code_unique_products_associatetransportoutput))) /\ ((exists ge_balance_positive_unique_products_associatetransportoutputreal ge_balance_negative_unique_products_associatetransportoutputreal. (((((ge_representation_real_code_unique_products_associatetransportoutput) = 2 * (ge_balance_positive_unique_products_associatetransportoutputreal) /\ (ge_balance_negative_unique_products_associatetransportoutputreal) = 0) \/ exists ge_signed_half_unique_products_associatetransportoutputrealdecode. (((ge_representation_real_code_unique_products_associatetransportoutput) = 2 * ge_signed_half_unique_products_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_unique_products_associatetransportoutputreal) = 0) /\ (ge_balance_negative_unique_products_associatetransportoutputreal) = S ge_signed_half_unique_products_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))))))) + ge_balance_negative_unique_products_associatetransportoutputreal = (((((((ge_first_rp_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))))))) + ge_balance_positive_unique_products_associatetransportoutputreal))) /\ (exists ge_balance_positive_unique_products_associatetransportoutputimaginary ge_balance_negative_unique_products_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_unique_products_associatetransportoutput) = 2 * (ge_balance_positive_unique_products_associatetransportoutputimaginary) /\ (ge_balance_negative_unique_products_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_unique_products_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_unique_products_associatetransportoutput) = 2 * ge_signed_half_unique_products_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unique_products_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_unique_products_associatetransportoutputimaginary) = S ge_signed_half_unique_products_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))))))) + ge_balance_negative_unique_products_associatetransportoutputimaginary = (((((((ge_first_rp_unique_products_associatetransport) * (ge_second_in_unique_products_associatetransport))) + (((ge_first_rn_unique_products_associatetransport) * (ge_second_ip_unique_products_associatetransport))))) + (((((ge_first_ip_unique_products_associatetransport) * (ge_second_rn_unique_products_associatetransport))) + (((ge_first_in_unique_products_associatetransport) * (ge_second_rp_unique_products_associatetransport))))))) + ge_balance_positive_unique_products_associatetransportoutputimaginary))))))))))) -> ((((l)=(m)) /\ (exists gr_unique_map_product_unique gr_unique_scale_product_unique. (((((forall pfp_i_product_uniquematchingbijectionbounded. (exists pfp_gap_product_uniquematchingbijectionboundedindex. pfp_gap_product_uniquematchingbijectionboundedindex + S (pfp_i_product_uniquematchingbijectionbounded) = (l)) -> exists pfp_a_product_uniquematchingbijectionbounded. (((exists ff_h_pfp_product_uniquematchingbijectionboundedentry. ff_h_pfp_product_uniquematchingbijectionboundedentry + S (pfp_a_product_uniquematchingbijectionbounded) = S ((S (pfp_i_product_uniquematchingbijectionbounded)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectionboundedentry. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectionboundedentry * S ((S (pfp_i_product_uniquematchingbijectionbounded)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectionbounded))) /\ (exists pfp_gap_product_uniquematchingbijectionboundedvalue. pfp_gap_product_uniquematchingbijectionboundedvalue + S (pfp_a_product_uniquematchingbijectionbounded) = (l))) /\ (((forall pfp_i_product_uniquematchingbijectioninjective pfp_j_product_uniquematchingbijectioninjective pfp_a_product_uniquematchingbijectioninjective. (exists pfp_gap_product_uniquematchingbijectioninjectivefirst. pfp_gap_product_uniquematchingbijectioninjectivefirst + S (pfp_i_product_uniquematchingbijectioninjective) = (l)) -> (exists pfp_gap_product_uniquematchingbijectioninjectivesecond. pfp_gap_product_uniquematchingbijectioninjectivesecond + S (pfp_j_product_uniquematchingbijectioninjective) = (l)) -> (((exists ff_h_pfp_product_uniquematchingbijectioninjectiveleft. ff_h_pfp_product_uniquematchingbijectioninjectiveleft + S (pfp_a_product_uniquematchingbijectioninjective) = S ((S (pfp_i_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectioninjectiveleft. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectioninjectiveleft * S ((S (pfp_i_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectioninjective))) -> (((exists ff_h_pfp_product_uniquematchingbijectioninjectiveright. ff_h_pfp_product_uniquematchingbijectioninjectiveright + S (pfp_a_product_uniquematchingbijectioninjective) = S ((S (pfp_j_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectioninjectiveright. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectioninjectiveright * S ((S (pfp_j_product_uniquematchingbijectioninjective)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectioninjective))) -> pfp_i_product_uniquematchingbijectioninjective = pfp_j_product_uniquematchingbijectioninjective) /\ (forall pfp_a_product_uniquematchingbijectionsurjective. (exists pfp_gap_product_uniquematchingbijectionsurjectivevalue. pfp_gap_product_uniquematchingbijectionsurjectivevalue + S (pfp_a_product_uniquematchingbijectionsurjective) = (l)) -> exists pfp_i_product_uniquematchingbijectionsurjective. (exists pfp_gap_product_uniquematchingbijectionsurjectiveindex. pfp_gap_product_uniquematchingbijectionsurjectiveindex + S (pfp_i_product_uniquematchingbijectionsurjective) = (l)) /\ (((exists ff_h_pfp_product_uniquematchingbijectionsurjectiveentry. ff_h_pfp_product_uniquematchingbijectionsurjectiveentry + S (pfp_a_product_uniquematchingbijectionsurjective) = S ((S (pfp_i_product_uniquematchingbijectionsurjective)) * gr_unique_scale_product_unique)) /\ exists ff_q_pfp_product_uniquematchingbijectionsurjectiveentry. gr_unique_map_product_unique = ff_q_pfp_product_uniquematchingbijectionsurjectiveentry * S ((S (pfp_i_product_uniquematchingbijectionsurjective)) * gr_unique_scale_product_unique) + (pfp_a_product_uniquematchingbijectionsurjective)))))))) /\ (forall gr_match_index_product_uniquematchingmatching gr_match_image_product_uniquematchingmatching gr_match_source_product_uniquematchingmatching gr_match_target_product_uniquematchingmatching. (exists ge_gap_product_uniquematchingmatchingindex. ge_gap_product_uniquematchingmatchingindex + S (gr_match_index_product_uniquematchingmatching) = (l)) -> (((exists ff_h_gprod_product_uniquematchingmatchingmap. ff_h_gprod_product_uniquematchingmatchingmap + S (gr_match_image_product_uniquematchingmatching) = S ((S (gr_match_index_product_uniquematchingmatching)) * gr_unique_scale_product_unique)) /\ exists ff_q_gprod_product_uniquematchingmatchingmap. gr_unique_map_product_unique = ff_q_gprod_product_uniquematchingmatchingmap * S ((S (gr_match_index_product_uniquematchingmatching)) * gr_unique_scale_product_unique) + (gr_match_image_product_uniquematchingmatching))) -> (((exists ff_h_gprod_product_uniquematchingmatchingsource. ff_h_gprod_product_uniquematchingmatchingsource + S (gr_match_source_product_uniquematchingmatching) = S ((S (gr_match_index_product_uniquematchingmatching)) * c)) /\ exists ff_q_gprod_product_uniquematchingmatchingsource. b = ff_q_gprod_product_uniquematchingmatchingsource * S ((S (gr_match_index_product_uniquematchingmatching)) * c) + (gr_match_source_product_uniquematchingmatching))) -> (((exists ff_h_gprod_product_uniquematchingmatchingtarget. ff_h_gprod_product_uniquematchingmatchingtarget + S (gr_match_target_product_uniquematchingmatching) = S ((S (gr_match_image_product_uniquematchingmatching)) * e)) /\ exists ff_q_gprod_product_uniquematchingmatchingtarget. d = ff_q_gprod_product_uniquematchingmatchingtarget * S ((S (gr_match_image_product_uniquematchingmatching)) * e) + (gr_match_target_product_uniquematchingmatching))) -> (exists gr_unit_product_uniquematchingmatchingunit_witness. ((exists gr_inverse_product_uniquematchingmatchingunit_witnessunit. (exists ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst. (((gr_unit_product_uniquematchingmatchingunit_witness) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond. (((gr_inverse_product_uniquematchingmatchingunit_witnessunit) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_in_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_ip_product_uniquematchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rn_product_uniquematchingmatchingunit_witnessunitidentity))) + (((ge_first_in_product_uniquematchingmatchingunit_witnessunitidentity) * (ge_second_rp_product_uniquematchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_product_uniquematchingmatchingunit_witnesstransport ge_first_rn_product_uniquematchingmatchingunit_witnesstransport ge_first_ip_product_uniquematchingmatchingunit_witnesstransport ge_first_in_product_uniquematchingmatchingunit_witnesstransport ge_second_rp_product_uniquematchingmatchingunit_witnesstransport ge_second_rn_product_uniquematchingmatchingunit_witnesstransport ge_second_ip_product_uniquematchingmatchingunit_witnesstransport ge_second_in_product_uniquematchingmatchingunit_witnesstransport. ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst. (((gr_unit_product_uniquematchingmatchingunit_witness) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstreal = (ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportfirstimaginary = (ge_first_in_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond. (((gr_match_source_product_uniquematchingmatching) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondreal = (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportsecondimaginary = (ge_second_in_product_uniquematchingmatchingunit_witnesstransport) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput. (((gr_match_target_product_uniquematchingmatching) = ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_product_uniquematchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_product_uniquematchingmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_negative_product_uniquematchingmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_in_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_rn_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_ip_product_uniquematchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rn_product_uniquematchingmatchingunit_witnesstransport))) + (((ge_first_in_product_uniquematchingmatchingunit_witnesstransport) * (ge_second_rp_product_uniquematchingmatchingunit_witnesstransport))))))) + ge_balance_positive_product_uniquematchingmatchingunit_witnesstransportoutputimaginary)))))))))))))))))

Complete tactic proof in conservative notation

All 348 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

348 script commands · 79 reading checkpoints · 21 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 (21)

01Induction on lL1–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

L1
induction l
L2
intro b
L3
intro c
L4
intro P
L5
intro m
L6
intro d
L7
intro e
L8
intro Q
L9
intro hall
L10
intro hP

02Fix variables and assumptionsL11–13

Work with arbitrary variables or the premises of the current implication.

L11
intro hrall
L12
intro hQ
L13
intro hassoc

03Establish hidentityL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product empty value.

L14
have hidentity : P=6
L15
specialize gaussian_product_empty_value (b)
L16
specialize gaussian_product_empty_value (c)
L17
specialize gaussian_product_empty_value (P)
L18
apply gaussian_product_empty_value
L19
exact hP

04Establish hunitL20–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor associate unit.

L20
have hunit : GUnit(Q)Definitions: GUnit(Q)Original native command in the exact edition
L21
specialize gaussian_factor_associate_unit (P)
L22
specialize gaussian_factor_associate_unit (Q)
L23
apply gaussian_factor_associate_unit
L24
exact hassoc
L25
rewrite hidentity
L26
exact gaussian_one_unit

05Establish hlengthL27–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian all irreducible product unit length zero.

L27
have hlength : m=0
L28
specialize gaussian_all_irreducible_product_unit_length_zero (d)
L29
specialize gaussian_all_irreducible_product_unit_length_zero (e)
L30
specialize gaussian_all_irreducible_product_unit_length_zero (m)
L31
specialize gaussian_all_irreducible_product_unit_length_zero (Q)
L32
apply gaussian_all_irreducible_product_unit_length_zero
L33
exact hrall
L34
exact hQ
L35
exact hunit

06Separate the logical casesL36–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L36
split

07Calculate and transport equalitiesL37–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L37
symm

08Use earlier factsL38–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

L38
exact hlength

09Construct an explicit witnessL39–40

Supply the displayed value, then prove that it has the required property.

L39
exists (0)
L40
exists (0)

10Use earlier factsL41–45

Instantiate or apply named facts and discharge the corresponding proof obligations.

L41
specialize gaussian_factor_empty_matching (b)
L42
specialize gaussian_factor_empty_matching (c)
L43
specialize gaussian_factor_empty_matching (d)
L44
specialize gaussian_factor_empty_matching (e)
L45
apply gaussian_factor_empty_matching

11Fix variables and assumptionsL46–55

Work with arbitrary variables or the premises of the current implication.

L46
intro b
L47
intro c
L48
intro P
L49
intro m
L50
intro d
L51
intro e
L52
intro Q
L53
intro hall
L54
intro hP
L55
intro hrall

12Fix variables and assumptionsL56–57

Work with arbitrary variables or the premises of the current implication.

L56
intro hQ
L57
intro hassoc

13Establish hfirstL58–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product successor decompose.

L58
have hfirst : ∃ p. ∃ R. BetaAt(b,c,l,p) ∧ (GProduct(b,c,l,R) ∧ GMul(R,p,P))Definitions: BetaAt(b,c,l,p)GProduct(b,c,l,R)GMul(R,p,P)Original native command in the exact edition
L59
specialize gaussian_product_successor_decompose (b)
L60
specialize gaussian_product_successor_decompose (c)
L61
specialize gaussian_product_successor_decompose (l)
L62
specialize gaussian_product_successor_decompose (P)
L63
apply gaussian_product_successor_decompose
L64
exact hP

14Separate the logical casesL65–68

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L65
cases hfirst
L66
cases hfirst_witness
L67
cases hfirst_witness_witness
L68
cases hfirst_witness_witness_right

15Establish hirL69–75

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hall.

L69
have hir : GIrreducible(x)Definitions: GIrreducible(x)Original native command in the exact edition
L70
specialize hall (l)
L71
specialize hall (x)
L72
apply hall
L73
specialize le_refl (S l)
L74
apply le_refl
L75
exact hfirst_witness_witness_left

16Establish hdivL76–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian divides transitive.

L76
have hdiv : GDvd(x,Q)Definitions: GDvd(x,Q)Original native command in the exact edition
L77
specialize gaussian_divides_transitive (x)
L78
specialize gaussian_divides_transitive (P)
L79
specialize gaussian_divides_transitive (Q)
L80
apply gaussian_divides_transitive

17Construct an explicit witnessL81–81

Supply the displayed value, then prove that it has the required property.

L81
exists (x1)

18Use earlier factsL82–90

Instantiate or apply named facts and discharge the corresponding proof obligations.

L82
specialize gaussian_multiply_commutative (x1)
L83
specialize gaussian_multiply_commutative (x)
L84
specialize gaussian_multiply_commutative (P)
L85
apply gaussian_multiply_commutative
L86
exact hfirst_witness_witness_right_right
L87
specialize gaussian_associate_divides (P)
L88
specialize gaussian_associate_divides (Q)
L89
apply gaussian_associate_divides
L90
exact hassoc

19Establish hmemberL91–100

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian irreducible divisor product member.

L91
have hmember : ∃ i. ∃ q. Lt(i,m) ∧ (BetaAt(d,e,i,q) ∧ GAssociate(x,q))Definitions: Lt(i,m)BetaAt(d,e,i,q)GAssociate(x,q)Original native command in the exact edition
L92
specialize gaussian_irreducible_divisor_product_member (m)
L93
specialize gaussian_irreducible_divisor_product_member (d)
L94
specialize gaussian_irreducible_divisor_product_member (e)
L95
specialize gaussian_irreducible_divisor_product_member (Q)
L96
specialize gaussian_irreducible_divisor_product_member (x)
L97
apply gaussian_irreducible_divisor_product_member
L98
exact hrall
L99
exact hQ
L100
exact hir

20Use earlier factsL101–101

Instantiate or apply named facts and discharge the corresponding proof obligations.

L101
exact hdiv

21Separate the logical casesL102–105

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L102
cases hmember
L103
cases hmember_witness
L104
cases hmember_witness_witness
L105
cases hmember_witness_witness_right

22Establish hmL106–108

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply zero or succ.

L106
have hm : m=0 \/ exists k. m=S k
L107
specialize zero_or_succ (m)
L108
apply zero_or_succ

23Separate the logical casesL109–110

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L109
cases hm
L110
exfalso

24Use earlier factsL111–112

Instantiate or apply named facts and discharge the corresponding proof obligations.

L111
specialize gaussian_search_no_index_below_zero (x2)
L112
apply gaussian_search_no_index_below_zero

25Calculate and transport equalitiesL113–113

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L113
rewrite hm_left at hmember_witness_witness_left

26Use earlier factsL114–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

L114
exact hmember_witness_witness_left

27Separate the logical casesL115–115

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L115
cases hm_right

28Establish hrightL116–124

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product length transport.

L116
have hright : GProduct(d,e,S x4,Q)Definitions: GProduct(d,e,S x4,Q)Original native command in the exact edition
L117
specialize gaussian_product_length_transport (d)
L118
specialize gaussian_product_length_transport (e)
L119
specialize gaussian_product_length_transport (m)
L120
specialize gaussian_product_length_transport (S x4)
L121
specialize gaussian_product_length_transport (Q)
L122
apply gaussian_product_length_transport
L123
exact hm_right_witness
L124
exact hQ

29Establish hrightallL125–133

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian all irreducible length transport.

L125
have hrightall : GAllIrreducible(d,e,S x4)Definitions: GAllIrreducible(d,e,S x4)Original native command in the exact edition
L126
specialize gaussian_all_irreducible_length_transport (d)
L127
specialize gaussian_all_irreducible_length_transport (e)
L128
specialize gaussian_all_irreducible_length_transport (m)
L129
specialize gaussian_all_irreducible_length_transport (S x4)
L130
apply gaussian_all_irreducible_length_transport
L131
exact hm_right_witness
L132
exact hrall
L133
rewrite hm_right_witness at hmember_witness_witness_left

30Establish hcaseL134–138

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

L134
have hcase : x2 = x4 ∨ Lt(x2,x4)Definitions: Lt(x2,x4)Original native command in the exact edition
L135
specialize finite_lt_succ_eq_or_lt (x4)
L136
specialize finite_lt_succ_eq_or_lt (x2)
L137
apply finite_lt_succ_eq_or_lt
L138
exact hmember_witness_witness_left

31Separate the logical casesL139–139

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L139
cases hcase

32Establish hlastL140–148

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product beta index transport.

L140
have hlast : BetaAt(d,e,x4,x3)Definitions: BetaAt(d,e,x4,x3)Original native command in the exact edition
L141
specialize gaussian_product_beta_index_transport (d)
L142
specialize gaussian_product_beta_index_transport (e)
L143
specialize gaussian_product_beta_index_transport (x2)
L144
specialize gaussian_product_beta_index_transport (x4)
L145
specialize gaussian_product_beta_index_transport (x3)
L146
apply gaussian_product_beta_index_transport
L147
exact hcase_left
L148
exact hmember_witness_witness_right_left

33Establish htailL149–157

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product decompose at last.

L149
have htail : ∃ T. GProduct(d,e,x4,T) ∧ GMul(T,x3,Q)Definitions: GProduct(d,e,x4,T)GMul(T,x3,Q)Original native command in the exact edition
L150
specialize gaussian_product_decompose_at_last (d)
L151
specialize gaussian_product_decompose_at_last (e)
L152
specialize gaussian_product_decompose_at_last (x4)
L153
specialize gaussian_product_decompose_at_last (Q)
L154
specialize gaussian_product_decompose_at_last (x3)
L155
apply gaussian_product_decompose_at_last
L156
exact hright
L157
exact hlast

34Separate the logical casesL158–159

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L158
cases htail
L159
cases htail_witness

35Establish hprefixL160–169

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor associate cancel products.

L160
have hprefix : GAssociate(x1,x5)Definitions: GAssociate(x1,x5)Original native command in the exact edition
L161
specialize gaussian_factor_associate_cancel_products (x1)
L162
specialize gaussian_factor_associate_cancel_products (x)
L163
specialize gaussian_factor_associate_cancel_products (P)
L164
specialize gaussian_factor_associate_cancel_products (x5)
L165
specialize gaussian_factor_associate_cancel_products (x3)
L166
specialize gaussian_factor_associate_cancel_products (Q)
L167
apply gaussian_factor_associate_cancel_products
L168
exact hfirst_witness_witness_right_right
L169
exact htail_witness_right

36Use earlier factsL170–171

Instantiate or apply named facts and discharge the corresponding proof obligations.

L170
exact hassoc
L171
exact hmember_witness_witness_right_right

37Separate the logical casesL172–174

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L172
cases hir
L173
cases hir_right
L174
cases hir_right_right

38Use earlier factsL175–175

Instantiate or apply named facts and discharge the corresponding proof obligations.

L175
exact hir_right_left

39Establish hrecL176–185

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

L176
have hrec : l = x4 ∧ (∃ x. ∃ y. GMatchedFactors(b,c,d,e,x,y,l))Definitions: GMatchedFactors(b,c,d,e,x,y,l)Original native command in the exact edition
L177
specialize IH (b)
L178
specialize IH (c)
L179
specialize IH (x1)
L180
specialize IH (x4)
L181
specialize IH (d)
L182
specialize IH (e)
L183
specialize IH (x5)
L184
apply IH
L185
specialize gaussian_all_irreducible_prefix (b)

40Use earlier factsL186–195

Instantiate or apply named facts and discharge the corresponding proof obligations.

L186
specialize gaussian_all_irreducible_prefix (c)
L187
specialize gaussian_all_irreducible_prefix (l)
L188
apply gaussian_all_irreducible_prefix
L189
exact hall
L190
exact hfirst_witness_witness_right_left
L191
specialize gaussian_all_irreducible_prefix (d)
L192
specialize gaussian_all_irreducible_prefix (e)
L193
specialize gaussian_all_irreducible_prefix (x4)
L194
apply gaussian_all_irreducible_prefix
L195
exact hrightall

41Use earlier factsL196–197

Instantiate or apply named facts and discharge the corresponding proof obligations.

L196
exact htail_witness_left
L197
exact hprefix

42Separate the logical casesL198–201

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L198
cases hrec
L199
cases hrec_right
L200
cases hrec_right_witness
L201
split

43Calculate and transport equalitiesL202–203

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L202
trans S x4
L203
congr

44Use earlier factsL204–204

Instantiate or apply named facts and discharge the corresponding proof obligations.

L204
exact hrec_left

45Calculate and transport equalitiesL205–205

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L205
symm

46Use earlier factsL206–206

Instantiate or apply named facts and discharge the corresponding proof obligations.

L206
exact hm_right_witness

47Establish hfullL207–216

Establish this local claim before using it. It is not an additional assumption.

L207
have hfull : ∃ U. ∃ V. GMatchedFactors(b,c,d,e,U,V,S l) ∧ (BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(x6,x7,x,y) → BetaAt(U,V,x,y)))Definitions: GMatchedFactors(b,c,d,e,U,V,S l)BetaAt(U,V,l,l)Lt(x,l)BetaAt(x6,x7,x,y)BetaAt(U,V,x,y)Original native command in the exact edition
L208
specialize gaussian_factor_matched_append (b)
L209
specialize gaussian_factor_matched_append (c)
L210
specialize gaussian_factor_matched_append (d)
L211
specialize gaussian_factor_matched_append (e)
L212
specialize gaussian_factor_matched_append (x6)
L213
specialize gaussian_factor_matched_append (x7)
L214
specialize gaussian_factor_matched_append (l)
L215
specialize gaussian_factor_matched_append (x)
L216
specialize gaussian_factor_matched_append (x3)

48Use earlier factsL217–225

Instantiate or apply named facts and discharge the corresponding proof obligations.

L217
apply gaussian_factor_matched_append
L218
exact hrec_right_witness_witness
L219
exact hfirst_witness_witness_left
L220
specialize gaussian_product_beta_index_transport (d)
L221
specialize gaussian_product_beta_index_transport (e)
L222
specialize gaussian_product_beta_index_transport (x4)
L223
specialize gaussian_product_beta_index_transport (l)
L224
specialize gaussian_product_beta_index_transport (x3)
L225
apply gaussian_product_beta_index_transport

49Calculate and transport equalitiesL226–226

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L226
symm

50Use earlier factsL227–229

Instantiate or apply named facts and discharge the corresponding proof obligations.

L227
exact hrec_left
L228
exact hlast
L229
exact hmember_witness_witness_right_right

51Separate the logical casesL230–232

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L230
cases hfull
L231
cases hfull_witness
L232
cases hfull_witness_witness

52Construct an explicit witnessL233–234

Supply the displayed value, then prove that it has the required property.

L233
exists (x8)
L234
exists (x9)

53Use earlier factsL235–235

Instantiate or apply named facts and discharge the corresponding proof obligations.

L235
exact hfull_witness_witness_left

54Establish hswapL236–245

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor swapped product exists.

L236
have hswap : ∃ D. ∃ E. ∃ t. GAllIrreducible(D,E,S x4) ∧ (GProduct(D,E,S x4,Q) ∧ (BetaAt(d,e,x2,x3) ∧ (BetaAt(d,e,x4,t) ∧ (BetaAt(D,E,x2,t) ∧ (BetaAt(D,E,x4,x3) ∧ (∀ x. ∀ y. Lt(x,S x4) → ¬x = x2 → ¬x = x4 → BetaAt(d,e,x,y) → BetaAt(D,E,x,y)))))))Definitions: GAllIrreducible(D,E,S x4)GProduct(D,E,S x4,Q)BetaAt(d,e,x2,x3)BetaAt(d,e,x4,t)BetaAt(D,E,x2,t)BetaAt(D,E,x4,x3)Lt(x,S x4)BetaAt(d,e,x,y)BetaAt(D,E,x,y)Original native command in the exact edition
L237
specialize gaussian_factor_swapped_product_exists (d)
L238
specialize gaussian_factor_swapped_product_exists (e)
L239
specialize gaussian_factor_swapped_product_exists (x4)
L240
specialize gaussian_factor_swapped_product_exists (x2)
L241
specialize gaussian_factor_swapped_product_exists (x3)
L242
specialize gaussian_factor_swapped_product_exists (Q)
L243
apply gaussian_factor_swapped_product_exists
L244
exact hrightall
L245
exact hright

55Use earlier factsL246–247

Instantiate or apply named facts and discharge the corresponding proof obligations.

L246
exact hcase_right
L247
exact hmember_witness_witness_right_left

56Separate the logical casesL248–252

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L248
cases hswap
L249
cases hswap_witness
L250
cases hswap_witness_witness
L251
cases hswap_witness_witness_witness
L252
cases hswap_witness_witness_witness_right

57Establish hlastL253–253

Establish this local claim before using it. It is not an additional assumption.

L253
have hlast : BetaAt(x5,x6,x4,x3)Definitions: BetaAt(x5,x6,x4,x3)Original native command in the exact edition

58Separate the logical casesL254–257

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L254
cases hswap_witness_witness_witness_right_right
L255
cases hswap_witness_witness_witness_right_right_right
L256
cases hswap_witness_witness_witness_right_right_right_right
L257
cases hswap_witness_witness_witness_right_right_right_right_right

59Use earlier factsL258–258

Instantiate or apply named facts and discharge the corresponding proof obligations.

L258
exact hswap_witness_witness_witness_right_right_right_right_right_left

60Establish htailL259–267

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian product decompose at last.

L259
have htail : ∃ T. GProduct(x5,x6,x4,T) ∧ GMul(T,x3,Q)Definitions: GProduct(x5,x6,x4,T)GMul(T,x3,Q)Original native command in the exact edition
L260
specialize gaussian_product_decompose_at_last (x5)
L261
specialize gaussian_product_decompose_at_last (x6)
L262
specialize gaussian_product_decompose_at_last (x4)
L263
specialize gaussian_product_decompose_at_last (Q)
L264
specialize gaussian_product_decompose_at_last (x3)
L265
apply gaussian_product_decompose_at_last
L266
exact hswap_witness_witness_witness_right_left
L267
exact hlast

61Separate the logical casesL268–269

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L268
cases htail
L269
cases htail_witness

62Establish hprefixL270–279

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor associate cancel products.

L270
have hprefix : GAssociate(x1,x8)Definitions: GAssociate(x1,x8)Original native command in the exact edition
L271
specialize gaussian_factor_associate_cancel_products (x1)
L272
specialize gaussian_factor_associate_cancel_products (x)
L273
specialize gaussian_factor_associate_cancel_products (P)
L274
specialize gaussian_factor_associate_cancel_products (x8)
L275
specialize gaussian_factor_associate_cancel_products (x3)
L276
specialize gaussian_factor_associate_cancel_products (Q)
L277
apply gaussian_factor_associate_cancel_products
L278
exact hfirst_witness_witness_right_right
L279
exact htail_witness_right

63Use earlier factsL280–281

Instantiate or apply named facts and discharge the corresponding proof obligations.

L280
exact hassoc
L281
exact hmember_witness_witness_right_right

64Separate the logical casesL282–284

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L282
cases hir
L283
cases hir_right
L284
cases hir_right_right

65Use earlier factsL285–285

Instantiate or apply named facts and discharge the corresponding proof obligations.

L285
exact hir_right_left

66Establish hrecL286–295

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.

L286
have hrec : l = x4 ∧ (∃ x. ∃ y. GMatchedFactors(b,c,x5,x6,x,y,l))Definitions: GMatchedFactors(b,c,x5,x6,x,y,l)Original native command in the exact edition
L287
specialize IH (b)
L288
specialize IH (c)
L289
specialize IH (x1)
L290
specialize IH (x4)
L291
specialize IH (x5)
L292
specialize IH (x6)
L293
specialize IH (x8)
L294
apply IH
L295
specialize gaussian_all_irreducible_prefix (b)

67Use earlier factsL296–305

Instantiate or apply named facts and discharge the corresponding proof obligations.

L296
specialize gaussian_all_irreducible_prefix (c)
L297
specialize gaussian_all_irreducible_prefix (l)
L298
apply gaussian_all_irreducible_prefix
L299
exact hall
L300
exact hfirst_witness_witness_right_left
L301
specialize gaussian_all_irreducible_prefix (x5)
L302
specialize gaussian_all_irreducible_prefix (x6)
L303
specialize gaussian_all_irreducible_prefix (x4)
L304
apply gaussian_all_irreducible_prefix
L305
exact hswap_witness_witness_witness_left

68Use earlier factsL306–307

Instantiate or apply named facts and discharge the corresponding proof obligations.

L306
exact htail_witness_left
L307
exact hprefix

69Separate the logical casesL308–311

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L308
cases hrec
L309
cases hrec_right
L310
cases hrec_right_witness
L311
split

70Calculate and transport equalitiesL312–313

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L312
trans S x4
L313
congr

71Use earlier factsL314–314

Instantiate or apply named facts and discharge the corresponding proof obligations.

L314
exact hrec_left

72Calculate and transport equalitiesL315–315

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L315
symm

73Use earlier factsL316–325

Instantiate or apply named facts and discharge the corresponding proof obligations.

L316
exact hm_right_witness
L317
specialize gaussian_factor_matched_unswap_exists (b)
L318
specialize gaussian_factor_matched_unswap_exists (c)
L319
specialize gaussian_factor_matched_unswap_exists (d)
L320
specialize gaussian_factor_matched_unswap_exists (e)
L321
specialize gaussian_factor_matched_unswap_exists (x5)
L322
specialize gaussian_factor_matched_unswap_exists (x6)
L323
specialize gaussian_factor_matched_unswap_exists (x9)
L324
specialize gaussian_factor_matched_unswap_exists (x10)
L325
specialize gaussian_factor_matched_unswap_exists (l)

74Use earlier factsL326–330

Instantiate or apply named facts and discharge the corresponding proof obligations.

L326
specialize gaussian_factor_matched_unswap_exists (x2)
L327
specialize gaussian_factor_matched_unswap_exists (x)
L328
specialize gaussian_factor_matched_unswap_exists (x3)
L329
specialize gaussian_factor_matched_unswap_exists (x7)
L330
apply gaussian_factor_matched_unswap_exists

75Calculate and transport equalitiesL331–331

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L331
rewrite <- hrec_left at hcase_right

76Use earlier factsL332–341

Instantiate or apply named facts and discharge the corresponding proof obligations.

L332
exact hcase_right
L333
exact hrec_right_witness_witness
L334
exact hfirst_witness_witness_left
L335
specialize gaussian_factor_swap_length_transport (d)
L336
specialize gaussian_factor_swap_length_transport (e)
L337
specialize gaussian_factor_swap_length_transport (x5)
L338
specialize gaussian_factor_swap_length_transport (x6)
L339
specialize gaussian_factor_swap_length_transport (x4)
L340
specialize gaussian_factor_swap_length_transport (l)
L341
specialize gaussian_factor_swap_length_transport (x2)

77Use earlier factsL342–344

Instantiate or apply named facts and discharge the corresponding proof obligations.

L342
specialize gaussian_factor_swap_length_transport (x3)
L343
specialize gaussian_factor_swap_length_transport (x7)
L344
apply gaussian_factor_swap_length_transport

78Calculate and transport equalitiesL345–345

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L345
symm

79Use earlier factsL346–348

Instantiate or apply named facts and discharge the corresponding proof obligations.

L346
exact hrec_left
L347
exact hswap_witness_witness_witness_right_right
L348
exact hmember_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 348 lines

0001induction l
0002intro b
0003intro c
0004intro P
0005intro m
0006intro d
0007intro e
0008intro Q
0009intro hall
0010intro hP
0011intro hrall
0012intro hQ
0013intro hassoc
0014have hidentity : P=6
0015specialize gaussian_product_empty_value (b)
0016specialize gaussian_product_empty_value (c)
0017specialize gaussian_product_empty_value (P)
0018apply gaussian_product_empty_value
0019exact hP
0020have hunit : GUnit(Q)
0021specialize gaussian_factor_associate_unit (P)
0022specialize gaussian_factor_associate_unit (Q)
0023apply gaussian_factor_associate_unit
0024exact hassoc
0025rewrite hidentity
0026exact gaussian_one_unit
0027have hlength : m=0
0028specialize gaussian_all_irreducible_product_unit_length_zero (d)
0029specialize gaussian_all_irreducible_product_unit_length_zero (e)
0030specialize gaussian_all_irreducible_product_unit_length_zero (m)
0031specialize gaussian_all_irreducible_product_unit_length_zero (Q)
0032apply gaussian_all_irreducible_product_unit_length_zero
0033exact hrall
0034exact hQ
0035exact hunit
0036split
0037symm
0038exact hlength
0039exists (0)
0040exists (0)
0041specialize gaussian_factor_empty_matching (b)
0042specialize gaussian_factor_empty_matching (c)
0043specialize gaussian_factor_empty_matching (d)
0044specialize gaussian_factor_empty_matching (e)
0045apply gaussian_factor_empty_matching
0046intro b
0047intro c
0048intro P
0049intro m
0050intro d
0051intro e
0052intro Q
0053intro hall
0054intro hP
0055intro hrall
0056intro hQ
0057intro hassoc
0058have hfirst : ∃ p. ∃ R. BetaAt(b,c,l,p) ∧ (GProduct(b,c,l,R) ∧ GMul(R,p,P))
0059specialize gaussian_product_successor_decompose (b)
0060specialize gaussian_product_successor_decompose (c)
0061specialize gaussian_product_successor_decompose (l)
0062specialize gaussian_product_successor_decompose (P)
0063apply gaussian_product_successor_decompose
0064exact hP
0065cases hfirst
0066cases hfirst_witness
0067cases hfirst_witness_witness
0068cases hfirst_witness_witness_right
0069have hir : GIrreducible(x)
0070specialize hall (l)
0071specialize hall (x)
0072apply hall
0073specialize le_refl (S l)
0074apply le_refl
0075exact hfirst_witness_witness_left
0076have hdiv : GDvd(x,Q)
0077specialize gaussian_divides_transitive (x)
0078specialize gaussian_divides_transitive (P)
0079specialize gaussian_divides_transitive (Q)
0080apply gaussian_divides_transitive
0081exists (x1)
0082specialize gaussian_multiply_commutative (x1)
0083specialize gaussian_multiply_commutative (x)
0084specialize gaussian_multiply_commutative (P)
0085apply gaussian_multiply_commutative
0086exact hfirst_witness_witness_right_right
0087specialize gaussian_associate_divides (P)
0088specialize gaussian_associate_divides (Q)
0089apply gaussian_associate_divides
0090exact hassoc
0091have hmember : ∃ i. ∃ q. Lt(i,m) ∧ (BetaAt(d,e,i,q) ∧ GAssociate(x,q))
0092specialize gaussian_irreducible_divisor_product_member (m)
0093specialize gaussian_irreducible_divisor_product_member (d)
0094specialize gaussian_irreducible_divisor_product_member (e)
0095specialize gaussian_irreducible_divisor_product_member (Q)
0096specialize gaussian_irreducible_divisor_product_member (x)
0097apply gaussian_irreducible_divisor_product_member
0098exact hrall
0099exact hQ
0100exact hir
0101exact hdiv
0102cases hmember
0103cases hmember_witness
0104cases hmember_witness_witness
0105cases hmember_witness_witness_right
0106have hm : m=0 \/ exists k. m=S k
0107specialize zero_or_succ (m)
0108apply zero_or_succ
0109cases hm
0110exfalso
0111specialize gaussian_search_no_index_below_zero (x2)
0112apply gaussian_search_no_index_below_zero
0113rewrite hm_left at hmember_witness_witness_left
0114exact hmember_witness_witness_left
0115cases hm_right
0116have hright : GProduct(d,e,S x4,Q)
0117specialize gaussian_product_length_transport (d)
0118specialize gaussian_product_length_transport (e)
0119specialize gaussian_product_length_transport (m)
0120specialize gaussian_product_length_transport (S x4)
0121specialize gaussian_product_length_transport (Q)
0122apply gaussian_product_length_transport
0123exact hm_right_witness
0124exact hQ
0125have hrightall : GAllIrreducible(d,e,S x4)
0126specialize gaussian_all_irreducible_length_transport (d)
0127specialize gaussian_all_irreducible_length_transport (e)
0128specialize gaussian_all_irreducible_length_transport (m)
0129specialize gaussian_all_irreducible_length_transport (S x4)
0130apply gaussian_all_irreducible_length_transport
0131exact hm_right_witness
0132exact hrall
0133rewrite hm_right_witness at hmember_witness_witness_left
0134have hcase : x2 = x4 ∨ Lt(x2,x4)
0135specialize finite_lt_succ_eq_or_lt (x4)
0136specialize finite_lt_succ_eq_or_lt (x2)
0137apply finite_lt_succ_eq_or_lt
0138exact hmember_witness_witness_left
0139cases hcase
0140have hlast : BetaAt(d,e,x4,x3)
0141specialize gaussian_product_beta_index_transport (d)
0142specialize gaussian_product_beta_index_transport (e)
0143specialize gaussian_product_beta_index_transport (x2)
0144specialize gaussian_product_beta_index_transport (x4)
0145specialize gaussian_product_beta_index_transport (x3)
0146apply gaussian_product_beta_index_transport
0147exact hcase_left
0148exact hmember_witness_witness_right_left
0149have htail : ∃ T. GProduct(d,e,x4,T) ∧ GMul(T,x3,Q)
0150specialize gaussian_product_decompose_at_last (d)
0151specialize gaussian_product_decompose_at_last (e)
0152specialize gaussian_product_decompose_at_last (x4)
0153specialize gaussian_product_decompose_at_last (Q)
0154specialize gaussian_product_decompose_at_last (x3)
0155apply gaussian_product_decompose_at_last
0156exact hright
0157exact hlast
0158cases htail
0159cases htail_witness
0160have hprefix : GAssociate(x1,x5)
0161specialize gaussian_factor_associate_cancel_products (x1)
0162specialize gaussian_factor_associate_cancel_products (x)
0163specialize gaussian_factor_associate_cancel_products (P)
0164specialize gaussian_factor_associate_cancel_products (x5)
0165specialize gaussian_factor_associate_cancel_products (x3)
0166specialize gaussian_factor_associate_cancel_products (Q)
0167apply gaussian_factor_associate_cancel_products
0168exact hfirst_witness_witness_right_right
0169exact htail_witness_right
0170exact hassoc
0171exact hmember_witness_witness_right_right
0172cases hir
0173cases hir_right
0174cases hir_right_right
0175exact hir_right_left
0176have hrec : l = x4 ∧ (∃ x. ∃ y. GMatchedFactors(b,c,d,e,x,y,l))
0177specialize IH (b)
0178specialize IH (c)
0179specialize IH (x1)
0180specialize IH (x4)
0181specialize IH (d)
0182specialize IH (e)
0183specialize IH (x5)
0184apply IH
0185specialize gaussian_all_irreducible_prefix (b)
0186specialize gaussian_all_irreducible_prefix (c)
0187specialize gaussian_all_irreducible_prefix (l)
0188apply gaussian_all_irreducible_prefix
0189exact hall
0190exact hfirst_witness_witness_right_left
0191specialize gaussian_all_irreducible_prefix (d)
0192specialize gaussian_all_irreducible_prefix (e)
0193specialize gaussian_all_irreducible_prefix (x4)
0194apply gaussian_all_irreducible_prefix
0195exact hrightall
0196exact htail_witness_left
0197exact hprefix
0198cases hrec
0199cases hrec_right
0200cases hrec_right_witness
0201split
0202trans S x4
0203congr
0204exact hrec_left
0205symm
0206exact hm_right_witness
0207have hfull : ∃ U. ∃ V. GMatchedFactors(b,c,d,e,U,V,S l) ∧ (BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(x6,x7,x,y) → BetaAt(U,V,x,y)))
0208specialize gaussian_factor_matched_append (b)
0209specialize gaussian_factor_matched_append (c)
0210specialize gaussian_factor_matched_append (d)
0211specialize gaussian_factor_matched_append (e)
0212specialize gaussian_factor_matched_append (x6)
0213specialize gaussian_factor_matched_append (x7)
0214specialize gaussian_factor_matched_append (l)
0215specialize gaussian_factor_matched_append (x)
0216specialize gaussian_factor_matched_append (x3)
0217apply gaussian_factor_matched_append
0218exact hrec_right_witness_witness
0219exact hfirst_witness_witness_left
0220specialize gaussian_product_beta_index_transport (d)
0221specialize gaussian_product_beta_index_transport (e)
0222specialize gaussian_product_beta_index_transport (x4)
0223specialize gaussian_product_beta_index_transport (l)
0224specialize gaussian_product_beta_index_transport (x3)
0225apply gaussian_product_beta_index_transport
0226symm
0227exact hrec_left
0228exact hlast
0229exact hmember_witness_witness_right_right
0230cases hfull
0231cases hfull_witness
0232cases hfull_witness_witness
0233exists (x8)
0234exists (x9)
0235exact hfull_witness_witness_left
0236have hswap : ∃ D. ∃ E. ∃ t. GAllIrreducible(D,E,S x4) ∧ (GProduct(D,E,S x4,Q) ∧ (BetaAt(d,e,x2,x3) ∧ (BetaAt(d,e,x4,t) ∧ (BetaAt(D,E,x2,t) ∧ (BetaAt(D,E,x4,x3) ∧ (∀ x. ∀ y. Lt(x,S x4) → ¬x = x2 → ¬x = x4 → BetaAt(d,e,x,y) → BetaAt(D,E,x,y)))))))
0237specialize gaussian_factor_swapped_product_exists (d)
0238specialize gaussian_factor_swapped_product_exists (e)
0239specialize gaussian_factor_swapped_product_exists (x4)
0240specialize gaussian_factor_swapped_product_exists (x2)
0241specialize gaussian_factor_swapped_product_exists (x3)
0242specialize gaussian_factor_swapped_product_exists (Q)
0243apply gaussian_factor_swapped_product_exists
0244exact hrightall
0245exact hright
0246exact hcase_right
0247exact hmember_witness_witness_right_left
0248cases hswap
0249cases hswap_witness
0250cases hswap_witness_witness
0251cases hswap_witness_witness_witness
0252cases hswap_witness_witness_witness_right
0253have hlast : BetaAt(x5,x6,x4,x3)
0254cases hswap_witness_witness_witness_right_right
0255cases hswap_witness_witness_witness_right_right_right
0256cases hswap_witness_witness_witness_right_right_right_right
0257cases hswap_witness_witness_witness_right_right_right_right_right
0258exact hswap_witness_witness_witness_right_right_right_right_right_left
0259have htail : ∃ T. GProduct(x5,x6,x4,T) ∧ GMul(T,x3,Q)
0260specialize gaussian_product_decompose_at_last (x5)
0261specialize gaussian_product_decompose_at_last (x6)
0262specialize gaussian_product_decompose_at_last (x4)
0263specialize gaussian_product_decompose_at_last (Q)
0264specialize gaussian_product_decompose_at_last (x3)
0265apply gaussian_product_decompose_at_last
0266exact hswap_witness_witness_witness_right_left
0267exact hlast
0268cases htail
0269cases htail_witness
0270have hprefix : GAssociate(x1,x8)
0271specialize gaussian_factor_associate_cancel_products (x1)
0272specialize gaussian_factor_associate_cancel_products (x)
0273specialize gaussian_factor_associate_cancel_products (P)
0274specialize gaussian_factor_associate_cancel_products (x8)
0275specialize gaussian_factor_associate_cancel_products (x3)
0276specialize gaussian_factor_associate_cancel_products (Q)
0277apply gaussian_factor_associate_cancel_products
0278exact hfirst_witness_witness_right_right
0279exact htail_witness_right
0280exact hassoc
0281exact hmember_witness_witness_right_right
0282cases hir
0283cases hir_right
0284cases hir_right_right
0285exact hir_right_left
0286have hrec : l = x4 ∧ (∃ x. ∃ y. GMatchedFactors(b,c,x5,x6,x,y,l))
0287specialize IH (b)
0288specialize IH (c)
0289specialize IH (x1)
0290specialize IH (x4)
0291specialize IH (x5)
0292specialize IH (x6)
0293specialize IH (x8)
0294apply IH
0295specialize gaussian_all_irreducible_prefix (b)
0296specialize gaussian_all_irreducible_prefix (c)
0297specialize gaussian_all_irreducible_prefix (l)
0298apply gaussian_all_irreducible_prefix
0299exact hall
0300exact hfirst_witness_witness_right_left
0301specialize gaussian_all_irreducible_prefix (x5)
0302specialize gaussian_all_irreducible_prefix (x6)
0303specialize gaussian_all_irreducible_prefix (x4)
0304apply gaussian_all_irreducible_prefix
0305exact hswap_witness_witness_witness_left
0306exact htail_witness_left
0307exact hprefix
0308cases hrec
0309cases hrec_right
0310cases hrec_right_witness
0311split
0312trans S x4
0313congr
0314exact hrec_left
0315symm
0316exact hm_right_witness
0317specialize gaussian_factor_matched_unswap_exists (b)
0318specialize gaussian_factor_matched_unswap_exists (c)
0319specialize gaussian_factor_matched_unswap_exists (d)
0320specialize gaussian_factor_matched_unswap_exists (e)
0321specialize gaussian_factor_matched_unswap_exists (x5)
0322specialize gaussian_factor_matched_unswap_exists (x6)
0323specialize gaussian_factor_matched_unswap_exists (x9)
0324specialize gaussian_factor_matched_unswap_exists (x10)
0325specialize gaussian_factor_matched_unswap_exists (l)
0326specialize gaussian_factor_matched_unswap_exists (x2)
0327specialize gaussian_factor_matched_unswap_exists (x)
0328specialize gaussian_factor_matched_unswap_exists (x3)
0329specialize gaussian_factor_matched_unswap_exists (x7)
0330apply gaussian_factor_matched_unswap_exists
0331rewrite <- hrec_left at hcase_right
0332exact hcase_right
0333exact hrec_right_witness_witness
0334exact hfirst_witness_witness_left
0335specialize gaussian_factor_swap_length_transport (d)
0336specialize gaussian_factor_swap_length_transport (e)
0337specialize gaussian_factor_swap_length_transport (x5)
0338specialize gaussian_factor_swap_length_transport (x6)
0339specialize gaussian_factor_swap_length_transport (x4)
0340specialize gaussian_factor_swap_length_transport (l)
0341specialize gaussian_factor_swap_length_transport (x2)
0342specialize gaussian_factor_swap_length_transport (x3)
0343specialize gaussian_factor_swap_length_transport (x7)
0344apply gaussian_factor_swap_length_transport
0345symm
0346exact hrec_left
0347exact hswap_witness_witness_witness_right_right
0348exact hmember_witness_witness_right_right