Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ b. ∀ c. ∀ l. ∀ i. ∀ p. ∀ P. GAllIrreducible(b,c,S l) → GProduct(b,c,S l,P) → Lt(i,l) → BetaAt(b,c,i,p) → ∃ x. ∃ y. ∃ z. GAllIrreducible(x,y,S l) ∧ (GProduct(x,y,S l,P) ∧ (BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,z) ∧ (BetaAt(x,y,i,z) ∧ (BetaAt(x,y,l,p) ∧ (∀ n. ∀ m. Lt(n,S l) → ¬n = i → ¬n = l → BetaAt(b,c,n,m) → BetaAt(x,y,n,m)))))))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
beta_at_exists · checked external prerequisitebeta_prefix_swap_last_from_entries · checked external prerequisitegaussian_factor_swap_all_irreduciblegaussian_all_irreducible_product_existsgaussian_product_swap_last_invariantgaussian_product_value_transport
Original expanded first-order statement
forall b c l i p P. (forall gr_factor_index_swap_product_original_factors gr_factor_value_swap_product_original_factors. (exists ge_gap_swap_product_original_factorsindex. ge_gap_swap_product_original_factorsindex + S (gr_factor_index_swap_product_original_factors) = (S l)) -> (((exists ff_h_gprod_swap_product_original_factorsentry. ff_h_gprod_swap_product_original_factorsentry + S (gr_factor_value_swap_product_original_factors) = S ((S (gr_factor_index_swap_product_original_factors)) * c)) /\ exists ff_q_gprod_swap_product_original_factorsentry. b = ff_q_gprod_swap_product_original_factorsentry * S ((S (gr_factor_index_swap_product_original_factors)) * c) + (gr_factor_value_swap_product_original_factors))) -> (((exists ge_real_positive_swap_product_original_factorsirreduciblecarrier ge_real_negative_swap_product_original_factorsirreduciblecarrier ge_imaginary_positive_swap_product_original_factorsirreduciblecarrier ge_imaginary_negative_swap_product_original_factorsirreduciblecarrier. (exists ge_real_code_swap_product_original_factorsirreduciblecarrierdecode ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode. (((gr_factor_value_swap_product_original_factors) = ((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode)) * S ((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_product_original_factorsirreduciblecarrier) /\ (ge_real_negative_swap_product_original_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_real. (((ge_real_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_product_original_factorsirreduciblecarrier) = 0) /\ (ge_real_negative_swap_product_original_factorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_product_original_factorsirreduciblecarrier) /\ (ge_imaginary_negative_swap_product_original_factorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_product_original_factorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_product_original_factorsirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_product_original_factorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_original_factorsirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_product_original_factors)=0)) /\ ((~(exists gr_inverse_swap_product_original_factorsirreduciblenonunit. (exists ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity ge_first_in_swap_product_original_factorsirreduciblenonunitidentity ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity ge_second_in_swap_product_original_factorsirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst. (((gr_factor_value_swap_product_original_factors) = ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond. (((gr_inverse_swap_product_original_factorsirreduciblenonunit) = ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_in_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_product_original_factorsirreducible gr_second_factor_swap_product_original_factorsirreducible. (exists ge_first_rp_swap_product_original_factorsirreduciblefactorization ge_first_rn_swap_product_original_factorsirreduciblefactorization ge_first_ip_swap_product_original_factorsirreduciblefactorization ge_first_in_swap_product_original_factorsirreduciblefactorization ge_second_rp_swap_product_original_factorsirreduciblefactorization ge_second_rn_swap_product_original_factorsirreduciblefactorization ge_second_ip_swap_product_original_factorsirreduciblefactorization ge_second_in_swap_product_original_factorsirreduciblefactorization. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst. (((gr_first_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond. (((gr_second_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondreal = (ge_second_rn_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblefactorization) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationsecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblefactorization) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput. (((gr_factor_value_swap_product_original_factors) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblefactorization) * (ge_second_in_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_rn_swap_product_original_factorsirreduciblefactorization) * (ge_second_ip_swap_product_original_factorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefactorization) * (ge_second_rn_swap_product_original_factorsirreduciblefactorization))) + (((ge_first_in_swap_product_original_factorsirreduciblefactorization) * (ge_second_rp_swap_product_original_factorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_product_original_factorsirreduciblefirst_unit. (exists ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_product_original_factorsirreduciblefirst_unit) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_product_original_factorsirreduciblesecond_unit. (exists ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_product_original_factorsirreducible) = ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_product_original_factorsirreduciblesecond_unit) = ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_factorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_original_factorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_original_factorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_original_factorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_original_factorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_original_factorsirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (exists gr_product_trace_swap_product_original_trace gr_product_scale_swap_product_original_trace. ((((exists ff_h_gprod_swap_product_original_tracestart. ff_h_gprod_swap_product_original_tracestart + S (6) = S ((S (0)) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_tracestart. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_tracestart * S ((S (0)) * gr_product_scale_swap_product_original_trace) + (6))) /\ ((((exists ff_h_gprod_swap_product_original_traceend. ff_h_gprod_swap_product_original_traceend + S (P) = S ((S (S l)) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_traceend. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_traceend * S ((S (S l)) * gr_product_scale_swap_product_original_trace) + (P))) /\ (forall gr_product_index_swap_product_original_tracesteps. (exists ge_gap_swap_product_original_tracestepsindex_bound. ge_gap_swap_product_original_tracestepsindex_bound + S (gr_product_index_swap_product_original_tracesteps) = (S l)) -> exists gr_product_factor_swap_product_original_tracesteps gr_product_before_swap_product_original_tracesteps gr_product_after_swap_product_original_tracesteps. ((((exists ff_h_gprod_swap_product_original_tracestepsfactor. ff_h_gprod_swap_product_original_tracestepsfactor + S (gr_product_factor_swap_product_original_tracesteps) = S ((S (gr_product_index_swap_product_original_tracesteps)) * c)) /\ exists ff_q_gprod_swap_product_original_tracestepsfactor. b = ff_q_gprod_swap_product_original_tracestepsfactor * S ((S (gr_product_index_swap_product_original_tracesteps)) * c) + (gr_product_factor_swap_product_original_tracesteps))) /\ ((((exists ff_h_gprod_swap_product_original_tracestepsbefore. ff_h_gprod_swap_product_original_tracestepsbefore + S (gr_product_before_swap_product_original_tracesteps) = S ((S (gr_product_index_swap_product_original_tracesteps)) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_tracestepsbefore. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_tracestepsbefore * S ((S (gr_product_index_swap_product_original_tracesteps)) * gr_product_scale_swap_product_original_trace) + (gr_product_before_swap_product_original_tracesteps))) /\ ((((exists ff_h_gprod_swap_product_original_tracestepsafter. ff_h_gprod_swap_product_original_tracestepsafter + S (gr_product_after_swap_product_original_tracesteps) = S ((S (S (gr_product_index_swap_product_original_tracesteps))) * gr_product_scale_swap_product_original_trace)) /\ exists ff_q_gprod_swap_product_original_tracestepsafter. gr_product_trace_swap_product_original_trace = ff_q_gprod_swap_product_original_tracestepsafter * S ((S (S (gr_product_index_swap_product_original_tracesteps))) * gr_product_scale_swap_product_original_trace) + (gr_product_after_swap_product_original_tracesteps))) /\ (exists ge_first_rp_swap_product_original_tracestepsmultiply ge_first_rn_swap_product_original_tracestepsmultiply ge_first_ip_swap_product_original_tracestepsmultiply ge_first_in_swap_product_original_tracestepsmultiply ge_second_rp_swap_product_original_tracestepsmultiply ge_second_rn_swap_product_original_tracestepsmultiply ge_second_ip_swap_product_original_tracestepsmultiply ge_second_in_swap_product_original_tracestepsmultiply. ((exists ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst. (((gr_product_before_swap_product_original_tracesteps) = ((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst)) * S ((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal. (((((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_product_original_tracestepsmultiplyfirst) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal) = S ge_signed_half_swap_product_original_tracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplyfirstreal = (ge_first_rn_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyfirst) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary) = S ge_signed_half_swap_product_original_tracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplyfirstimaginary = (ge_first_in_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_original_tracestepsmultiplysecond ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond. (((gr_product_factor_swap_product_original_tracesteps) = ((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond)) * S ((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal. (((((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_product_original_tracestepsmultiplysecond) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal) = S ge_signed_half_swap_product_original_tracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplysecondreal = (ge_second_rn_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplysecond) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary) = S ge_signed_half_swap_product_original_tracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_original_tracestepsmultiply) + ge_balance_negative_swap_product_original_tracestepsmultiplysecondimaginary = (ge_second_in_swap_product_original_tracestepsmultiply) + ge_balance_positive_swap_product_original_tracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput. (((gr_product_after_swap_product_original_tracesteps) = ((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput)) * S ((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal. (((((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_product_original_tracestepsmultiplyoutput) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal) = S ge_signed_half_swap_product_original_tracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))))))) + ge_balance_negative_swap_product_original_tracestepsmultiplyoutputreal = (((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))))))) + ge_balance_positive_swap_product_original_tracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_original_tracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_original_tracestepsmultiplyoutput) = 2 * ge_signed_half_swap_product_original_tracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary) = S ge_signed_half_swap_product_original_tracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))))))) + ge_balance_negative_swap_product_original_tracestepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_product_original_tracestepsmultiply) * (ge_second_in_swap_product_original_tracestepsmultiply))) + (((ge_first_rn_swap_product_original_tracestepsmultiply) * (ge_second_ip_swap_product_original_tracestepsmultiply))))) + (((((ge_first_ip_swap_product_original_tracestepsmultiply) * (ge_second_rn_swap_product_original_tracestepsmultiply))) + (((ge_first_in_swap_product_original_tracestepsmultiply) * (ge_second_rp_swap_product_original_tracestepsmultiply))))))) + ge_balance_positive_swap_product_original_tracestepsmultiplyoutputimaginary)))))))))))))))) -> (exists ge_gap_swap_product_selected_index. ge_gap_swap_product_selected_index + S (i) = (l)) -> (((exists ff_h_gprod_swap_product_selected_factor. ff_h_gprod_swap_product_selected_factor + S (p) = S ((S (i)) * c)) /\ exists ff_q_gprod_swap_product_selected_factor. b = ff_q_gprod_swap_product_selected_factor * S ((S (i)) * c) + (p))) -> exists d e q. (((forall gr_factor_index_swap_product_resultfactors gr_factor_value_swap_product_resultfactors. (exists ge_gap_swap_product_resultfactorsindex. ge_gap_swap_product_resultfactorsindex + S (gr_factor_index_swap_product_resultfactors) = (S (l))) -> (((exists ff_h_gprod_swap_product_resultfactorsentry. ff_h_gprod_swap_product_resultfactorsentry + S (gr_factor_value_swap_product_resultfactors) = S ((S (gr_factor_index_swap_product_resultfactors)) * e)) /\ exists ff_q_gprod_swap_product_resultfactorsentry. d = ff_q_gprod_swap_product_resultfactorsentry * S ((S (gr_factor_index_swap_product_resultfactors)) * e) + (gr_factor_value_swap_product_resultfactors))) -> (((exists ge_real_positive_swap_product_resultfactorsirreduciblecarrier ge_real_negative_swap_product_resultfactorsirreduciblecarrier ge_imaginary_positive_swap_product_resultfactorsirreduciblecarrier ge_imaginary_negative_swap_product_resultfactorsirreduciblecarrier. (exists ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode. (((gr_factor_value_swap_product_resultfactors) = ((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode)) * S ((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode) + (ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_product_resultfactorsirreduciblecarrier) /\ (ge_real_negative_swap_product_resultfactorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_real. (((ge_real_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_product_resultfactorsirreduciblecarrier) = 0) /\ (ge_real_negative_swap_product_resultfactorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_product_resultfactorsirreduciblecarrier) /\ (ge_imaginary_negative_swap_product_resultfactorsirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_product_resultfactorsirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_product_resultfactorsirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_product_resultfactorsirreduciblecarrier) = S ge_signed_half_ge_swap_product_resultfactorsirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_product_resultfactors)=0)) /\ ((~(exists gr_inverse_swap_product_resultfactorsirreduciblenonunit. (exists ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst. (((gr_factor_value_swap_product_resultfactors) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond. (((gr_inverse_swap_product_resultfactorsirreduciblenonunit) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblenonunitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblenonunitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblenonunitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_product_resultfactorsirreducible gr_second_factor_swap_product_resultfactorsirreducible. (exists ge_first_rp_swap_product_resultfactorsirreduciblefactorization ge_first_rn_swap_product_resultfactorsirreduciblefactorization ge_first_ip_swap_product_resultfactorsirreduciblefactorization ge_first_in_swap_product_resultfactorsirreduciblefactorization ge_second_rp_swap_product_resultfactorsirreduciblefactorization ge_second_rn_swap_product_resultfactorsirreduciblefactorization ge_second_ip_swap_product_resultfactorsirreduciblefactorization ge_second_in_swap_product_resultfactorsirreduciblefactorization. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst. (((gr_first_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond. (((gr_second_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblefactorization) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationsecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblefactorization) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput. (((gr_factor_value_swap_product_resultfactors) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefactorization) * (ge_second_in_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefactorization) * (ge_second_ip_swap_product_resultfactorsirreduciblefactorization))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rn_swap_product_resultfactorsirreduciblefactorization))) + (((ge_first_in_swap_product_resultfactorsirreduciblefactorization) * (ge_second_rp_swap_product_resultfactorsirreduciblefactorization))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_product_resultfactorsirreduciblefirst_unit. (exists ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_product_resultfactorsirreduciblefirst_unit) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblefirst_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblefirst_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_product_resultfactorsirreduciblesecond_unit. (exists ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_product_resultfactorsirreducible) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_product_resultfactorsirreduciblesecond_unit) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultfactorsirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_in_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_ip_swap_product_resultfactorsirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rn_swap_product_resultfactorsirreduciblesecond_unitidentity))) + (((ge_first_in_swap_product_resultfactorsirreduciblesecond_unitidentity) * (ge_second_rp_swap_product_resultfactorsirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_product_resultfactorsirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ ((exists gr_product_trace_swap_product_resultproduct gr_product_scale_swap_product_resultproduct. ((((exists ff_h_gprod_swap_product_resultproductstart. ff_h_gprod_swap_product_resultproductstart + S (6) = S ((S (0)) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductstart. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductstart * S ((S (0)) * gr_product_scale_swap_product_resultproduct) + (6))) /\ ((((exists ff_h_gprod_swap_product_resultproductend. ff_h_gprod_swap_product_resultproductend + S (P) = S ((S (S (l))) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductend. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductend * S ((S (S (l))) * gr_product_scale_swap_product_resultproduct) + (P))) /\ (forall gr_product_index_swap_product_resultproductsteps. (exists ge_gap_swap_product_resultproductstepsindex_bound. ge_gap_swap_product_resultproductstepsindex_bound + S (gr_product_index_swap_product_resultproductsteps) = (S (l))) -> exists gr_product_factor_swap_product_resultproductsteps gr_product_before_swap_product_resultproductsteps gr_product_after_swap_product_resultproductsteps. ((((exists ff_h_gprod_swap_product_resultproductstepsfactor. ff_h_gprod_swap_product_resultproductstepsfactor + S (gr_product_factor_swap_product_resultproductsteps) = S ((S (gr_product_index_swap_product_resultproductsteps)) * e)) /\ exists ff_q_gprod_swap_product_resultproductstepsfactor. d = ff_q_gprod_swap_product_resultproductstepsfactor * S ((S (gr_product_index_swap_product_resultproductsteps)) * e) + (gr_product_factor_swap_product_resultproductsteps))) /\ ((((exists ff_h_gprod_swap_product_resultproductstepsbefore. ff_h_gprod_swap_product_resultproductstepsbefore + S (gr_product_before_swap_product_resultproductsteps) = S ((S (gr_product_index_swap_product_resultproductsteps)) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductstepsbefore. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductstepsbefore * S ((S (gr_product_index_swap_product_resultproductsteps)) * gr_product_scale_swap_product_resultproduct) + (gr_product_before_swap_product_resultproductsteps))) /\ ((((exists ff_h_gprod_swap_product_resultproductstepsafter. ff_h_gprod_swap_product_resultproductstepsafter + S (gr_product_after_swap_product_resultproductsteps) = S ((S (S (gr_product_index_swap_product_resultproductsteps))) * gr_product_scale_swap_product_resultproduct)) /\ exists ff_q_gprod_swap_product_resultproductstepsafter. gr_product_trace_swap_product_resultproduct = ff_q_gprod_swap_product_resultproductstepsafter * S ((S (S (gr_product_index_swap_product_resultproductsteps))) * gr_product_scale_swap_product_resultproduct) + (gr_product_after_swap_product_resultproductsteps))) /\ (exists ge_first_rp_swap_product_resultproductstepsmultiply ge_first_rn_swap_product_resultproductstepsmultiply ge_first_ip_swap_product_resultproductstepsmultiply ge_first_in_swap_product_resultproductstepsmultiply ge_second_rp_swap_product_resultproductstepsmultiply ge_second_rn_swap_product_resultproductstepsmultiply ge_second_ip_swap_product_resultproductstepsmultiply ge_second_in_swap_product_resultproductstepsmultiply. ((exists ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst. (((gr_product_before_swap_product_resultproductsteps) = ((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst)) * S ((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst)) + ((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst))) /\ ((exists ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal. (((((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyfirstrealdecode. (((ge_representation_real_code_swap_product_resultproductstepsmultiplyfirst) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal) = S ge_signed_half_swap_product_resultproductstepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplyfirstreal = (ge_first_rn_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplyfirstreal))) /\ (exists ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyfirst) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary) = S ge_signed_half_swap_product_resultproductstepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplyfirstimaginary = (ge_first_in_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_product_resultproductstepsmultiplysecond ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond. (((gr_product_factor_swap_product_resultproductsteps) = ((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond)) * S ((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond)) + ((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond))) /\ ((exists ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal. (((((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplysecondrealdecode. (((ge_representation_real_code_swap_product_resultproductstepsmultiplysecond) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal) = S ge_signed_half_swap_product_resultproductstepsmultiplysecondrealdecode))) /\ ((ge_second_rp_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplysecondreal = (ge_second_rn_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplysecondreal))) /\ (exists ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplysecond) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary) = S ge_signed_half_swap_product_resultproductstepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_swap_product_resultproductstepsmultiply) + ge_balance_negative_swap_product_resultproductstepsmultiplysecondimaginary = (ge_second_in_swap_product_resultproductstepsmultiply) + ge_balance_positive_swap_product_resultproductstepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput. (((gr_product_after_swap_product_resultproductsteps) = ((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput)) * S ((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput)) + ((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput) + (ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput))) /\ ((exists ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal. (((((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyoutputrealdecode. (((ge_representation_real_code_swap_product_resultproductstepsmultiplyoutput) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal) = S ge_signed_half_swap_product_resultproductstepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))))))) + ge_balance_negative_swap_product_resultproductstepsmultiplyoutputreal = (((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))))))) + ge_balance_positive_swap_product_resultproductstepsmultiplyoutputreal))) /\ (exists ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput) = 2 * (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_swap_product_resultproductstepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_swap_product_resultproductstepsmultiplyoutput) = 2 * ge_signed_half_swap_product_resultproductstepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary) = S ge_signed_half_swap_product_resultproductstepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))))))) + ge_balance_negative_swap_product_resultproductstepsmultiplyoutputimaginary = (((((((ge_first_rp_swap_product_resultproductstepsmultiply) * (ge_second_in_swap_product_resultproductstepsmultiply))) + (((ge_first_rn_swap_product_resultproductstepsmultiply) * (ge_second_ip_swap_product_resultproductstepsmultiply))))) + (((((ge_first_ip_swap_product_resultproductstepsmultiply) * (ge_second_rn_swap_product_resultproductstepsmultiply))) + (((ge_first_in_swap_product_resultproductstepsmultiply) * (ge_second_rp_swap_product_resultproductstepsmultiply))))))) + ge_balance_positive_swap_product_resultproductstepsmultiplyoutputimaginary)))))))))))))))) /\ (((((exists ff_h_pfp_swap_product_resultswapoldi. ff_h_pfp_swap_product_resultswapoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_product_resultswapoldi. b = ff_q_pfp_swap_product_resultswapoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_product_resultswapoldlast. ff_h_pfp_swap_product_resultswapoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_product_resultswapoldlast. b = ff_q_pfp_swap_product_resultswapoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_product_resultswapnewi. ff_h_pfp_swap_product_resultswapnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_product_resultswapnewi. d = ff_q_pfp_swap_product_resultswapnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_product_resultswapnewlast. ff_h_pfp_swap_product_resultswapnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_product_resultswapnewlast. d = ff_q_pfp_swap_product_resultswapnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_product_resultswap pfp_a_swap_product_resultswap. (exists pfp_gap_swap_product_resultswapbound. pfp_gap_swap_product_resultswapbound + S (pfp_j_swap_product_resultswap) = (S (l))) -> ~(pfp_j_swap_product_resultswap = i) -> ~(pfp_j_swap_product_resultswap = l) -> (((exists ff_h_pfp_swap_product_resultswapold. ff_h_pfp_swap_product_resultswapold + S (pfp_a_swap_product_resultswap) = S ((S (pfp_j_swap_product_resultswap)) * c)) /\ exists ff_q_pfp_swap_product_resultswapold. b = ff_q_pfp_swap_product_resultswapold * S ((S (pfp_j_swap_product_resultswap)) * c) + (pfp_a_swap_product_resultswap))) -> (((exists ff_h_pfp_swap_product_resultswapnew. ff_h_pfp_swap_product_resultswapnew + S (pfp_a_swap_product_resultswap) = S ((S (pfp_j_swap_product_resultswap)) * e)) /\ exists ff_q_pfp_swap_product_resultswapnew. d = ff_q_pfp_swap_product_resultswapnew * S ((S (pfp_j_swap_product_resultswap)) * e) + (pfp_a_swap_product_resultswap)))))))))))))))Complete tactic proof in conservative notation
All 93 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
93 script commands · 28 reading checkpoints · 6 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 (4)
01Fix variables and assumptionsL1–10
02Establish hlastL11–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.
- L11
have hlast : ∃ q. BetaAt(b,c,l,q)Definitions: BetaAt(b,c,l,q)Original native command in the exact edition - L12
specialize beta_at_exists (b) - L13
specialize beta_at_exists (c) - L14
specialize beta_at_exists (l) - L15
apply beta_at_exists
03Separate the logical casesL16–16
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L16
cases hlast
04Establish hnewL17–26
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix swap last from entries.
- L17
have hnew : ∃ d. ∃ e. BetaAt(d,e,i,x) ∧ (BetaAt(d,e,l,p) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = i → ¬y = l → BetaAt(b,c,y,z) → BetaAt(d,e,y,z)))Definitions: BetaAt(d,e,i,x)BetaAt(d,e,l,p)Lt(y,S l)BetaAt(b,c,y,z)BetaAt(d,e,y,z)Original native command in the exact edition - L18
specialize beta_prefix_swap_last_from_entries (b) - L19
specialize beta_prefix_swap_last_from_entries (c) - L20
specialize beta_prefix_swap_last_from_entries (l) - L21
specialize beta_prefix_swap_last_from_entries (i) - L22
specialize beta_prefix_swap_last_from_entries (p) - L23
specialize beta_prefix_swap_last_from_entries (x) - L24
apply beta_prefix_swap_last_from_entries - L25
exact hi - L26
exact hp
05Use earlier factsL27–27
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L27
exact hlast_witness
06Separate the logical casesL28–31
07Establish hsL32–32
Establish this local claim before using it. It is not an additional assumption.
- L32
have hs : BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,x) ∧ (BetaAt(x1,x2,i,x) ∧ (BetaAt(x1,x2,l,p) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = i → ¬y = l → BetaAt(b,c,y,z) → BetaAt(x1,x2,y,z)))))Definitions: BetaAt(b,c,i,p)BetaAt(b,c,l,x)BetaAt(x1,x2,i,x)BetaAt(x1,x2,l,p)Lt(y,S l)BetaAt(b,c,y,z)BetaAt(x1,x2,y,z)Original native command in the exact edition
08Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
split
09Use earlier factsL34–34
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L34
exact hp
10Separate the logical casesL35–35
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L35
split
11Use earlier factsL36–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
exact hlast_witness
12Separate the logical casesL37–37
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L37
split
13Use earlier factsL38–38
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L38
exact hnew_witness_witness_left
14Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
split
15Use earlier factsL40–41
16Establish hallnewL42–51
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor swap all irreducible.
- L42
have hallnew : GAllIrreducible(x1,x2,S l)Definitions: GAllIrreducible(x1,x2,S l)Original native command in the exact edition - L43
specialize gaussian_factor_swap_all_irreducible (b) - L44
specialize gaussian_factor_swap_all_irreducible (c) - L45
specialize gaussian_factor_swap_all_irreducible (x1) - L46
specialize gaussian_factor_swap_all_irreducible (x2) - L47
specialize gaussian_factor_swap_all_irreducible (l) - L48
specialize gaussian_factor_swap_all_irreducible (i) - L49
specialize gaussian_factor_swap_all_irreducible (p) - L50
specialize gaussian_factor_swap_all_irreducible (x) - L51
apply gaussian_factor_swap_all_irreducible
17Use earlier factsL52–54
18Establish hQL55–60
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian all irreducible product exists.
- L55
have hQ : ∃ Q. GProduct(x1,x2,S l,Q)Definitions: GProduct(x1,x2,S l,Q)Original native command in the exact edition - L56
specialize gaussian_all_irreducible_product_exists (S l) - L57
specialize gaussian_all_irreducible_product_exists (x1) - L58
specialize gaussian_all_irreducible_product_exists (x2) - L59
apply gaussian_all_irreducible_product_exists - L60
exact hallnew
19Separate the logical casesL61–61
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L61
cases hQ
20Establish heqL62–71
Establish this local claim before using it. It is not an additional assumption.
- L62
have heq : P=x3 - L63
specialize gaussian_product_swap_last_invariant (b) - L64
specialize gaussian_product_swap_last_invariant (c) - L65
specialize gaussian_product_swap_last_invariant (x1) - L66
specialize gaussian_product_swap_last_invariant (x2) - L67
specialize gaussian_product_swap_last_invariant (l) - L68
specialize gaussian_product_swap_last_invariant (i) - L69
specialize gaussian_product_swap_last_invariant (p) - L70
specialize gaussian_product_swap_last_invariant (x) - L71
specialize gaussian_product_swap_last_invariant (P)
21Use earlier factsL72–77
22Construct an explicit witnessL78–80
23Separate the logical casesL81–81
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L81
split
24Use earlier factsL82–82
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L82
exact hallnew
25Separate the logical casesL83–83
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L83
split
26Use earlier factsL84–89
Instantiate or apply named facts and discharge the corresponding proof obligations.
27Calculate and transport equalitiesL90–90
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L90
symm
Original defined command ledger · 93 lines
- 0001
intro b - 0002
intro c - 0003
intro l - 0004
intro i - 0005
intro p - 0006
intro P - 0007
intro hall - 0008
intro hP - 0009
intro hi - 0010
intro hp - 0011
have hlast : ∃ q. BetaAt(b,c,l,q) - 0012
specialize beta_at_exists (b) - 0013
specialize beta_at_exists (c) - 0014
specialize beta_at_exists (l) - 0015
apply beta_at_exists - 0016
cases hlast - 0017
have hnew : ∃ d. ∃ e. BetaAt(d,e,i,x) ∧ (BetaAt(d,e,l,p) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = i → ¬y = l → BetaAt(b,c,y,z) → BetaAt(d,e,y,z))) - 0018
specialize beta_prefix_swap_last_from_entries (b) - 0019
specialize beta_prefix_swap_last_from_entries (c) - 0020
specialize beta_prefix_swap_last_from_entries (l) - 0021
specialize beta_prefix_swap_last_from_entries (i) - 0022
specialize beta_prefix_swap_last_from_entries (p) - 0023
specialize beta_prefix_swap_last_from_entries (x) - 0024
apply beta_prefix_swap_last_from_entries - 0025
exact hi - 0026
exact hp - 0027
exact hlast_witness - 0028
cases hnew - 0029
cases hnew_witness - 0030
cases hnew_witness_witness - 0031
cases hnew_witness_witness_right - 0032
have hs : BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,x) ∧ (BetaAt(x1,x2,i,x) ∧ (BetaAt(x1,x2,l,p) ∧ (∀ y. ∀ z. Lt(y,S l) → ¬y = i → ¬y = l → BetaAt(b,c,y,z) → BetaAt(x1,x2,y,z))))) - 0033
split - 0034
exact hp - 0035
split - 0036
exact hlast_witness - 0037
split - 0038
exact hnew_witness_witness_left - 0039
split - 0040
exact hnew_witness_witness_right_left - 0041
exact hnew_witness_witness_right_right - 0042
have hallnew : GAllIrreducible(x1,x2,S l) - 0043
specialize gaussian_factor_swap_all_irreducible (b) - 0044
specialize gaussian_factor_swap_all_irreducible (c) - 0045
specialize gaussian_factor_swap_all_irreducible (x1) - 0046
specialize gaussian_factor_swap_all_irreducible (x2) - 0047
specialize gaussian_factor_swap_all_irreducible (l) - 0048
specialize gaussian_factor_swap_all_irreducible (i) - 0049
specialize gaussian_factor_swap_all_irreducible (p) - 0050
specialize gaussian_factor_swap_all_irreducible (x) - 0051
apply gaussian_factor_swap_all_irreducible - 0052
exact hi - 0053
exact hall - 0054
exact hs - 0055
have hQ : ∃ Q. GProduct(x1,x2,S l,Q) - 0056
specialize gaussian_all_irreducible_product_exists (S l) - 0057
specialize gaussian_all_irreducible_product_exists (x1) - 0058
specialize gaussian_all_irreducible_product_exists (x2) - 0059
apply gaussian_all_irreducible_product_exists - 0060
exact hallnew - 0061
cases hQ - 0062
have heq : P=x3 - 0063
specialize gaussian_product_swap_last_invariant (b) - 0064
specialize gaussian_product_swap_last_invariant (c) - 0065
specialize gaussian_product_swap_last_invariant (x1) - 0066
specialize gaussian_product_swap_last_invariant (x2) - 0067
specialize gaussian_product_swap_last_invariant (l) - 0068
specialize gaussian_product_swap_last_invariant (i) - 0069
specialize gaussian_product_swap_last_invariant (p) - 0070
specialize gaussian_product_swap_last_invariant (x) - 0071
specialize gaussian_product_swap_last_invariant (P) - 0072
specialize gaussian_product_swap_last_invariant (x3) - 0073
apply gaussian_product_swap_last_invariant - 0074
exact hi - 0075
exact hs - 0076
exact hP - 0077
exact hQ_witness - 0078
exists (x1) - 0079
exists (x2) - 0080
exists (x) - 0081
split - 0082
exact hallnew - 0083
split - 0084
specialize gaussian_product_value_transport (x1) - 0085
specialize gaussian_product_value_transport (x2) - 0086
specialize gaussian_product_value_transport (S l) - 0087
specialize gaussian_product_value_transport (x3) - 0088
specialize gaussian_product_value_transport (P) - 0089
apply gaussian_product_value_transport - 0090
symm - 0091
exact heq - 0092
exact hQ_witness - 0093
exact hs