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
∀ p. ∀ q. p = q → GIrreducible(p) → GIrreducible(q)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall p q. p=q -> (((exists ge_real_positive_irreducible_transport_sourcecarrier ge_real_negative_irreducible_transport_sourcecarrier ge_imaginary_positive_irreducible_transport_sourcecarrier ge_imaginary_negative_irreducible_transport_sourcecarrier. (exists ge_real_code_irreducible_transport_sourcecarrierdecode ge_imaginary_code_irreducible_transport_sourcecarrierdecode. (((p) = ((ge_real_code_irreducible_transport_sourcecarrierdecode) + (ge_imaginary_code_irreducible_transport_sourcecarrierdecode)) * S ((ge_real_code_irreducible_transport_sourcecarrierdecode) + (ge_imaginary_code_irreducible_transport_sourcecarrierdecode)) + ((ge_imaginary_code_irreducible_transport_sourcecarrierdecode) + (ge_imaginary_code_irreducible_transport_sourcecarrierdecode))) /\ (((((ge_real_code_irreducible_transport_sourcecarrierdecode) = 2 * (ge_real_positive_irreducible_transport_sourcecarrier) /\ (ge_real_negative_irreducible_transport_sourcecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_transport_sourcecarrierdecode_real. (((ge_real_code_irreducible_transport_sourcecarrierdecode) = 2 * ge_signed_half_ge_irreducible_transport_sourcecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_transport_sourcecarrier) = 0) /\ (ge_real_negative_irreducible_transport_sourcecarrier) = S ge_signed_half_ge_irreducible_transport_sourcecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_transport_sourcecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_transport_sourcecarrier) /\ (ge_imaginary_negative_irreducible_transport_sourcecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_transport_sourcecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_transport_sourcecarrierdecode) = 2 * ge_signed_half_ge_irreducible_transport_sourcecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_transport_sourcecarrier) = 0) /\ (ge_imaginary_negative_irreducible_transport_sourcecarrier) = S ge_signed_half_ge_irreducible_transport_sourcecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_irreducible_transport_sourcenonunit. (exists ge_first_rp_irreducible_transport_sourcenonunitidentity ge_first_rn_irreducible_transport_sourcenonunitidentity ge_first_ip_irreducible_transport_sourcenonunitidentity ge_first_in_irreducible_transport_sourcenonunitidentity ge_second_rp_irreducible_transport_sourcenonunitidentity ge_second_rn_irreducible_transport_sourcenonunitidentity ge_second_ip_irreducible_transport_sourcenonunitidentity ge_second_in_irreducible_transport_sourcenonunitidentity. ((exists ge_representation_real_code_irreducible_transport_sourcenonunitidentityfirst ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_transport_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_transport_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstreal ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_transport_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_transport_sourcenonunitidentityfirst) = 2 * ge_signed_half_irreducible_transport_sourcenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstreal) = S ge_signed_half_irreducible_transport_sourcenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_sourcenonunitidentity) + ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstreal = (ge_first_rn_irreducible_transport_sourcenonunitidentity) + ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstimaginary ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityfirst) = 2 * ge_signed_half_irreducible_transport_sourcenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_transport_sourcenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_sourcenonunitidentity) + ge_balance_negative_irreducible_transport_sourcenonunitidentityfirstimaginary = (ge_first_in_irreducible_transport_sourcenonunitidentity) + ge_balance_positive_irreducible_transport_sourcenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_sourcenonunitidentitysecond ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond. (((gr_inverse_irreducible_transport_sourcenonunit) = ((ge_representation_real_code_irreducible_transport_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_transport_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondreal ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_transport_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_transport_sourcenonunitidentitysecond) = 2 * ge_signed_half_irreducible_transport_sourcenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondreal) = S ge_signed_half_irreducible_transport_sourcenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_sourcenonunitidentity) + ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondreal = (ge_second_rn_irreducible_transport_sourcenonunitidentity) + ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondimaginary ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentitysecond) = 2 * ge_signed_half_irreducible_transport_sourcenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_transport_sourcenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_sourcenonunitidentity) + ge_balance_negative_irreducible_transport_sourcenonunitidentitysecondimaginary = (ge_second_in_irreducible_transport_sourcenonunitidentity) + ge_balance_positive_irreducible_transport_sourcenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_sourcenonunitidentityoutput ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_transport_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_transport_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputreal ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_transport_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_transport_sourcenonunitidentityoutput) = 2 * ge_signed_half_irreducible_transport_sourcenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputreal) = S ge_signed_half_irreducible_transport_sourcenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcenonunitidentity) * (ge_second_rp_irreducible_transport_sourcenonunitidentity))) + (((ge_first_rn_irreducible_transport_sourcenonunitidentity) * (ge_second_rn_irreducible_transport_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcenonunitidentity) * (ge_second_in_irreducible_transport_sourcenonunitidentity))) + (((ge_first_in_irreducible_transport_sourcenonunitidentity) * (ge_second_ip_irreducible_transport_sourcenonunitidentity))))))) + ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_transport_sourcenonunitidentity) * (ge_second_rn_irreducible_transport_sourcenonunitidentity))) + (((ge_first_rn_irreducible_transport_sourcenonunitidentity) * (ge_second_rp_irreducible_transport_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcenonunitidentity) * (ge_second_ip_irreducible_transport_sourcenonunitidentity))) + (((ge_first_in_irreducible_transport_sourcenonunitidentity) * (ge_second_in_irreducible_transport_sourcenonunitidentity))))))) + ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputimaginary ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcenonunitidentityoutput) = 2 * ge_signed_half_irreducible_transport_sourcenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_transport_sourcenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcenonunitidentity) * (ge_second_ip_irreducible_transport_sourcenonunitidentity))) + (((ge_first_rn_irreducible_transport_sourcenonunitidentity) * (ge_second_in_irreducible_transport_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcenonunitidentity) * (ge_second_rp_irreducible_transport_sourcenonunitidentity))) + (((ge_first_in_irreducible_transport_sourcenonunitidentity) * (ge_second_rn_irreducible_transport_sourcenonunitidentity))))))) + ge_balance_negative_irreducible_transport_sourcenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_transport_sourcenonunitidentity) * (ge_second_in_irreducible_transport_sourcenonunitidentity))) + (((ge_first_rn_irreducible_transport_sourcenonunitidentity) * (ge_second_ip_irreducible_transport_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcenonunitidentity) * (ge_second_rn_irreducible_transport_sourcenonunitidentity))) + (((ge_first_in_irreducible_transport_sourcenonunitidentity) * (ge_second_rp_irreducible_transport_sourcenonunitidentity))))))) + ge_balance_positive_irreducible_transport_sourcenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_transport_source gr_second_factor_irreducible_transport_source. (exists ge_first_rp_irreducible_transport_sourcefactorization ge_first_rn_irreducible_transport_sourcefactorization ge_first_ip_irreducible_transport_sourcefactorization ge_first_in_irreducible_transport_sourcefactorization ge_second_rp_irreducible_transport_sourcefactorization ge_second_rn_irreducible_transport_sourcefactorization ge_second_ip_irreducible_transport_sourcefactorization ge_second_in_irreducible_transport_sourcefactorization. ((exists ge_representation_real_code_irreducible_transport_sourcefactorizationfirst ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst. (((gr_first_factor_irreducible_transport_source) = ((ge_representation_real_code_irreducible_transport_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst)) * S ((ge_representation_real_code_irreducible_transport_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_transport_sourcefactorizationfirstreal ge_balance_negative_irreducible_transport_sourcefactorizationfirstreal. (((((ge_representation_real_code_irreducible_transport_sourcefactorizationfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcefactorizationfirstreal) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_transport_sourcefactorizationfirst) = 2 * ge_signed_half_irreducible_transport_sourcefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationfirstreal) = S ge_signed_half_irreducible_transport_sourcefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_sourcefactorization) + ge_balance_negative_irreducible_transport_sourcefactorizationfirstreal = (ge_first_rn_irreducible_transport_sourcefactorization) + ge_balance_positive_irreducible_transport_sourcefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcefactorizationfirstimaginary ge_balance_negative_irreducible_transport_sourcefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationfirst) = 2 * ge_signed_half_irreducible_transport_sourcefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationfirstimaginary) = S ge_signed_half_irreducible_transport_sourcefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_sourcefactorization) + ge_balance_negative_irreducible_transport_sourcefactorizationfirstimaginary = (ge_first_in_irreducible_transport_sourcefactorization) + ge_balance_positive_irreducible_transport_sourcefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_sourcefactorizationsecond ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond. (((gr_second_factor_irreducible_transport_source) = ((ge_representation_real_code_irreducible_transport_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond)) * S ((ge_representation_real_code_irreducible_transport_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_transport_sourcefactorizationsecondreal ge_balance_negative_irreducible_transport_sourcefactorizationsecondreal. (((((ge_representation_real_code_irreducible_transport_sourcefactorizationsecond) = 2 * (ge_balance_positive_irreducible_transport_sourcefactorizationsecondreal) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_transport_sourcefactorizationsecond) = 2 * ge_signed_half_irreducible_transport_sourcefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationsecondreal) = S ge_signed_half_irreducible_transport_sourcefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_sourcefactorization) + ge_balance_negative_irreducible_transport_sourcefactorizationsecondreal = (ge_second_rn_irreducible_transport_sourcefactorization) + ge_balance_positive_irreducible_transport_sourcefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcefactorizationsecondimaginary ge_balance_negative_irreducible_transport_sourcefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond) = 2 * (ge_balance_positive_irreducible_transport_sourcefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationsecond) = 2 * ge_signed_half_irreducible_transport_sourcefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationsecondimaginary) = S ge_signed_half_irreducible_transport_sourcefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_sourcefactorization) + ge_balance_negative_irreducible_transport_sourcefactorizationsecondimaginary = (ge_second_in_irreducible_transport_sourcefactorization) + ge_balance_positive_irreducible_transport_sourcefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_sourcefactorizationoutput ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput. (((p) = ((ge_representation_real_code_irreducible_transport_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput)) * S ((ge_representation_real_code_irreducible_transport_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_transport_sourcefactorizationoutputreal ge_balance_negative_irreducible_transport_sourcefactorizationoutputreal. (((((ge_representation_real_code_irreducible_transport_sourcefactorizationoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcefactorizationoutputreal) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_transport_sourcefactorizationoutput) = 2 * ge_signed_half_irreducible_transport_sourcefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationoutputreal) = S ge_signed_half_irreducible_transport_sourcefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcefactorization) * (ge_second_rp_irreducible_transport_sourcefactorization))) + (((ge_first_rn_irreducible_transport_sourcefactorization) * (ge_second_rn_irreducible_transport_sourcefactorization))))) + (((((ge_first_ip_irreducible_transport_sourcefactorization) * (ge_second_in_irreducible_transport_sourcefactorization))) + (((ge_first_in_irreducible_transport_sourcefactorization) * (ge_second_ip_irreducible_transport_sourcefactorization))))))) + ge_balance_negative_irreducible_transport_sourcefactorizationoutputreal = (((((((ge_first_rp_irreducible_transport_sourcefactorization) * (ge_second_rn_irreducible_transport_sourcefactorization))) + (((ge_first_rn_irreducible_transport_sourcefactorization) * (ge_second_rp_irreducible_transport_sourcefactorization))))) + (((((ge_first_ip_irreducible_transport_sourcefactorization) * (ge_second_ip_irreducible_transport_sourcefactorization))) + (((ge_first_in_irreducible_transport_sourcefactorization) * (ge_second_in_irreducible_transport_sourcefactorization))))))) + ge_balance_positive_irreducible_transport_sourcefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcefactorizationoutputimaginary ge_balance_negative_irreducible_transport_sourcefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcefactorizationoutput) = 2 * ge_signed_half_irreducible_transport_sourcefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefactorizationoutputimaginary) = S ge_signed_half_irreducible_transport_sourcefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcefactorization) * (ge_second_ip_irreducible_transport_sourcefactorization))) + (((ge_first_rn_irreducible_transport_sourcefactorization) * (ge_second_in_irreducible_transport_sourcefactorization))))) + (((((ge_first_ip_irreducible_transport_sourcefactorization) * (ge_second_rp_irreducible_transport_sourcefactorization))) + (((ge_first_in_irreducible_transport_sourcefactorization) * (ge_second_rn_irreducible_transport_sourcefactorization))))))) + ge_balance_negative_irreducible_transport_sourcefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_transport_sourcefactorization) * (ge_second_in_irreducible_transport_sourcefactorization))) + (((ge_first_rn_irreducible_transport_sourcefactorization) * (ge_second_ip_irreducible_transport_sourcefactorization))))) + (((((ge_first_ip_irreducible_transport_sourcefactorization) * (ge_second_rn_irreducible_transport_sourcefactorization))) + (((ge_first_in_irreducible_transport_sourcefactorization) * (ge_second_rp_irreducible_transport_sourcefactorization))))))) + ge_balance_positive_irreducible_transport_sourcefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_transport_sourcefirst_unit. (exists ge_first_rp_irreducible_transport_sourcefirst_unitidentity ge_first_rn_irreducible_transport_sourcefirst_unitidentity ge_first_ip_irreducible_transport_sourcefirst_unitidentity ge_first_in_irreducible_transport_sourcefirst_unitidentity ge_second_rp_irreducible_transport_sourcefirst_unitidentity ge_second_rn_irreducible_transport_sourcefirst_unitidentity ge_second_ip_irreducible_transport_sourcefirst_unitidentity ge_second_in_irreducible_transport_sourcefirst_unitidentity. ((exists ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst. (((gr_first_factor_irreducible_transport_source) = ((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstreal ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_sourcefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_transport_sourcefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_sourcefirst_unitidentity) + ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstreal = (ge_first_rn_irreducible_transport_sourcefirst_unitidentity) + ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_sourcefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_transport_sourcefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_sourcefirst_unitidentity) + ge_balance_negative_irreducible_transport_sourcefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_transport_sourcefirst_unitidentity) + ge_balance_positive_irreducible_transport_sourcefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_sourcefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond. (((gr_inverse_irreducible_transport_sourcefirst_unit) = ((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondreal ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_sourcefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_transport_sourcefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_sourcefirst_unitidentity) + ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondreal = (ge_second_rn_irreducible_transport_sourcefirst_unitidentity) + ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_sourcefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_transport_sourcefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_sourcefirst_unitidentity) + ge_balance_negative_irreducible_transport_sourcefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_transport_sourcefirst_unitidentity) + ge_balance_positive_irreducible_transport_sourcefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputreal ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_transport_sourcefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_sourcefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_transport_sourcefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rp_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rn_irreducible_transport_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcefirst_unitidentity) * (ge_second_in_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_transport_sourcefirst_unitidentity) * (ge_second_ip_irreducible_transport_sourcefirst_unitidentity))))))) + ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rn_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rp_irreducible_transport_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcefirst_unitidentity) * (ge_second_ip_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_transport_sourcefirst_unitidentity) * (ge_second_in_irreducible_transport_sourcefirst_unitidentity))))))) + ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_sourcefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_transport_sourcefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcefirst_unitidentity) * (ge_second_ip_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcefirst_unitidentity) * (ge_second_in_irreducible_transport_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rp_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rn_irreducible_transport_sourcefirst_unitidentity))))))) + ge_balance_negative_irreducible_transport_sourcefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_transport_sourcefirst_unitidentity) * (ge_second_in_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcefirst_unitidentity) * (ge_second_ip_irreducible_transport_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rn_irreducible_transport_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_transport_sourcefirst_unitidentity) * (ge_second_rp_irreducible_transport_sourcefirst_unitidentity))))))) + ge_balance_positive_irreducible_transport_sourcefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_transport_sourcesecond_unit. (exists ge_first_rp_irreducible_transport_sourcesecond_unitidentity ge_first_rn_irreducible_transport_sourcesecond_unitidentity ge_first_ip_irreducible_transport_sourcesecond_unitidentity ge_first_in_irreducible_transport_sourcesecond_unitidentity ge_second_rp_irreducible_transport_sourcesecond_unitidentity ge_second_rn_irreducible_transport_sourcesecond_unitidentity ge_second_ip_irreducible_transport_sourcesecond_unitidentity ge_second_in_irreducible_transport_sourcesecond_unitidentity. ((exists ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst. (((gr_second_factor_irreducible_transport_source) = ((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstreal ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_sourcesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_transport_sourcesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_sourcesecond_unitidentity) + ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstreal = (ge_first_rn_irreducible_transport_sourcesecond_unitidentity) + ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_sourcesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_transport_sourcesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_sourcesecond_unitidentity) + ge_balance_negative_irreducible_transport_sourcesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_transport_sourcesecond_unitidentity) + ge_balance_positive_irreducible_transport_sourcesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_sourcesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond. (((gr_inverse_irreducible_transport_sourcesecond_unit) = ((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondreal ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_sourcesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_transport_sourcesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_sourcesecond_unitidentity) + ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondreal = (ge_second_rn_irreducible_transport_sourcesecond_unitidentity) + ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_sourcesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_transport_sourcesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_sourcesecond_unitidentity) + ge_balance_negative_irreducible_transport_sourcesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_transport_sourcesecond_unitidentity) + ge_balance_positive_irreducible_transport_sourcesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputreal ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_sourcesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_transport_sourcesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_sourcesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_transport_sourcesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rp_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rn_irreducible_transport_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcesecond_unitidentity) * (ge_second_in_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_transport_sourcesecond_unitidentity) * (ge_second_ip_irreducible_transport_sourcesecond_unitidentity))))))) + ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rn_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rp_irreducible_transport_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcesecond_unitidentity) * (ge_second_ip_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_transport_sourcesecond_unitidentity) * (ge_second_in_irreducible_transport_sourcesecond_unitidentity))))))) + ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_sourcesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_sourcesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_sourcesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_transport_sourcesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_sourcesecond_unitidentity) * (ge_second_ip_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcesecond_unitidentity) * (ge_second_in_irreducible_transport_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rp_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rn_irreducible_transport_sourcesecond_unitidentity))))))) + ge_balance_negative_irreducible_transport_sourcesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_transport_sourcesecond_unitidentity) * (ge_second_in_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_transport_sourcesecond_unitidentity) * (ge_second_ip_irreducible_transport_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rn_irreducible_transport_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_transport_sourcesecond_unitidentity) * (ge_second_rp_irreducible_transport_sourcesecond_unitidentity))))))) + ge_balance_positive_irreducible_transport_sourcesecond_unitidentityoutputimaginary))))))))))))))) -> (((exists ge_real_positive_irreducible_transport_targetcarrier ge_real_negative_irreducible_transport_targetcarrier ge_imaginary_positive_irreducible_transport_targetcarrier ge_imaginary_negative_irreducible_transport_targetcarrier. (exists ge_real_code_irreducible_transport_targetcarrierdecode ge_imaginary_code_irreducible_transport_targetcarrierdecode. (((q) = ((ge_real_code_irreducible_transport_targetcarrierdecode) + (ge_imaginary_code_irreducible_transport_targetcarrierdecode)) * S ((ge_real_code_irreducible_transport_targetcarrierdecode) + (ge_imaginary_code_irreducible_transport_targetcarrierdecode)) + ((ge_imaginary_code_irreducible_transport_targetcarrierdecode) + (ge_imaginary_code_irreducible_transport_targetcarrierdecode))) /\ (((((ge_real_code_irreducible_transport_targetcarrierdecode) = 2 * (ge_real_positive_irreducible_transport_targetcarrier) /\ (ge_real_negative_irreducible_transport_targetcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_transport_targetcarrierdecode_real. (((ge_real_code_irreducible_transport_targetcarrierdecode) = 2 * ge_signed_half_ge_irreducible_transport_targetcarrierdecode_real + 1 /\ (ge_real_positive_irreducible_transport_targetcarrier) = 0) /\ (ge_real_negative_irreducible_transport_targetcarrier) = S ge_signed_half_ge_irreducible_transport_targetcarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_transport_targetcarrierdecode) = 2 * (ge_imaginary_positive_irreducible_transport_targetcarrier) /\ (ge_imaginary_negative_irreducible_transport_targetcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_transport_targetcarrierdecode_imaginary. (((ge_imaginary_code_irreducible_transport_targetcarrierdecode) = 2 * ge_signed_half_ge_irreducible_transport_targetcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_transport_targetcarrier) = 0) /\ (ge_imaginary_negative_irreducible_transport_targetcarrier) = S ge_signed_half_ge_irreducible_transport_targetcarrierdecode_imaginary))))))) /\ ((~((q)=0)) /\ ((~(exists gr_inverse_irreducible_transport_targetnonunit. (exists ge_first_rp_irreducible_transport_targetnonunitidentity ge_first_rn_irreducible_transport_targetnonunitidentity ge_first_ip_irreducible_transport_targetnonunitidentity ge_first_in_irreducible_transport_targetnonunitidentity ge_second_rp_irreducible_transport_targetnonunitidentity ge_second_rn_irreducible_transport_targetnonunitidentity ge_second_ip_irreducible_transport_targetnonunitidentity ge_second_in_irreducible_transport_targetnonunitidentity. ((exists ge_representation_real_code_irreducible_transport_targetnonunitidentityfirst ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst. (((q) = ((ge_representation_real_code_irreducible_transport_targetnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_transport_targetnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_transport_targetnonunitidentityfirstreal ge_balance_negative_irreducible_transport_targetnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_transport_targetnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_targetnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_transport_targetnonunitidentityfirst) = 2 * ge_signed_half_irreducible_transport_targetnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityfirstreal) = S ge_signed_half_irreducible_transport_targetnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_targetnonunitidentity) + ge_balance_negative_irreducible_transport_targetnonunitidentityfirstreal = (ge_first_rn_irreducible_transport_targetnonunitidentity) + ge_balance_positive_irreducible_transport_targetnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_targetnonunitidentityfirstimaginary ge_balance_negative_irreducible_transport_targetnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_targetnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityfirst) = 2 * ge_signed_half_irreducible_transport_targetnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_transport_targetnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_targetnonunitidentity) + ge_balance_negative_irreducible_transport_targetnonunitidentityfirstimaginary = (ge_first_in_irreducible_transport_targetnonunitidentity) + ge_balance_positive_irreducible_transport_targetnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_targetnonunitidentitysecond ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond. (((gr_inverse_irreducible_transport_targetnonunit) = ((ge_representation_real_code_irreducible_transport_targetnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_transport_targetnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_transport_targetnonunitidentitysecondreal ge_balance_negative_irreducible_transport_targetnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_transport_targetnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_targetnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_transport_targetnonunitidentitysecond) = 2 * ge_signed_half_irreducible_transport_targetnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentitysecondreal) = S ge_signed_half_irreducible_transport_targetnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_targetnonunitidentity) + ge_balance_negative_irreducible_transport_targetnonunitidentitysecondreal = (ge_second_rn_irreducible_transport_targetnonunitidentity) + ge_balance_positive_irreducible_transport_targetnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_transport_targetnonunitidentitysecondimaginary ge_balance_negative_irreducible_transport_targetnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_targetnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentitysecond) = 2 * ge_signed_half_irreducible_transport_targetnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_transport_targetnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_targetnonunitidentity) + ge_balance_negative_irreducible_transport_targetnonunitidentitysecondimaginary = (ge_second_in_irreducible_transport_targetnonunitidentity) + ge_balance_positive_irreducible_transport_targetnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_targetnonunitidentityoutput ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_transport_targetnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_transport_targetnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_transport_targetnonunitidentityoutputreal ge_balance_negative_irreducible_transport_targetnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_transport_targetnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_targetnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_transport_targetnonunitidentityoutput) = 2 * ge_signed_half_irreducible_transport_targetnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityoutputreal) = S ge_signed_half_irreducible_transport_targetnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetnonunitidentity) * (ge_second_rp_irreducible_transport_targetnonunitidentity))) + (((ge_first_rn_irreducible_transport_targetnonunitidentity) * (ge_second_rn_irreducible_transport_targetnonunitidentity))))) + (((((ge_first_ip_irreducible_transport_targetnonunitidentity) * (ge_second_in_irreducible_transport_targetnonunitidentity))) + (((ge_first_in_irreducible_transport_targetnonunitidentity) * (ge_second_ip_irreducible_transport_targetnonunitidentity))))))) + ge_balance_negative_irreducible_transport_targetnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_transport_targetnonunitidentity) * (ge_second_rn_irreducible_transport_targetnonunitidentity))) + (((ge_first_rn_irreducible_transport_targetnonunitidentity) * (ge_second_rp_irreducible_transport_targetnonunitidentity))))) + (((((ge_first_ip_irreducible_transport_targetnonunitidentity) * (ge_second_ip_irreducible_transport_targetnonunitidentity))) + (((ge_first_in_irreducible_transport_targetnonunitidentity) * (ge_second_in_irreducible_transport_targetnonunitidentity))))))) + ge_balance_positive_irreducible_transport_targetnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_targetnonunitidentityoutputimaginary ge_balance_negative_irreducible_transport_targetnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_targetnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetnonunitidentityoutput) = 2 * ge_signed_half_irreducible_transport_targetnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_transport_targetnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetnonunitidentity) * (ge_second_ip_irreducible_transport_targetnonunitidentity))) + (((ge_first_rn_irreducible_transport_targetnonunitidentity) * (ge_second_in_irreducible_transport_targetnonunitidentity))))) + (((((ge_first_ip_irreducible_transport_targetnonunitidentity) * (ge_second_rp_irreducible_transport_targetnonunitidentity))) + (((ge_first_in_irreducible_transport_targetnonunitidentity) * (ge_second_rn_irreducible_transport_targetnonunitidentity))))))) + ge_balance_negative_irreducible_transport_targetnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_transport_targetnonunitidentity) * (ge_second_in_irreducible_transport_targetnonunitidentity))) + (((ge_first_rn_irreducible_transport_targetnonunitidentity) * (ge_second_ip_irreducible_transport_targetnonunitidentity))))) + (((((ge_first_ip_irreducible_transport_targetnonunitidentity) * (ge_second_rn_irreducible_transport_targetnonunitidentity))) + (((ge_first_in_irreducible_transport_targetnonunitidentity) * (ge_second_rp_irreducible_transport_targetnonunitidentity))))))) + ge_balance_positive_irreducible_transport_targetnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_transport_target gr_second_factor_irreducible_transport_target. (exists ge_first_rp_irreducible_transport_targetfactorization ge_first_rn_irreducible_transport_targetfactorization ge_first_ip_irreducible_transport_targetfactorization ge_first_in_irreducible_transport_targetfactorization ge_second_rp_irreducible_transport_targetfactorization ge_second_rn_irreducible_transport_targetfactorization ge_second_ip_irreducible_transport_targetfactorization ge_second_in_irreducible_transport_targetfactorization. ((exists ge_representation_real_code_irreducible_transport_targetfactorizationfirst ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst. (((gr_first_factor_irreducible_transport_target) = ((ge_representation_real_code_irreducible_transport_targetfactorizationfirst) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst)) * S ((ge_representation_real_code_irreducible_transport_targetfactorizationfirst) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_transport_targetfactorizationfirstreal ge_balance_negative_irreducible_transport_targetfactorizationfirstreal. (((((ge_representation_real_code_irreducible_transport_targetfactorizationfirst) = 2 * (ge_balance_positive_irreducible_transport_targetfactorizationfirstreal) /\ (ge_balance_negative_irreducible_transport_targetfactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetfactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_transport_targetfactorizationfirst) = 2 * ge_signed_half_irreducible_transport_targetfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetfactorizationfirstreal) = S ge_signed_half_irreducible_transport_targetfactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_targetfactorization) + ge_balance_negative_irreducible_transport_targetfactorizationfirstreal = (ge_first_rn_irreducible_transport_targetfactorization) + ge_balance_positive_irreducible_transport_targetfactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_targetfactorizationfirstimaginary ge_balance_negative_irreducible_transport_targetfactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst) = 2 * (ge_balance_positive_irreducible_transport_targetfactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_transport_targetfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetfactorizationfirst) = 2 * ge_signed_half_irreducible_transport_targetfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetfactorizationfirstimaginary) = S ge_signed_half_irreducible_transport_targetfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_targetfactorization) + ge_balance_negative_irreducible_transport_targetfactorizationfirstimaginary = (ge_first_in_irreducible_transport_targetfactorization) + ge_balance_positive_irreducible_transport_targetfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_targetfactorizationsecond ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond. (((gr_second_factor_irreducible_transport_target) = ((ge_representation_real_code_irreducible_transport_targetfactorizationsecond) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond)) * S ((ge_representation_real_code_irreducible_transport_targetfactorizationsecond) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_transport_targetfactorizationsecondreal ge_balance_negative_irreducible_transport_targetfactorizationsecondreal. (((((ge_representation_real_code_irreducible_transport_targetfactorizationsecond) = 2 * (ge_balance_positive_irreducible_transport_targetfactorizationsecondreal) /\ (ge_balance_negative_irreducible_transport_targetfactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetfactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_transport_targetfactorizationsecond) = 2 * ge_signed_half_irreducible_transport_targetfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetfactorizationsecondreal) = S ge_signed_half_irreducible_transport_targetfactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_targetfactorization) + ge_balance_negative_irreducible_transport_targetfactorizationsecondreal = (ge_second_rn_irreducible_transport_targetfactorization) + ge_balance_positive_irreducible_transport_targetfactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_transport_targetfactorizationsecondimaginary ge_balance_negative_irreducible_transport_targetfactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond) = 2 * (ge_balance_positive_irreducible_transport_targetfactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_transport_targetfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetfactorizationsecond) = 2 * ge_signed_half_irreducible_transport_targetfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetfactorizationsecondimaginary) = S ge_signed_half_irreducible_transport_targetfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_targetfactorization) + ge_balance_negative_irreducible_transport_targetfactorizationsecondimaginary = (ge_second_in_irreducible_transport_targetfactorization) + ge_balance_positive_irreducible_transport_targetfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_targetfactorizationoutput ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput. (((q) = ((ge_representation_real_code_irreducible_transport_targetfactorizationoutput) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput)) * S ((ge_representation_real_code_irreducible_transport_targetfactorizationoutput) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput) + (ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_transport_targetfactorizationoutputreal ge_balance_negative_irreducible_transport_targetfactorizationoutputreal. (((((ge_representation_real_code_irreducible_transport_targetfactorizationoutput) = 2 * (ge_balance_positive_irreducible_transport_targetfactorizationoutputreal) /\ (ge_balance_negative_irreducible_transport_targetfactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetfactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_transport_targetfactorizationoutput) = 2 * ge_signed_half_irreducible_transport_targetfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetfactorizationoutputreal) = S ge_signed_half_irreducible_transport_targetfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetfactorization) * (ge_second_rp_irreducible_transport_targetfactorization))) + (((ge_first_rn_irreducible_transport_targetfactorization) * (ge_second_rn_irreducible_transport_targetfactorization))))) + (((((ge_first_ip_irreducible_transport_targetfactorization) * (ge_second_in_irreducible_transport_targetfactorization))) + (((ge_first_in_irreducible_transport_targetfactorization) * (ge_second_ip_irreducible_transport_targetfactorization))))))) + ge_balance_negative_irreducible_transport_targetfactorizationoutputreal = (((((((ge_first_rp_irreducible_transport_targetfactorization) * (ge_second_rn_irreducible_transport_targetfactorization))) + (((ge_first_rn_irreducible_transport_targetfactorization) * (ge_second_rp_irreducible_transport_targetfactorization))))) + (((((ge_first_ip_irreducible_transport_targetfactorization) * (ge_second_ip_irreducible_transport_targetfactorization))) + (((ge_first_in_irreducible_transport_targetfactorization) * (ge_second_in_irreducible_transport_targetfactorization))))))) + ge_balance_positive_irreducible_transport_targetfactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_targetfactorizationoutputimaginary ge_balance_negative_irreducible_transport_targetfactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput) = 2 * (ge_balance_positive_irreducible_transport_targetfactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_transport_targetfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetfactorizationoutput) = 2 * ge_signed_half_irreducible_transport_targetfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetfactorizationoutputimaginary) = S ge_signed_half_irreducible_transport_targetfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetfactorization) * (ge_second_ip_irreducible_transport_targetfactorization))) + (((ge_first_rn_irreducible_transport_targetfactorization) * (ge_second_in_irreducible_transport_targetfactorization))))) + (((((ge_first_ip_irreducible_transport_targetfactorization) * (ge_second_rp_irreducible_transport_targetfactorization))) + (((ge_first_in_irreducible_transport_targetfactorization) * (ge_second_rn_irreducible_transport_targetfactorization))))))) + ge_balance_negative_irreducible_transport_targetfactorizationoutputimaginary = (((((((ge_first_rp_irreducible_transport_targetfactorization) * (ge_second_in_irreducible_transport_targetfactorization))) + (((ge_first_rn_irreducible_transport_targetfactorization) * (ge_second_ip_irreducible_transport_targetfactorization))))) + (((((ge_first_ip_irreducible_transport_targetfactorization) * (ge_second_rn_irreducible_transport_targetfactorization))) + (((ge_first_in_irreducible_transport_targetfactorization) * (ge_second_rp_irreducible_transport_targetfactorization))))))) + ge_balance_positive_irreducible_transport_targetfactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_transport_targetfirst_unit. (exists ge_first_rp_irreducible_transport_targetfirst_unitidentity ge_first_rn_irreducible_transport_targetfirst_unitidentity ge_first_ip_irreducible_transport_targetfirst_unitidentity ge_first_in_irreducible_transport_targetfirst_unitidentity ge_second_rp_irreducible_transport_targetfirst_unitidentity ge_second_rn_irreducible_transport_targetfirst_unitidentity ge_second_ip_irreducible_transport_targetfirst_unitidentity ge_second_in_irreducible_transport_targetfirst_unitidentity. ((exists ge_representation_real_code_irreducible_transport_targetfirst_unitidentityfirst ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst. (((gr_first_factor_irreducible_transport_target) = ((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstreal ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_targetfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstreal) = S ge_signed_half_irreducible_transport_targetfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_targetfirst_unitidentity) + ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstreal = (ge_first_rn_irreducible_transport_targetfirst_unitidentity) + ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstimaginary ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_targetfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_transport_targetfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_targetfirst_unitidentity) + ge_balance_negative_irreducible_transport_targetfirst_unitidentityfirstimaginary = (ge_first_in_irreducible_transport_targetfirst_unitidentity) + ge_balance_positive_irreducible_transport_targetfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_targetfirst_unitidentitysecond ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond. (((gr_inverse_irreducible_transport_targetfirst_unit) = ((ge_representation_real_code_irreducible_transport_targetfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_transport_targetfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondreal ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_transport_targetfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_transport_targetfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_targetfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondreal) = S ge_signed_half_irreducible_transport_targetfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_targetfirst_unitidentity) + ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondreal = (ge_second_rn_irreducible_transport_targetfirst_unitidentity) + ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondimaginary ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_targetfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_transport_targetfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_targetfirst_unitidentity) + ge_balance_negative_irreducible_transport_targetfirst_unitidentitysecondimaginary = (ge_second_in_irreducible_transport_targetfirst_unitidentity) + ge_balance_positive_irreducible_transport_targetfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_targetfirst_unitidentityoutput ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputreal ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_transport_targetfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_targetfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputreal) = S ge_signed_half_irreducible_transport_targetfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetfirst_unitidentity) * (ge_second_rp_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_rn_irreducible_transport_targetfirst_unitidentity) * (ge_second_rn_irreducible_transport_targetfirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetfirst_unitidentity) * (ge_second_in_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_in_irreducible_transport_targetfirst_unitidentity) * (ge_second_ip_irreducible_transport_targetfirst_unitidentity))))))) + ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_transport_targetfirst_unitidentity) * (ge_second_rn_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_rn_irreducible_transport_targetfirst_unitidentity) * (ge_second_rp_irreducible_transport_targetfirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetfirst_unitidentity) * (ge_second_ip_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_in_irreducible_transport_targetfirst_unitidentity) * (ge_second_in_irreducible_transport_targetfirst_unitidentity))))))) + ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputimaginary ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetfirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_targetfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_transport_targetfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetfirst_unitidentity) * (ge_second_ip_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_rn_irreducible_transport_targetfirst_unitidentity) * (ge_second_in_irreducible_transport_targetfirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetfirst_unitidentity) * (ge_second_rp_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_in_irreducible_transport_targetfirst_unitidentity) * (ge_second_rn_irreducible_transport_targetfirst_unitidentity))))))) + ge_balance_negative_irreducible_transport_targetfirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_transport_targetfirst_unitidentity) * (ge_second_in_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_rn_irreducible_transport_targetfirst_unitidentity) * (ge_second_ip_irreducible_transport_targetfirst_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetfirst_unitidentity) * (ge_second_rn_irreducible_transport_targetfirst_unitidentity))) + (((ge_first_in_irreducible_transport_targetfirst_unitidentity) * (ge_second_rp_irreducible_transport_targetfirst_unitidentity))))))) + ge_balance_positive_irreducible_transport_targetfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_transport_targetsecond_unit. (exists ge_first_rp_irreducible_transport_targetsecond_unitidentity ge_first_rn_irreducible_transport_targetsecond_unitidentity ge_first_ip_irreducible_transport_targetsecond_unitidentity ge_first_in_irreducible_transport_targetsecond_unitidentity ge_second_rp_irreducible_transport_targetsecond_unitidentity ge_second_rn_irreducible_transport_targetsecond_unitidentity ge_second_ip_irreducible_transport_targetsecond_unitidentity ge_second_in_irreducible_transport_targetsecond_unitidentity. ((exists ge_representation_real_code_irreducible_transport_targetsecond_unitidentityfirst ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst. (((gr_second_factor_irreducible_transport_target) = ((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstreal ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_targetsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstreal) = S ge_signed_half_irreducible_transport_targetsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_transport_targetsecond_unitidentity) + ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstreal = (ge_first_rn_irreducible_transport_targetsecond_unitidentity) + ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstimaginary ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_transport_targetsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_transport_targetsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_transport_targetsecond_unitidentity) + ge_balance_negative_irreducible_transport_targetsecond_unitidentityfirstimaginary = (ge_first_in_irreducible_transport_targetsecond_unitidentity) + ge_balance_positive_irreducible_transport_targetsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_transport_targetsecond_unitidentitysecond ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond. (((gr_inverse_irreducible_transport_targetsecond_unit) = ((ge_representation_real_code_irreducible_transport_targetsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_transport_targetsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondreal ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_transport_targetsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_transport_targetsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_targetsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondreal) = S ge_signed_half_irreducible_transport_targetsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_transport_targetsecond_unitidentity) + ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondreal = (ge_second_rn_irreducible_transport_targetsecond_unitidentity) + ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondimaginary ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_transport_targetsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_transport_targetsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_transport_targetsecond_unitidentity) + ge_balance_negative_irreducible_transport_targetsecond_unitidentitysecondimaginary = (ge_second_in_irreducible_transport_targetsecond_unitidentity) + ge_balance_positive_irreducible_transport_targetsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_transport_targetsecond_unitidentityoutput ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputreal ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_transport_targetsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_transport_targetsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_targetsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputreal) = S ge_signed_half_irreducible_transport_targetsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetsecond_unitidentity) * (ge_second_rp_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_rn_irreducible_transport_targetsecond_unitidentity) * (ge_second_rn_irreducible_transport_targetsecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetsecond_unitidentity) * (ge_second_in_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_in_irreducible_transport_targetsecond_unitidentity) * (ge_second_ip_irreducible_transport_targetsecond_unitidentity))))))) + ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_transport_targetsecond_unitidentity) * (ge_second_rn_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_rn_irreducible_transport_targetsecond_unitidentity) * (ge_second_rp_irreducible_transport_targetsecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetsecond_unitidentity) * (ge_second_ip_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_in_irreducible_transport_targetsecond_unitidentity) * (ge_second_in_irreducible_transport_targetsecond_unitidentity))))))) + ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputimaginary ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_transport_targetsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_transport_targetsecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_transport_targetsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_transport_targetsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_transport_targetsecond_unitidentity) * (ge_second_ip_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_rn_irreducible_transport_targetsecond_unitidentity) * (ge_second_in_irreducible_transport_targetsecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetsecond_unitidentity) * (ge_second_rp_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_in_irreducible_transport_targetsecond_unitidentity) * (ge_second_rn_irreducible_transport_targetsecond_unitidentity))))))) + ge_balance_negative_irreducible_transport_targetsecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_transport_targetsecond_unitidentity) * (ge_second_in_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_rn_irreducible_transport_targetsecond_unitidentity) * (ge_second_ip_irreducible_transport_targetsecond_unitidentity))))) + (((((ge_first_ip_irreducible_transport_targetsecond_unitidentity) * (ge_second_rn_irreducible_transport_targetsecond_unitidentity))) + (((ge_first_in_irreducible_transport_targetsecond_unitidentity) * (ge_second_rp_irreducible_transport_targetsecond_unitidentity))))))) + ge_balance_positive_irreducible_transport_targetsecond_unitidentityoutputimaginary)))))))))))))))Complete tactic proof in conservative notation
All 9 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
9 script commands · 3 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–4
02Calculate and transport equalitiesL5–8
03Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
exact h