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
∀ z. ∀ N. GNorm(z,N) → ¬z = 0 → ¬GUnit(z) → GIrreducible(z) ∨ (∃ x. ∃ y. ∃ n. ∃ m. GStrictNonunitFactorization(z,N,x,y,n,m))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall z N. (exists ge_norm_rp_irreducible_split_norm ge_norm_rn_irreducible_split_norm ge_norm_ip_irreducible_split_norm ge_norm_in_irreducible_split_norm. ((exists ge_representation_real_code_irreducible_split_normrepresentation ge_representation_imaginary_code_irreducible_split_normrepresentation. (((z) = ((ge_representation_real_code_irreducible_split_normrepresentation) + (ge_representation_imaginary_code_irreducible_split_normrepresentation)) * S ((ge_representation_real_code_irreducible_split_normrepresentation) + (ge_representation_imaginary_code_irreducible_split_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_split_normrepresentation) + (ge_representation_imaginary_code_irreducible_split_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_split_normrepresentationreal ge_balance_negative_irreducible_split_normrepresentationreal. (((((ge_representation_real_code_irreducible_split_normrepresentation) = 2 * (ge_balance_positive_irreducible_split_normrepresentationreal) /\ (ge_balance_negative_irreducible_split_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_split_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_split_normrepresentation) = 2 * ge_signed_half_irreducible_split_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_split_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_split_normrepresentationreal) = S ge_signed_half_irreducible_split_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_split_norm) + ge_balance_negative_irreducible_split_normrepresentationreal = (ge_norm_rn_irreducible_split_norm) + ge_balance_positive_irreducible_split_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_split_normrepresentationimaginary ge_balance_negative_irreducible_split_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_split_normrepresentation) = 2 * (ge_balance_positive_irreducible_split_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_split_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_split_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_normrepresentation) = 2 * ge_signed_half_irreducible_split_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_split_normrepresentationimaginary) = S ge_signed_half_irreducible_split_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_split_norm) + ge_balance_negative_irreducible_split_normrepresentationimaginary = (ge_norm_in_irreducible_split_norm) + ge_balance_positive_irreducible_split_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_split_normsquare ge_imaginary_square_irreducible_split_normsquare. ((((((ge_norm_rp_irreducible_split_norm) * (ge_norm_rp_irreducible_split_norm))) + (((ge_norm_rn_irreducible_split_norm) * (ge_norm_rn_irreducible_split_norm)))) = ((ge_real_square_irreducible_split_normsquare) + (((((ge_norm_rp_irreducible_split_norm) * (ge_norm_rn_irreducible_split_norm))) + (((ge_norm_rn_irreducible_split_norm) * (ge_norm_rp_irreducible_split_norm))))))) /\ ((((((ge_norm_ip_irreducible_split_norm) * (ge_norm_ip_irreducible_split_norm))) + (((ge_norm_in_irreducible_split_norm) * (ge_norm_in_irreducible_split_norm)))) = ((ge_imaginary_square_irreducible_split_normsquare) + (((((ge_norm_ip_irreducible_split_norm) * (ge_norm_in_irreducible_split_norm))) + (((ge_norm_in_irreducible_split_norm) * (ge_norm_ip_irreducible_split_norm))))))) /\ ((N) = ge_real_square_irreducible_split_normsquare + ge_imaginary_square_irreducible_split_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_irreducible_split_nonunit. (exists ge_first_rp_irreducible_split_nonunitidentity ge_first_rn_irreducible_split_nonunitidentity ge_first_ip_irreducible_split_nonunitidentity ge_first_in_irreducible_split_nonunitidentity ge_second_rp_irreducible_split_nonunitidentity ge_second_rn_irreducible_split_nonunitidentity ge_second_ip_irreducible_split_nonunitidentity ge_second_in_irreducible_split_nonunitidentity. ((exists ge_representation_real_code_irreducible_split_nonunitidentityfirst ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_split_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_split_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_split_nonunitidentityfirstreal ge_balance_negative_irreducible_split_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_split_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_split_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_split_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstreal) = S ge_signed_half_irreducible_split_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentityfirstreal = (ge_first_rn_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_split_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_split_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentityfirstimaginary = (ge_first_in_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_split_nonunitidentitysecond ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond. (((gr_inverse_irreducible_split_nonunit) = ((ge_representation_real_code_irreducible_split_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_split_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_split_nonunitidentitysecondreal ge_balance_negative_irreducible_split_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_split_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_split_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_split_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_split_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondreal) = S ge_signed_half_irreducible_split_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentitysecondreal = (ge_second_rn_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_split_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_split_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_split_nonunitidentity) + ge_balance_negative_irreducible_split_nonunitidentitysecondimaginary = (ge_second_in_irreducible_split_nonunitidentity) + ge_balance_positive_irreducible_split_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_split_nonunitidentityoutput ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_split_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_split_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_split_nonunitidentityoutputreal ge_balance_negative_irreducible_split_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_split_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_split_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_split_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputreal) = S ge_signed_half_irreducible_split_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))))))) + ge_balance_negative_irreducible_split_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))))))) + ge_balance_positive_irreducible_split_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_split_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_split_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_split_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_split_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))))))) + ge_balance_negative_irreducible_split_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_split_nonunitidentity) * (ge_second_in_irreducible_split_nonunitidentity))) + (((ge_first_rn_irreducible_split_nonunitidentity) * (ge_second_ip_irreducible_split_nonunitidentity))))) + (((((ge_first_ip_irreducible_split_nonunitidentity) * (ge_second_rn_irreducible_split_nonunitidentity))) + (((ge_first_in_irreducible_split_nonunitidentity) * (ge_second_rp_irreducible_split_nonunitidentity))))))) + ge_balance_positive_irreducible_split_nonunitidentityoutputimaginary)))))))))) -> ((((exists ge_real_positive_irreducible_splitirreduciblecarrier ge_real_negative_irreducible_splitirreduciblecarrier ge_imaginary_positive_irreducible_splitirreduciblecarrier ge_imaginary_negative_irreducible_splitirreduciblecarrier. (exists ge_real_code_irreducible_splitirreduciblecarrierdecode ge_imaginary_code_irreducible_splitirreduciblecarrierdecode. (((z) = ((ge_real_code_irreducible_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_splitirreduciblecarrierdecode)) * S ((ge_real_code_irreducible_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_splitirreduciblecarrierdecode)) + ((ge_imaginary_code_irreducible_splitirreduciblecarrierdecode) + (ge_imaginary_code_irreducible_splitirreduciblecarrierdecode))) /\ (((((ge_real_code_irreducible_splitirreduciblecarrierdecode) = 2 * (ge_real_positive_irreducible_splitirreduciblecarrier) /\ (ge_real_negative_irreducible_splitirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_real. (((ge_real_code_irreducible_splitirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_splitirreduciblecarrier) = 0) /\ (ge_real_negative_irreducible_splitirreduciblecarrier) = S ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_splitirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_splitirreduciblecarrier) /\ (ge_imaginary_negative_irreducible_splitirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_splitirreduciblecarrierdecode) = 2 * ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_splitirreduciblecarrier) = 0) /\ (ge_imaginary_negative_irreducible_splitirreduciblecarrier) = S ge_signed_half_ge_irreducible_splitirreduciblecarrierdecode_imaginary))))))) /\ ((~((z)=0)) /\ ((~(exists gr_inverse_irreducible_splitirreduciblenonunit. (exists ge_first_rp_irreducible_splitirreduciblenonunitidentity ge_first_rn_irreducible_splitirreduciblenonunitidentity ge_first_ip_irreducible_splitirreduciblenonunitidentity ge_first_in_irreducible_splitirreduciblenonunitidentity ge_second_rp_irreducible_splitirreduciblenonunitidentity ge_second_rn_irreducible_splitirreduciblenonunitidentity ge_second_ip_irreducible_splitirreduciblenonunitidentity ge_second_in_irreducible_splitirreduciblenonunitidentity. ((exists ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst. (((z) = ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstreal = (ge_first_rn_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityfirstimaginary = (ge_first_in_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond. (((gr_inverse_irreducible_splitirreduciblenonunit) = ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal) = S ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondreal = (ge_second_rn_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_splitirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblenonunitidentity) + ge_balance_negative_irreducible_splitirreduciblenonunitidentitysecondimaginary = (ge_second_in_irreducible_splitirreduciblenonunitidentity) + ge_balance_positive_irreducible_splitirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblenonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblenonunitidentity) * (ge_second_in_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_rn_irreducible_splitirreduciblenonunitidentity) * (ge_second_ip_irreducible_splitirreduciblenonunitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblenonunitidentity) * (ge_second_rn_irreducible_splitirreduciblenonunitidentity))) + (((ge_first_in_irreducible_splitirreduciblenonunitidentity) * (ge_second_rp_irreducible_splitirreduciblenonunitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_splitirreducible gr_second_factor_irreducible_splitirreducible. (exists ge_first_rp_irreducible_splitirreduciblefactorization ge_first_rn_irreducible_splitirreduciblefactorization ge_first_ip_irreducible_splitirreduciblefactorization ge_first_in_irreducible_splitirreduciblefactorization ge_second_rp_irreducible_splitirreduciblefactorization ge_second_rn_irreducible_splitirreduciblefactorization ge_second_ip_irreducible_splitirreduciblefactorization ge_second_in_irreducible_splitirreduciblefactorization. ((exists ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst. (((gr_first_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal) = S ge_signed_half_irreducible_splitirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationfirstreal = (ge_first_rn_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationfirstimaginary = (ge_first_in_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond. (((gr_second_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal) = S ge_signed_half_irreducible_splitirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationsecondreal = (ge_second_rn_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationsecond) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary) = S ge_signed_half_irreducible_splitirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblefactorization) + ge_balance_negative_irreducible_splitirreduciblefactorizationsecondimaginary = (ge_second_in_irreducible_splitirreduciblefactorization) + ge_balance_positive_irreducible_splitirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput. (((z) = ((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal) = S ge_signed_half_irreducible_splitirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))))))) + ge_balance_negative_irreducible_splitirreduciblefactorizationoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))))))) + ge_balance_positive_irreducible_splitirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefactorizationoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))))))) + ge_balance_negative_irreducible_splitirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblefactorization) * (ge_second_in_irreducible_splitirreduciblefactorization))) + (((ge_first_rn_irreducible_splitirreduciblefactorization) * (ge_second_ip_irreducible_splitirreduciblefactorization))))) + (((((ge_first_ip_irreducible_splitirreduciblefactorization) * (ge_second_rn_irreducible_splitirreduciblefactorization))) + (((ge_first_in_irreducible_splitirreduciblefactorization) * (ge_second_rp_irreducible_splitirreduciblefactorization))))))) + ge_balance_positive_irreducible_splitirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_splitirreduciblefirst_unit. (exists ge_first_rp_irreducible_splitirreduciblefirst_unitidentity ge_first_rn_irreducible_splitirreduciblefirst_unitidentity ge_first_ip_irreducible_splitirreduciblefirst_unitidentity ge_first_in_irreducible_splitirreduciblefirst_unitidentity ge_second_rp_irreducible_splitirreduciblefirst_unitidentity ge_second_rn_irreducible_splitirreduciblefirst_unitidentity ge_second_ip_irreducible_splitirreduciblefirst_unitidentity ge_second_in_irreducible_splitirreduciblefirst_unitidentity. ((exists ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst. (((gr_first_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstreal = (ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond. (((gr_inverse_irreducible_splitirreduciblefirst_unit) = ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondreal = (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_splitirreduciblefirst_unitidentity) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_in_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_ip_irreducible_splitirreduciblefirst_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rn_irreducible_splitirreduciblefirst_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblefirst_unitidentity) * (ge_second_rp_irreducible_splitirreduciblefirst_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_splitirreduciblesecond_unit. (exists ge_first_rp_irreducible_splitirreduciblesecond_unitidentity ge_first_rn_irreducible_splitirreduciblesecond_unitidentity ge_first_ip_irreducible_splitirreduciblesecond_unitidentity ge_first_in_irreducible_splitirreduciblesecond_unitidentity ge_second_rp_irreducible_splitirreduciblesecond_unitidentity ge_second_rn_irreducible_splitirreduciblesecond_unitidentity ge_second_ip_irreducible_splitirreduciblesecond_unitidentity ge_second_in_irreducible_splitirreduciblesecond_unitidentity. ((exists ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst. (((gr_second_factor_irreducible_splitirreducible) = ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstreal = (ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond. (((gr_inverse_irreducible_splitirreduciblesecond_unit) = ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondreal = (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_splitirreduciblesecond_unitidentity) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_splitirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_negative_irreducible_splitirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_in_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_rn_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_ip_irreducible_splitirreduciblesecond_unitidentity))))) + (((((ge_first_ip_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rn_irreducible_splitirreduciblesecond_unitidentity))) + (((ge_first_in_irreducible_splitirreduciblesecond_unitidentity) * (ge_second_rp_irreducible_splitirreduciblesecond_unitidentity))))))) + ge_balance_positive_irreducible_splitirreduciblesecond_unitidentityoutputimaginary))))))))))))))) \/ (exists gr_split_first_irreducible_split gr_split_second_irreducible_split gr_split_first_norm_irreducible_split gr_split_second_norm_irreducible_split. (((exists ge_first_rp_irreducible_splitsplitproduct ge_first_rn_irreducible_splitsplitproduct ge_first_ip_irreducible_splitsplitproduct ge_first_in_irreducible_splitsplitproduct ge_second_rp_irreducible_splitsplitproduct ge_second_rn_irreducible_splitsplitproduct ge_second_ip_irreducible_splitsplitproduct ge_second_in_irreducible_splitsplitproduct. ((exists ge_representation_real_code_irreducible_splitsplitproductfirst ge_representation_imaginary_code_irreducible_splitsplitproductfirst. (((gr_split_first_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_splitsplitproductfirst)) * S ((ge_representation_real_code_irreducible_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_splitsplitproductfirst)) + ((ge_representation_imaginary_code_irreducible_splitsplitproductfirst) + (ge_representation_imaginary_code_irreducible_splitsplitproductfirst))) /\ ((exists ge_balance_positive_irreducible_splitsplitproductfirstreal ge_balance_negative_irreducible_splitsplitproductfirstreal. (((((ge_representation_real_code_irreducible_splitsplitproductfirst) = 2 * (ge_balance_positive_irreducible_splitsplitproductfirstreal) /\ (ge_balance_negative_irreducible_splitsplitproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductfirstrealdecode. (((ge_representation_real_code_irreducible_splitsplitproductfirst) = 2 * ge_signed_half_irreducible_splitsplitproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductfirstreal) = S ge_signed_half_irreducible_splitsplitproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductfirstreal = (ge_first_rn_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductfirstreal))) /\ (exists ge_balance_positive_irreducible_splitsplitproductfirstimaginary ge_balance_negative_irreducible_splitsplitproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitproductfirst) = 2 * (ge_balance_positive_irreducible_splitsplitproductfirstimaginary) /\ (ge_balance_negative_irreducible_splitsplitproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitproductfirst) = 2 * ge_signed_half_irreducible_splitsplitproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductfirstimaginary) = S ge_signed_half_irreducible_splitsplitproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductfirstimaginary = (ge_first_in_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitsplitproductsecond ge_representation_imaginary_code_irreducible_splitsplitproductsecond. (((gr_split_second_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_splitsplitproductsecond)) * S ((ge_representation_real_code_irreducible_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_splitsplitproductsecond)) + ((ge_representation_imaginary_code_irreducible_splitsplitproductsecond) + (ge_representation_imaginary_code_irreducible_splitsplitproductsecond))) /\ ((exists ge_balance_positive_irreducible_splitsplitproductsecondreal ge_balance_negative_irreducible_splitsplitproductsecondreal. (((((ge_representation_real_code_irreducible_splitsplitproductsecond) = 2 * (ge_balance_positive_irreducible_splitsplitproductsecondreal) /\ (ge_balance_negative_irreducible_splitsplitproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductsecondrealdecode. (((ge_representation_real_code_irreducible_splitsplitproductsecond) = 2 * ge_signed_half_irreducible_splitsplitproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductsecondreal) = S ge_signed_half_irreducible_splitsplitproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductsecondreal = (ge_second_rn_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductsecondreal))) /\ (exists ge_balance_positive_irreducible_splitsplitproductsecondimaginary ge_balance_negative_irreducible_splitsplitproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitproductsecond) = 2 * (ge_balance_positive_irreducible_splitsplitproductsecondimaginary) /\ (ge_balance_negative_irreducible_splitsplitproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitproductsecond) = 2 * ge_signed_half_irreducible_splitsplitproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductsecondimaginary) = S ge_signed_half_irreducible_splitsplitproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitsplitproduct) + ge_balance_negative_irreducible_splitsplitproductsecondimaginary = (ge_second_in_irreducible_splitsplitproduct) + ge_balance_positive_irreducible_splitsplitproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitsplitproductoutput ge_representation_imaginary_code_irreducible_splitsplitproductoutput. (((z) = ((ge_representation_real_code_irreducible_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_splitsplitproductoutput)) * S ((ge_representation_real_code_irreducible_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_splitsplitproductoutput)) + ((ge_representation_imaginary_code_irreducible_splitsplitproductoutput) + (ge_representation_imaginary_code_irreducible_splitsplitproductoutput))) /\ ((exists ge_balance_positive_irreducible_splitsplitproductoutputreal ge_balance_negative_irreducible_splitsplitproductoutputreal. (((((ge_representation_real_code_irreducible_splitsplitproductoutput) = 2 * (ge_balance_positive_irreducible_splitsplitproductoutputreal) /\ (ge_balance_negative_irreducible_splitsplitproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductoutputrealdecode. (((ge_representation_real_code_irreducible_splitsplitproductoutput) = 2 * ge_signed_half_irreducible_splitsplitproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductoutputreal) = S ge_signed_half_irreducible_splitsplitproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))))))) + ge_balance_negative_irreducible_splitsplitproductoutputreal = (((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))))))) + ge_balance_positive_irreducible_splitsplitproductoutputreal))) /\ (exists ge_balance_positive_irreducible_splitsplitproductoutputimaginary ge_balance_negative_irreducible_splitsplitproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitproductoutput) = 2 * (ge_balance_positive_irreducible_splitsplitproductoutputimaginary) /\ (ge_balance_negative_irreducible_splitsplitproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitproductoutput) = 2 * ge_signed_half_irreducible_splitsplitproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitproductoutputimaginary) = S ge_signed_half_irreducible_splitsplitproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))))))) + ge_balance_negative_irreducible_splitsplitproductoutputimaginary = (((((((ge_first_rp_irreducible_splitsplitproduct) * (ge_second_in_irreducible_splitsplitproduct))) + (((ge_first_rn_irreducible_splitsplitproduct) * (ge_second_ip_irreducible_splitsplitproduct))))) + (((((ge_first_ip_irreducible_splitsplitproduct) * (ge_second_rn_irreducible_splitsplitproduct))) + (((ge_first_in_irreducible_splitsplitproduct) * (ge_second_rp_irreducible_splitsplitproduct))))))) + ge_balance_positive_irreducible_splitsplitproductoutputimaginary))))))))) /\ ((exists ge_norm_rp_irreducible_splitsplitfirst_norm ge_norm_rn_irreducible_splitsplitfirst_norm ge_norm_ip_irreducible_splitsplitfirst_norm ge_norm_in_irreducible_splitsplitfirst_norm. ((exists ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation. (((gr_split_first_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitfirst_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal) = S ge_signed_half_irreducible_splitsplitfirst_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_splitsplitfirst_norm) + ge_balance_negative_irreducible_splitsplitfirst_normrepresentationreal = (ge_norm_rn_irreducible_splitsplitfirst_norm) + ge_balance_positive_irreducible_splitsplitfirst_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitfirst_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary) = S ge_signed_half_irreducible_splitsplitfirst_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_splitsplitfirst_norm) + ge_balance_negative_irreducible_splitsplitfirst_normrepresentationimaginary = (ge_norm_in_irreducible_splitsplitfirst_norm) + ge_balance_positive_irreducible_splitsplitfirst_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_splitsplitfirst_normsquare ge_imaginary_square_irreducible_splitsplitfirst_normsquare. ((((((ge_norm_rp_irreducible_splitsplitfirst_norm) * (ge_norm_rp_irreducible_splitsplitfirst_norm))) + (((ge_norm_rn_irreducible_splitsplitfirst_norm) * (ge_norm_rn_irreducible_splitsplitfirst_norm)))) = ((ge_real_square_irreducible_splitsplitfirst_normsquare) + (((((ge_norm_rp_irreducible_splitsplitfirst_norm) * (ge_norm_rn_irreducible_splitsplitfirst_norm))) + (((ge_norm_rn_irreducible_splitsplitfirst_norm) * (ge_norm_rp_irreducible_splitsplitfirst_norm))))))) /\ ((((((ge_norm_ip_irreducible_splitsplitfirst_norm) * (ge_norm_ip_irreducible_splitsplitfirst_norm))) + (((ge_norm_in_irreducible_splitsplitfirst_norm) * (ge_norm_in_irreducible_splitsplitfirst_norm)))) = ((ge_imaginary_square_irreducible_splitsplitfirst_normsquare) + (((((ge_norm_ip_irreducible_splitsplitfirst_norm) * (ge_norm_in_irreducible_splitsplitfirst_norm))) + (((ge_norm_in_irreducible_splitsplitfirst_norm) * (ge_norm_ip_irreducible_splitsplitfirst_norm))))))) /\ ((gr_split_first_norm_irreducible_split) = ge_real_square_irreducible_splitsplitfirst_normsquare + ge_imaginary_square_irreducible_splitsplitfirst_normsquare)))))) /\ ((exists ge_norm_rp_irreducible_splitsplitsecond_norm ge_norm_rn_irreducible_splitsplitsecond_norm ge_norm_ip_irreducible_splitsplitsecond_norm ge_norm_in_irreducible_splitsplitsecond_norm. ((exists ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation. (((gr_split_second_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_normrepresentationrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitsecond_normrepresentationrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal) = S ge_signed_half_irreducible_splitsplitsecond_normrepresentationrealdecode))) /\ ((ge_norm_rp_irreducible_splitsplitsecond_norm) + ge_balance_negative_irreducible_splitsplitsecond_normrepresentationreal = (ge_norm_rn_irreducible_splitsplitsecond_norm) + ge_balance_positive_irreducible_splitsplitsecond_normrepresentationreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_normrepresentation) = 2 * ge_signed_half_irreducible_splitsplitsecond_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary) = S ge_signed_half_irreducible_splitsplitsecond_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_irreducible_splitsplitsecond_norm) + ge_balance_negative_irreducible_splitsplitsecond_normrepresentationimaginary = (ge_norm_in_irreducible_splitsplitsecond_norm) + ge_balance_positive_irreducible_splitsplitsecond_normrepresentationimaginary)))))) /\ (exists ge_real_square_irreducible_splitsplitsecond_normsquare ge_imaginary_square_irreducible_splitsplitsecond_normsquare. ((((((ge_norm_rp_irreducible_splitsplitsecond_norm) * (ge_norm_rp_irreducible_splitsplitsecond_norm))) + (((ge_norm_rn_irreducible_splitsplitsecond_norm) * (ge_norm_rn_irreducible_splitsplitsecond_norm)))) = ((ge_real_square_irreducible_splitsplitsecond_normsquare) + (((((ge_norm_rp_irreducible_splitsplitsecond_norm) * (ge_norm_rn_irreducible_splitsplitsecond_norm))) + (((ge_norm_rn_irreducible_splitsplitsecond_norm) * (ge_norm_rp_irreducible_splitsplitsecond_norm))))))) /\ ((((((ge_norm_ip_irreducible_splitsplitsecond_norm) * (ge_norm_ip_irreducible_splitsplitsecond_norm))) + (((ge_norm_in_irreducible_splitsplitsecond_norm) * (ge_norm_in_irreducible_splitsplitsecond_norm)))) = ((ge_imaginary_square_irreducible_splitsplitsecond_normsquare) + (((((ge_norm_ip_irreducible_splitsplitsecond_norm) * (ge_norm_in_irreducible_splitsplitsecond_norm))) + (((ge_norm_in_irreducible_splitsplitsecond_norm) * (ge_norm_ip_irreducible_splitsplitsecond_norm))))))) /\ ((gr_split_second_norm_irreducible_split) = ge_real_square_irreducible_splitsplitsecond_normsquare + ge_imaginary_square_irreducible_splitsplitsecond_normsquare)))))) /\ ((~(exists gr_inverse_irreducible_splitsplitfirst_nonunit. (exists ge_first_rp_irreducible_splitsplitfirst_nonunitidentity ge_first_rn_irreducible_splitsplitfirst_nonunitidentity ge_first_ip_irreducible_splitsplitfirst_nonunitidentity ge_first_in_irreducible_splitsplitfirst_nonunitidentity ge_second_rp_irreducible_splitsplitfirst_nonunitidentity ge_second_rn_irreducible_splitsplitfirst_nonunitidentity ge_second_ip_irreducible_splitsplitfirst_nonunitidentity ge_second_in_irreducible_splitsplitfirst_nonunitidentity. ((exists ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst. (((gr_split_first_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstreal = (ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityfirstimaginary = (ge_first_in_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond. (((gr_inverse_irreducible_splitsplitfirst_nonunit) = ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondreal = (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentitysecondimaginary = (ge_second_in_irreducible_splitsplitfirst_nonunitidentity) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitfirst_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_splitsplitfirst_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitfirst_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_in_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_ip_irreducible_splitsplitfirst_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rn_irreducible_splitsplitfirst_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitfirst_nonunitidentity) * (ge_second_rp_irreducible_splitsplitfirst_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitfirst_nonunitidentityoutputimaginary))))))))))) /\ ((~(exists gr_inverse_irreducible_splitsplitsecond_nonunit. (exists ge_first_rp_irreducible_splitsplitsecond_nonunitidentity ge_first_rn_irreducible_splitsplitsecond_nonunitidentity ge_first_ip_irreducible_splitsplitsecond_nonunitidentity ge_first_in_irreducible_splitsplitsecond_nonunitidentity ge_second_rp_irreducible_splitsplitsecond_nonunitidentity ge_second_rn_irreducible_splitsplitsecond_nonunitidentity ge_second_ip_irreducible_splitsplitsecond_nonunitidentity ge_second_in_irreducible_splitsplitsecond_nonunitidentity. ((exists ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst. (((gr_split_second_irreducible_split) = ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstreal = (ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityfirst) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityfirstimaginary = (ge_first_in_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond. (((gr_inverse_irreducible_splitsplitsecond_nonunit) = ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondreal = (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentitysecond) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentitysecondimaginary = (ge_second_in_irreducible_splitsplitsecond_nonunitidentity) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputreal = (((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_splitsplitsecond_nonunitidentityoutput) = 2 * ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary) = S ge_signed_half_irreducible_splitsplitsecond_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_negative_irreducible_splitsplitsecond_nonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_in_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_rn_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_ip_irreducible_splitsplitsecond_nonunitidentity))))) + (((((ge_first_ip_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rn_irreducible_splitsplitsecond_nonunitidentity))) + (((ge_first_in_irreducible_splitsplitsecond_nonunitidentity) * (ge_second_rp_irreducible_splitsplitsecond_nonunitidentity))))))) + ge_balance_positive_irreducible_splitsplitsecond_nonunitidentityoutputimaginary))))))))))) /\ ((exists ge_gap_irreducible_splitsplitfirst_strict. ge_gap_irreducible_splitsplitfirst_strict + S (gr_split_first_norm_irreducible_split) = (N)) /\ (exists ge_gap_irreducible_splitsplitsecond_strict. ge_gap_irreducible_splitsplitsecond_strict + S (gr_split_second_norm_irreducible_split) = (N)))))))))))Complete tactic proof in conservative notation
All 77 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
77 script commands · 23 reading checkpoints · 4 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (7)
01Fix variables and assumptionsL1–5
02Establish hsearchL6–10
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor search complete.
- L6
have hsearch : (∃ x. GProperNormDivisor(x,z,N)) ∨ (∀ x. ¬GProperNormDivisor(x,z,N))Definitions: GProperNormDivisor(x,z,N)Original native command in the exact edition - L7
specialize gaussian_factor_search_complete (z) - L8
specialize gaussian_factor_search_complete (N) - L9
apply gaussian_factor_search_complete - L10
exact hn
03Separate the logical casesL11–12
04Establish hsL13–20
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian proper norm divisor split.
- L13
have hs : ∃ q. ∃ D. ∃ Q. GStrictNonunitFactorization(z,N,x,q,D,Q)Definitions: GStrictNonunitFactorization(z,N,x,q,D,Q)Original native command in the exact edition - L14
specialize gaussian_proper_norm_divisor_split (x) - L15
specialize gaussian_proper_norm_divisor_split (z) - L16
specialize gaussian_proper_norm_divisor_split (N) - L17
apply gaussian_proper_norm_divisor_split - L18
exact hsearch_left_witness - L19
exact hn - L20
exact hz
05Separate the logical casesL21–24
06Construct an explicit witnessL25–28
07Use earlier factsL29–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L29
exact hs_witness_witness_witness
08Separate the logical casesL30–31
09Use earlier factsL32–35
10Separate the logical casesL36–36
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L36
split
11Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
exact hz
12Separate the logical casesL38–38
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L38
split
13Use earlier factsL39–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L39
exact hu
14Fix variables and assumptionsL40–42
15Establish haL43–50
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian unit decidable.
16Separate the logical casesL51–52
17Use earlier factsL53–53
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L53
exact ha_left
18Establish hbL54–61
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian unit decidable.
19Separate the logical casesL62–63
20Use earlier factsL64–64
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L64
exact hb_left
21Separate the logical casesL65–65
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L65
exfalso
22Use earlier factsL66–75
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L66
specialize hsearch_right (a) - L67
apply hsearch_right - L68
specialize gaussian_nonunit_factor_is_proper_norm_divisor (z) - L69
specialize gaussian_nonunit_factor_is_proper_norm_divisor (N) - L70
specialize gaussian_nonunit_factor_is_proper_norm_divisor (a) - L71
specialize gaussian_nonunit_factor_is_proper_norm_divisor (b) - L72
apply gaussian_nonunit_factor_is_proper_norm_divisor - L73
exact hn - L74
exact hm - L75
exact hz
Original defined command ledger · 77 lines
- 0001
intro z - 0002
intro N - 0003
intro hn - 0004
intro hz - 0005
intro hu - 0006
have hsearch : (∃ x. GProperNormDivisor(x,z,N)) ∨ (∀ x. ¬GProperNormDivisor(x,z,N)) - 0007
specialize gaussian_factor_search_complete (z) - 0008
specialize gaussian_factor_search_complete (N) - 0009
apply gaussian_factor_search_complete - 0010
exact hn - 0011
cases hsearch - 0012
cases hsearch_left - 0013
have hs : ∃ q. ∃ D. ∃ Q. GStrictNonunitFactorization(z,N,x,q,D,Q) - 0014
specialize gaussian_proper_norm_divisor_split (x) - 0015
specialize gaussian_proper_norm_divisor_split (z) - 0016
specialize gaussian_proper_norm_divisor_split (N) - 0017
apply gaussian_proper_norm_divisor_split - 0018
exact hsearch_left_witness - 0019
exact hn - 0020
exact hz - 0021
cases hs - 0022
cases hs_witness - 0023
cases hs_witness_witness - 0024
right - 0025
exists (x) - 0026
exists (x1) - 0027
exists (x2) - 0028
exists (x3) - 0029
exact hs_witness_witness_witness - 0030
left - 0031
split - 0032
specialize gaussian_norm_input_valid (z) - 0033
specialize gaussian_norm_input_valid (N) - 0034
apply gaussian_norm_input_valid - 0035
exact hn - 0036
split - 0037
exact hz - 0038
split - 0039
exact hu - 0040
intro a - 0041
intro b - 0042
intro hm - 0043
have ha : GUnit(a) ∨ ¬GUnit(a) - 0044
specialize gaussian_unit_decidable (a) - 0045
apply gaussian_unit_decidable - 0046
specialize gaussian_multiply_input_left_valid (a) - 0047
specialize gaussian_multiply_input_left_valid (b) - 0048
specialize gaussian_multiply_input_left_valid (z) - 0049
apply gaussian_multiply_input_left_valid - 0050
exact hm - 0051
cases ha - 0052
left - 0053
exact ha_left - 0054
have hb : GUnit(b) ∨ ¬GUnit(b) - 0055
specialize gaussian_unit_decidable (b) - 0056
apply gaussian_unit_decidable - 0057
specialize gaussian_multiply_input_right_valid (a) - 0058
specialize gaussian_multiply_input_right_valid (b) - 0059
specialize gaussian_multiply_input_right_valid (z) - 0060
apply gaussian_multiply_input_right_valid - 0061
exact hm - 0062
cases hb - 0063
right - 0064
exact hb_left - 0065
exfalso - 0066
specialize hsearch_right (a) - 0067
apply hsearch_right - 0068
specialize gaussian_nonunit_factor_is_proper_norm_divisor (z) - 0069
specialize gaussian_nonunit_factor_is_proper_norm_divisor (N) - 0070
specialize gaussian_nonunit_factor_is_proper_norm_divisor (a) - 0071
specialize gaussian_nonunit_factor_is_proper_norm_divisor (b) - 0072
apply gaussian_nonunit_factor_is_proper_norm_divisor - 0073
exact hn - 0074
exact hm - 0075
exact hz - 0076
exact ha_right - 0077
exact hb_right