Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ i. ∀ p. ∀ q. Lt(i,l) → GAllIrreducible(b,c,S l) → BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,q) ∧ (BetaAt(d,e,i,q) ∧ (BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))))) → GAllIrreducible(d,e,S l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
eq_decidable · checked external prerequisitebeta_at_unique · checked external prerequisitegaussian_product_beta_index_transportgaussian_irreducible_code_transportle_refl · checked external prerequisitele_succ · checked external prerequisitefactor_permutation_swap_reflect_unchanged · checked external prerequisite
Original expanded first-order statement
forall b c d e l i p q. (exists ge_gap_swap_irreducible_index. ge_gap_swap_irreducible_index + S (i) = (l)) -> (forall gr_factor_index_swap_irreducible_old gr_factor_value_swap_irreducible_old. (exists ge_gap_swap_irreducible_oldindex. ge_gap_swap_irreducible_oldindex + S (gr_factor_index_swap_irreducible_old) = (S l)) -> (((exists ff_h_gprod_swap_irreducible_oldentry. ff_h_gprod_swap_irreducible_oldentry + S (gr_factor_value_swap_irreducible_old) = S ((S (gr_factor_index_swap_irreducible_old)) * c)) /\ exists ff_q_gprod_swap_irreducible_oldentry. b = ff_q_gprod_swap_irreducible_oldentry * S ((S (gr_factor_index_swap_irreducible_old)) * c) + (gr_factor_value_swap_irreducible_old))) -> (((exists ge_real_positive_swap_irreducible_oldirreduciblecarrier ge_real_negative_swap_irreducible_oldirreduciblecarrier ge_imaginary_positive_swap_irreducible_oldirreduciblecarrier ge_imaginary_negative_swap_irreducible_oldirreduciblecarrier. (exists ge_real_code_swap_irreducible_oldirreduciblecarrierdecode ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode. (((gr_factor_value_swap_irreducible_old) = ((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode)) * S ((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_irreducible_oldirreduciblecarrier) /\ (ge_real_negative_swap_irreducible_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_real. (((ge_real_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_irreducible_oldirreduciblecarrier) = 0) /\ (ge_real_negative_swap_irreducible_oldirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_irreducible_oldirreduciblecarrier) /\ (ge_imaginary_negative_swap_irreducible_oldirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_irreducible_oldirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_irreducible_oldirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_irreducible_oldirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_oldirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_irreducible_old)=0)) /\ ((~(exists gr_inverse_swap_irreducible_oldirreduciblenonunit. (exists ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity ge_first_in_swap_irreducible_oldirreduciblenonunitidentity ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity ge_second_in_swap_irreducible_oldirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst. (((gr_factor_value_swap_irreducible_old) = ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond. (((gr_inverse_swap_irreducible_oldirreduciblenonunit) = ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_irreducible_oldirreducible gr_second_factor_swap_irreducible_oldirreducible. (exists ge_first_rp_swap_irreducible_oldirreduciblefactorization ge_first_rn_swap_irreducible_oldirreduciblefactorization ge_first_ip_swap_irreducible_oldirreduciblefactorization ge_first_in_swap_irreducible_oldirreduciblefactorization ge_second_rp_swap_irreducible_oldirreduciblefactorization ge_second_rn_swap_irreducible_oldirreduciblefactorization ge_second_ip_swap_irreducible_oldirreduciblefactorization ge_second_in_swap_irreducible_oldirreduciblefactorization. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst. (((gr_first_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond. (((gr_second_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondreal = (ge_second_rn_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblefactorization) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationsecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblefactorization) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput. (((gr_factor_value_swap_irreducible_old) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblefactorization) * (ge_second_in_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_oldirreduciblefactorization) * (ge_second_ip_swap_irreducible_oldirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefactorization) * (ge_second_rn_swap_irreducible_oldirreduciblefactorization))) + (((ge_first_in_swap_irreducible_oldirreduciblefactorization) * (ge_second_rp_swap_irreducible_oldirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_irreducible_oldirreduciblefirst_unit. (exists ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_irreducible_oldirreduciblefirst_unit) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_irreducible_oldirreduciblesecond_unit. (exists ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_irreducible_oldirreducible) = ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_irreducible_oldirreduciblesecond_unit) = ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_oldirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_oldirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_oldirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_oldirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_oldirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_oldirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) -> (((((exists ff_h_pfp_swap_irreducible_dataoldi. ff_h_pfp_swap_irreducible_dataoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_irreducible_dataoldi. b = ff_q_pfp_swap_irreducible_dataoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_irreducible_dataoldlast. ff_h_pfp_swap_irreducible_dataoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_irreducible_dataoldlast. b = ff_q_pfp_swap_irreducible_dataoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_irreducible_datanewi. ff_h_pfp_swap_irreducible_datanewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_irreducible_datanewi. d = ff_q_pfp_swap_irreducible_datanewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_irreducible_datanewlast. ff_h_pfp_swap_irreducible_datanewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_irreducible_datanewlast. d = ff_q_pfp_swap_irreducible_datanewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_irreducible_data pfp_a_swap_irreducible_data. (exists pfp_gap_swap_irreducible_databound. pfp_gap_swap_irreducible_databound + S (pfp_j_swap_irreducible_data) = (S (l))) -> ~(pfp_j_swap_irreducible_data = i) -> ~(pfp_j_swap_irreducible_data = l) -> (((exists ff_h_pfp_swap_irreducible_dataold. ff_h_pfp_swap_irreducible_dataold + S (pfp_a_swap_irreducible_data) = S ((S (pfp_j_swap_irreducible_data)) * c)) /\ exists ff_q_pfp_swap_irreducible_dataold. b = ff_q_pfp_swap_irreducible_dataold * S ((S (pfp_j_swap_irreducible_data)) * c) + (pfp_a_swap_irreducible_data))) -> (((exists ff_h_pfp_swap_irreducible_datanew. ff_h_pfp_swap_irreducible_datanew + S (pfp_a_swap_irreducible_data) = S ((S (pfp_j_swap_irreducible_data)) * e)) /\ exists ff_q_pfp_swap_irreducible_datanew. d = ff_q_pfp_swap_irreducible_datanew * S ((S (pfp_j_swap_irreducible_data)) * e) + (pfp_a_swap_irreducible_data)))))))))))) -> (forall gr_factor_index_swap_irreducible_new gr_factor_value_swap_irreducible_new. (exists ge_gap_swap_irreducible_newindex. ge_gap_swap_irreducible_newindex + S (gr_factor_index_swap_irreducible_new) = (S l)) -> (((exists ff_h_gprod_swap_irreducible_newentry. ff_h_gprod_swap_irreducible_newentry + S (gr_factor_value_swap_irreducible_new) = S ((S (gr_factor_index_swap_irreducible_new)) * e)) /\ exists ff_q_gprod_swap_irreducible_newentry. d = ff_q_gprod_swap_irreducible_newentry * S ((S (gr_factor_index_swap_irreducible_new)) * e) + (gr_factor_value_swap_irreducible_new))) -> (((exists ge_real_positive_swap_irreducible_newirreduciblecarrier ge_real_negative_swap_irreducible_newirreduciblecarrier ge_imaginary_positive_swap_irreducible_newirreduciblecarrier ge_imaginary_negative_swap_irreducible_newirreduciblecarrier. (exists ge_real_code_swap_irreducible_newirreduciblecarrierdecode ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode. (((gr_factor_value_swap_irreducible_new) = ((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode)) * S ((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode)) + ((ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode) + (ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode))) /\ (((((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * (ge_real_positive_swap_irreducible_newirreduciblecarrier) /\ (ge_real_negative_swap_irreducible_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_real. (((ge_real_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_swap_irreducible_newirreduciblecarrier) = 0) /\ (ge_real_negative_swap_irreducible_newirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_swap_irreducible_newirreduciblecarrier) /\ (ge_imaginary_negative_swap_irreducible_newirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_swap_irreducible_newirreduciblecarrierdecode) = 2 * ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_swap_irreducible_newirreduciblecarrier) = 0) /\ (ge_imaginary_negative_swap_irreducible_newirreduciblecarrier) = S ge_signed_half_ge_swap_irreducible_newirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_swap_irreducible_new)=0)) /\ ((~(exists gr_inverse_swap_irreducible_newirreduciblenonunit. (exists ge_first_rp_swap_irreducible_newirreduciblenonunitidentity ge_first_rn_swap_irreducible_newirreduciblenonunitidentity ge_first_ip_swap_irreducible_newirreduciblenonunitidentity ge_first_in_swap_irreducible_newirreduciblenonunitidentity ge_second_rp_swap_irreducible_newirreduciblenonunitidentity ge_second_rn_swap_irreducible_newirreduciblenonunitidentity ge_second_ip_swap_irreducible_newirreduciblenonunitidentity ge_second_in_swap_irreducible_newirreduciblenonunitidentity. ((exists ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst. (((gr_factor_value_swap_irreducible_new) = ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstreal = (ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond. (((gr_inverse_swap_irreducible_newirreduciblenonunit) = ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondreal = (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentitysecondimaginary = (ge_second_in_swap_irreducible_newirreduciblenonunitidentity) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblenonunitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_in_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_ip_swap_irreducible_newirreduciblenonunitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rn_swap_irreducible_newirreduciblenonunitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblenonunitidentity) * (ge_second_rp_swap_irreducible_newirreduciblenonunitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_swap_irreducible_newirreducible gr_second_factor_swap_irreducible_newirreducible. (exists ge_first_rp_swap_irreducible_newirreduciblefactorization ge_first_rn_swap_irreducible_newirreduciblefactorization ge_first_ip_swap_irreducible_newirreduciblefactorization ge_first_in_swap_irreducible_newirreduciblefactorization ge_second_rp_swap_irreducible_newirreduciblefactorization ge_second_rn_swap_irreducible_newirreduciblefactorization ge_second_ip_swap_irreducible_newirreduciblefactorization ge_second_in_swap_irreducible_newirreduciblefactorization. ((exists ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst. (((gr_first_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstreal = (ge_first_rn_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond. (((gr_second_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondreal = (ge_second_rn_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationsecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblefactorization) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationsecondimaginary = (ge_second_in_swap_irreducible_newirreduciblefactorization) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput. (((gr_factor_value_swap_irreducible_new) = ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefactorizationoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_negative_swap_irreducible_newirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblefactorization) * (ge_second_in_swap_irreducible_newirreduciblefactorization))) + (((ge_first_rn_swap_irreducible_newirreduciblefactorization) * (ge_second_ip_swap_irreducible_newirreduciblefactorization))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefactorization) * (ge_second_rn_swap_irreducible_newirreduciblefactorization))) + (((ge_first_in_swap_irreducible_newirreduciblefactorization) * (ge_second_rp_swap_irreducible_newirreduciblefactorization))))))) + ge_balance_positive_swap_irreducible_newirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_swap_irreducible_newirreduciblefirst_unit. (exists ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity. ((exists ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst. (((gr_first_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstreal = (ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond. (((gr_inverse_swap_irreducible_newirreduciblefirst_unit) = ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondreal = (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblefirst_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblefirst_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblefirst_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblefirst_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_swap_irreducible_newirreduciblesecond_unit. (exists ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity. ((exists ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst. (((gr_second_factor_swap_irreducible_newirreducible) = ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstreal = (ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond. (((gr_inverse_swap_irreducible_newirreduciblesecond_unit) = ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondreal = (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_swap_irreducible_newirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_negative_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_in_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_rn_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_ip_swap_irreducible_newirreduciblesecond_unitidentity))))) + (((((ge_first_ip_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rn_swap_irreducible_newirreduciblesecond_unitidentity))) + (((ge_first_in_swap_irreducible_newirreduciblesecond_unitidentity) * (ge_second_rp_swap_irreducible_newirreduciblesecond_unitidentity))))))) + ge_balance_positive_swap_irreducible_newirreduciblesecond_unitidentityoutputimaginary))))))))))))))))Complete tactic proof in conservative notation
All 103 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
103 script commands · 16 reading checkpoints · 4 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro hs
03Separate the logical casesL12–15
04Fix variables and assumptionsL16–19
05Establish hkiL20–23
06Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
cases hki
07Establish heqL25–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
- L25
have heq : q=a - L26
specialize beta_at_unique (d) - L27
specialize beta_at_unique (e) - L28
specialize beta_at_unique (i) - L29
specialize beta_at_unique (q) - L30
specialize beta_at_unique (a) - L31
apply beta_at_unique - L32
exact hs_right_right_left - L33
specialize gaussian_product_beta_index_transport (d) - L34
specialize gaussian_product_beta_index_transport (e)
08Use earlier factsL35–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L35
specialize gaussian_product_beta_index_transport (k) - L36
specialize gaussian_product_beta_index_transport (i) - L37
specialize gaussian_product_beta_index_transport (a) - L38
apply gaussian_product_beta_index_transport - L39
exact hki_left - L40
exact ha - L41
specialize gaussian_irreducible_code_transport (q) - L42
specialize gaussian_irreducible_code_transport (a) - L43
apply gaussian_irreducible_code_transport - L44
exact heq
09Use earlier factsL45–50
10Establish hklL51–54
11Separate the logical casesL55–55
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L55
cases hkl
12Establish heqL56–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
- L56
have heq : p=a - L57
specialize beta_at_unique (d) - L58
specialize beta_at_unique (e) - L59
specialize beta_at_unique (l) - L60
specialize beta_at_unique (p) - L61
specialize beta_at_unique (a) - L62
apply beta_at_unique - L63
exact hs_right_right_right_left - L64
specialize gaussian_product_beta_index_transport (d) - L65
specialize gaussian_product_beta_index_transport (e)
13Use earlier factsL66–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L66
specialize gaussian_product_beta_index_transport (k) - L67
specialize gaussian_product_beta_index_transport (l) - L68
specialize gaussian_product_beta_index_transport (a) - L69
apply gaussian_product_beta_index_transport - L70
exact hkl_left - L71
exact ha - L72
specialize gaussian_irreducible_code_transport (p) - L73
specialize gaussian_irreducible_code_transport (a) - L74
apply gaussian_irreducible_code_transport - L75
exact heq
14Use earlier factsL76–85
15Use earlier factsL86–95
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L86
apply hall - L87
exact hk - L88
specialize factor_permutation_swap_reflect_unchanged (b) - L89
specialize factor_permutation_swap_reflect_unchanged (c) - L90
specialize factor_permutation_swap_reflect_unchanged (d) - L91
specialize factor_permutation_swap_reflect_unchanged (e) - L92
specialize factor_permutation_swap_reflect_unchanged (l) - L93
specialize factor_permutation_swap_reflect_unchanged (i) - L94
specialize factor_permutation_swap_reflect_unchanged (p) - L95
specialize factor_permutation_swap_reflect_unchanged (q)
16Use earlier factsL96–103
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 103 lines
- 0001
intro b - 0002
intro c - 0003
intro d - 0004
intro e - 0005
intro l - 0006
intro i - 0007
intro p - 0008
intro q - 0009
intro hi - 0010
intro hall - 0011
intro hs - 0012
cases hs - 0013
cases hs_right - 0014
cases hs_right_right - 0015
cases hs_right_right_right - 0016
intro k - 0017
intro a - 0018
intro hk - 0019
intro ha - 0020
have hki : k=i \/ ~(k=i) - 0021
specialize eq_decidable (k) - 0022
specialize eq_decidable (i) - 0023
apply eq_decidable - 0024
cases hki - 0025
have heq : q=a - 0026
specialize beta_at_unique (d) - 0027
specialize beta_at_unique (e) - 0028
specialize beta_at_unique (i) - 0029
specialize beta_at_unique (q) - 0030
specialize beta_at_unique (a) - 0031
apply beta_at_unique - 0032
exact hs_right_right_left - 0033
specialize gaussian_product_beta_index_transport (d) - 0034
specialize gaussian_product_beta_index_transport (e) - 0035
specialize gaussian_product_beta_index_transport (k) - 0036
specialize gaussian_product_beta_index_transport (i) - 0037
specialize gaussian_product_beta_index_transport (a) - 0038
apply gaussian_product_beta_index_transport - 0039
exact hki_left - 0040
exact ha - 0041
specialize gaussian_irreducible_code_transport (q) - 0042
specialize gaussian_irreducible_code_transport (a) - 0043
apply gaussian_irreducible_code_transport - 0044
exact heq - 0045
specialize hall (l) - 0046
specialize hall (q) - 0047
apply hall - 0048
specialize le_refl (S l) - 0049
apply le_refl - 0050
exact hs_right_left - 0051
have hkl : k=l \/ ~(k=l) - 0052
specialize eq_decidable (k) - 0053
specialize eq_decidable (l) - 0054
apply eq_decidable - 0055
cases hkl - 0056
have heq : p=a - 0057
specialize beta_at_unique (d) - 0058
specialize beta_at_unique (e) - 0059
specialize beta_at_unique (l) - 0060
specialize beta_at_unique (p) - 0061
specialize beta_at_unique (a) - 0062
apply beta_at_unique - 0063
exact hs_right_right_right_left - 0064
specialize gaussian_product_beta_index_transport (d) - 0065
specialize gaussian_product_beta_index_transport (e) - 0066
specialize gaussian_product_beta_index_transport (k) - 0067
specialize gaussian_product_beta_index_transport (l) - 0068
specialize gaussian_product_beta_index_transport (a) - 0069
apply gaussian_product_beta_index_transport - 0070
exact hkl_left - 0071
exact ha - 0072
specialize gaussian_irreducible_code_transport (p) - 0073
specialize gaussian_irreducible_code_transport (a) - 0074
apply gaussian_irreducible_code_transport - 0075
exact heq - 0076
specialize hall (i) - 0077
specialize hall (p) - 0078
apply hall - 0079
specialize le_succ (S i) - 0080
specialize le_succ (l) - 0081
apply le_succ - 0082
exact hi - 0083
exact hs_left - 0084
specialize hall (k) - 0085
specialize hall (a) - 0086
apply hall - 0087
exact hk - 0088
specialize factor_permutation_swap_reflect_unchanged (b) - 0089
specialize factor_permutation_swap_reflect_unchanged (c) - 0090
specialize factor_permutation_swap_reflect_unchanged (d) - 0091
specialize factor_permutation_swap_reflect_unchanged (e) - 0092
specialize factor_permutation_swap_reflect_unchanged (l) - 0093
specialize factor_permutation_swap_reflect_unchanged (i) - 0094
specialize factor_permutation_swap_reflect_unchanged (p) - 0095
specialize factor_permutation_swap_reflect_unchanged (q) - 0096
specialize factor_permutation_swap_reflect_unchanged (k) - 0097
specialize factor_permutation_swap_reflect_unchanged (a) - 0098
apply factor_permutation_swap_reflect_unchanged - 0099
exact hs - 0100
exact hk - 0101
exact hki_right - 0102
exact hkl_right - 0103
exact ha