Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ z. ∀ u. ∀ b. ∀ c. ∀ l. ∀ p. ∀ w. GIrreducibleFactorization(z,u,b,c,l) → GIrreducible(p) → GMul(z,p,w) → ∃ x. ∃ y. GIrreducibleFactorization(w,u,x,y,S l)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall z u b c l p w. (((exists gr_inverse_factor_append_oldunit. (exists ge_first_rp_factor_append_oldunitidentity ge_first_rn_factor_append_oldunitidentity ge_first_ip_factor_append_oldunitidentity ge_first_in_factor_append_oldunitidentity ge_second_rp_factor_append_oldunitidentity ge_second_rn_factor_append_oldunitidentity ge_second_ip_factor_append_oldunitidentity ge_second_in_factor_append_oldunitidentity. ((exists ge_representation_real_code_factor_append_oldunitidentityfirst ge_representation_imaginary_code_factor_append_oldunitidentityfirst. (((u) = ((ge_representation_real_code_factor_append_oldunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldunitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldunitidentityfirstreal ge_balance_negative_factor_append_oldunitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldunitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldunitidentityfirst) = 2 * ge_signed_half_factor_append_oldunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityfirstreal) = S ge_signed_half_factor_append_oldunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentityfirstreal = (ge_first_rn_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldunitidentityfirstimaginary ge_balance_negative_factor_append_oldunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldunitidentityfirst) = 2 * ge_signed_half_factor_append_oldunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityfirstimaginary) = S ge_signed_half_factor_append_oldunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentityfirstimaginary = (ge_first_in_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldunitidentitysecond ge_representation_imaginary_code_factor_append_oldunitidentitysecond. (((gr_inverse_factor_append_oldunit) = ((ge_representation_real_code_factor_append_oldunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldunitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldunitidentitysecondreal ge_balance_negative_factor_append_oldunitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldunitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldunitidentitysecond) = 2 * ge_signed_half_factor_append_oldunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldunitidentitysecondreal) = S ge_signed_half_factor_append_oldunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentitysecondreal = (ge_second_rn_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldunitidentitysecondimaginary ge_balance_negative_factor_append_oldunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldunitidentitysecond) = 2 * ge_signed_half_factor_append_oldunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldunitidentitysecondimaginary) = S ge_signed_half_factor_append_oldunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldunitidentity) + ge_balance_negative_factor_append_oldunitidentitysecondimaginary = (ge_second_in_factor_append_oldunitidentity) + ge_balance_positive_factor_append_oldunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldunitidentityoutput ge_representation_imaginary_code_factor_append_oldunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldunitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldunitidentityoutputreal ge_balance_negative_factor_append_oldunitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldunitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldunitidentityoutput) = 2 * ge_signed_half_factor_append_oldunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityoutputreal) = S ge_signed_half_factor_append_oldunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))))))) + ge_balance_negative_factor_append_oldunitidentityoutputreal = (((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))))))) + ge_balance_positive_factor_append_oldunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldunitidentityoutputimaginary ge_balance_negative_factor_append_oldunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldunitidentityoutput) = 2 * ge_signed_half_factor_append_oldunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldunitidentityoutputimaginary) = S ge_signed_half_factor_append_oldunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))))))) + ge_balance_negative_factor_append_oldunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldunitidentity) * (ge_second_in_factor_append_oldunitidentity))) + (((ge_first_rn_factor_append_oldunitidentity) * (ge_second_ip_factor_append_oldunitidentity))))) + (((((ge_first_ip_factor_append_oldunitidentity) * (ge_second_rn_factor_append_oldunitidentity))) + (((ge_first_in_factor_append_oldunitidentity) * (ge_second_rp_factor_append_oldunitidentity))))))) + ge_balance_positive_factor_append_oldunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factor_append_oldirreducible gr_factor_value_factor_append_oldirreducible. (exists ge_gap_factor_append_oldirreducibleindex. ge_gap_factor_append_oldirreducibleindex + S (gr_factor_index_factor_append_oldirreducible) = (l)) -> (((exists ff_h_gprod_factor_append_oldirreducibleentry. ff_h_gprod_factor_append_oldirreducibleentry + S (gr_factor_value_factor_append_oldirreducible) = S ((S (gr_factor_index_factor_append_oldirreducible)) * c)) /\ exists ff_q_gprod_factor_append_oldirreducibleentry. b = ff_q_gprod_factor_append_oldirreducibleentry * S ((S (gr_factor_index_factor_append_oldirreducible)) * c) + (gr_factor_value_factor_append_oldirreducible))) -> (((exists ge_real_positive_factor_append_oldirreducibleirreduciblecarrier ge_real_negative_factor_append_oldirreducibleirreduciblecarrier ge_imaginary_positive_factor_append_oldirreducibleirreduciblecarrier ge_imaginary_negative_factor_append_oldirreducibleirreduciblecarrier. (exists ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode. (((gr_factor_value_factor_append_oldirreducible) = ((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factor_append_oldirreducibleirreduciblecarrier) /\ (ge_real_negative_factor_append_oldirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factor_append_oldirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factor_append_oldirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factor_append_oldirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factor_append_oldirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factor_append_oldirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_append_oldirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factor_append_oldirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_oldirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factor_append_oldirreducible)=0)) /\ ((~(exists gr_inverse_factor_append_oldirreducibleirreduciblenonunit. (exists ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factor_append_oldirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factor_append_oldirreducibleirreduciblenonunit) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_append_oldirreducibleirreducible gr_second_factor_factor_append_oldirreducibleirreducible. (exists ge_first_rp_factor_append_oldirreducibleirreduciblefactorization ge_first_rn_factor_append_oldirreducibleirreduciblefactorization ge_first_ip_factor_append_oldirreducibleirreduciblefactorization ge_first_in_factor_append_oldirreducibleirreduciblefactorization ge_second_rp_factor_append_oldirreducibleirreduciblefactorization ge_second_rn_factor_append_oldirreducibleirreduciblefactorization ge_second_ip_factor_append_oldirreducibleirreduciblefactorization ge_second_in_factor_append_oldirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factor_append_oldirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_in_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_oldirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_oldirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_oldirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_append_oldirreducibleirreduciblefirst_unit. (exists ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factor_append_oldirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_append_oldirreducibleirreduciblesecond_unit. (exists ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factor_append_oldirreducibleirreducible) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factor_append_oldirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_oldirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_oldirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_oldirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_oldirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factor_append_old. ((exists gr_product_trace_factor_append_oldtrace gr_product_scale_factor_append_oldtrace. ((((exists ff_h_gprod_factor_append_oldtracestart. ff_h_gprod_factor_append_oldtracestart + S (6) = S ((S (0)) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtracestart. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtracestart * S ((S (0)) * gr_product_scale_factor_append_oldtrace) + (6))) /\ ((((exists ff_h_gprod_factor_append_oldtraceend. ff_h_gprod_factor_append_oldtraceend + S (gr_factor_product_factor_append_old) = S ((S (l)) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtraceend. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtraceend * S ((S (l)) * gr_product_scale_factor_append_oldtrace) + (gr_factor_product_factor_append_old))) /\ (forall gr_product_index_factor_append_oldtracesteps. (exists ge_gap_factor_append_oldtracestepsindex_bound. ge_gap_factor_append_oldtracestepsindex_bound + S (gr_product_index_factor_append_oldtracesteps) = (l)) -> exists gr_product_factor_factor_append_oldtracesteps gr_product_before_factor_append_oldtracesteps gr_product_after_factor_append_oldtracesteps. ((((exists ff_h_gprod_factor_append_oldtracestepsfactor. ff_h_gprod_factor_append_oldtracestepsfactor + S (gr_product_factor_factor_append_oldtracesteps) = S ((S (gr_product_index_factor_append_oldtracesteps)) * c)) /\ exists ff_q_gprod_factor_append_oldtracestepsfactor. b = ff_q_gprod_factor_append_oldtracestepsfactor * S ((S (gr_product_index_factor_append_oldtracesteps)) * c) + (gr_product_factor_factor_append_oldtracesteps))) /\ ((((exists ff_h_gprod_factor_append_oldtracestepsbefore. ff_h_gprod_factor_append_oldtracestepsbefore + S (gr_product_before_factor_append_oldtracesteps) = S ((S (gr_product_index_factor_append_oldtracesteps)) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtracestepsbefore. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtracestepsbefore * S ((S (gr_product_index_factor_append_oldtracesteps)) * gr_product_scale_factor_append_oldtrace) + (gr_product_before_factor_append_oldtracesteps))) /\ ((((exists ff_h_gprod_factor_append_oldtracestepsafter. ff_h_gprod_factor_append_oldtracestepsafter + S (gr_product_after_factor_append_oldtracesteps) = S ((S (S (gr_product_index_factor_append_oldtracesteps))) * gr_product_scale_factor_append_oldtrace)) /\ exists ff_q_gprod_factor_append_oldtracestepsafter. gr_product_trace_factor_append_oldtrace = ff_q_gprod_factor_append_oldtracestepsafter * S ((S (S (gr_product_index_factor_append_oldtracesteps))) * gr_product_scale_factor_append_oldtrace) + (gr_product_after_factor_append_oldtracesteps))) /\ (exists ge_first_rp_factor_append_oldtracestepsmultiply ge_first_rn_factor_append_oldtracestepsmultiply ge_first_ip_factor_append_oldtracestepsmultiply ge_first_in_factor_append_oldtracestepsmultiply ge_second_rp_factor_append_oldtracestepsmultiply ge_second_rn_factor_append_oldtracestepsmultiply ge_second_ip_factor_append_oldtracestepsmultiply ge_second_in_factor_append_oldtracestepsmultiply. ((exists ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst. (((gr_product_before_factor_append_oldtracesteps) = ((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst)) * S ((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal. (((((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factor_append_oldtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal) = S ge_signed_half_factor_append_oldtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplyfirstreal = (ge_first_rn_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary) = S ge_signed_half_factor_append_oldtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplyfirstimaginary = (ge_first_in_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldtracestepsmultiplysecond ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond. (((gr_product_factor_factor_append_oldtracesteps) = ((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond)) * S ((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal. (((((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factor_append_oldtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal) = S ge_signed_half_factor_append_oldtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplysecondreal = (ge_second_rn_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary) = S ge_signed_half_factor_append_oldtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldtracestepsmultiply) + ge_balance_negative_factor_append_oldtracestepsmultiplysecondimaginary = (ge_second_in_factor_append_oldtracestepsmultiply) + ge_balance_positive_factor_append_oldtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput. (((gr_product_after_factor_append_oldtracesteps) = ((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput)) * S ((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal. (((((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factor_append_oldtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal) = S ge_signed_half_factor_append_oldtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))))))) + ge_balance_negative_factor_append_oldtracestepsmultiplyoutputreal = (((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))))))) + ge_balance_positive_factor_append_oldtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_oldtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary) = S ge_signed_half_factor_append_oldtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))))))) + ge_balance_negative_factor_append_oldtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factor_append_oldtracestepsmultiply) * (ge_second_in_factor_append_oldtracestepsmultiply))) + (((ge_first_rn_factor_append_oldtracestepsmultiply) * (ge_second_ip_factor_append_oldtracestepsmultiply))))) + (((((ge_first_ip_factor_append_oldtracestepsmultiply) * (ge_second_rn_factor_append_oldtracestepsmultiply))) + (((ge_first_in_factor_append_oldtracestepsmultiply) * (ge_second_rp_factor_append_oldtracestepsmultiply))))))) + ge_balance_positive_factor_append_oldtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factor_append_oldreconstruct ge_first_rn_factor_append_oldreconstruct ge_first_ip_factor_append_oldreconstruct ge_first_in_factor_append_oldreconstruct ge_second_rp_factor_append_oldreconstruct ge_second_rn_factor_append_oldreconstruct ge_second_ip_factor_append_oldreconstruct ge_second_in_factor_append_oldreconstruct. ((exists ge_representation_real_code_factor_append_oldreconstructfirst ge_representation_imaginary_code_factor_append_oldreconstructfirst. (((u) = ((ge_representation_real_code_factor_append_oldreconstructfirst) + (ge_representation_imaginary_code_factor_append_oldreconstructfirst)) * S ((ge_representation_real_code_factor_append_oldreconstructfirst) + (ge_representation_imaginary_code_factor_append_oldreconstructfirst)) + ((ge_representation_imaginary_code_factor_append_oldreconstructfirst) + (ge_representation_imaginary_code_factor_append_oldreconstructfirst))) /\ ((exists ge_balance_positive_factor_append_oldreconstructfirstreal ge_balance_negative_factor_append_oldreconstructfirstreal. (((((ge_representation_real_code_factor_append_oldreconstructfirst) = 2 * (ge_balance_positive_factor_append_oldreconstructfirstreal) /\ (ge_balance_negative_factor_append_oldreconstructfirstreal) = 0) \/ exists ge_signed_half_factor_append_oldreconstructfirstrealdecode. (((ge_representation_real_code_factor_append_oldreconstructfirst) = 2 * ge_signed_half_factor_append_oldreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructfirstreal) = 0) /\ (ge_balance_negative_factor_append_oldreconstructfirstreal) = S ge_signed_half_factor_append_oldreconstructfirstrealdecode))) /\ ((ge_first_rp_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructfirstreal = (ge_first_rn_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructfirstreal))) /\ (exists ge_balance_positive_factor_append_oldreconstructfirstimaginary ge_balance_negative_factor_append_oldreconstructfirstimaginary. (((((ge_representation_imaginary_code_factor_append_oldreconstructfirst) = 2 * (ge_balance_positive_factor_append_oldreconstructfirstimaginary) /\ (ge_balance_negative_factor_append_oldreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_oldreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldreconstructfirst) = 2 * ge_signed_half_factor_append_oldreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_oldreconstructfirstimaginary) = S ge_signed_half_factor_append_oldreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructfirstimaginary = (ge_first_in_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_oldreconstructsecond ge_representation_imaginary_code_factor_append_oldreconstructsecond. (((gr_factor_product_factor_append_old) = ((ge_representation_real_code_factor_append_oldreconstructsecond) + (ge_representation_imaginary_code_factor_append_oldreconstructsecond)) * S ((ge_representation_real_code_factor_append_oldreconstructsecond) + (ge_representation_imaginary_code_factor_append_oldreconstructsecond)) + ((ge_representation_imaginary_code_factor_append_oldreconstructsecond) + (ge_representation_imaginary_code_factor_append_oldreconstructsecond))) /\ ((exists ge_balance_positive_factor_append_oldreconstructsecondreal ge_balance_negative_factor_append_oldreconstructsecondreal. (((((ge_representation_real_code_factor_append_oldreconstructsecond) = 2 * (ge_balance_positive_factor_append_oldreconstructsecondreal) /\ (ge_balance_negative_factor_append_oldreconstructsecondreal) = 0) \/ exists ge_signed_half_factor_append_oldreconstructsecondrealdecode. (((ge_representation_real_code_factor_append_oldreconstructsecond) = 2 * ge_signed_half_factor_append_oldreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructsecondreal) = 0) /\ (ge_balance_negative_factor_append_oldreconstructsecondreal) = S ge_signed_half_factor_append_oldreconstructsecondrealdecode))) /\ ((ge_second_rp_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructsecondreal = (ge_second_rn_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructsecondreal))) /\ (exists ge_balance_positive_factor_append_oldreconstructsecondimaginary ge_balance_negative_factor_append_oldreconstructsecondimaginary. (((((ge_representation_imaginary_code_factor_append_oldreconstructsecond) = 2 * (ge_balance_positive_factor_append_oldreconstructsecondimaginary) /\ (ge_balance_negative_factor_append_oldreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_oldreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldreconstructsecond) = 2 * ge_signed_half_factor_append_oldreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_oldreconstructsecondimaginary) = S ge_signed_half_factor_append_oldreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_oldreconstruct) + ge_balance_negative_factor_append_oldreconstructsecondimaginary = (ge_second_in_factor_append_oldreconstruct) + ge_balance_positive_factor_append_oldreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_oldreconstructoutput ge_representation_imaginary_code_factor_append_oldreconstructoutput. (((z) = ((ge_representation_real_code_factor_append_oldreconstructoutput) + (ge_representation_imaginary_code_factor_append_oldreconstructoutput)) * S ((ge_representation_real_code_factor_append_oldreconstructoutput) + (ge_representation_imaginary_code_factor_append_oldreconstructoutput)) + ((ge_representation_imaginary_code_factor_append_oldreconstructoutput) + (ge_representation_imaginary_code_factor_append_oldreconstructoutput))) /\ ((exists ge_balance_positive_factor_append_oldreconstructoutputreal ge_balance_negative_factor_append_oldreconstructoutputreal. (((((ge_representation_real_code_factor_append_oldreconstructoutput) = 2 * (ge_balance_positive_factor_append_oldreconstructoutputreal) /\ (ge_balance_negative_factor_append_oldreconstructoutputreal) = 0) \/ exists ge_signed_half_factor_append_oldreconstructoutputrealdecode. (((ge_representation_real_code_factor_append_oldreconstructoutput) = 2 * ge_signed_half_factor_append_oldreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructoutputreal) = 0) /\ (ge_balance_negative_factor_append_oldreconstructoutputreal) = S ge_signed_half_factor_append_oldreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))))))) + ge_balance_negative_factor_append_oldreconstructoutputreal = (((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))))))) + ge_balance_positive_factor_append_oldreconstructoutputreal))) /\ (exists ge_balance_positive_factor_append_oldreconstructoutputimaginary ge_balance_negative_factor_append_oldreconstructoutputimaginary. (((((ge_representation_imaginary_code_factor_append_oldreconstructoutput) = 2 * (ge_balance_positive_factor_append_oldreconstructoutputimaginary) /\ (ge_balance_negative_factor_append_oldreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_oldreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_oldreconstructoutput) = 2 * ge_signed_half_factor_append_oldreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_oldreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_oldreconstructoutputimaginary) = S ge_signed_half_factor_append_oldreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))))))) + ge_balance_negative_factor_append_oldreconstructoutputimaginary = (((((((ge_first_rp_factor_append_oldreconstruct) * (ge_second_in_factor_append_oldreconstruct))) + (((ge_first_rn_factor_append_oldreconstruct) * (ge_second_ip_factor_append_oldreconstruct))))) + (((((ge_first_ip_factor_append_oldreconstruct) * (ge_second_rn_factor_append_oldreconstruct))) + (((ge_first_in_factor_append_oldreconstruct) * (ge_second_rp_factor_append_oldreconstruct))))))) + ge_balance_positive_factor_append_oldreconstructoutputimaginary)))))))))))))) -> (((exists ge_real_positive_factor_append_primecarrier ge_real_negative_factor_append_primecarrier ge_imaginary_positive_factor_append_primecarrier ge_imaginary_negative_factor_append_primecarrier. (exists ge_real_code_factor_append_primecarrierdecode ge_imaginary_code_factor_append_primecarrierdecode. (((p) = ((ge_real_code_factor_append_primecarrierdecode) + (ge_imaginary_code_factor_append_primecarrierdecode)) * S ((ge_real_code_factor_append_primecarrierdecode) + (ge_imaginary_code_factor_append_primecarrierdecode)) + ((ge_imaginary_code_factor_append_primecarrierdecode) + (ge_imaginary_code_factor_append_primecarrierdecode))) /\ (((((ge_real_code_factor_append_primecarrierdecode) = 2 * (ge_real_positive_factor_append_primecarrier) /\ (ge_real_negative_factor_append_primecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_primecarrierdecode_real. (((ge_real_code_factor_append_primecarrierdecode) = 2 * ge_signed_half_ge_factor_append_primecarrierdecode_real + 1 /\ (ge_real_positive_factor_append_primecarrier) = 0) /\ (ge_real_negative_factor_append_primecarrier) = S ge_signed_half_ge_factor_append_primecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_append_primecarrierdecode) = 2 * (ge_imaginary_positive_factor_append_primecarrier) /\ (ge_imaginary_negative_factor_append_primecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_primecarrierdecode_imaginary. (((ge_imaginary_code_factor_append_primecarrierdecode) = 2 * ge_signed_half_ge_factor_append_primecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_append_primecarrier) = 0) /\ (ge_imaginary_negative_factor_append_primecarrier) = S ge_signed_half_ge_factor_append_primecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_factor_append_primenonunit. (exists ge_first_rp_factor_append_primenonunitidentity ge_first_rn_factor_append_primenonunitidentity ge_first_ip_factor_append_primenonunitidentity ge_first_in_factor_append_primenonunitidentity ge_second_rp_factor_append_primenonunitidentity ge_second_rn_factor_append_primenonunitidentity ge_second_ip_factor_append_primenonunitidentity ge_second_in_factor_append_primenonunitidentity. ((exists ge_representation_real_code_factor_append_primenonunitidentityfirst ge_representation_imaginary_code_factor_append_primenonunitidentityfirst. (((p) = ((ge_representation_real_code_factor_append_primenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_primenonunitidentityfirst)) * S ((ge_representation_real_code_factor_append_primenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_primenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_primenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_primenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_primenonunitidentityfirstreal ge_balance_negative_factor_append_primenonunitidentityfirstreal. (((((ge_representation_real_code_factor_append_primenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_primenonunitidentityfirstreal) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_primenonunitidentityfirst) = 2 * ge_signed_half_factor_append_primenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstreal) = S ge_signed_half_factor_append_primenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentityfirstreal = (ge_first_rn_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_primenonunitidentityfirstimaginary ge_balance_negative_factor_append_primenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_primenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primenonunitidentityfirst) = 2 * ge_signed_half_factor_append_primenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityfirstimaginary) = S ge_signed_half_factor_append_primenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentityfirstimaginary = (ge_first_in_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primenonunitidentitysecond ge_representation_imaginary_code_factor_append_primenonunitidentitysecond. (((gr_inverse_factor_append_primenonunit) = ((ge_representation_real_code_factor_append_primenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_primenonunitidentitysecond)) * S ((ge_representation_real_code_factor_append_primenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_primenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_primenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_primenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_primenonunitidentitysecondreal ge_balance_negative_factor_append_primenonunitidentitysecondreal. (((((ge_representation_real_code_factor_append_primenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_primenonunitidentitysecondreal) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_primenonunitidentitysecond) = 2 * ge_signed_half_factor_append_primenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondreal) = S ge_signed_half_factor_append_primenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentitysecondreal = (ge_second_rn_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_primenonunitidentitysecondimaginary ge_balance_negative_factor_append_primenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_primenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_primenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primenonunitidentitysecond) = 2 * ge_signed_half_factor_append_primenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentitysecondimaginary) = S ge_signed_half_factor_append_primenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primenonunitidentity) + ge_balance_negative_factor_append_primenonunitidentitysecondimaginary = (ge_second_in_factor_append_primenonunitidentity) + ge_balance_positive_factor_append_primenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primenonunitidentityoutput ge_representation_imaginary_code_factor_append_primenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_primenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_primenonunitidentityoutput)) * S ((ge_representation_real_code_factor_append_primenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_primenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_primenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_primenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_primenonunitidentityoutputreal ge_balance_negative_factor_append_primenonunitidentityoutputreal. (((((ge_representation_real_code_factor_append_primenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_primenonunitidentityoutputreal) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_primenonunitidentityoutput) = 2 * ge_signed_half_factor_append_primenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputreal) = S ge_signed_half_factor_append_primenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))))))) + ge_balance_negative_factor_append_primenonunitidentityoutputreal = (((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))))))) + ge_balance_positive_factor_append_primenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_primenonunitidentityoutputimaginary ge_balance_negative_factor_append_primenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_primenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primenonunitidentityoutput) = 2 * ge_signed_half_factor_append_primenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primenonunitidentityoutputimaginary) = S ge_signed_half_factor_append_primenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))))))) + ge_balance_negative_factor_append_primenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_primenonunitidentity) * (ge_second_in_factor_append_primenonunitidentity))) + (((ge_first_rn_factor_append_primenonunitidentity) * (ge_second_ip_factor_append_primenonunitidentity))))) + (((((ge_first_ip_factor_append_primenonunitidentity) * (ge_second_rn_factor_append_primenonunitidentity))) + (((ge_first_in_factor_append_primenonunitidentity) * (ge_second_rp_factor_append_primenonunitidentity))))))) + ge_balance_positive_factor_append_primenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_append_prime gr_second_factor_factor_append_prime. (exists ge_first_rp_factor_append_primefactorization ge_first_rn_factor_append_primefactorization ge_first_ip_factor_append_primefactorization ge_first_in_factor_append_primefactorization ge_second_rp_factor_append_primefactorization ge_second_rn_factor_append_primefactorization ge_second_ip_factor_append_primefactorization ge_second_in_factor_append_primefactorization. ((exists ge_representation_real_code_factor_append_primefactorizationfirst ge_representation_imaginary_code_factor_append_primefactorizationfirst. (((gr_first_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primefactorizationfirst) + (ge_representation_imaginary_code_factor_append_primefactorizationfirst)) * S ((ge_representation_real_code_factor_append_primefactorizationfirst) + (ge_representation_imaginary_code_factor_append_primefactorizationfirst)) + ((ge_representation_imaginary_code_factor_append_primefactorizationfirst) + (ge_representation_imaginary_code_factor_append_primefactorizationfirst))) /\ ((exists ge_balance_positive_factor_append_primefactorizationfirstreal ge_balance_negative_factor_append_primefactorizationfirstreal. (((((ge_representation_real_code_factor_append_primefactorizationfirst) = 2 * (ge_balance_positive_factor_append_primefactorizationfirstreal) /\ (ge_balance_negative_factor_append_primefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_append_primefactorizationfirstrealdecode. (((ge_representation_real_code_factor_append_primefactorizationfirst) = 2 * ge_signed_half_factor_append_primefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_append_primefactorizationfirstreal) = S ge_signed_half_factor_append_primefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationfirstreal = (ge_first_rn_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_append_primefactorizationfirstimaginary ge_balance_negative_factor_append_primefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primefactorizationfirst) = 2 * (ge_balance_positive_factor_append_primefactorizationfirstimaginary) /\ (ge_balance_negative_factor_append_primefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefactorizationfirst) = 2 * ge_signed_half_factor_append_primefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primefactorizationfirstimaginary) = S ge_signed_half_factor_append_primefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationfirstimaginary = (ge_first_in_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primefactorizationsecond ge_representation_imaginary_code_factor_append_primefactorizationsecond. (((gr_second_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primefactorizationsecond) + (ge_representation_imaginary_code_factor_append_primefactorizationsecond)) * S ((ge_representation_real_code_factor_append_primefactorizationsecond) + (ge_representation_imaginary_code_factor_append_primefactorizationsecond)) + ((ge_representation_imaginary_code_factor_append_primefactorizationsecond) + (ge_representation_imaginary_code_factor_append_primefactorizationsecond))) /\ ((exists ge_balance_positive_factor_append_primefactorizationsecondreal ge_balance_negative_factor_append_primefactorizationsecondreal. (((((ge_representation_real_code_factor_append_primefactorizationsecond) = 2 * (ge_balance_positive_factor_append_primefactorizationsecondreal) /\ (ge_balance_negative_factor_append_primefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_append_primefactorizationsecondrealdecode. (((ge_representation_real_code_factor_append_primefactorizationsecond) = 2 * ge_signed_half_factor_append_primefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_append_primefactorizationsecondreal) = S ge_signed_half_factor_append_primefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationsecondreal = (ge_second_rn_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_append_primefactorizationsecondimaginary ge_balance_negative_factor_append_primefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_primefactorizationsecond) = 2 * (ge_balance_positive_factor_append_primefactorizationsecondimaginary) /\ (ge_balance_negative_factor_append_primefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefactorizationsecond) = 2 * ge_signed_half_factor_append_primefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primefactorizationsecondimaginary) = S ge_signed_half_factor_append_primefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primefactorization) + ge_balance_negative_factor_append_primefactorizationsecondimaginary = (ge_second_in_factor_append_primefactorization) + ge_balance_positive_factor_append_primefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primefactorizationoutput ge_representation_imaginary_code_factor_append_primefactorizationoutput. (((p) = ((ge_representation_real_code_factor_append_primefactorizationoutput) + (ge_representation_imaginary_code_factor_append_primefactorizationoutput)) * S ((ge_representation_real_code_factor_append_primefactorizationoutput) + (ge_representation_imaginary_code_factor_append_primefactorizationoutput)) + ((ge_representation_imaginary_code_factor_append_primefactorizationoutput) + (ge_representation_imaginary_code_factor_append_primefactorizationoutput))) /\ ((exists ge_balance_positive_factor_append_primefactorizationoutputreal ge_balance_negative_factor_append_primefactorizationoutputreal. (((((ge_representation_real_code_factor_append_primefactorizationoutput) = 2 * (ge_balance_positive_factor_append_primefactorizationoutputreal) /\ (ge_balance_negative_factor_append_primefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_append_primefactorizationoutputrealdecode. (((ge_representation_real_code_factor_append_primefactorizationoutput) = 2 * ge_signed_half_factor_append_primefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_append_primefactorizationoutputreal) = S ge_signed_half_factor_append_primefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))))))) + ge_balance_negative_factor_append_primefactorizationoutputreal = (((((((ge_first_rp_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))))))) + ge_balance_positive_factor_append_primefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_append_primefactorizationoutputimaginary ge_balance_negative_factor_append_primefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primefactorizationoutput) = 2 * (ge_balance_positive_factor_append_primefactorizationoutputimaginary) /\ (ge_balance_negative_factor_append_primefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefactorizationoutput) = 2 * ge_signed_half_factor_append_primefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primefactorizationoutputimaginary) = S ge_signed_half_factor_append_primefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))))))) + ge_balance_negative_factor_append_primefactorizationoutputimaginary = (((((((ge_first_rp_factor_append_primefactorization) * (ge_second_in_factor_append_primefactorization))) + (((ge_first_rn_factor_append_primefactorization) * (ge_second_ip_factor_append_primefactorization))))) + (((((ge_first_ip_factor_append_primefactorization) * (ge_second_rn_factor_append_primefactorization))) + (((ge_first_in_factor_append_primefactorization) * (ge_second_rp_factor_append_primefactorization))))))) + ge_balance_positive_factor_append_primefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_append_primefirst_unit. (exists ge_first_rp_factor_append_primefirst_unitidentity ge_first_rn_factor_append_primefirst_unitidentity ge_first_ip_factor_append_primefirst_unitidentity ge_first_in_factor_append_primefirst_unitidentity ge_second_rp_factor_append_primefirst_unitidentity ge_second_rn_factor_append_primefirst_unitidentity ge_second_ip_factor_append_primefirst_unitidentity ge_second_in_factor_append_primefirst_unitidentity. ((exists ge_representation_real_code_factor_append_primefirst_unitidentityfirst ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst. (((gr_first_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_primefirst_unitidentityfirstreal ge_balance_negative_factor_append_primefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_primefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_primefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstreal) = S ge_signed_half_factor_append_primefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentityfirstreal = (ge_first_rn_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_primefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_append_primefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentityfirstimaginary = (ge_first_in_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primefirst_unitidentitysecond ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond. (((gr_inverse_factor_append_primefirst_unit) = ((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_primefirst_unitidentitysecondreal ge_balance_negative_factor_append_primefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_primefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_primefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondreal) = S ge_signed_half_factor_append_primefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentitysecondreal = (ge_second_rn_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_primefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_append_primefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primefirst_unitidentity) + ge_balance_negative_factor_append_primefirst_unitidentitysecondimaginary = (ge_second_in_factor_append_primefirst_unitidentity) + ge_balance_positive_factor_append_primefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primefirst_unitidentityoutput ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_primefirst_unitidentityoutputreal ge_balance_negative_factor_append_primefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_primefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_primefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputreal) = S ge_signed_half_factor_append_primefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))))))) + ge_balance_negative_factor_append_primefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))))))) + ge_balance_positive_factor_append_primefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_primefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_append_primefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))))))) + ge_balance_negative_factor_append_primefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_primefirst_unitidentity) * (ge_second_in_factor_append_primefirst_unitidentity))) + (((ge_first_rn_factor_append_primefirst_unitidentity) * (ge_second_ip_factor_append_primefirst_unitidentity))))) + (((((ge_first_ip_factor_append_primefirst_unitidentity) * (ge_second_rn_factor_append_primefirst_unitidentity))) + (((ge_first_in_factor_append_primefirst_unitidentity) * (ge_second_rp_factor_append_primefirst_unitidentity))))))) + ge_balance_positive_factor_append_primefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_append_primesecond_unit. (exists ge_first_rp_factor_append_primesecond_unitidentity ge_first_rn_factor_append_primesecond_unitidentity ge_first_ip_factor_append_primesecond_unitidentity ge_first_in_factor_append_primesecond_unitidentity ge_second_rp_factor_append_primesecond_unitidentity ge_second_rn_factor_append_primesecond_unitidentity ge_second_ip_factor_append_primesecond_unitidentity ge_second_in_factor_append_primesecond_unitidentity. ((exists ge_representation_real_code_factor_append_primesecond_unitidentityfirst ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst. (((gr_second_factor_factor_append_prime) = ((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_primesecond_unitidentityfirstreal ge_balance_negative_factor_append_primesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_primesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_primesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstreal) = S ge_signed_half_factor_append_primesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentityfirstreal = (ge_first_rn_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_primesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_primesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_append_primesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentityfirstimaginary = (ge_first_in_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_primesecond_unitidentitysecond ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond. (((gr_inverse_factor_append_primesecond_unit) = ((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_primesecond_unitidentitysecondreal ge_balance_negative_factor_append_primesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_primesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_primesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondreal) = S ge_signed_half_factor_append_primesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentitysecondreal = (ge_second_rn_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_primesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_primesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_append_primesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_primesecond_unitidentity) + ge_balance_negative_factor_append_primesecond_unitidentitysecondimaginary = (ge_second_in_factor_append_primesecond_unitidentity) + ge_balance_positive_factor_append_primesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_primesecond_unitidentityoutput ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_primesecond_unitidentityoutputreal ge_balance_negative_factor_append_primesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_primesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_primesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputreal) = S ge_signed_half_factor_append_primesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))))))) + ge_balance_negative_factor_append_primesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))))))) + ge_balance_positive_factor_append_primesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_primesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_primesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_primesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_append_primesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))))))) + ge_balance_negative_factor_append_primesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_primesecond_unitidentity) * (ge_second_in_factor_append_primesecond_unitidentity))) + (((ge_first_rn_factor_append_primesecond_unitidentity) * (ge_second_ip_factor_append_primesecond_unitidentity))))) + (((((ge_first_ip_factor_append_primesecond_unitidentity) * (ge_second_rn_factor_append_primesecond_unitidentity))) + (((ge_first_in_factor_append_primesecond_unitidentity) * (ge_second_rp_factor_append_primesecond_unitidentity))))))) + ge_balance_positive_factor_append_primesecond_unitidentityoutputimaginary))))))))))))))) -> (exists ge_first_rp_factor_append_equation ge_first_rn_factor_append_equation ge_first_ip_factor_append_equation ge_first_in_factor_append_equation ge_second_rp_factor_append_equation ge_second_rn_factor_append_equation ge_second_ip_factor_append_equation ge_second_in_factor_append_equation. ((exists ge_representation_real_code_factor_append_equationfirst ge_representation_imaginary_code_factor_append_equationfirst. (((z) = ((ge_representation_real_code_factor_append_equationfirst) + (ge_representation_imaginary_code_factor_append_equationfirst)) * S ((ge_representation_real_code_factor_append_equationfirst) + (ge_representation_imaginary_code_factor_append_equationfirst)) + ((ge_representation_imaginary_code_factor_append_equationfirst) + (ge_representation_imaginary_code_factor_append_equationfirst))) /\ ((exists ge_balance_positive_factor_append_equationfirstreal ge_balance_negative_factor_append_equationfirstreal. (((((ge_representation_real_code_factor_append_equationfirst) = 2 * (ge_balance_positive_factor_append_equationfirstreal) /\ (ge_balance_negative_factor_append_equationfirstreal) = 0) \/ exists ge_signed_half_factor_append_equationfirstrealdecode. (((ge_representation_real_code_factor_append_equationfirst) = 2 * ge_signed_half_factor_append_equationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_equationfirstreal) = 0) /\ (ge_balance_negative_factor_append_equationfirstreal) = S ge_signed_half_factor_append_equationfirstrealdecode))) /\ ((ge_first_rp_factor_append_equation) + ge_balance_negative_factor_append_equationfirstreal = (ge_first_rn_factor_append_equation) + ge_balance_positive_factor_append_equationfirstreal))) /\ (exists ge_balance_positive_factor_append_equationfirstimaginary ge_balance_negative_factor_append_equationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_equationfirst) = 2 * (ge_balance_positive_factor_append_equationfirstimaginary) /\ (ge_balance_negative_factor_append_equationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_equationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_equationfirst) = 2 * ge_signed_half_factor_append_equationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_equationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_equationfirstimaginary) = S ge_signed_half_factor_append_equationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_equation) + ge_balance_negative_factor_append_equationfirstimaginary = (ge_first_in_factor_append_equation) + ge_balance_positive_factor_append_equationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_equationsecond ge_representation_imaginary_code_factor_append_equationsecond. (((p) = ((ge_representation_real_code_factor_append_equationsecond) + (ge_representation_imaginary_code_factor_append_equationsecond)) * S ((ge_representation_real_code_factor_append_equationsecond) + (ge_representation_imaginary_code_factor_append_equationsecond)) + ((ge_representation_imaginary_code_factor_append_equationsecond) + (ge_representation_imaginary_code_factor_append_equationsecond))) /\ ((exists ge_balance_positive_factor_append_equationsecondreal ge_balance_negative_factor_append_equationsecondreal. (((((ge_representation_real_code_factor_append_equationsecond) = 2 * (ge_balance_positive_factor_append_equationsecondreal) /\ (ge_balance_negative_factor_append_equationsecondreal) = 0) \/ exists ge_signed_half_factor_append_equationsecondrealdecode. (((ge_representation_real_code_factor_append_equationsecond) = 2 * ge_signed_half_factor_append_equationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_equationsecondreal) = 0) /\ (ge_balance_negative_factor_append_equationsecondreal) = S ge_signed_half_factor_append_equationsecondrealdecode))) /\ ((ge_second_rp_factor_append_equation) + ge_balance_negative_factor_append_equationsecondreal = (ge_second_rn_factor_append_equation) + ge_balance_positive_factor_append_equationsecondreal))) /\ (exists ge_balance_positive_factor_append_equationsecondimaginary ge_balance_negative_factor_append_equationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_equationsecond) = 2 * (ge_balance_positive_factor_append_equationsecondimaginary) /\ (ge_balance_negative_factor_append_equationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_equationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_equationsecond) = 2 * ge_signed_half_factor_append_equationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_equationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_equationsecondimaginary) = S ge_signed_half_factor_append_equationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_equation) + ge_balance_negative_factor_append_equationsecondimaginary = (ge_second_in_factor_append_equation) + ge_balance_positive_factor_append_equationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_equationoutput ge_representation_imaginary_code_factor_append_equationoutput. (((w) = ((ge_representation_real_code_factor_append_equationoutput) + (ge_representation_imaginary_code_factor_append_equationoutput)) * S ((ge_representation_real_code_factor_append_equationoutput) + (ge_representation_imaginary_code_factor_append_equationoutput)) + ((ge_representation_imaginary_code_factor_append_equationoutput) + (ge_representation_imaginary_code_factor_append_equationoutput))) /\ ((exists ge_balance_positive_factor_append_equationoutputreal ge_balance_negative_factor_append_equationoutputreal. (((((ge_representation_real_code_factor_append_equationoutput) = 2 * (ge_balance_positive_factor_append_equationoutputreal) /\ (ge_balance_negative_factor_append_equationoutputreal) = 0) \/ exists ge_signed_half_factor_append_equationoutputrealdecode. (((ge_representation_real_code_factor_append_equationoutput) = 2 * ge_signed_half_factor_append_equationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_equationoutputreal) = 0) /\ (ge_balance_negative_factor_append_equationoutputreal) = S ge_signed_half_factor_append_equationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_equation) * (ge_second_rp_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_rn_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_in_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_ip_factor_append_equation))))))) + ge_balance_negative_factor_append_equationoutputreal = (((((((ge_first_rp_factor_append_equation) * (ge_second_rn_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_rp_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_ip_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_in_factor_append_equation))))))) + ge_balance_positive_factor_append_equationoutputreal))) /\ (exists ge_balance_positive_factor_append_equationoutputimaginary ge_balance_negative_factor_append_equationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_equationoutput) = 2 * (ge_balance_positive_factor_append_equationoutputimaginary) /\ (ge_balance_negative_factor_append_equationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_equationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_equationoutput) = 2 * ge_signed_half_factor_append_equationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_equationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_equationoutputimaginary) = S ge_signed_half_factor_append_equationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_equation) * (ge_second_ip_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_in_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_rp_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_rn_factor_append_equation))))))) + ge_balance_negative_factor_append_equationoutputimaginary = (((((((ge_first_rp_factor_append_equation) * (ge_second_in_factor_append_equation))) + (((ge_first_rn_factor_append_equation) * (ge_second_ip_factor_append_equation))))) + (((((ge_first_ip_factor_append_equation) * (ge_second_rn_factor_append_equation))) + (((ge_first_in_factor_append_equation) * (ge_second_rp_factor_append_equation))))))) + ge_balance_positive_factor_append_equationoutputimaginary))))))))) -> exists d e. (((exists gr_inverse_factor_append_newunit. (exists ge_first_rp_factor_append_newunitidentity ge_first_rn_factor_append_newunitidentity ge_first_ip_factor_append_newunitidentity ge_first_in_factor_append_newunitidentity ge_second_rp_factor_append_newunitidentity ge_second_rn_factor_append_newunitidentity ge_second_ip_factor_append_newunitidentity ge_second_in_factor_append_newunitidentity. ((exists ge_representation_real_code_factor_append_newunitidentityfirst ge_representation_imaginary_code_factor_append_newunitidentityfirst. (((u) = ((ge_representation_real_code_factor_append_newunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newunitidentityfirst)) * S ((ge_representation_real_code_factor_append_newunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newunitidentityfirstreal ge_balance_negative_factor_append_newunitidentityfirstreal. (((((ge_representation_real_code_factor_append_newunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newunitidentityfirstreal) /\ (ge_balance_negative_factor_append_newunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newunitidentityfirst) = 2 * ge_signed_half_factor_append_newunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newunitidentityfirstreal) = S ge_signed_half_factor_append_newunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentityfirstreal = (ge_first_rn_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newunitidentityfirstimaginary ge_balance_negative_factor_append_newunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newunitidentityfirst) = 2 * ge_signed_half_factor_append_newunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newunitidentityfirstimaginary) = S ge_signed_half_factor_append_newunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentityfirstimaginary = (ge_first_in_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newunitidentitysecond ge_representation_imaginary_code_factor_append_newunitidentitysecond. (((gr_inverse_factor_append_newunit) = ((ge_representation_real_code_factor_append_newunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newunitidentitysecond)) * S ((ge_representation_real_code_factor_append_newunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newunitidentitysecondreal ge_balance_negative_factor_append_newunitidentitysecondreal. (((((ge_representation_real_code_factor_append_newunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newunitidentitysecondreal) /\ (ge_balance_negative_factor_append_newunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newunitidentitysecond) = 2 * ge_signed_half_factor_append_newunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newunitidentitysecondreal) = S ge_signed_half_factor_append_newunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentitysecondreal = (ge_second_rn_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newunitidentitysecondimaginary ge_balance_negative_factor_append_newunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newunitidentitysecond) = 2 * ge_signed_half_factor_append_newunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newunitidentitysecondimaginary) = S ge_signed_half_factor_append_newunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newunitidentity) + ge_balance_negative_factor_append_newunitidentitysecondimaginary = (ge_second_in_factor_append_newunitidentity) + ge_balance_positive_factor_append_newunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newunitidentityoutput ge_representation_imaginary_code_factor_append_newunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newunitidentityoutput)) * S ((ge_representation_real_code_factor_append_newunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newunitidentityoutputreal ge_balance_negative_factor_append_newunitidentityoutputreal. (((((ge_representation_real_code_factor_append_newunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newunitidentityoutputreal) /\ (ge_balance_negative_factor_append_newunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newunitidentityoutput) = 2 * ge_signed_half_factor_append_newunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newunitidentityoutputreal) = S ge_signed_half_factor_append_newunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))))))) + ge_balance_negative_factor_append_newunitidentityoutputreal = (((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))))))) + ge_balance_positive_factor_append_newunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newunitidentityoutputimaginary ge_balance_negative_factor_append_newunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newunitidentityoutput) = 2 * ge_signed_half_factor_append_newunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newunitidentityoutputimaginary) = S ge_signed_half_factor_append_newunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))))))) + ge_balance_negative_factor_append_newunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newunitidentity) * (ge_second_in_factor_append_newunitidentity))) + (((ge_first_rn_factor_append_newunitidentity) * (ge_second_ip_factor_append_newunitidentity))))) + (((((ge_first_ip_factor_append_newunitidentity) * (ge_second_rn_factor_append_newunitidentity))) + (((ge_first_in_factor_append_newunitidentity) * (ge_second_rp_factor_append_newunitidentity))))))) + ge_balance_positive_factor_append_newunitidentityoutputimaginary)))))))))) /\ ((forall gr_factor_index_factor_append_newirreducible gr_factor_value_factor_append_newirreducible. (exists ge_gap_factor_append_newirreducibleindex. ge_gap_factor_append_newirreducibleindex + S (gr_factor_index_factor_append_newirreducible) = (S l)) -> (((exists ff_h_gprod_factor_append_newirreducibleentry. ff_h_gprod_factor_append_newirreducibleentry + S (gr_factor_value_factor_append_newirreducible) = S ((S (gr_factor_index_factor_append_newirreducible)) * e)) /\ exists ff_q_gprod_factor_append_newirreducibleentry. d = ff_q_gprod_factor_append_newirreducibleentry * S ((S (gr_factor_index_factor_append_newirreducible)) * e) + (gr_factor_value_factor_append_newirreducible))) -> (((exists ge_real_positive_factor_append_newirreducibleirreduciblecarrier ge_real_negative_factor_append_newirreducibleirreduciblecarrier ge_imaginary_positive_factor_append_newirreducibleirreduciblecarrier ge_imaginary_negative_factor_append_newirreducibleirreduciblecarrier. (exists ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode. (((gr_factor_value_factor_append_newirreducible) = ((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode)) * S ((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode)) + ((ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode) + (ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode))) /\ (((((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * (ge_real_positive_factor_append_newirreducibleirreduciblecarrier) /\ (ge_real_negative_factor_append_newirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_real. (((ge_real_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_real + 1 /\ (ge_real_positive_factor_append_newirreducibleirreduciblecarrier) = 0) /\ (ge_real_negative_factor_append_newirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * (ge_imaginary_positive_factor_append_newirreducibleirreduciblecarrier) /\ (ge_imaginary_negative_factor_append_newirreducibleirreduciblecarrier) = 0) \/ exists ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_imaginary. (((ge_imaginary_code_factor_append_newirreducibleirreduciblecarrierdecode) = 2 * ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_factor_append_newirreducibleirreduciblecarrier) = 0) /\ (ge_imaginary_negative_factor_append_newirreducibleirreduciblecarrier) = S ge_signed_half_ge_factor_append_newirreducibleirreduciblecarrierdecode_imaginary))))))) /\ ((~((gr_factor_value_factor_append_newirreducible)=0)) /\ ((~(exists gr_inverse_factor_append_newirreducibleirreduciblenonunit. (exists ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst. (((gr_factor_value_factor_append_newirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond. (((gr_inverse_factor_append_newirreducibleirreduciblenonunit) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblenonunitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblenonunitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblenonunitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblenonunitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblenonunitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_factor_append_newirreducibleirreducible gr_second_factor_factor_append_newirreducibleirreducible. (exists ge_first_rp_factor_append_newirreducibleirreduciblefactorization ge_first_rn_factor_append_newirreducibleirreduciblefactorization ge_first_ip_factor_append_newirreducibleirreduciblefactorization ge_first_in_factor_append_newirreducibleirreduciblefactorization ge_second_rp_factor_append_newirreducibleirreduciblefactorization ge_second_rn_factor_append_newirreducibleirreduciblefactorization ge_second_ip_factor_append_newirreducibleirreduciblefactorization ge_second_in_factor_append_newirreducibleirreduciblefactorization. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst. (((gr_first_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond. (((gr_second_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationsecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblefactorization) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationsecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblefactorization) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput. (((gr_factor_value_factor_append_newirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefactorizationoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefactorizationoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefactorization) * (ge_second_in_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefactorization) * (ge_second_ip_factor_append_newirreducibleirreduciblefactorization))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rn_factor_append_newirreducibleirreduciblefactorization))) + (((ge_first_in_factor_append_newirreducibleirreduciblefactorization) * (ge_second_rp_factor_append_newirreducibleirreduciblefactorization))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_factor_append_newirreducibleirreduciblefirst_unit. (exists ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst. (((gr_first_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond. (((gr_inverse_factor_append_newirreducibleirreduciblefirst_unit) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblefirst_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblefirst_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblefirst_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblefirst_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_factor_append_newirreducibleirreduciblesecond_unit. (exists ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity. ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst. (((gr_second_factor_factor_append_newirreducibleirreducible) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal = (ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary = (ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond. (((gr_inverse_factor_append_newirreducibleirreduciblesecond_unit) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal = (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary = (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newirreducibleirreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_negative_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_in_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_rn_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_ip_factor_append_newirreducibleirreduciblesecond_unitidentity))))) + (((((ge_first_ip_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rn_factor_append_newirreducibleirreduciblesecond_unitidentity))) + (((ge_first_in_factor_append_newirreducibleirreduciblesecond_unitidentity) * (ge_second_rp_factor_append_newirreducibleirreduciblesecond_unitidentity))))))) + ge_balance_positive_factor_append_newirreducibleirreduciblesecond_unitidentityoutputimaginary)))))))))))))))) /\ (exists gr_factor_product_factor_append_new. ((exists gr_product_trace_factor_append_newtrace gr_product_scale_factor_append_newtrace. ((((exists ff_h_gprod_factor_append_newtracestart. ff_h_gprod_factor_append_newtracestart + S (6) = S ((S (0)) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtracestart. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtracestart * S ((S (0)) * gr_product_scale_factor_append_newtrace) + (6))) /\ ((((exists ff_h_gprod_factor_append_newtraceend. ff_h_gprod_factor_append_newtraceend + S (gr_factor_product_factor_append_new) = S ((S (S l)) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtraceend. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtraceend * S ((S (S l)) * gr_product_scale_factor_append_newtrace) + (gr_factor_product_factor_append_new))) /\ (forall gr_product_index_factor_append_newtracesteps. (exists ge_gap_factor_append_newtracestepsindex_bound. ge_gap_factor_append_newtracestepsindex_bound + S (gr_product_index_factor_append_newtracesteps) = (S l)) -> exists gr_product_factor_factor_append_newtracesteps gr_product_before_factor_append_newtracesteps gr_product_after_factor_append_newtracesteps. ((((exists ff_h_gprod_factor_append_newtracestepsfactor. ff_h_gprod_factor_append_newtracestepsfactor + S (gr_product_factor_factor_append_newtracesteps) = S ((S (gr_product_index_factor_append_newtracesteps)) * e)) /\ exists ff_q_gprod_factor_append_newtracestepsfactor. d = ff_q_gprod_factor_append_newtracestepsfactor * S ((S (gr_product_index_factor_append_newtracesteps)) * e) + (gr_product_factor_factor_append_newtracesteps))) /\ ((((exists ff_h_gprod_factor_append_newtracestepsbefore. ff_h_gprod_factor_append_newtracestepsbefore + S (gr_product_before_factor_append_newtracesteps) = S ((S (gr_product_index_factor_append_newtracesteps)) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtracestepsbefore. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtracestepsbefore * S ((S (gr_product_index_factor_append_newtracesteps)) * gr_product_scale_factor_append_newtrace) + (gr_product_before_factor_append_newtracesteps))) /\ ((((exists ff_h_gprod_factor_append_newtracestepsafter. ff_h_gprod_factor_append_newtracestepsafter + S (gr_product_after_factor_append_newtracesteps) = S ((S (S (gr_product_index_factor_append_newtracesteps))) * gr_product_scale_factor_append_newtrace)) /\ exists ff_q_gprod_factor_append_newtracestepsafter. gr_product_trace_factor_append_newtrace = ff_q_gprod_factor_append_newtracestepsafter * S ((S (S (gr_product_index_factor_append_newtracesteps))) * gr_product_scale_factor_append_newtrace) + (gr_product_after_factor_append_newtracesteps))) /\ (exists ge_first_rp_factor_append_newtracestepsmultiply ge_first_rn_factor_append_newtracestepsmultiply ge_first_ip_factor_append_newtracestepsmultiply ge_first_in_factor_append_newtracestepsmultiply ge_second_rp_factor_append_newtracestepsmultiply ge_second_rn_factor_append_newtracestepsmultiply ge_second_ip_factor_append_newtracestepsmultiply ge_second_in_factor_append_newtracestepsmultiply. ((exists ge_representation_real_code_factor_append_newtracestepsmultiplyfirst ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst. (((gr_product_before_factor_append_newtracesteps) = ((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst)) * S ((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst)) + ((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst))) /\ ((exists ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal. (((((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyfirstrealdecode. (((ge_representation_real_code_factor_append_newtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal) = S ge_signed_half_factor_append_newtracestepsmultiplyfirstrealdecode))) /\ ((ge_first_rp_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplyfirstreal = (ge_first_rn_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplyfirstreal))) /\ (exists ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyfirst) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary) = S ge_signed_half_factor_append_newtracestepsmultiplyfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplyfirstimaginary = (ge_first_in_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplyfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newtracestepsmultiplysecond ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond. (((gr_product_factor_factor_append_newtracesteps) = ((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond)) * S ((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond)) + ((ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond))) /\ ((exists ge_balance_positive_factor_append_newtracestepsmultiplysecondreal ge_balance_negative_factor_append_newtracestepsmultiplysecondreal. (((((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplysecondreal) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondreal) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplysecondrealdecode. (((ge_representation_real_code_factor_append_newtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_newtracestepsmultiplysecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplysecondreal) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondreal) = S ge_signed_half_factor_append_newtracestepsmultiplysecondrealdecode))) /\ ((ge_second_rp_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplysecondreal = (ge_second_rn_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplysecondreal))) /\ (exists ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary. (((((ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplysecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newtracestepsmultiplysecond) = 2 * ge_signed_half_factor_append_newtracestepsmultiplysecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary) = S ge_signed_half_factor_append_newtracestepsmultiplysecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newtracestepsmultiply) + ge_balance_negative_factor_append_newtracestepsmultiplysecondimaginary = (ge_second_in_factor_append_newtracestepsmultiply) + ge_balance_positive_factor_append_newtracestepsmultiplysecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newtracestepsmultiplyoutput ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput. (((gr_product_after_factor_append_newtracesteps) = ((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput)) * S ((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput)) + ((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput) + (ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput))) /\ ((exists ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal. (((((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyoutputrealdecode. (((ge_representation_real_code_factor_append_newtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal) = S ge_signed_half_factor_append_newtracestepsmultiplyoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))))))) + ge_balance_negative_factor_append_newtracestepsmultiplyoutputreal = (((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))))))) + ge_balance_positive_factor_append_newtracestepsmultiplyoutputreal))) /\ (exists ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput) = 2 * (ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newtracestepsmultiplyoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newtracestepsmultiplyoutput) = 2 * ge_signed_half_factor_append_newtracestepsmultiplyoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary) = S ge_signed_half_factor_append_newtracestepsmultiplyoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))))))) + ge_balance_negative_factor_append_newtracestepsmultiplyoutputimaginary = (((((((ge_first_rp_factor_append_newtracestepsmultiply) * (ge_second_in_factor_append_newtracestepsmultiply))) + (((ge_first_rn_factor_append_newtracestepsmultiply) * (ge_second_ip_factor_append_newtracestepsmultiply))))) + (((((ge_first_ip_factor_append_newtracestepsmultiply) * (ge_second_rn_factor_append_newtracestepsmultiply))) + (((ge_first_in_factor_append_newtracestepsmultiply) * (ge_second_rp_factor_append_newtracestepsmultiply))))))) + ge_balance_positive_factor_append_newtracestepsmultiplyoutputimaginary)))))))))))))))) /\ (exists ge_first_rp_factor_append_newreconstruct ge_first_rn_factor_append_newreconstruct ge_first_ip_factor_append_newreconstruct ge_first_in_factor_append_newreconstruct ge_second_rp_factor_append_newreconstruct ge_second_rn_factor_append_newreconstruct ge_second_ip_factor_append_newreconstruct ge_second_in_factor_append_newreconstruct. ((exists ge_representation_real_code_factor_append_newreconstructfirst ge_representation_imaginary_code_factor_append_newreconstructfirst. (((u) = ((ge_representation_real_code_factor_append_newreconstructfirst) + (ge_representation_imaginary_code_factor_append_newreconstructfirst)) * S ((ge_representation_real_code_factor_append_newreconstructfirst) + (ge_representation_imaginary_code_factor_append_newreconstructfirst)) + ((ge_representation_imaginary_code_factor_append_newreconstructfirst) + (ge_representation_imaginary_code_factor_append_newreconstructfirst))) /\ ((exists ge_balance_positive_factor_append_newreconstructfirstreal ge_balance_negative_factor_append_newreconstructfirstreal. (((((ge_representation_real_code_factor_append_newreconstructfirst) = 2 * (ge_balance_positive_factor_append_newreconstructfirstreal) /\ (ge_balance_negative_factor_append_newreconstructfirstreal) = 0) \/ exists ge_signed_half_factor_append_newreconstructfirstrealdecode. (((ge_representation_real_code_factor_append_newreconstructfirst) = 2 * ge_signed_half_factor_append_newreconstructfirstrealdecode + 1 /\ (ge_balance_positive_factor_append_newreconstructfirstreal) = 0) /\ (ge_balance_negative_factor_append_newreconstructfirstreal) = S ge_signed_half_factor_append_newreconstructfirstrealdecode))) /\ ((ge_first_rp_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructfirstreal = (ge_first_rn_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructfirstreal))) /\ (exists ge_balance_positive_factor_append_newreconstructfirstimaginary ge_balance_negative_factor_append_newreconstructfirstimaginary. (((((ge_representation_imaginary_code_factor_append_newreconstructfirst) = 2 * (ge_balance_positive_factor_append_newreconstructfirstimaginary) /\ (ge_balance_negative_factor_append_newreconstructfirstimaginary) = 0) \/ exists ge_signed_half_factor_append_newreconstructfirstimaginarydecode. (((ge_representation_imaginary_code_factor_append_newreconstructfirst) = 2 * ge_signed_half_factor_append_newreconstructfirstimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newreconstructfirstimaginary) = 0) /\ (ge_balance_negative_factor_append_newreconstructfirstimaginary) = S ge_signed_half_factor_append_newreconstructfirstimaginarydecode))) /\ ((ge_first_ip_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructfirstimaginary = (ge_first_in_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructfirstimaginary)))))) /\ ((exists ge_representation_real_code_factor_append_newreconstructsecond ge_representation_imaginary_code_factor_append_newreconstructsecond. (((gr_factor_product_factor_append_new) = ((ge_representation_real_code_factor_append_newreconstructsecond) + (ge_representation_imaginary_code_factor_append_newreconstructsecond)) * S ((ge_representation_real_code_factor_append_newreconstructsecond) + (ge_representation_imaginary_code_factor_append_newreconstructsecond)) + ((ge_representation_imaginary_code_factor_append_newreconstructsecond) + (ge_representation_imaginary_code_factor_append_newreconstructsecond))) /\ ((exists ge_balance_positive_factor_append_newreconstructsecondreal ge_balance_negative_factor_append_newreconstructsecondreal. (((((ge_representation_real_code_factor_append_newreconstructsecond) = 2 * (ge_balance_positive_factor_append_newreconstructsecondreal) /\ (ge_balance_negative_factor_append_newreconstructsecondreal) = 0) \/ exists ge_signed_half_factor_append_newreconstructsecondrealdecode. (((ge_representation_real_code_factor_append_newreconstructsecond) = 2 * ge_signed_half_factor_append_newreconstructsecondrealdecode + 1 /\ (ge_balance_positive_factor_append_newreconstructsecondreal) = 0) /\ (ge_balance_negative_factor_append_newreconstructsecondreal) = S ge_signed_half_factor_append_newreconstructsecondrealdecode))) /\ ((ge_second_rp_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructsecondreal = (ge_second_rn_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructsecondreal))) /\ (exists ge_balance_positive_factor_append_newreconstructsecondimaginary ge_balance_negative_factor_append_newreconstructsecondimaginary. (((((ge_representation_imaginary_code_factor_append_newreconstructsecond) = 2 * (ge_balance_positive_factor_append_newreconstructsecondimaginary) /\ (ge_balance_negative_factor_append_newreconstructsecondimaginary) = 0) \/ exists ge_signed_half_factor_append_newreconstructsecondimaginarydecode. (((ge_representation_imaginary_code_factor_append_newreconstructsecond) = 2 * ge_signed_half_factor_append_newreconstructsecondimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newreconstructsecondimaginary) = 0) /\ (ge_balance_negative_factor_append_newreconstructsecondimaginary) = S ge_signed_half_factor_append_newreconstructsecondimaginarydecode))) /\ ((ge_second_ip_factor_append_newreconstruct) + ge_balance_negative_factor_append_newreconstructsecondimaginary = (ge_second_in_factor_append_newreconstruct) + ge_balance_positive_factor_append_newreconstructsecondimaginary)))))) /\ (exists ge_representation_real_code_factor_append_newreconstructoutput ge_representation_imaginary_code_factor_append_newreconstructoutput. (((w) = ((ge_representation_real_code_factor_append_newreconstructoutput) + (ge_representation_imaginary_code_factor_append_newreconstructoutput)) * S ((ge_representation_real_code_factor_append_newreconstructoutput) + (ge_representation_imaginary_code_factor_append_newreconstructoutput)) + ((ge_representation_imaginary_code_factor_append_newreconstructoutput) + (ge_representation_imaginary_code_factor_append_newreconstructoutput))) /\ ((exists ge_balance_positive_factor_append_newreconstructoutputreal ge_balance_negative_factor_append_newreconstructoutputreal. (((((ge_representation_real_code_factor_append_newreconstructoutput) = 2 * (ge_balance_positive_factor_append_newreconstructoutputreal) /\ (ge_balance_negative_factor_append_newreconstructoutputreal) = 0) \/ exists ge_signed_half_factor_append_newreconstructoutputrealdecode. (((ge_representation_real_code_factor_append_newreconstructoutput) = 2 * ge_signed_half_factor_append_newreconstructoutputrealdecode + 1 /\ (ge_balance_positive_factor_append_newreconstructoutputreal) = 0) /\ (ge_balance_negative_factor_append_newreconstructoutputreal) = S ge_signed_half_factor_append_newreconstructoutputrealdecode))) /\ ((((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))))))) + ge_balance_negative_factor_append_newreconstructoutputreal = (((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))))))) + ge_balance_positive_factor_append_newreconstructoutputreal))) /\ (exists ge_balance_positive_factor_append_newreconstructoutputimaginary ge_balance_negative_factor_append_newreconstructoutputimaginary. (((((ge_representation_imaginary_code_factor_append_newreconstructoutput) = 2 * (ge_balance_positive_factor_append_newreconstructoutputimaginary) /\ (ge_balance_negative_factor_append_newreconstructoutputimaginary) = 0) \/ exists ge_signed_half_factor_append_newreconstructoutputimaginarydecode. (((ge_representation_imaginary_code_factor_append_newreconstructoutput) = 2 * ge_signed_half_factor_append_newreconstructoutputimaginarydecode + 1 /\ (ge_balance_positive_factor_append_newreconstructoutputimaginary) = 0) /\ (ge_balance_negative_factor_append_newreconstructoutputimaginary) = S ge_signed_half_factor_append_newreconstructoutputimaginarydecode))) /\ ((((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))))))) + ge_balance_negative_factor_append_newreconstructoutputimaginary = (((((((ge_first_rp_factor_append_newreconstruct) * (ge_second_in_factor_append_newreconstruct))) + (((ge_first_rn_factor_append_newreconstruct) * (ge_second_ip_factor_append_newreconstruct))))) + (((((ge_first_ip_factor_append_newreconstruct) * (ge_second_rn_factor_append_newreconstruct))) + (((ge_first_in_factor_append_newreconstruct) * (ge_second_rp_factor_append_newreconstruct))))))) + ge_balance_positive_factor_append_newreconstructoutputimaginary))))))))))))))Complete tactic proof in conservative notation
All 84 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
84 script commands · 18 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (5)
01Fix variables and assumptionsL1–10
02Separate the logical casesL11–17
03Establish hextL18–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix extend.
- L18
have hext : ∃ d. ∃ e. BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))Definitions: BetaAt(d,e,l,p)Lt(x,l)BetaAt(b,c,x,y)BetaAt(d,e,x,y)Original native command in the exact edition - L19
specialize beta_prefix_extend (l) - L20
specialize beta_prefix_extend (b) - L21
specialize beta_prefix_extend (c) - L22
specialize beta_prefix_extend (p) - L23
apply beta_prefix_extend
04Separate the logical casesL24–26
05Establish hQL27–36
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply exists.
- L27
- L28
specialize gaussian_multiply_exists (x) - L29
specialize gaussian_multiply_exists (p) - L30
apply gaussian_multiply_exists - L31
specialize gaussian_product_result_valid (l) - L32
specialize gaussian_product_result_valid (b) - L33
specialize gaussian_product_result_valid (c) - L34
specialize gaussian_product_result_valid (x) - L35
apply gaussian_product_result_valid - L36
exact hf_right_right_witness_left
06Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
exact hp_left
07Separate the logical casesL38–38
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L38
cases hQ
08Construct an explicit witnessL39–40
09Separate the logical casesL41–41
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L41
split
10Use earlier factsL42–42
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L42
exact hf_left
11Separate the logical casesL43–43
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L43
split
12Use earlier factsL44–53
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
specialize gaussian_all_irreducible_append (b) - L45
specialize gaussian_all_irreducible_append (c) - L46
specialize gaussian_all_irreducible_append (x1) - L47
specialize gaussian_all_irreducible_append (x2) - L48
specialize gaussian_all_irreducible_append (l) - L49
specialize gaussian_all_irreducible_append (p) - L50
apply gaussian_all_irreducible_append - L51
exact hf_right_left - L52
exact hext_witness_witness_right - L53
exact hext_witness_witness_left
13Use earlier factsL54–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
exact hp
14Construct an explicit witnessL55–55
Supply the displayed value, then prove that it has the required property.
- L55
exists (x3)
15Separate the logical casesL56–56
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L56
split
16Use earlier factsL57–66
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L57
specialize gaussian_product_successor_intro (x1) - L58
specialize gaussian_product_successor_intro (x2) - L59
specialize gaussian_product_successor_intro (l) - L60
specialize gaussian_product_successor_intro (x) - L61
specialize gaussian_product_successor_intro (p) - L62
specialize gaussian_product_successor_intro (x3) - L63
apply gaussian_product_successor_intro - L64
specialize gaussian_product_prefix_recode (b) - L65
specialize gaussian_product_prefix_recode (c) - L66
specialize gaussian_product_prefix_recode (x1)
17Use earlier factsL67–76
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L67
specialize gaussian_product_prefix_recode (x2) - L68
specialize gaussian_product_prefix_recode (l) - L69
specialize gaussian_product_prefix_recode (x) - L70
apply gaussian_product_prefix_recode - L71
exact hf_right_right_witness_left - L72
exact hext_witness_witness_right - L73
exact hext_witness_witness_left - L74
exact hQ_witness - L75
specialize gaussian_multiply_associative (u) - L76
specialize gaussian_multiply_associative (x)
18Use earlier factsL77–84
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 84 lines
- 0001
intro z - 0002
intro u - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro p - 0007
intro w - 0008
intro hf - 0009
intro hp - 0010
intro hm - 0011
cases hf - 0012
cases hf_right - 0013
cases hf_right_right - 0014
cases hf_right_right_witness - 0015
cases hp - 0016
cases hp_right - 0017
cases hp_right_right - 0018
have hext : ∃ d. ∃ e. BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)) - 0019
specialize beta_prefix_extend (l) - 0020
specialize beta_prefix_extend (b) - 0021
specialize beta_prefix_extend (c) - 0022
specialize beta_prefix_extend (p) - 0023
apply beta_prefix_extend - 0024
cases hext - 0025
cases hext_witness - 0026
cases hext_witness_witness - 0027
have hQ : ∃ Q. GMul(x,p,Q) - 0028
specialize gaussian_multiply_exists (x) - 0029
specialize gaussian_multiply_exists (p) - 0030
apply gaussian_multiply_exists - 0031
specialize gaussian_product_result_valid (l) - 0032
specialize gaussian_product_result_valid (b) - 0033
specialize gaussian_product_result_valid (c) - 0034
specialize gaussian_product_result_valid (x) - 0035
apply gaussian_product_result_valid - 0036
exact hf_right_right_witness_left - 0037
exact hp_left - 0038
cases hQ - 0039
exists (x1) - 0040
exists (x2) - 0041
split - 0042
exact hf_left - 0043
split - 0044
specialize gaussian_all_irreducible_append (b) - 0045
specialize gaussian_all_irreducible_append (c) - 0046
specialize gaussian_all_irreducible_append (x1) - 0047
specialize gaussian_all_irreducible_append (x2) - 0048
specialize gaussian_all_irreducible_append (l) - 0049
specialize gaussian_all_irreducible_append (p) - 0050
apply gaussian_all_irreducible_append - 0051
exact hf_right_left - 0052
exact hext_witness_witness_right - 0053
exact hext_witness_witness_left - 0054
exact hp - 0055
exists (x3) - 0056
split - 0057
specialize gaussian_product_successor_intro (x1) - 0058
specialize gaussian_product_successor_intro (x2) - 0059
specialize gaussian_product_successor_intro (l) - 0060
specialize gaussian_product_successor_intro (x) - 0061
specialize gaussian_product_successor_intro (p) - 0062
specialize gaussian_product_successor_intro (x3) - 0063
apply gaussian_product_successor_intro - 0064
specialize gaussian_product_prefix_recode (b) - 0065
specialize gaussian_product_prefix_recode (c) - 0066
specialize gaussian_product_prefix_recode (x1) - 0067
specialize gaussian_product_prefix_recode (x2) - 0068
specialize gaussian_product_prefix_recode (l) - 0069
specialize gaussian_product_prefix_recode (x) - 0070
apply gaussian_product_prefix_recode - 0071
exact hf_right_right_witness_left - 0072
exact hext_witness_witness_right - 0073
exact hext_witness_witness_left - 0074
exact hQ_witness - 0075
specialize gaussian_multiply_associative (u) - 0076
specialize gaussian_multiply_associative (x) - 0077
specialize gaussian_multiply_associative (p) - 0078
specialize gaussian_multiply_associative (z) - 0079
specialize gaussian_multiply_associative (x3) - 0080
specialize gaussian_multiply_associative (w) - 0081
apply gaussian_multiply_associative - 0082
exact hf_right_right_witness_right - 0083
exact hm - 0084
exact hQ_witness