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. GIrreducible(p) → GPrime(p)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall p. (((exists ge_real_positive_irreducible_prime_sourcecarrier ge_real_negative_irreducible_prime_sourcecarrier ge_imaginary_positive_irreducible_prime_sourcecarrier ge_imaginary_negative_irreducible_prime_sourcecarrier. (exists ge_real_code_irreducible_prime_sourcecarrierdecode ge_imaginary_code_irreducible_prime_sourcecarrierdecode. (((p) = ((ge_real_code_irreducible_prime_sourcecarrierdecode) + (ge_imaginary_code_irreducible_prime_sourcecarrierdecode)) * S ((ge_real_code_irreducible_prime_sourcecarrierdecode) + (ge_imaginary_code_irreducible_prime_sourcecarrierdecode)) + ((ge_imaginary_code_irreducible_prime_sourcecarrierdecode) + (ge_imaginary_code_irreducible_prime_sourcecarrierdecode))) /\ (((((ge_real_code_irreducible_prime_sourcecarrierdecode) = 2 * (ge_real_positive_irreducible_prime_sourcecarrier) /\ (ge_real_negative_irreducible_prime_sourcecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_real. (((ge_real_code_irreducible_prime_sourcecarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_prime_sourcecarrier) = 0) /\ (ge_real_negative_irreducible_prime_sourcecarrier) = S ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_prime_sourcecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_prime_sourcecarrier) /\ (ge_imaginary_negative_irreducible_prime_sourcecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_prime_sourcecarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_prime_sourcecarrier) = 0) /\ (ge_imaginary_negative_irreducible_prime_sourcecarrier) = S ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_irreducible_prime_sourcenonunit. (exists ge_first_rp_irreducible_prime_sourcenonunitidentity ge_first_rn_irreducible_prime_sourcenonunitidentity ge_first_ip_irreducible_prime_sourcenonunitidentity ge_first_in_irreducible_prime_sourcenonunitidentity ge_second_rp_irreducible_prime_sourcenonunitidentity ge_second_rn_irreducible_prime_sourcenonunitidentity ge_second_ip_irreducible_prime_sourcenonunitidentity ge_second_in_irreducible_prime_sourcenonunitidentity. ((exists ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal) = S ge_signed_half_irreducible_prime_sourcenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal = (ge_first_rn_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_sourcenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary = (ge_first_in_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond. (((gr_inverse_irreducible_prime_sourcenonunit) = ((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal) = S ge_signed_half_irreducible_prime_sourcenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal = (ge_second_rn_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_sourcenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary = (ge_second_in_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal) = S ge_signed_half_irreducible_prime_sourcenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_sourcenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_prime_source gr_second_factor_irreducible_prime_source. (exists ge_first_rp_irreducible_prime_sourcefactorization ge_first_rn_irreducible_prime_sourcefactorization ge_first_ip_irreducible_prime_sourcefactorization ge_first_in_irreducible_prime_sourcefactorization ge_second_rp_irreducible_prime_sourcefactorization ge_second_rn_irreducible_prime_sourcefactorization ge_second_ip_irreducible_prime_sourcefactorization ge_second_in_irreducible_prime_sourcefactorization. ((exists ge_representation_real_code_irreducible_prime_sourcefactorizationfirst ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst. (((gr_first_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal) = S ge_signed_half_irreducible_prime_sourcefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal = (ge_first_rn_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary) = S ge_signed_half_irreducible_prime_sourcefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary = (ge_first_in_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcefactorizationsecond ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond. (((gr_second_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond)) * S ((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal. (((((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal) = S ge_signed_half_irreducible_prime_sourcefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal = (ge_second_rn_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary) = S ge_signed_half_irreducible_prime_sourcefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary = (ge_second_in_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcefactorizationoutput ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput. (((p) = ((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal) = S ge_signed_half_irreducible_prime_sourcefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))))))) + ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal = (((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))))))) + ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary) = S ge_signed_half_irreducible_prime_sourcefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))))))) + ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))))))) + ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_prime_sourcefirst_unit. (exists ge_first_rp_irreducible_prime_sourcefirst_unitidentity ge_first_rn_irreducible_prime_sourcefirst_unitidentity ge_first_ip_irreducible_prime_sourcefirst_unitidentity ge_first_in_irreducible_prime_sourcefirst_unitidentity ge_second_rp_irreducible_prime_sourcefirst_unitidentity ge_second_rn_irreducible_prime_sourcefirst_unitidentity ge_second_ip_irreducible_prime_sourcefirst_unitidentity ge_second_in_irreducible_prime_sourcefirst_unitidentity. ((exists ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst. (((gr_first_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal = (ge_first_rn_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond. (((gr_inverse_irreducible_prime_sourcefirst_unit) = ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal = (ge_second_rn_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_prime_sourcesecond_unit. (exists ge_first_rp_irreducible_prime_sourcesecond_unitidentity ge_first_rn_irreducible_prime_sourcesecond_unitidentity ge_first_ip_irreducible_prime_sourcesecond_unitidentity ge_first_in_irreducible_prime_sourcesecond_unitidentity ge_second_rp_irreducible_prime_sourcesecond_unitidentity ge_second_rn_irreducible_prime_sourcesecond_unitidentity ge_second_ip_irreducible_prime_sourcesecond_unitidentity ge_second_in_irreducible_prime_sourcesecond_unitidentity. ((exists ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst. (((gr_second_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal = (ge_first_rn_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond. (((gr_inverse_irreducible_prime_sourcesecond_unit) = ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal = (ge_second_rn_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary))))))))))))))) -> (((exists ge_real_positive_irreducible_prime_resultcarrier ge_real_negative_irreducible_prime_resultcarrier ge_imaginary_positive_irreducible_prime_resultcarrier ge_imaginary_negative_irreducible_prime_resultcarrier. (exists ge_real_code_irreducible_prime_resultcarrierdecode ge_imaginary_code_irreducible_prime_resultcarrierdecode. (((p) = ((ge_real_code_irreducible_prime_resultcarrierdecode) + (ge_imaginary_code_irreducible_prime_resultcarrierdecode)) * S ((ge_real_code_irreducible_prime_resultcarrierdecode) + (ge_imaginary_code_irreducible_prime_resultcarrierdecode)) + ((ge_imaginary_code_irreducible_prime_resultcarrierdecode) + (ge_imaginary_code_irreducible_prime_resultcarrierdecode))) /\ (((((ge_real_code_irreducible_prime_resultcarrierdecode) = 2 * (ge_real_positive_irreducible_prime_resultcarrier) /\ (ge_real_negative_irreducible_prime_resultcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_resultcarrierdecode_real. (((ge_real_code_irreducible_prime_resultcarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_resultcarrierdecode_real + 1 /\ (ge_real_positive_irreducible_prime_resultcarrier) = 0) /\ (ge_real_negative_irreducible_prime_resultcarrier) = S ge_signed_half_ge_irreducible_prime_resultcarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_prime_resultcarrierdecode) = 2 * (ge_imaginary_positive_irreducible_prime_resultcarrier) /\ (ge_imaginary_negative_irreducible_prime_resultcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_resultcarrierdecode_imaginary. (((ge_imaginary_code_irreducible_prime_resultcarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_resultcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_prime_resultcarrier) = 0) /\ (ge_imaginary_negative_irreducible_prime_resultcarrier) = S ge_signed_half_ge_irreducible_prime_resultcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_irreducible_prime_resultnonunit. (exists ge_first_rp_irreducible_prime_resultnonunitidentity ge_first_rn_irreducible_prime_resultnonunitidentity ge_first_ip_irreducible_prime_resultnonunitidentity ge_first_in_irreducible_prime_resultnonunitidentity ge_second_rp_irreducible_prime_resultnonunitidentity ge_second_rn_irreducible_prime_resultnonunitidentity ge_second_ip_irreducible_prime_resultnonunitidentity ge_second_in_irreducible_prime_resultnonunitidentity. ((exists ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal) = S ge_signed_half_irreducible_prime_resultnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal = (ge_first_rn_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_resultnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary = (ge_first_in_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond. (((gr_inverse_irreducible_prime_resultnonunit) = ((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal) = S ge_signed_half_irreducible_prime_resultnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal = (ge_second_rn_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_resultnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary = (ge_second_in_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal) = S ge_signed_half_irreducible_prime_resultnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))))))) + ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))))))) + ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_resultnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))))))) + ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))))))) + ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_prime_result gr_second_factor_irreducible_prime_result gr_product_irreducible_prime_result. (exists ge_first_rp_irreducible_prime_resultproduct ge_first_rn_irreducible_prime_resultproduct ge_first_ip_irreducible_prime_resultproduct ge_first_in_irreducible_prime_resultproduct ge_second_rp_irreducible_prime_resultproduct ge_second_rn_irreducible_prime_resultproduct ge_second_ip_irreducible_prime_resultproduct ge_second_in_irreducible_prime_resultproduct. ((exists ge_representation_real_code_irreducible_prime_resultproductfirst ge_representation_imaginary_code_irreducible_prime_resultproductfirst. (((gr_first_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultproductfirstreal ge_balance_negative_irreducible_prime_resultproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultproductfirst) = 2 * ge_signed_half_irreducible_prime_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductfirstreal) = S ge_signed_half_irreducible_prime_resultproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductfirstreal = (ge_first_rn_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultproductfirstimaginary ge_balance_negative_irreducible_prime_resultproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultproductfirst) = 2 * ge_signed_half_irreducible_prime_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductfirstimaginary = (ge_first_in_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultproductsecond ge_representation_imaginary_code_irreducible_prime_resultproductsecond. (((gr_second_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultproductsecondreal ge_balance_negative_irreducible_prime_resultproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultproductsecond) = 2 * ge_signed_half_irreducible_prime_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductsecondreal) = S ge_signed_half_irreducible_prime_resultproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductsecondreal = (ge_second_rn_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultproductsecondimaginary ge_balance_negative_irreducible_prime_resultproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultproductsecond) = 2 * ge_signed_half_irreducible_prime_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductsecondimaginary = (ge_second_in_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultproductoutput ge_representation_imaginary_code_irreducible_prime_resultproductoutput. (((gr_product_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultproductoutputreal ge_balance_negative_irreducible_prime_resultproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultproductoutput) = 2 * ge_signed_half_irreducible_prime_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductoutputreal) = S ge_signed_half_irreducible_prime_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))))))) + ge_balance_negative_irreducible_prime_resultproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))))))) + ge_balance_positive_irreducible_prime_resultproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultproductoutputimaginary ge_balance_negative_irreducible_prime_resultproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultproductoutput) = 2 * ge_signed_half_irreducible_prime_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))))))) + ge_balance_negative_irreducible_prime_resultproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))))))) + ge_balance_positive_irreducible_prime_resultproductoutputimaginary))))))))) -> (exists gr_quotient_irreducible_prime_resultdivisor. (exists ge_first_rp_irreducible_prime_resultdivisorproduct ge_first_rn_irreducible_prime_resultdivisorproduct ge_first_ip_irreducible_prime_resultdivisorproduct ge_first_in_irreducible_prime_resultdivisorproduct ge_second_rp_irreducible_prime_resultdivisorproduct ge_second_rn_irreducible_prime_resultdivisorproduct ge_second_ip_irreducible_prime_resultdivisorproduct ge_second_in_irreducible_prime_resultdivisorproduct. ((exists ge_representation_real_code_irreducible_prime_resultdivisorproductfirst ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal) = S ge_signed_half_irreducible_prime_resultdivisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal = (ge_first_rn_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultdivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary = (ge_first_in_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultdivisorproductsecond ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond. (((gr_quotient_irreducible_prime_resultdivisor) = ((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal) = S ge_signed_half_irreducible_prime_resultdivisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal = (ge_second_rn_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultdivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary = (ge_second_in_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultdivisorproductoutput ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput. (((gr_product_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal) = S ge_signed_half_irreducible_prime_resultdivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))))))) + ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))))))) + ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultdivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))))))) + ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))))))) + ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_irreducible_prime_resultfirst_divisor. (exists ge_first_rp_irreducible_prime_resultfirst_divisorproduct ge_first_rn_irreducible_prime_resultfirst_divisorproduct ge_first_ip_irreducible_prime_resultfirst_divisorproduct ge_first_in_irreducible_prime_resultfirst_divisorproduct ge_second_rp_irreducible_prime_resultfirst_divisorproduct ge_second_rn_irreducible_prime_resultfirst_divisorproduct ge_second_ip_irreducible_prime_resultfirst_divisorproduct ge_second_in_irreducible_prime_resultfirst_divisorproduct. ((exists ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal = (ge_first_rn_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary = (ge_first_in_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond. (((gr_quotient_irreducible_prime_resultfirst_divisor) = ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal = (ge_second_rn_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary = (ge_second_in_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput. (((gr_first_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_irreducible_prime_resultsecond_divisor. (exists ge_first_rp_irreducible_prime_resultsecond_divisorproduct ge_first_rn_irreducible_prime_resultsecond_divisorproduct ge_first_ip_irreducible_prime_resultsecond_divisorproduct ge_first_in_irreducible_prime_resultsecond_divisorproduct ge_second_rp_irreducible_prime_resultsecond_divisorproduct ge_second_rn_irreducible_prime_resultsecond_divisorproduct ge_second_ip_irreducible_prime_resultsecond_divisorproduct ge_second_in_irreducible_prime_resultsecond_divisorproduct. ((exists ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal = (ge_first_rn_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary = (ge_first_in_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond. (((gr_quotient_irreducible_prime_resultsecond_divisor) = ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal = (ge_second_rn_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary = (ge_second_in_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput. (((gr_second_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary)))))))))))))))Complete tactic proof in conservative notation
All 30 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
30 script commands · 15 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.
Named ingredients (1)
01Fix variables and assumptionsL1–2
02Separate the logical casesL3–6
03Use earlier factsL7–7
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L7
exact h_left
04Separate the logical casesL8–8
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L8
split
05Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
exact h_right_left
06Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
split
07Use earlier factsL11–11
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L11
exact h_right_right_left
08Fix variables and assumptionsL12–16
09Use earlier factsL17–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
10Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
split
11Use earlier factsL23–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L23
exact h_left
12Separate the logical casesL24–24
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L24
split
13Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact h_right_left
14Separate the logical casesL26–26
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L26
split
Original defined command ledger · 30 lines
- 0001
intro p - 0002
intro h - 0003
cases h - 0004
cases h_right - 0005
cases h_right_right - 0006
split - 0007
exact h_left - 0008
split - 0009
exact h_right_left - 0010
split - 0011
exact h_right_right_left - 0012
intro a - 0013
intro b - 0014
intro c - 0015
intro hprod - 0016
intro hdiv - 0017
specialize gaussian_irreducible_dvd_product (p) - 0018
specialize gaussian_irreducible_dvd_product (a) - 0019
specialize gaussian_irreducible_dvd_product (b) - 0020
specialize gaussian_irreducible_dvd_product (c) - 0021
apply gaussian_irreducible_dvd_product - 0022
split - 0023
exact h_left - 0024
split - 0025
exact h_right_left - 0026
split - 0027
exact h_right_right_left - 0028
exact h_right_right_right - 0029
exact hprod - 0030
exact hdiv