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
∀ k. ∀ z. ∀ N. Le(N,k) → GNorm(z,N) → ¬z = 0 → ∃ x. ∃ y. ∃ n. ∃ m. GIrreducibleFactorization(z,x,y,n,m)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
le_zero · checked external prerequisitegaussian_norm_zero_implies_code_zerogaussian_norm_value_transportgaussian_unit_decidablegaussian_norm_input_validgaussian_unit_empty_factorizationgaussian_irreducible_factor_reductionle_of_succ_le_succ · checked external prerequisitelt_of_lt_of_le · checked external prerequisitegaussian_factorization_append_irreduciblegaussian_multiply_commutative
Original expanded first-order statement
forall k z N. (exists ge_gap_factorization_bound. ge_gap_factorization_bound + (N) = (k)) -> (exists ge_norm_rp_factorization_norm ge_norm_rn_factorization_norm ge_norm_ip_factorization_norm ge_norm_in_factorization_norm. ((exists ge_representation_real_code_factorization_normrepresentation ge_representation_imaginary_code_factorization_normrepresentation. (((z) = ((ge_representation_real_code_factorization_normrepresentation) + (ge_representation_imaginary_code_factorization_normrepresentation)) * S ((ge_representation_real_code_factorization_normrepresentation) + (ge_representation_imaginary_code_factorization_normrepresentation)) + ((ge_representation_imaginary_code_factorization_normrepresentation) + (ge_representation_imaginary_code_factorization_normrepresentation))) /\ ((exists ge_balance_positive_factorization_normrepresentationreal ge_balance_negative_factorization_normrepresentationreal. (((((ge_representation_real_code_factorization_normrepresentation) = 2 * (ge_balance_positive_factorization_normrepresentationreal) /\ (ge_balance_negative_factorization_normrepresentationreal) = 0) \/ exists ge_signed_half_factorization_normrepresentationrealdecode. (((ge_representation_real_code_factorization_normrepresentation) = 2 * ge_signed_half_factorization_normrepresentationrealdecode + 1 /\ (ge_balance_positive_factorization_normrepresentationreal) = 0) /\ (ge_balance_negative_factorization_normrepresentationreal) = S ge_signed_half_factorization_normrepresentationrealdecode))) /\ ((ge_norm_rp_factorization_norm) + ge_balance_negative_factorization_normrepresentationreal = (ge_norm_rn_factorization_norm) + ge_balance_positive_factorization_normrepresentationreal))) /\ (exists ge_balance_positive_factorization_normrepresentationimaginary ge_balance_negative_factorization_normrepresentationimaginary. (((((ge_representation_imaginary_code_factorization_normrepresentation) = 2 * (ge_balance_positive_factorization_normrepresentationimaginary) /\ (ge_balance_negative_factorization_normrepresentationimaginary) = 0) \/ exists ge_signed_half_factorization_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_factorization_normrepresentation) = 2 * ge_signed_half_factorization_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_factorization_normrepresentationimaginary) = 0) /\ (ge_balance_negative_factorization_normrepresentationimaginary) = S ge_signed_half_factorization_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_factorization_norm) + ge_balance_negative_factorization_normrepresentationimaginary = (ge_norm_in_factorization_norm) + ge_balance_positive_factorization_normrepresentationimaginary)))))) /\ (exists ge_real_square_factorization_normsquare ge_imaginary_square_factorization_normsquare. ((((((ge_norm_rp_factorization_norm) * (ge_norm_rp_factorization_norm))) + (((ge_norm_rn_factorization_norm) * (ge_norm_rn_factorization_norm)))) = ((ge_real_square_factorization_normsquare) + (((((ge_norm_rp_factorization_norm) * (ge_norm_rn_factorization_norm))) + (((ge_norm_rn_factorization_norm) * (ge_norm_rp_factorization_norm))))))) /\ ((((((ge_norm_ip_factorization_norm) * (ge_norm_ip_factorization_norm))) + (((ge_norm_in_factorization_norm) * (ge_norm_in_factorization_norm)))) = ((ge_imaginary_square_factorization_normsquare) + (((((ge_norm_ip_factorization_norm) * (ge_norm_in_factorization_norm))) + (((ge_norm_in_factorization_norm) * (ge_norm_ip_factorization_norm))))))) /\ ((N) = ge_real_square_factorization_normsquare + ge_imaginary_square_factorization_normsquare)))))) -> ~(z=0) -> (exists u b c l. ((exists gr_inverse_factorization_existsunit. (exists ge_first_rp_factorization_existsunitidentity ge_first_rn_factorization_existsunitidentity ge_first_ip_factorization_existsunitidentity ge_first_in_factorization_existsunitidentity ge_second_rp_factorization_existsunitidentity ge_second_rn_factorization_existsunitidentity ge_second_ip_factorization_existsunitidentity ge_second_in_factorization_existsunitidentity. ((exists ge_representation_real_code_factorization_existsunitidentityfirst ge_representation_imaginary_code_factorization_existsunitidentityfirst. (((u) = ((ge_representation_real_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst)) * S ((ge_representation_real_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsunitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsunitidentityfirstreal ge_balance_negative_factorization_existsunitidentityfirstreal. (((((ge_representation_real_code_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsunitidentityfirstreal) /\ (ge_balance_negative_factorization_existsunitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsunitidentityfirst) = 2 * ge_signed_half_factorization_existsunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentityfirstreal) = S ge_signed_half_factorization_existsunitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentityfirstreal = (ge_first_rn_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsunitidentityfirstimaginary ge_balance_negative_factorization_existsunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsunitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentityfirst) = 2 * ge_signed_half_factorization_existsunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentityfirstimaginary) = S ge_signed_half_factorization_existsunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentityfirstimaginary = (ge_first_in_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsunitidentitysecond ge_representation_imaginary_code_factorization_existsunitidentitysecond. (((gr_inverse_factorization_existsunit) = ((ge_representation_real_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond)) * S ((ge_representation_real_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsunitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsunitidentitysecondreal ge_balance_negative_factorization_existsunitidentitysecondreal. (((((ge_representation_real_code_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsunitidentitysecondreal) /\ (ge_balance_negative_factorization_existsunitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsunitidentitysecond) = 2 * ge_signed_half_factorization_existsunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentitysecondreal) = S ge_signed_half_factorization_existsunitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentitysecondreal = (ge_second_rn_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsunitidentitysecondimaginary ge_balance_negative_factorization_existsunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsunitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentitysecond) = 2 * ge_signed_half_factorization_existsunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentitysecondimaginary) = S ge_signed_half_factorization_existsunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsunitidentity) + ge_balance_negative_factorization_existsunitidentitysecondimaginary = (ge_second_in_factorization_existsunitidentity) + ge_balance_positive_factorization_existsunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsunitidentityoutput ge_representation_imaginary_code_factorization_existsunitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput)) * S ((ge_representation_real_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsunitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsunitidentityoutputreal ge_balance_negative_factorization_existsunitidentityoutputreal. (((((ge_representation_real_code_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsunitidentityoutputreal) /\ (ge_balance_negative_factorization_existsunitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsunitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsunitidentityoutput) = 2 * ge_signed_half_factorization_existsunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsunitidentityoutputreal) = S ge_signed_half_factorization_existsunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))))))) + ge_balance_negative_factorization_existsunitidentityoutputreal = (((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))))))) + ge_balance_positive_factorization_existsunitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsunitidentityoutputimaginary ge_balance_negative_factorization_existsunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsunitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsunitidentityoutput) = 2 * ge_signed_half_factorization_existsunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsunitidentityoutputimaginary) = S ge_signed_half_factorization_existsunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))))))) + ge_balance_negative_factorization_existsunitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsunitidentity) * (ge_second_in_factorization_existsunitidentity))) + (((ge_first_rn_factorization_existsunitidentity) * (ge_second_ip_factorization_existsunitidentity))))) + (((((ge_first_ip_factorization_existsunitidentity) * (ge_second_rn_factorization_existsunitidentity))) + (((ge_first_in_factorization_existsunitidentity) * (ge_second_rp_factorization_existsunitidentity))))))) + ge_balance_positive_factorization_existsunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factorization_existsirreducible gr_factor_value_factorization_existsirreducible. (exists ge_gap_factorization_existsirreducibleindex. ge_gap_factorization_existsirreducibleindex + S (gr_factor_index_factorization_existsirreducible) = (l)) -> (((exists ff_h_gprod_factorization_existsirreducibleentry. ff_h_gprod_factorization_existsirreducibleentry + S (gr_factor_value_factorization_existsirreducible) = S ((S (gr_factor_index_factorization_existsirreducible)) * c)) /\ exists ff_q_gprod_factorization_existsirreducibleentry. b = ff_q_gprod_factorization_existsirreducibleentry * S ((S (gr_factor_index_factorization_existsirreducible)) * c) + (gr_factor_value_factorization_existsirreducible))) -> (((exists ge_real_positive_factorization_existsirreducibleirreduciblecarrier ge_real_negative_factorization_existsirreducibleirreduciblecarrier ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier. (exists ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode. (((gr_factor_value_factorization_existsirreducible) = ((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factorization_existsirreducibleirreduciblecarrier) /\ (ge_real_negative_factorization_existsirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factorization_existsirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factorization_existsirreducibleirreduciblecarrier) = S ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factorization_existsirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factorization_existsirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factorization_existsirreducibleirreduciblecarrier) = S ge_signed_half_ge_factorization_existsirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factorization_existsirreducible)=0)) /\ ((~(exists gr_inverse_factorization_existsirreducibleirreduciblenonunit. (exists ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factorization_existsirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblenonunit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblenonunitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factorization_existsirreducibleirreducible gr_second_factor_factorization_existsirreducibleirreducible. (exists ge_first_rp_factorization_existsirreducibleirreduciblefactorization ge_first_rn_factorization_existsirreducibleirreduciblefactorization ge_first_ip_factorization_existsirreducibleirreduciblefactorization ge_first_in_factorization_existsirreducibleirreduciblefactorization ge_second_rp_factorization_existsirreducibleirreduciblefactorization ge_second_rn_factorization_existsirreducibleirreduciblefactorization ge_second_ip_factorization_existsirreducibleirreduciblefactorization ge_second_in_factorization_existsirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblefactorization) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblefactorization) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factorization_existsirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefactorization) * (ge_second_in_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefactorization) * (ge_second_ip_factorization_existsirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rn_factorization_existsirreducibleirreduciblefactorization))) + (((ge_first_in_factorization_existsirreducibleirreduciblefactorization) * (ge_second_rp_factorization_existsirreducibleirreduciblefactorization))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factorization_existsirreducibleirreduciblefirst_unit. (exists ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factorization_existsirreducibleirreduciblesecond_unit. (exists ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factorization_existsirreducibleirreducible) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factorization_existsirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factorization_existsirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factorization_existsirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factorization_existsirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factorization_existsirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factorization_existsirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factorization_exists. ((exists gr_product_trace_factorization_existstrace gr_product_scale_factorization_existstrace. ((((exists ff_h_gprod_factorization_existstracestart. ff_h_gprod_factorization_existstracestart + S (6) = S ((S (0)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestart. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestart * S ((S (0)) * gr_product_scale_factorization_existstrace) + (6))) /\ ((((exists ff_h_gprod_factorization_existstraceend. ff_h_gprod_factorization_existstraceend + S (gr_factor_product_factorization_exists) = S ((S (l)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstraceend. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstraceend * S ((S (l)) * gr_product_scale_factorization_existstrace) + (gr_factor_product_factorization_exists))) /\ (forall gr_product_index_factorization_existstracesteps. (exists ge_gap_factorization_existstracestepsindex_bound. ge_gap_factorization_existstracestepsindex_bound + S (gr_product_index_factorization_existstracesteps) = (l)) -> exists gr_product_factor_factorization_existstracesteps gr_product_before_factorization_existstracesteps gr_product_after_factorization_existstracesteps. ((((exists ff_h_gprod_factorization_existstracestepsfactor. ff_h_gprod_factorization_existstracestepsfactor + S (gr_product_factor_factorization_existstracesteps) = S ((S (gr_product_index_factorization_existstracesteps)) * c)) /\ exists ff_q_gprod_factorization_existstracestepsfactor. b = ff_q_gprod_factorization_existstracestepsfactor * S ((S (gr_product_index_factorization_existstracesteps)) * c) + (gr_product_factor_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_factorization_existstracestepsbefore. ff_h_gprod_factorization_existstracestepsbefore + S (gr_product_before_factorization_existstracesteps) = S ((S (gr_product_index_factorization_existstracesteps)) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestepsbefore. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestepsbefore * S ((S (gr_product_index_factorization_existstracesteps)) * gr_product_scale_factorization_existstrace) + (gr_product_before_factorization_existstracesteps))) /\ ((((exists ff_h_gprod_factorization_existstracestepsafter. ff_h_gprod_factorization_existstracestepsafter + S (gr_product_after_factorization_existstracesteps) = S ((S (S (gr_product_index_factorization_existstracesteps))) * gr_product_scale_factorization_existstrace)) /\ exists ff_q_gprod_factorization_existstracestepsafter. gr_product_trace_factorization_existstrace = ff_q_gprod_factorization_existstracestepsafter * S ((S (S (gr_product_index_factorization_existstracesteps))) * gr_product_scale_factorization_existstrace) + (gr_product_after_factorization_existstracesteps))) /\ (exists ge_first_rp_factorization_existstracestepsmultiply ge_first_rn_factorization_existstracestepsmultiply ge_first_ip_factorization_existstracestepsmultiply ge_first_in_factorization_existstracestepsmultiply ge_second_rp_factorization_existstracestepsmultiply ge_second_rn_factorization_existstracestepsmultiply ge_second_ip_factorization_existstracestepsmultiply ge_second_in_factorization_existstracestepsmultiply. ((exists ge_representation_real_code_factorization_existstracestepsmultiplyfirst ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst. (((gr_product_before_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplyfirstreal ge_balance_negative_factorization_existstracestepsmultiplyfirstreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyfirstreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstreal) = S ge_signed_half_factorization_existstracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplyfirstreal = (ge_first_rn_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplyfirst) = 2 * ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary) = S ge_signed_half_factorization_existstracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplyfirstimaginary = (ge_first_in_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existstracestepsmultiplysecond ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond. (((gr_product_factor_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplysecondreal ge_balance_negative_factorization_existstracestepsmultiplysecondreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplysecondreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondreal) = S ge_signed_half_factorization_existstracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplysecondreal = (ge_second_rn_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplysecond) = 2 * ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary) = S ge_signed_half_factorization_existstracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factorization_existstracestepsmultiply) + ge_balance_negative_factorization_existstracestepsmultiplysecondimaginary = (ge_second_in_factorization_existstracestepsmultiply) + ge_balance_positive_factorization_existstracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existstracestepsmultiplyoutput ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput. (((gr_product_after_factorization_existstracesteps) = ((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput)) * S ((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) + (ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factorization_existstracestepsmultiplyoutputreal ge_balance_negative_factorization_existstracestepsmultiplyoutputreal. (((((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyoutputreal) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputreal) = S ge_signed_half_factorization_existstracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))))))) + ge_balance_negative_factorization_existstracestepsmultiplyoutputreal = (((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))))))) + ge_balance_positive_factorization_existstracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) = 2 * (ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existstracestepsmultiplyoutput) = 2 * ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary) = S ge_signed_half_factorization_existstracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))))))) + ge_balance_negative_factorization_existstracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factorization_existstracestepsmultiply) * (ge_second_in_factorization_existstracestepsmultiply))) + (((ge_first_rn_factorization_existstracestepsmultiply) * (ge_second_ip_factorization_existstracestepsmultiply))))) + (((((ge_first_ip_factorization_existstracestepsmultiply) * (ge_second_rn_factorization_existstracestepsmultiply))) + (((ge_first_in_factorization_existstracestepsmultiply) * (ge_second_rp_factorization_existstracestepsmultiply))))))) + ge_balance_positive_factorization_existstracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factorization_existsreconstruct ge_first_rn_factorization_existsreconstruct ge_first_ip_factorization_existsreconstruct ge_first_in_factorization_existsreconstruct ge_second_rp_factorization_existsreconstruct ge_second_rn_factorization_existsreconstruct ge_second_ip_factorization_existsreconstruct ge_second_in_factorization_existsreconstruct. ((exists ge_representation_real_code_factorization_existsreconstructfirst ge_representation_imaginary_code_factorization_existsreconstructfirst. (((u) = ((ge_representation_real_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst)) * S ((ge_representation_real_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst)) + ((ge_representation_imaginary_code_factorization_existsreconstructfirst) + (ge_representation_imaginary_code_factorization_existsreconstructfirst))) /\ ((exists ge_balance_positive_factorization_existsreconstructfirstreal ge_balance_negative_factorization_existsreconstructfirstreal. (((((ge_representation_real_code_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_factorization_existsreconstructfirstreal) /\ (ge_balance_negative_factorization_existsreconstructfirstreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructfirstrealdecode. (((ge_representation_real_code_factorization_existsreconstructfirst) = 2 * ge_signed_half_factorization_existsreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructfirstreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructfirstreal) = S ge_signed_half_factorization_existsreconstructfirstrealdecode))) /\ ((ge_first_rp_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructfirstreal = (ge_first_rn_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructfirstreal))) /\ (exists ge_balance_positive_factorization_existsreconstructfirstimaginary ge_balance_negative_factorization_existsreconstructfirstimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructfirst) = 2 * (ge_balance_positive_factorization_existsreconstructfirstimaginary) /\ (ge_balance_negative_factorization_existsreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructfirst) = 2 * ge_signed_half_factorization_existsreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructfirstimaginary) = S ge_signed_half_factorization_existsreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructfirstimaginary = (ge_first_in_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factorization_existsreconstructsecond ge_representation_imaginary_code_factorization_existsreconstructsecond. (((gr_factor_product_factorization_exists) = ((ge_representation_real_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond)) * S ((ge_representation_real_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond)) + ((ge_representation_imaginary_code_factorization_existsreconstructsecond) + (ge_representation_imaginary_code_factorization_existsreconstructsecond))) /\ ((exists ge_balance_positive_factorization_existsreconstructsecondreal ge_balance_negative_factorization_existsreconstructsecondreal. (((((ge_representation_real_code_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_factorization_existsreconstructsecondreal) /\ (ge_balance_negative_factorization_existsreconstructsecondreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructsecondrealdecode. (((ge_representation_real_code_factorization_existsreconstructsecond) = 2 * ge_signed_half_factorization_existsreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructsecondreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructsecondreal) = S ge_signed_half_factorization_existsreconstructsecondrealdecode))) /\ ((ge_second_rp_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructsecondreal = (ge_second_rn_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructsecondreal))) /\ (exists ge_balance_positive_factorization_existsreconstructsecondimaginary ge_balance_negative_factorization_existsreconstructsecondimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructsecond) = 2 * (ge_balance_positive_factorization_existsreconstructsecondimaginary) /\ (ge_balance_negative_factorization_existsreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructsecond) = 2 * ge_signed_half_factorization_existsreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructsecondimaginary) = S ge_signed_half_factorization_existsreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factorization_existsreconstruct) + ge_balance_negative_factorization_existsreconstructsecondimaginary = (ge_second_in_factorization_existsreconstruct) + ge_balance_positive_factorization_existsreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factorization_existsreconstructoutput ge_representation_imaginary_code_factorization_existsreconstructoutput. (((z) = ((ge_representation_real_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput)) * S ((ge_representation_real_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput)) + ((ge_representation_imaginary_code_factorization_existsreconstructoutput) + (ge_representation_imaginary_code_factorization_existsreconstructoutput))) /\ ((exists ge_balance_positive_factorization_existsreconstructoutputreal ge_balance_negative_factorization_existsreconstructoutputreal. (((((ge_representation_real_code_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_factorization_existsreconstructoutputreal) /\ (ge_balance_negative_factorization_existsreconstructoutputreal) = 0) \/ exists ge_signed_half_factorization_existsreconstructoutputrealdecode. (((ge_representation_real_code_factorization_existsreconstructoutput) = 2 * ge_signed_half_factorization_existsreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factorization_existsreconstructoutputreal) = 0) /\ (ge_balance_negative_factorization_existsreconstructoutputreal) = S ge_signed_half_factorization_existsreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))))))) + ge_balance_negative_factorization_existsreconstructoutputreal = (((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))))))) + ge_balance_positive_factorization_existsreconstructoutputreal))) /\ (exists ge_balance_positive_factorization_existsreconstructoutputimaginary ge_balance_negative_factorization_existsreconstructoutputimaginary. (((((ge_representation_imaginary_code_factorization_existsreconstructoutput) = 2 * (ge_balance_positive_factorization_existsreconstructoutputimaginary) /\ (ge_balance_negative_factorization_existsreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factorization_existsreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factorization_existsreconstructoutput) = 2 * ge_signed_half_factorization_existsreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factorization_existsreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factorization_existsreconstructoutputimaginary) = S ge_signed_half_factorization_existsreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))))))) + ge_balance_negative_factorization_existsreconstructoutputimaginary = (((((((ge_first_rp_factorization_existsreconstruct) * (ge_second_in_factorization_existsreconstruct))) + (((ge_first_rn_factorization_existsreconstruct) * (ge_second_ip_factorization_existsreconstruct))))) + (((((ge_first_ip_factorization_existsreconstruct) * (ge_second_rn_factorization_existsreconstruct))) + (((ge_first_in_factorization_existsreconstruct) * (ge_second_rp_factorization_existsreconstruct))))))) + ge_balance_positive_factorization_existsreconstructoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 94 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
94 script commands · 19 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 (8)
01Induction on kL1–6
02Separate the logical casesL7–7
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L7
exfalso
03Use earlier factsL8–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L8
apply hz - L9
specialize gaussian_norm_zero_implies_code_zero (z) - L10
apply gaussian_norm_zero_implies_code_zero - L11
specialize gaussian_norm_value_transport (z) - L12
specialize gaussian_norm_value_transport (N) - L13
specialize gaussian_norm_value_transport (0) - L14
apply gaussian_norm_value_transport - L15
specialize le_zero (N) - L16
apply le_zero - L17
exact hb
04Use earlier factsL18–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
exact hn
05Fix variables and assumptionsL19–23
06Establish huL24–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian unit decidable.
07Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
cases hu
08Construct an explicit witnessL32–35
09Use earlier factsL36–38
10Establish hrL39–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian irreducible factor reduction.
- L39
have hr : ∃ p. ∃ q. ∃ Q. GIrreducible(p) ∧ (GMul(p,q,z) ∧ (GNorm(q,Q) ∧ (Lt(Q,N) ∧ ¬q = 0)))Definitions: GIrreducible(p)GMul(p,q,z)GNorm(q,Q)Lt(Q,N)Original native command in the exact edition - L40
specialize gaussian_irreducible_factor_reduction (z) - L41
specialize gaussian_irreducible_factor_reduction (N) - L42
apply gaussian_irreducible_factor_reduction - L43
exact hn - L44
exact hz - L45
exact hu_right
11Separate the logical casesL46–52
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
12Establish hrecL53–62
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L53
have hrec : ∃ u. ∃ b. ∃ c. ∃ l. GIrreducibleFactorization(x1,u,b,c,l)Definitions: GIrreducibleFactorization(x1,u,b,c,l)Original native command in the exact edition - L54
specialize IH (x1) - L55
specialize IH (x2) - L56
apply IH - L57
specialize le_of_succ_le_succ (x2) - L58
specialize le_of_succ_le_succ (k) - L59
apply le_of_succ_le_succ - L60
specialize lt_of_lt_of_le (x2) - L61
specialize lt_of_lt_of_le (N) - L62
specialize lt_of_lt_of_le (S k)
13Use earlier factsL63–67
14Separate the logical casesL68–71
15Establish hextL72–81
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factorization append irreducible.
- L72
have hext : ∃ d. ∃ e. GIrreducibleFactorization(z,x3,d,e,S x6)Definitions: GIrreducibleFactorization(z,x3,d,e,S x6)Original native command in the exact edition - L73
specialize gaussian_factorization_append_irreducible (x1) - L74
specialize gaussian_factorization_append_irreducible (x3) - L75
specialize gaussian_factorization_append_irreducible (x4) - L76
specialize gaussian_factorization_append_irreducible (x5) - L77
specialize gaussian_factorization_append_irreducible (x6) - L78
specialize gaussian_factorization_append_irreducible (x) - L79
specialize gaussian_factorization_append_irreducible (z) - L80
apply gaussian_factorization_append_irreducible - L81
exact hrec_witness_witness_witness_witness
16Use earlier factsL82–87
Instantiate or apply named facts and discharge the corresponding proof obligations.
17Separate the logical casesL88–89
18Construct an explicit witnessL90–93
19Use earlier factsL94–94
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L94
exact hext_witness_witness
Original defined command ledger · 94 lines
- 0001
induction k - 0002
intro z - 0003
intro N - 0004
intro hb - 0005
intro hn - 0006
intro hz - 0007
exfalso - 0008
apply hz - 0009
specialize gaussian_norm_zero_implies_code_zero (z) - 0010
apply gaussian_norm_zero_implies_code_zero - 0011
specialize gaussian_norm_value_transport (z) - 0012
specialize gaussian_norm_value_transport (N) - 0013
specialize gaussian_norm_value_transport (0) - 0014
apply gaussian_norm_value_transport - 0015
specialize le_zero (N) - 0016
apply le_zero - 0017
exact hb - 0018
exact hn - 0019
intro z - 0020
intro N - 0021
intro hb - 0022
intro hn - 0023
intro hz - 0024
have hu : GUnit(z) ∨ ¬GUnit(z) - 0025
specialize gaussian_unit_decidable (z) - 0026
apply gaussian_unit_decidable - 0027
specialize gaussian_norm_input_valid (z) - 0028
specialize gaussian_norm_input_valid (N) - 0029
apply gaussian_norm_input_valid - 0030
exact hn - 0031
cases hu - 0032
exists (z) - 0033
exists (0) - 0034
exists (0) - 0035
exists (0) - 0036
specialize gaussian_unit_empty_factorization (z) - 0037
apply gaussian_unit_empty_factorization - 0038
exact hu_left - 0039
have hr : ∃ p. ∃ q. ∃ Q. GIrreducible(p) ∧ (GMul(p,q,z) ∧ (GNorm(q,Q) ∧ (Lt(Q,N) ∧ ¬q = 0))) - 0040
specialize gaussian_irreducible_factor_reduction (z) - 0041
specialize gaussian_irreducible_factor_reduction (N) - 0042
apply gaussian_irreducible_factor_reduction - 0043
exact hn - 0044
exact hz - 0045
exact hu_right - 0046
cases hr - 0047
cases hr_witness - 0048
cases hr_witness_witness - 0049
cases hr_witness_witness_witness - 0050
cases hr_witness_witness_witness_right - 0051
cases hr_witness_witness_witness_right_right - 0052
cases hr_witness_witness_witness_right_right_right - 0053
have hrec : ∃ u. ∃ b. ∃ c. ∃ l. GIrreducibleFactorization(x1,u,b,c,l) - 0054
specialize IH (x1) - 0055
specialize IH (x2) - 0056
apply IH - 0057
specialize le_of_succ_le_succ (x2) - 0058
specialize le_of_succ_le_succ (k) - 0059
apply le_of_succ_le_succ - 0060
specialize lt_of_lt_of_le (x2) - 0061
specialize lt_of_lt_of_le (N) - 0062
specialize lt_of_lt_of_le (S k) - 0063
apply lt_of_lt_of_le - 0064
exact hr_witness_witness_witness_right_right_right_left - 0065
exact hb - 0066
exact hr_witness_witness_witness_right_right_left - 0067
exact hr_witness_witness_witness_right_right_right_right - 0068
cases hrec - 0069
cases hrec_witness - 0070
cases hrec_witness_witness - 0071
cases hrec_witness_witness_witness - 0072
have hext : ∃ d. ∃ e. GIrreducibleFactorization(z,x3,d,e,S x6) - 0073
specialize gaussian_factorization_append_irreducible (x1) - 0074
specialize gaussian_factorization_append_irreducible (x3) - 0075
specialize gaussian_factorization_append_irreducible (x4) - 0076
specialize gaussian_factorization_append_irreducible (x5) - 0077
specialize gaussian_factorization_append_irreducible (x6) - 0078
specialize gaussian_factorization_append_irreducible (x) - 0079
specialize gaussian_factorization_append_irreducible (z) - 0080
apply gaussian_factorization_append_irreducible - 0081
exact hrec_witness_witness_witness_witness - 0082
exact hr_witness_witness_witness_left - 0083
specialize gaussian_multiply_commutative (x) - 0084
specialize gaussian_multiply_commutative (x1) - 0085
specialize gaussian_multiply_commutative (z) - 0086
apply gaussian_multiply_commutative - 0087
exact hr_witness_witness_witness_right_left - 0088
cases hext - 0089
cases hext_witness - 0090
exists (x3) - 0091
exists (x7) - 0092
exists (x8) - 0093
exists (S x6) - 0094
exact hext_witness_witness