Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ z. ZPairValid(z) → ¬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
gaussian_norm_exists · checked external prerequisitegaussian_irreducible_factorization_bounded_normle_refl · checked external prerequisite
Original expanded first-order statement
forall z. (exists ge_real_positive_factorization_domain ge_real_negative_factorization_domain ge_imaginary_positive_factorization_domain ge_imaginary_negative_factorization_domain. (exists ge_real_code_factorization_domaindecode ge_imaginary_code_factorization_domaindecode. (((z) = ((ge_real_code_factorization_domaindecode) + (ge_imaginary_code_factorization_domaindecode)) * S ((ge_real_code_factorization_domaindecode) + (ge_imaginary_code_factorization_domaindecode)) + ((ge_imaginary_code_factorization_domaindecode) + (ge_imaginary_code_factorization_domaindecode))) /\ (((((ge_real_code_factorization_domaindecode) = 2 * (ge_real_positive_factorization_domain) /\ (ge_real_negative_factorization_domain) = 0) \/ exists ge_signed_half_ge_factorization_domaindecode_real. (((ge_real_code_factorization_domaindecode) = 2 * ge_signed_half_ge_factorization_domaindecode_real + 1 /\ (ge_real_positive_factorization_domain) = 0) /\ (ge_real_negative_factorization_domain) = S ge_signed_half_ge_factorization_domaindecode_real))) /\ ((((ge_imaginary_code_factorization_domaindecode) = 2 * (ge_imaginary_positive_factorization_domain) /\ (ge_imaginary_negative_factorization_domain) = 0) \/ exists ge_signed_half_ge_factorization_domaindecode_imaginary. (((ge_imaginary_code_factorization_domaindecode) = 2 * ge_signed_half_ge_factorization_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_factorization_domain) = 0) /\ (ge_imaginary_negative_factorization_domain) = S ge_signed_half_ge_factorization_domaindecode_imaginary))))))) -> ~(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 16 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
16 script commands · 4 reading checkpoints · 1 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–3
02Establish hnL4–7
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.
03Separate the logical casesL8–8
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L8
cases hn
04Use earlier factsL9–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
specialize gaussian_irreducible_factorization_bounded_norm (x) - L10
specialize gaussian_irreducible_factorization_bounded_norm (z) - L11
specialize gaussian_irreducible_factorization_bounded_norm (x) - L12
apply gaussian_irreducible_factorization_bounded_norm - L13
specialize le_refl (x) - L14
apply le_refl - L15
exact hn_witness - L16
exact hz
Original defined command ledger · 16 lines
- 0001
intro z - 0002
intro hv - 0003
intro hz - 0004
have hn : ∃ N. GNorm(z,N) - 0005
specialize gaussian_norm_exists (z) - 0006
apply gaussian_norm_exists - 0007
exact hv - 0008
cases hn - 0009
specialize gaussian_irreducible_factorization_bounded_norm (x) - 0010
specialize gaussian_irreducible_factorization_bounded_norm (z) - 0011
specialize gaussian_irreducible_factorization_bounded_norm (x) - 0012
apply gaussian_irreducible_factorization_bounded_norm - 0013
specialize le_refl (x) - 0014
apply le_refl - 0015
exact hn_witness - 0016
exact hz