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.
Definition in prerequisite notation
GUnit(u) ∧ (GAllIrreducible(b,c,l) ∧ (∃ x. GProduct(b,c,l,x) ∧ GMul(u,x,z)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((exists gr_inverse_gaussianfactorizationunit. (exists ge_first_rp_gaussianfactorizationunitidentity ge_first_rn_gaussianfactorizationunitidentity ge_first_ip_gaussianfactorizationunitidentity ge_first_in_gaussianfactorizationunitidentity ge_second_rp_gaussianfactorizationunitidentity ge_second_rn_gaussianfactorizationunitidentity ge_second_ip_gaussianfactorizationunitidentity ge_second_in_gaussianfactorizationunitidentity. ((exists ge_representation_real_code_gaussianfactorizationunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst. ((((u)) = ((ge_representation_real_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentityfirstreal ge_balance_negative_gaussianfactorizationunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentityfirstreal = (ge_first_rn_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond. (((gr_inverse_gaussianfactorizationunit) = ((ge_representation_real_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentitysecondreal ge_balance_negative_gaussianfactorizationunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentitysecondreal = (ge_second_rn_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentityoutputreal ge_balance_negative_gaussianfactorizationunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))))))) + ge_balance_negative_gaussianfactorizationunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))))))) + ge_balance_positive_gaussianfactorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))))))) + ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))))))) + ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_gaussianfactorizationirreducible gr_factor_value_gaussianfactorizationirreducible. (exists ge_gap_gaussianfactorizationirreducibleindex. ge_gap_gaussianfactorizationirreducibleindex + S (gr_factor_index_gaussianfactorizationirreducible) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationirreducibleentry. ff_h_gprod_gaussianfactorizationirreducibleentry + S (gr_factor_value_gaussianfactorizationirreducible) = S ((S (gr_factor_index_gaussianfactorizationirreducible)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationirreducibleentry. (b) = ff_q_gprod_gaussianfactorizationirreducibleentry * S ((S (gr_factor_index_gaussianfactorizationirreducible)) * (c)) + (gr_factor_value_gaussianfactorizationirreducible))) -> (((exists ge_real_positive_gaussianfactorizationirreducibleirreduciblecarrier ge_real_negative_gaussianfactorizationirreducibleirreduciblecarrier ge_imaginary_positive_gaussianfactorizationirreducibleirreduciblecarrier ge_imaginary_negative_gaussianfactorizationirreducibleirreduciblecarrier. (exists ge_real_code_gaussianfactorizationirreducibleirreduciblecarrierdecode ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode. (((gr_factor_value_gaussianfactorizationirreducible) = ((ge_real_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_gaussianfactorizationirreducibleirreduciblecarrier) /\ (ge_real_negative_gaussianfactorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationirreducibleirreduciblecarrierdecode_real. (((ge_real_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_gaussianfactorizationirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_gaussianfactorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_gaussianfactorizationirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_gaussianfactorizationirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_gaussianfactorizationirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_gaussianfactorizationirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_gaussianfactorizationirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_gaussianfactorizationirreducibleirreduciblecarrier) = S ge_signed_half_ge_gaussianfactorizationirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_gaussianfactorizationirreducible)=0)) /\ ((~(exists gr_inverse_gaussianfactorizationirreducibleirreduciblenonunit. (exists ge_first_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_first_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_first_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_first_in_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_second_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_second_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_second_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity ge_second_in_gaussianfactorizationirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_gaussianfactorizationirreducible) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_gaussianfactorizationirreducibleirreduciblenonunit) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationirreducibleirreduciblenonunitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblenonunitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblenonunitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_gaussianfactorizationirreducibleirreducible gr_second_factor_gaussianfactorizationirreducibleirreducible. (exists ge_first_rp_gaussianfactorizationirreducibleirreduciblefactorization ge_first_rn_gaussianfactorizationirreducibleirreduciblefactorization ge_first_ip_gaussianfactorizationirreducibleirreduciblefactorization ge_first_in_gaussianfactorizationirreducibleirreduciblefactorization ge_second_rp_gaussianfactorizationirreducibleirreduciblefactorization ge_second_rn_gaussianfactorizationirreducibleirreduciblefactorization ge_second_ip_gaussianfactorizationirreducibleirreduciblefactorization ge_second_in_gaussianfactorizationirreducibleirreduciblefactorization. ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst. (((gr_first_factor_gaussianfactorizationirreducibleirreducible) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond. (((gr_second_factor_gaussianfactorizationirreducibleirreducible) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_gaussianfactorizationirreducibleirreduciblefactorization) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput. (((gr_factor_value_gaussianfactorizationirreducible) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefactorization))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefactorization))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefactorization))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefactorization) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefactorization))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_gaussianfactorizationirreducibleirreduciblefirst_unit. (exists ge_first_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_first_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_first_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_first_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_second_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_second_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_second_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity ge_second_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_gaussianfactorizationirreducibleirreducible) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_gaussianfactorizationirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_gaussianfactorizationirreducibleirreduciblesecond_unit. (exists ge_first_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_first_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_first_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_first_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_second_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_second_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_second_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity ge_second_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_gaussianfactorizationirreducibleirreducible) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_gaussianfactorizationirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_gaussianfactorizationirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_gaussianfactorizationirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_gaussianfactorizationirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_gaussianfactorization. ((exists gr_product_trace_gaussianfactorizationtrace gr_product_scale_gaussianfactorizationtrace. ((((exists ff_h_gprod_gaussianfactorizationtracestart. ff_h_gprod_gaussianfactorizationtracestart + S (6) = S ((S (0)) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtracestart. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtracestart * S ((S (0)) * gr_product_scale_gaussianfactorizationtrace) + (6))) /\ ((((exists ff_h_gprod_gaussianfactorizationtraceend. ff_h_gprod_gaussianfactorizationtraceend + S (gr_factor_product_gaussianfactorization) = S ((S ((l))) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtraceend. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtraceend * S ((S ((l))) * gr_product_scale_gaussianfactorizationtrace) + (gr_factor_product_gaussianfactorization))) /\ (forall gr_product_index_gaussianfactorizationtracesteps. (exists ge_gap_gaussianfactorizationtracestepsindex_bound. ge_gap_gaussianfactorizationtracestepsindex_bound + S (gr_product_index_gaussianfactorizationtracesteps) = ((l))) -> exists gr_product_factor_gaussianfactorizationtracesteps gr_product_before_gaussianfactorizationtracesteps gr_product_after_gaussianfactorizationtracesteps. ((((exists ff_h_gprod_gaussianfactorizationtracestepsfactor. ff_h_gprod_gaussianfactorizationtracestepsfactor + S (gr_product_factor_gaussianfactorizationtracesteps) = S ((S (gr_product_index_gaussianfactorizationtracesteps)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationtracestepsfactor. (b) = ff_q_gprod_gaussianfactorizationtracestepsfactor * S ((S (gr_product_index_gaussianfactorizationtracesteps)) * (c)) + (gr_product_factor_gaussianfactorizationtracesteps))) /\ ((((exists ff_h_gprod_gaussianfactorizationtracestepsbefore. ff_h_gprod_gaussianfactorizationtracestepsbefore + S (gr_product_before_gaussianfactorizationtracesteps) = S ((S (gr_product_index_gaussianfactorizationtracesteps)) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtracestepsbefore. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtracestepsbefore * S ((S (gr_product_index_gaussianfactorizationtracesteps)) * gr_product_scale_gaussianfactorizationtrace) + (gr_product_before_gaussianfactorizationtracesteps))) /\ ((((exists ff_h_gprod_gaussianfactorizationtracestepsafter. ff_h_gprod_gaussianfactorizationtracestepsafter + S (gr_product_after_gaussianfactorizationtracesteps) = S ((S (S (gr_product_index_gaussianfactorizationtracesteps))) * gr_product_scale_gaussianfactorizationtrace)) /\ exists ff_q_gprod_gaussianfactorizationtracestepsafter. gr_product_trace_gaussianfactorizationtrace = ff_q_gprod_gaussianfactorizationtracestepsafter * S ((S (S (gr_product_index_gaussianfactorizationtracesteps))) * gr_product_scale_gaussianfactorizationtrace) + (gr_product_after_gaussianfactorizationtracesteps))) /\ (exists ge_first_rp_gaussianfactorizationtracestepsmultiply ge_first_rn_gaussianfactorizationtracestepsmultiply ge_first_ip_gaussianfactorizationtracestepsmultiply ge_first_in_gaussianfactorizationtracestepsmultiply ge_second_rp_gaussianfactorizationtracestepsmultiply ge_second_rn_gaussianfactorizationtracestepsmultiply ge_second_ip_gaussianfactorizationtracestepsmultiply ge_second_in_gaussianfactorizationtracestepsmultiply. ((exists ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst. (((gr_product_before_gaussianfactorizationtracesteps) = ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst)) * S ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal. (((((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstreal = (ge_first_rn_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyfirst) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyfirstimaginary = (ge_first_in_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond. (((gr_product_factor_gaussianfactorizationtracesteps) = ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond)) * S ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal. (((((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal) = S ge_signed_half_gaussianfactorizationtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondreal = (ge_second_rn_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplysecond) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary) = S ge_signed_half_gaussianfactorizationtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationtracestepsmultiply) + ge_balance_negative_gaussianfactorizationtracestepsmultiplysecondimaginary = (ge_second_in_gaussianfactorizationtracestepsmultiply) + ge_balance_positive_gaussianfactorizationtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput. (((gr_product_after_gaussianfactorizationtracesteps) = ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput)) * S ((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput) + (ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal. (((((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputreal = (((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtracestepsmultiplyoutput) = 2 * ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary) = S ge_signed_half_gaussianfactorizationtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_negative_gaussianfactorizationtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_gaussianfactorizationtracestepsmultiply) * (ge_second_in_gaussianfactorizationtracestepsmultiply))) + (((ge_first_rn_gaussianfactorizationtracestepsmultiply) * (ge_second_ip_gaussianfactorizationtracestepsmultiply))))) + (((((ge_first_ip_gaussianfactorizationtracestepsmultiply) * (ge_second_rn_gaussianfactorizationtracestepsmultiply))) + (((ge_first_in_gaussianfactorizationtracestepsmultiply) * (ge_second_rp_gaussianfactorizationtracestepsmultiply))))))) + ge_balance_positive_gaussianfactorizationtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_gaussianfactorizationreconstruct ge_first_rn_gaussianfactorizationreconstruct ge_first_ip_gaussianfactorizationreconstruct ge_first_in_gaussianfactorizationreconstruct ge_second_rp_gaussianfactorizationreconstruct ge_second_rn_gaussianfactorizationreconstruct ge_second_ip_gaussianfactorizationreconstruct ge_second_in_gaussianfactorizationreconstruct. ((exists ge_representation_real_code_gaussianfactorizationreconstructfirst ge_representation_imaginary_code_gaussianfactorizationreconstructfirst. ((((u)) = ((ge_representation_real_code_gaussianfactorizationreconstructfirst) + (ge_representation_imaginary_code_gaussianfactorizationreconstructfirst)) * S ((ge_representation_real_code_gaussianfactorizationreconstructfirst) + (ge_representation_imaginary_code_gaussianfactorizationreconstructfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationreconstructfirst) + (ge_representation_imaginary_code_gaussianfactorizationreconstructfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationreconstructfirstreal ge_balance_negative_gaussianfactorizationreconstructfirstreal. (((((ge_representation_real_code_gaussianfactorizationreconstructfirst) = 2 * (ge_balance_positive_gaussianfactorizationreconstructfirstreal) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationreconstructfirst) = 2 * ge_signed_half_gaussianfactorizationreconstructfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstreal) = S ge_signed_half_gaussianfactorizationreconstructfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructfirstreal = (ge_first_rn_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationreconstructfirstimaginary ge_balance_negative_gaussianfactorizationreconstructfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationreconstructfirst) = 2 * (ge_balance_positive_gaussianfactorizationreconstructfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationreconstructfirst) = 2 * ge_signed_half_gaussianfactorizationreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructfirstimaginary) = S ge_signed_half_gaussianfactorizationreconstructfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructfirstimaginary = (ge_first_in_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationreconstructsecond ge_representation_imaginary_code_gaussianfactorizationreconstructsecond. (((gr_factor_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationreconstructsecond) + (ge_representation_imaginary_code_gaussianfactorizationreconstructsecond)) * S ((ge_representation_real_code_gaussianfactorizationreconstructsecond) + (ge_representation_imaginary_code_gaussianfactorizationreconstructsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationreconstructsecond) + (ge_representation_imaginary_code_gaussianfactorizationreconstructsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationreconstructsecondreal ge_balance_negative_gaussianfactorizationreconstructsecondreal. (((((ge_representation_real_code_gaussianfactorizationreconstructsecond) = 2 * (ge_balance_positive_gaussianfactorizationreconstructsecondreal) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationreconstructsecond) = 2 * ge_signed_half_gaussianfactorizationreconstructsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondreal) = S ge_signed_half_gaussianfactorizationreconstructsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructsecondreal = (ge_second_rn_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationreconstructsecondimaginary ge_balance_negative_gaussianfactorizationreconstructsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationreconstructsecond) = 2 * (ge_balance_positive_gaussianfactorizationreconstructsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationreconstructsecond) = 2 * ge_signed_half_gaussianfactorizationreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructsecondimaginary) = S ge_signed_half_gaussianfactorizationreconstructsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationreconstruct) + ge_balance_negative_gaussianfactorizationreconstructsecondimaginary = (ge_second_in_gaussianfactorizationreconstruct) + ge_balance_positive_gaussianfactorizationreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationreconstructoutput ge_representation_imaginary_code_gaussianfactorizationreconstructoutput. ((((z)) = ((ge_representation_real_code_gaussianfactorizationreconstructoutput) + (ge_representation_imaginary_code_gaussianfactorizationreconstructoutput)) * S ((ge_representation_real_code_gaussianfactorizationreconstructoutput) + (ge_representation_imaginary_code_gaussianfactorizationreconstructoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationreconstructoutput) + (ge_representation_imaginary_code_gaussianfactorizationreconstructoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationreconstructoutputreal ge_balance_negative_gaussianfactorizationreconstructoutputreal. (((((ge_representation_real_code_gaussianfactorizationreconstructoutput) = 2 * (ge_balance_positive_gaussianfactorizationreconstructoutputreal) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationreconstructoutput) = 2 * ge_signed_half_gaussianfactorizationreconstructoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputreal) = S ge_signed_half_gaussianfactorizationreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))))))) + ge_balance_negative_gaussianfactorizationreconstructoutputreal = (((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))))))) + ge_balance_positive_gaussianfactorizationreconstructoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationreconstructoutputimaginary ge_balance_negative_gaussianfactorizationreconstructoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationreconstructoutput) = 2 * (ge_balance_positive_gaussianfactorizationreconstructoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationreconstructoutput) = 2 * ge_signed_half_gaussianfactorizationreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationreconstructoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationreconstructoutputimaginary) = S ge_signed_half_gaussianfactorizationreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))))))) + ge_balance_negative_gaussianfactorizationreconstructoutputimaginary = (((((((ge_first_rp_gaussianfactorizationreconstruct) * (ge_second_in_gaussianfactorizationreconstruct))) + (((ge_first_rn_gaussianfactorizationreconstruct) * (ge_second_ip_gaussianfactorizationreconstruct))))) + (((((ge_first_ip_gaussianfactorizationreconstruct) * (ge_second_rn_gaussianfactorizationreconstruct))) + (((ge_first_in_gaussianfactorizationreconstruct) * (ge_second_rp_gaussianfactorizationreconstruct))))))) + ge_balance_positive_gaussianfactorizationreconstructoutputimaginary)))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
none
Checked theorems using this definition
GF0092 · gaussian_unit_empty_factorizationGF0093 · gaussian_factorization_append_irreducibleGF0094 · gaussian_irreducible_factorization_bounded_normGF0095 · gaussian_irreducible_factorization_existsGF0096 · gaussian_irreducible_factorization_is_primeGF0097 · gaussian_prime_factorization_is_irreducibleGF0098 · gaussian_prime_factorization_existsGF009D · gaussian_factorization_value_validGF009E · gaussian_factorization_value_nonzeroGF00B0 · gaussian_irreducible_factorizations_uniqueGF00B4 · gaussian_unit_prime_factorization_length_zero