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. GUnit(z) → GIrreducibleFactorization(z,z,0,0,0)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall z. (exists gr_inverse_unit_factorization_input. (exists ge_first_rp_unit_factorization_inputidentity ge_first_rn_unit_factorization_inputidentity ge_first_ip_unit_factorization_inputidentity ge_first_in_unit_factorization_inputidentity ge_second_rp_unit_factorization_inputidentity ge_second_rn_unit_factorization_inputidentity ge_second_ip_unit_factorization_inputidentity ge_second_in_unit_factorization_inputidentity. ((exists ge_representation_real_code_unit_factorization_inputidentityfirst ge_representation_imaginary_code_unit_factorization_inputidentityfirst. (((z) = ((ge_representation_real_code_unit_factorization_inputidentityfirst) + (ge_representation_imaginary_code_unit_factorization_inputidentityfirst)) * S ((ge_representation_real_code_unit_factorization_inputidentityfirst) + (ge_representation_imaginary_code_unit_factorization_inputidentityfirst)) + ((ge_representation_imaginary_code_unit_factorization_inputidentityfirst) + (ge_representation_imaginary_code_unit_factorization_inputidentityfirst))) /\ ((exists ge_balance_positive_unit_factorization_inputidentityfirstreal ge_balance_negative_unit_factorization_inputidentityfirstreal. (((((ge_representation_real_code_unit_factorization_inputidentityfirst) = 2 * (ge_balance_positive_unit_factorization_inputidentityfirstreal) /\ (ge_balance_negative_unit_factorization_inputidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factorization_inputidentityfirstrealdecode. (((ge_representation_real_code_unit_factorization_inputidentityfirst) = 2 * ge_signed_half_unit_factorization_inputidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorization_inputidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factorization_inputidentityfirstreal) = S ge_signed_half_unit_factorization_inputidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factorization_inputidentity) + ge_balance_negative_unit_factorization_inputidentityfirstreal = (ge_first_rn_unit_factorization_inputidentity) + ge_balance_positive_unit_factorization_inputidentityfirstreal))) /\ (exists ge_balance_positive_unit_factorization_inputidentityfirstimaginary ge_balance_negative_unit_factorization_inputidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factorization_inputidentityfirst) = 2 * (ge_balance_positive_unit_factorization_inputidentityfirstimaginary) /\ (ge_balance_negative_unit_factorization_inputidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorization_inputidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorization_inputidentityfirst) = 2 * ge_signed_half_unit_factorization_inputidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorization_inputidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorization_inputidentityfirstimaginary) = S ge_signed_half_unit_factorization_inputidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorization_inputidentity) + ge_balance_negative_unit_factorization_inputidentityfirstimaginary = (ge_first_in_unit_factorization_inputidentity) + ge_balance_positive_unit_factorization_inputidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorization_inputidentitysecond ge_representation_imaginary_code_unit_factorization_inputidentitysecond. (((gr_inverse_unit_factorization_input) = ((ge_representation_real_code_unit_factorization_inputidentitysecond) + (ge_representation_imaginary_code_unit_factorization_inputidentitysecond)) * S ((ge_representation_real_code_unit_factorization_inputidentitysecond) + (ge_representation_imaginary_code_unit_factorization_inputidentitysecond)) + ((ge_representation_imaginary_code_unit_factorization_inputidentitysecond) + (ge_representation_imaginary_code_unit_factorization_inputidentitysecond))) /\ ((exists ge_balance_positive_unit_factorization_inputidentitysecondreal ge_balance_negative_unit_factorization_inputidentitysecondreal. (((((ge_representation_real_code_unit_factorization_inputidentitysecond) = 2 * (ge_balance_positive_unit_factorization_inputidentitysecondreal) /\ (ge_balance_negative_unit_factorization_inputidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factorization_inputidentitysecondrealdecode. (((ge_representation_real_code_unit_factorization_inputidentitysecond) = 2 * ge_signed_half_unit_factorization_inputidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factorization_inputidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factorization_inputidentitysecondreal) = S ge_signed_half_unit_factorization_inputidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factorization_inputidentity) + ge_balance_negative_unit_factorization_inputidentitysecondreal = (ge_second_rn_unit_factorization_inputidentity) + ge_balance_positive_unit_factorization_inputidentitysecondreal))) /\ (exists ge_balance_positive_unit_factorization_inputidentitysecondimaginary ge_balance_negative_unit_factorization_inputidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factorization_inputidentitysecond) = 2 * (ge_balance_positive_unit_factorization_inputidentitysecondimaginary) /\ (ge_balance_negative_unit_factorization_inputidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factorization_inputidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorization_inputidentitysecond) = 2 * ge_signed_half_unit_factorization_inputidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorization_inputidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factorization_inputidentitysecondimaginary) = S ge_signed_half_unit_factorization_inputidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factorization_inputidentity) + ge_balance_negative_unit_factorization_inputidentitysecondimaginary = (ge_second_in_unit_factorization_inputidentity) + ge_balance_positive_unit_factorization_inputidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorization_inputidentityoutput ge_representation_imaginary_code_unit_factorization_inputidentityoutput. (((6) = ((ge_representation_real_code_unit_factorization_inputidentityoutput) + (ge_representation_imaginary_code_unit_factorization_inputidentityoutput)) * S ((ge_representation_real_code_unit_factorization_inputidentityoutput) + (ge_representation_imaginary_code_unit_factorization_inputidentityoutput)) + ((ge_representation_imaginary_code_unit_factorization_inputidentityoutput) + (ge_representation_imaginary_code_unit_factorization_inputidentityoutput))) /\ ((exists ge_balance_positive_unit_factorization_inputidentityoutputreal ge_balance_negative_unit_factorization_inputidentityoutputreal. (((((ge_representation_real_code_unit_factorization_inputidentityoutput) = 2 * (ge_balance_positive_unit_factorization_inputidentityoutputreal) /\ (ge_balance_negative_unit_factorization_inputidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factorization_inputidentityoutputrealdecode. (((ge_representation_real_code_unit_factorization_inputidentityoutput) = 2 * ge_signed_half_unit_factorization_inputidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorization_inputidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factorization_inputidentityoutputreal) = S ge_signed_half_unit_factorization_inputidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorization_inputidentity) * (ge_second_rp_unit_factorization_inputidentity))) + (((ge_first_rn_unit_factorization_inputidentity) * (ge_second_rn_unit_factorization_inputidentity))))) + (((((ge_first_ip_unit_factorization_inputidentity) * (ge_second_in_unit_factorization_inputidentity))) + (((ge_first_in_unit_factorization_inputidentity) * (ge_second_ip_unit_factorization_inputidentity))))))) + ge_balance_negative_unit_factorization_inputidentityoutputreal = (((((((ge_first_rp_unit_factorization_inputidentity) * (ge_second_rn_unit_factorization_inputidentity))) + (((ge_first_rn_unit_factorization_inputidentity) * (ge_second_rp_unit_factorization_inputidentity))))) + (((((ge_first_ip_unit_factorization_inputidentity) * (ge_second_ip_unit_factorization_inputidentity))) + (((ge_first_in_unit_factorization_inputidentity) * (ge_second_in_unit_factorization_inputidentity))))))) + ge_balance_positive_unit_factorization_inputidentityoutputreal))) /\ (exists ge_balance_positive_unit_factorization_inputidentityoutputimaginary ge_balance_negative_unit_factorization_inputidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factorization_inputidentityoutput) = 2 * (ge_balance_positive_unit_factorization_inputidentityoutputimaginary) /\ (ge_balance_negative_unit_factorization_inputidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorization_inputidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorization_inputidentityoutput) = 2 * ge_signed_half_unit_factorization_inputidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorization_inputidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorization_inputidentityoutputimaginary) = S ge_signed_half_unit_factorization_inputidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorization_inputidentity) * (ge_second_ip_unit_factorization_inputidentity))) + (((ge_first_rn_unit_factorization_inputidentity) * (ge_second_in_unit_factorization_inputidentity))))) + (((((ge_first_ip_unit_factorization_inputidentity) * (ge_second_rp_unit_factorization_inputidentity))) + (((ge_first_in_unit_factorization_inputidentity) * (ge_second_rn_unit_factorization_inputidentity))))))) + ge_balance_negative_unit_factorization_inputidentityoutputimaginary = (((((((ge_first_rp_unit_factorization_inputidentity) * (ge_second_in_unit_factorization_inputidentity))) + (((ge_first_rn_unit_factorization_inputidentity) * (ge_second_ip_unit_factorization_inputidentity))))) + (((((ge_first_ip_unit_factorization_inputidentity) * (ge_second_rn_unit_factorization_inputidentity))) + (((ge_first_in_unit_factorization_inputidentity) * (ge_second_rp_unit_factorization_inputidentity))))))) + ge_balance_positive_unit_factorization_inputidentityoutputimaginary)))))))))) -> (((exists gr_inverse_unit_factorizationunit. (exists ge_first_rp_unit_factorizationunitidentity ge_first_rn_unit_factorizationunitidentity ge_first_ip_unit_factorizationunitidentity ge_first_in_unit_factorizationunitidentity ge_second_rp_unit_factorizationunitidentity ge_second_rn_unit_factorizationunitidentity ge_second_ip_unit_factorizationunitidentity ge_second_in_unit_factorizationunitidentity. ((exists ge_representation_real_code_unit_factorizationunitidentityfirst ge_representation_imaginary_code_unit_factorizationunitidentityfirst. (((z) = ((ge_representation_real_code_unit_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationunitidentityfirst)) * S ((ge_representation_real_code_unit_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationunitidentityfirst)) + ((ge_representation_imaginary_code_unit_factorizationunitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationunitidentityfirst))) /\ ((exists ge_balance_positive_unit_factorizationunitidentityfirstreal ge_balance_negative_unit_factorizationunitidentityfirstreal. (((((ge_representation_real_code_unit_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationunitidentityfirstreal) /\ (ge_balance_negative_unit_factorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationunitidentityfirstrealdecode. (((ge_representation_real_code_unit_factorizationunitidentityfirst) = 2 * ge_signed_half_unit_factorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationunitidentityfirstreal) = S ge_signed_half_unit_factorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationunitidentity) + ge_balance_negative_unit_factorizationunitidentityfirstreal = (ge_first_rn_unit_factorizationunitidentity) + ge_balance_positive_unit_factorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_unit_factorizationunitidentityfirstimaginary ge_balance_negative_unit_factorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationunitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationunitidentityfirstimaginary) /\ (ge_balance_negative_unit_factorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationunitidentityfirst) = 2 * ge_signed_half_unit_factorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationunitidentityfirstimaginary) = S ge_signed_half_unit_factorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationunitidentity) + ge_balance_negative_unit_factorizationunitidentityfirstimaginary = (ge_first_in_unit_factorizationunitidentity) + ge_balance_positive_unit_factorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationunitidentitysecond ge_representation_imaginary_code_unit_factorizationunitidentitysecond. (((gr_inverse_unit_factorizationunit) = ((ge_representation_real_code_unit_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationunitidentitysecond)) * S ((ge_representation_real_code_unit_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationunitidentitysecond)) + ((ge_representation_imaginary_code_unit_factorizationunitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationunitidentitysecond))) /\ ((exists ge_balance_positive_unit_factorizationunitidentitysecondreal ge_balance_negative_unit_factorizationunitidentitysecondreal. (((((ge_representation_real_code_unit_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationunitidentitysecondreal) /\ (ge_balance_negative_unit_factorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factorizationunitidentitysecondrealdecode. (((ge_representation_real_code_unit_factorizationunitidentitysecond) = 2 * ge_signed_half_unit_factorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factorizationunitidentitysecondreal) = S ge_signed_half_unit_factorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factorizationunitidentity) + ge_balance_negative_unit_factorizationunitidentitysecondreal = (ge_second_rn_unit_factorizationunitidentity) + ge_balance_positive_unit_factorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_unit_factorizationunitidentitysecondimaginary ge_balance_negative_unit_factorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationunitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationunitidentitysecondimaginary) /\ (ge_balance_negative_unit_factorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationunitidentitysecond) = 2 * ge_signed_half_unit_factorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationunitidentitysecondimaginary) = S ge_signed_half_unit_factorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationunitidentity) + ge_balance_negative_unit_factorizationunitidentitysecondimaginary = (ge_second_in_unit_factorizationunitidentity) + ge_balance_positive_unit_factorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationunitidentityoutput ge_representation_imaginary_code_unit_factorizationunitidentityoutput. (((6) = ((ge_representation_real_code_unit_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationunitidentityoutput)) * S ((ge_representation_real_code_unit_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationunitidentityoutput)) + ((ge_representation_imaginary_code_unit_factorizationunitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationunitidentityoutput))) /\ ((exists ge_balance_positive_unit_factorizationunitidentityoutputreal ge_balance_negative_unit_factorizationunitidentityoutputreal. (((((ge_representation_real_code_unit_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationunitidentityoutputreal) /\ (ge_balance_negative_unit_factorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationunitidentityoutputrealdecode. (((ge_representation_real_code_unit_factorizationunitidentityoutput) = 2 * ge_signed_half_unit_factorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationunitidentityoutputreal) = S ge_signed_half_unit_factorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationunitidentity) * (ge_second_rp_unit_factorizationunitidentity))) + (((ge_first_rn_unit_factorizationunitidentity) * (ge_second_rn_unit_factorizationunitidentity))))) + (((((ge_first_ip_unit_factorizationunitidentity) * (ge_second_in_unit_factorizationunitidentity))) + (((ge_first_in_unit_factorizationunitidentity) * (ge_second_ip_unit_factorizationunitidentity))))))) + ge_balance_negative_unit_factorizationunitidentityoutputreal = (((((((ge_first_rp_unit_factorizationunitidentity) * (ge_second_rn_unit_factorizationunitidentity))) + (((ge_first_rn_unit_factorizationunitidentity) * (ge_second_rp_unit_factorizationunitidentity))))) + (((((ge_first_ip_unit_factorizationunitidentity) * (ge_second_ip_unit_factorizationunitidentity))) + (((ge_first_in_unit_factorizationunitidentity) * (ge_second_in_unit_factorizationunitidentity))))))) + ge_balance_positive_unit_factorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_unit_factorizationunitidentityoutputimaginary ge_balance_negative_unit_factorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationunitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationunitidentityoutputimaginary) /\ (ge_balance_negative_unit_factorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationunitidentityoutput) = 2 * ge_signed_half_unit_factorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationunitidentityoutputimaginary) = S ge_signed_half_unit_factorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationunitidentity) * (ge_second_ip_unit_factorizationunitidentity))) + (((ge_first_rn_unit_factorizationunitidentity) * (ge_second_in_unit_factorizationunitidentity))))) + (((((ge_first_ip_unit_factorizationunitidentity) * (ge_second_rp_unit_factorizationunitidentity))) + (((ge_first_in_unit_factorizationunitidentity) * (ge_second_rn_unit_factorizationunitidentity))))))) + ge_balance_negative_unit_factorizationunitidentityoutputimaginary = (((((((ge_first_rp_unit_factorizationunitidentity) * (ge_second_in_unit_factorizationunitidentity))) + (((ge_first_rn_unit_factorizationunitidentity) * (ge_second_ip_unit_factorizationunitidentity))))) + (((((ge_first_ip_unit_factorizationunitidentity) * (ge_second_rn_unit_factorizationunitidentity))) + (((ge_first_in_unit_factorizationunitidentity) * (ge_second_rp_unit_factorizationunitidentity))))))) + ge_balance_positive_unit_factorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_unit_factorizationirreducible gr_factor_value_unit_factorizationirreducible. (exists ge_gap_unit_factorizationirreducibleindex. ge_gap_unit_factorizationirreducibleindex + S (gr_factor_index_unit_factorizationirreducible) = (0)) -> (((exists ff_h_gprod_unit_factorizationirreducibleentry. ff_h_gprod_unit_factorizationirreducibleentry + S (gr_factor_value_unit_factorizationirreducible) = S ((S (gr_factor_index_unit_factorizationirreducible)) * 0)) /\ exists ff_q_gprod_unit_factorizationirreducibleentry. 0 = ff_q_gprod_unit_factorizationirreducibleentry * S ((S (gr_factor_index_unit_factorizationirreducible)) * 0) + (gr_factor_value_unit_factorizationirreducible))) -> (((exists ge_real_positive_unit_factorizationirreducibleirreduciblecarrier ge_real_negative_unit_factorizationirreducibleirreduciblecarrier ge_imaginary_positive_unit_factorizationirreducibleirreduciblecarrier ge_imaginary_negative_unit_factorizationirreducibleirreduciblecarrier. (exists ge_real_code_unit_factorizationirreducibleirreduciblecarrierdecode ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode. (((gr_factor_value_unit_factorizationirreducible) = ((ge_real_code_unit_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_unit_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_unit_factorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_unit_factorizationirreducibleirreduciblecarrier) /\ (ge_real_negative_unit_factorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unit_factorizationirreducibleirreduciblecarrierdecode_real. (((ge_real_code_unit_factorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unit_factorizationirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_unit_factorizationirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_unit_factorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_unit_factorizationirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_unit_factorizationirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_unit_factorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_unit_factorizationirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_unit_factorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_unit_factorizationirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_unit_factorizationirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_unit_factorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_unit_factorizationirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_unit_factorizationirreducible)=0)) /\ ((~(exists gr_inverse_unit_factorizationirreducibleirreduciblenonunit. (exists ge_first_rp_unit_factorizationirreducibleirreduciblenonunitidentity ge_first_rn_unit_factorizationirreducibleirreduciblenonunitidentity ge_first_ip_unit_factorizationirreducibleirreduciblenonunitidentity ge_first_in_unit_factorizationirreducibleirreduciblenonunitidentity ge_second_rp_unit_factorizationirreducibleirreduciblenonunitidentity ge_second_rn_unit_factorizationirreducibleirreduciblenonunitidentity ge_second_ip_unit_factorizationirreducibleirreduciblenonunitidentity ge_second_in_unit_factorizationirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_unit_factorizationirreducible) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_unit_factorizationirreducibleirreduciblenonunit) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_unit_factorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_unit_factorizationirreducibleirreducible gr_second_factor_unit_factorizationirreducibleirreducible. (exists ge_first_rp_unit_factorizationirreducibleirreduciblefactorization ge_first_rn_unit_factorizationirreducibleirreduciblefactorization ge_first_ip_unit_factorizationirreducibleirreduciblefactorization ge_first_in_unit_factorizationirreducibleirreduciblefactorization ge_second_rp_unit_factorizationirreducibleirreduciblefactorization ge_second_rn_unit_factorizationirreducibleirreduciblefactorization ge_second_ip_unit_factorizationirreducibleirreduciblefactorization ge_second_in_unit_factorizationirreducibleirreduciblefactorization. ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst. (((gr_first_factor_unit_factorizationirreducibleirreducible) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstreal ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond. (((gr_second_factor_unit_factorizationirreducibleirreducible) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondreal ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_unit_factorizationirreducibleirreduciblefactorization) + ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput. (((gr_factor_value_unit_factorizationirreducible) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputreal ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unit_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unit_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unit_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unit_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unit_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unit_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_in_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_ip_unit_factorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rn_unit_factorizationirreducibleirreduciblefactorization))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefactorization) * (ge_second_rp_unit_factorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_unit_factorizationirreducibleirreduciblefirst_unit. (exists ge_first_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_first_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_first_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_first_in_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_second_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_second_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_second_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity ge_second_in_unit_factorizationirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_unit_factorizationirreducibleirreducible) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_unit_factorizationirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_unit_factorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_unit_factorizationirreducibleirreduciblesecond_unit. (exists ge_first_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_first_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_first_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_first_in_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_second_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_second_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_second_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity ge_second_in_unit_factorizationirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_unit_factorizationirreducibleirreducible) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_unit_factorizationirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_unit_factorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_unit_factorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_unit_factorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_unit_factorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_unit_factorizationirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_unit_factorization. ((exists gr_product_trace_unit_factorizationtrace gr_product_scale_unit_factorizationtrace. ((((exists ff_h_gprod_unit_factorizationtracestart. ff_h_gprod_unit_factorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_unit_factorizationtrace)) /\ exists ff_q_gprod_unit_factorizationtracestart. gr_product_trace_unit_factorizationtrace = ff_q_gprod_unit_factorizationtracestart * S ((S (0)) * gr_product_scale_unit_factorizationtrace) + (6))) /\ ((((exists ff_h_gprod_unit_factorizationtraceend. ff_h_gprod_unit_factorizationtraceend + S (gr_factor_product_unit_factorization) = S ((S (0)) * gr_product_scale_unit_factorizationtrace)) /\ exists ff_q_gprod_unit_factorizationtraceend. gr_product_trace_unit_factorizationtrace = ff_q_gprod_unit_factorizationtraceend * S ((S (0)) * gr_product_scale_unit_factorizationtrace) + (gr_factor_product_unit_factorization))) /\ (forall gr_product_index_unit_factorizationtracesteps. (exists ge_gap_unit_factorizationtracestepsindex_bound. ge_gap_unit_factorizationtracestepsindex_bound + S (gr_product_index_unit_factorizationtracesteps) = (0)) -> exists gr_product_factor_unit_factorizationtracesteps gr_product_before_unit_factorizationtracesteps gr_product_after_unit_factorizationtracesteps. ((((exists ff_h_gprod_unit_factorizationtracestepsfactor. ff_h_gprod_unit_factorizationtracestepsfactor + S (gr_product_factor_unit_factorizationtracesteps) = S ((S (gr_product_index_unit_factorizationtracesteps)) * 0)) /\ exists ff_q_gprod_unit_factorizationtracestepsfactor. 0 = ff_q_gprod_unit_factorizationtracestepsfactor * S ((S (gr_product_index_unit_factorizationtracesteps)) * 0) + (gr_product_factor_unit_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unit_factorizationtracestepsbefore. ff_h_gprod_unit_factorizationtracestepsbefore + S (gr_product_before_unit_factorizationtracesteps) = S ((S (gr_product_index_unit_factorizationtracesteps)) * gr_product_scale_unit_factorizationtrace)) /\ exists ff_q_gprod_unit_factorizationtracestepsbefore. gr_product_trace_unit_factorizationtrace = ff_q_gprod_unit_factorizationtracestepsbefore * S ((S (gr_product_index_unit_factorizationtracesteps)) * gr_product_scale_unit_factorizationtrace) + (gr_product_before_unit_factorizationtracesteps))) /\ ((((exists ff_h_gprod_unit_factorizationtracestepsafter. ff_h_gprod_unit_factorizationtracestepsafter + S (gr_product_after_unit_factorizationtracesteps) = S ((S (S (gr_product_index_unit_factorizationtracesteps))) * gr_product_scale_unit_factorizationtrace)) /\ exists ff_q_gprod_unit_factorizationtracestepsafter. gr_product_trace_unit_factorizationtrace = ff_q_gprod_unit_factorizationtracestepsafter * S ((S (S (gr_product_index_unit_factorizationtracesteps))) * gr_product_scale_unit_factorizationtrace) + (gr_product_after_unit_factorizationtracesteps))) /\ (exists ge_first_rp_unit_factorizationtracestepsmultiply ge_first_rn_unit_factorizationtracestepsmultiply ge_first_ip_unit_factorizationtracestepsmultiply ge_first_in_unit_factorizationtracestepsmultiply ge_second_rp_unit_factorizationtracestepsmultiply ge_second_rn_unit_factorizationtracestepsmultiply ge_second_ip_unit_factorizationtracestepsmultiply ge_second_in_unit_factorizationtracestepsmultiply. ((exists ge_representation_real_code_unit_factorizationtracestepsmultiplyfirst ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst. (((gr_product_before_unit_factorizationtracesteps) = ((ge_representation_real_code_unit_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_unit_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_unit_factorizationtracestepsmultiplyfirstreal ge_balance_negative_unit_factorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_unit_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unit_factorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_unit_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unit_factorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyfirstreal) = S ge_signed_half_unit_factorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationtracestepsmultiply) + ge_balance_negative_unit_factorizationtracestepsmultiplyfirstreal = (ge_first_rn_unit_factorizationtracestepsmultiply) + ge_balance_positive_unit_factorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_unit_factorizationtracestepsmultiplyfirstimaginary ge_balance_negative_unit_factorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_unit_factorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_unit_factorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_unit_factorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationtracestepsmultiply) + ge_balance_negative_unit_factorizationtracestepsmultiplyfirstimaginary = (ge_first_in_unit_factorizationtracestepsmultiply) + ge_balance_positive_unit_factorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationtracestepsmultiplysecond ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond. (((gr_product_factor_unit_factorizationtracesteps) = ((ge_representation_real_code_unit_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_unit_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_unit_factorizationtracestepsmultiplysecondreal ge_balance_negative_unit_factorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_unit_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unit_factorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_unit_factorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_unit_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unit_factorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplysecondreal) = S ge_signed_half_unit_factorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_unit_factorizationtracestepsmultiply) + ge_balance_negative_unit_factorizationtracestepsmultiplysecondreal = (ge_second_rn_unit_factorizationtracestepsmultiply) + ge_balance_positive_unit_factorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_unit_factorizationtracestepsmultiplysecondimaginary ge_balance_negative_unit_factorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_unit_factorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplysecond) = 2 * ge_signed_half_unit_factorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_unit_factorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationtracestepsmultiply) + ge_balance_negative_unit_factorizationtracestepsmultiplysecondimaginary = (ge_second_in_unit_factorizationtracestepsmultiply) + ge_balance_positive_unit_factorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationtracestepsmultiplyoutput ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput. (((gr_product_after_unit_factorizationtracesteps) = ((ge_representation_real_code_unit_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_unit_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_unit_factorizationtracestepsmultiplyoutputreal ge_balance_negative_unit_factorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_unit_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unit_factorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_unit_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unit_factorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyoutputreal) = S ge_signed_half_unit_factorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationtracestepsmultiply) * (ge_second_rp_unit_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_factorizationtracestepsmultiply) * (ge_second_rn_unit_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_factorizationtracestepsmultiply) * (ge_second_in_unit_factorizationtracestepsmultiply))) + (((ge_first_in_unit_factorizationtracestepsmultiply) * (ge_second_ip_unit_factorizationtracestepsmultiply))))))) + ge_balance_negative_unit_factorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_unit_factorizationtracestepsmultiply) * (ge_second_rn_unit_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_factorizationtracestepsmultiply) * (ge_second_rp_unit_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_factorizationtracestepsmultiply) * (ge_second_ip_unit_factorizationtracestepsmultiply))) + (((ge_first_in_unit_factorizationtracestepsmultiply) * (ge_second_in_unit_factorizationtracestepsmultiply))))))) + ge_balance_positive_unit_factorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_unit_factorizationtracestepsmultiplyoutputimaginary ge_balance_negative_unit_factorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_unit_factorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_unit_factorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_unit_factorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationtracestepsmultiply) * (ge_second_ip_unit_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_factorizationtracestepsmultiply) * (ge_second_in_unit_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_factorizationtracestepsmultiply) * (ge_second_rp_unit_factorizationtracestepsmultiply))) + (((ge_first_in_unit_factorizationtracestepsmultiply) * (ge_second_rn_unit_factorizationtracestepsmultiply))))))) + ge_balance_negative_unit_factorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_unit_factorizationtracestepsmultiply) * (ge_second_in_unit_factorizationtracestepsmultiply))) + (((ge_first_rn_unit_factorizationtracestepsmultiply) * (ge_second_ip_unit_factorizationtracestepsmultiply))))) + (((((ge_first_ip_unit_factorizationtracestepsmultiply) * (ge_second_rn_unit_factorizationtracestepsmultiply))) + (((ge_first_in_unit_factorizationtracestepsmultiply) * (ge_second_rp_unit_factorizationtracestepsmultiply))))))) + ge_balance_positive_unit_factorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_unit_factorizationreconstruct ge_first_rn_unit_factorizationreconstruct ge_first_ip_unit_factorizationreconstruct ge_first_in_unit_factorizationreconstruct ge_second_rp_unit_factorizationreconstruct ge_second_rn_unit_factorizationreconstruct ge_second_ip_unit_factorizationreconstruct ge_second_in_unit_factorizationreconstruct. ((exists ge_representation_real_code_unit_factorizationreconstructfirst ge_representation_imaginary_code_unit_factorizationreconstructfirst. (((z) = ((ge_representation_real_code_unit_factorizationreconstructfirst) + (ge_representation_imaginary_code_unit_factorizationreconstructfirst)) * S ((ge_representation_real_code_unit_factorizationreconstructfirst) + (ge_representation_imaginary_code_unit_factorizationreconstructfirst)) + ((ge_representation_imaginary_code_unit_factorizationreconstructfirst) + (ge_representation_imaginary_code_unit_factorizationreconstructfirst))) /\ ((exists ge_balance_positive_unit_factorizationreconstructfirstreal ge_balance_negative_unit_factorizationreconstructfirstreal. (((((ge_representation_real_code_unit_factorizationreconstructfirst) = 2 * (ge_balance_positive_unit_factorizationreconstructfirstreal) /\ (ge_balance_negative_unit_factorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_unit_factorizationreconstructfirstrealdecode. (((ge_representation_real_code_unit_factorizationreconstructfirst) = 2 * ge_signed_half_unit_factorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_unit_factorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_unit_factorizationreconstructfirstreal) = S ge_signed_half_unit_factorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_unit_factorizationreconstruct) + ge_balance_negative_unit_factorizationreconstructfirstreal = (ge_first_rn_unit_factorizationreconstruct) + ge_balance_positive_unit_factorizationreconstructfirstreal))) /\ (exists ge_balance_positive_unit_factorizationreconstructfirstimaginary ge_balance_negative_unit_factorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_unit_factorizationreconstructfirst) = 2 * (ge_balance_positive_unit_factorizationreconstructfirstimaginary) /\ (ge_balance_negative_unit_factorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_unit_factorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationreconstructfirst) = 2 * ge_signed_half_unit_factorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_unit_factorizationreconstructfirstimaginary) = S ge_signed_half_unit_factorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_unit_factorizationreconstruct) + ge_balance_negative_unit_factorizationreconstructfirstimaginary = (ge_first_in_unit_factorizationreconstruct) + ge_balance_positive_unit_factorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factorizationreconstructsecond ge_representation_imaginary_code_unit_factorizationreconstructsecond. (((gr_factor_product_unit_factorization) = ((ge_representation_real_code_unit_factorizationreconstructsecond) + (ge_representation_imaginary_code_unit_factorizationreconstructsecond)) * S ((ge_representation_real_code_unit_factorizationreconstructsecond) + (ge_representation_imaginary_code_unit_factorizationreconstructsecond)) + ((ge_representation_imaginary_code_unit_factorizationreconstructsecond) + (ge_representation_imaginary_code_unit_factorizationreconstructsecond))) /\ ((exists ge_balance_positive_unit_factorizationreconstructsecondreal ge_balance_negative_unit_factorizationreconstructsecondreal. (((((ge_representation_real_code_unit_factorizationreconstructsecond) = 2 * (ge_balance_positive_unit_factorizationreconstructsecondreal) /\ (ge_balance_negative_unit_factorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_unit_factorizationreconstructsecondrealdecode. (((ge_representation_real_code_unit_factorizationreconstructsecond) = 2 * ge_signed_half_unit_factorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_unit_factorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_unit_factorizationreconstructsecondreal) = S ge_signed_half_unit_factorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_unit_factorizationreconstruct) + ge_balance_negative_unit_factorizationreconstructsecondreal = (ge_second_rn_unit_factorizationreconstruct) + ge_balance_positive_unit_factorizationreconstructsecondreal))) /\ (exists ge_balance_positive_unit_factorizationreconstructsecondimaginary ge_balance_negative_unit_factorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_unit_factorizationreconstructsecond) = 2 * (ge_balance_positive_unit_factorizationreconstructsecondimaginary) /\ (ge_balance_negative_unit_factorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_unit_factorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationreconstructsecond) = 2 * ge_signed_half_unit_factorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_unit_factorizationreconstructsecondimaginary) = S ge_signed_half_unit_factorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_unit_factorizationreconstruct) + ge_balance_negative_unit_factorizationreconstructsecondimaginary = (ge_second_in_unit_factorizationreconstruct) + ge_balance_positive_unit_factorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factorizationreconstructoutput ge_representation_imaginary_code_unit_factorizationreconstructoutput. (((z) = ((ge_representation_real_code_unit_factorizationreconstructoutput) + (ge_representation_imaginary_code_unit_factorizationreconstructoutput)) * S ((ge_representation_real_code_unit_factorizationreconstructoutput) + (ge_representation_imaginary_code_unit_factorizationreconstructoutput)) + ((ge_representation_imaginary_code_unit_factorizationreconstructoutput) + (ge_representation_imaginary_code_unit_factorizationreconstructoutput))) /\ ((exists ge_balance_positive_unit_factorizationreconstructoutputreal ge_balance_negative_unit_factorizationreconstructoutputreal. (((((ge_representation_real_code_unit_factorizationreconstructoutput) = 2 * (ge_balance_positive_unit_factorizationreconstructoutputreal) /\ (ge_balance_negative_unit_factorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_unit_factorizationreconstructoutputrealdecode. (((ge_representation_real_code_unit_factorizationreconstructoutput) = 2 * ge_signed_half_unit_factorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_unit_factorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_unit_factorizationreconstructoutputreal) = S ge_signed_half_unit_factorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factorizationreconstruct) * (ge_second_rp_unit_factorizationreconstruct))) + (((ge_first_rn_unit_factorizationreconstruct) * (ge_second_rn_unit_factorizationreconstruct))))) + (((((ge_first_ip_unit_factorizationreconstruct) * (ge_second_in_unit_factorizationreconstruct))) + (((ge_first_in_unit_factorizationreconstruct) * (ge_second_ip_unit_factorizationreconstruct))))))) + ge_balance_negative_unit_factorizationreconstructoutputreal = (((((((ge_first_rp_unit_factorizationreconstruct) * (ge_second_rn_unit_factorizationreconstruct))) + (((ge_first_rn_unit_factorizationreconstruct) * (ge_second_rp_unit_factorizationreconstruct))))) + (((((ge_first_ip_unit_factorizationreconstruct) * (ge_second_ip_unit_factorizationreconstruct))) + (((ge_first_in_unit_factorizationreconstruct) * (ge_second_in_unit_factorizationreconstruct))))))) + ge_balance_positive_unit_factorizationreconstructoutputreal))) /\ (exists ge_balance_positive_unit_factorizationreconstructoutputimaginary ge_balance_negative_unit_factorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_unit_factorizationreconstructoutput) = 2 * (ge_balance_positive_unit_factorizationreconstructoutputimaginary) /\ (ge_balance_negative_unit_factorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_unit_factorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factorizationreconstructoutput) = 2 * ge_signed_half_unit_factorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_unit_factorizationreconstructoutputimaginary) = S ge_signed_half_unit_factorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factorizationreconstruct) * (ge_second_ip_unit_factorizationreconstruct))) + (((ge_first_rn_unit_factorizationreconstruct) * (ge_second_in_unit_factorizationreconstruct))))) + (((((ge_first_ip_unit_factorizationreconstruct) * (ge_second_rp_unit_factorizationreconstruct))) + (((ge_first_in_unit_factorizationreconstruct) * (ge_second_rn_unit_factorizationreconstruct))))))) + ge_balance_negative_unit_factorizationreconstructoutputimaginary = (((((((ge_first_rp_unit_factorizationreconstruct) * (ge_second_in_unit_factorizationreconstruct))) + (((ge_first_rn_unit_factorizationreconstruct) * (ge_second_ip_unit_factorizationreconstruct))))) + (((((ge_first_ip_unit_factorizationreconstruct) * (ge_second_rn_unit_factorizationreconstruct))) + (((ge_first_in_unit_factorizationreconstruct) * (ge_second_rp_unit_factorizationreconstruct))))))) + ge_balance_positive_unit_factorizationreconstructoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 23 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
23 script commands · 10 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (4)
01Fix variables and assumptionsL1–2
02Separate the logical casesL3–3
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L3
split
03Use earlier factsL4–4
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L4
exact hu
04Separate the logical casesL5–5
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L5
split
05Fix variables and assumptionsL6–9
06Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
exfalso
07Use earlier factsL11–13
08Construct an explicit witnessL14–14
Supply the displayed value, then prove that it has the required property.
- L14
exists (6)
09Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
10Use earlier factsL16–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 23 lines
- 0001
intro z - 0002
intro hu - 0003
split - 0004
exact hu - 0005
split - 0006
intro i - 0007
intro p - 0008
intro hi - 0009
intro hp - 0010
exfalso - 0011
specialize gaussian_search_no_index_below_zero (i) - 0012
apply gaussian_search_no_index_below_zero - 0013
exact hi - 0014
exists (6) - 0015
split - 0016
specialize gaussian_product_empty_exists (0) - 0017
specialize gaussian_product_empty_exists (0) - 0018
apply gaussian_product_empty_exists - 0019
specialize gaussian_multiply_one_right (z) - 0020
apply gaussian_multiply_one_right - 0021
specialize gaussian_unit_valid (z) - 0022
apply gaussian_unit_valid - 0023
exact hu