GF00A5 — gaussian_factor_associate_cancel_products

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

∀ R. ∀ p. ∀ P. ∀ T. ∀ q. ∀ Q. GMul(R,p,P) → GMul(T,q,Q) → GAssociate(P,Q) → GAssociate(p,q) → ¬p = 0 → GAssociate(R,T)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GMul(a,b,c) · 4 GAssociate(a,b) · 3

Actual proof prerequisites

gaussian_multiply_exists · checked external prerequisite gaussian_unit_valid gaussian_multiply_input_left_valid gaussian_multiply_associative_reverse gaussian_multiply_commutative gaussian_multiply_cancel_right gaussian_factor_associate_code_transport gaussian_associate_transitive gaussian_associate_symmetric

Original expanded first-order statement

forall R p P T q Q. (exists ge_first_rp_cancel_first_product ge_first_rn_cancel_first_product ge_first_ip_cancel_first_product ge_first_in_cancel_first_product ge_second_rp_cancel_first_product ge_second_rn_cancel_first_product ge_second_ip_cancel_first_product ge_second_in_cancel_first_product. ((exists ge_representation_real_code_cancel_first_productfirst ge_representation_imaginary_code_cancel_first_productfirst. (((R) = ((ge_representation_real_code_cancel_first_productfirst) + (ge_representation_imaginary_code_cancel_first_productfirst)) * S ((ge_representation_real_code_cancel_first_productfirst) + (ge_representation_imaginary_code_cancel_first_productfirst)) + ((ge_representation_imaginary_code_cancel_first_productfirst) + (ge_representation_imaginary_code_cancel_first_productfirst))) /\ ((exists ge_balance_positive_cancel_first_productfirstreal ge_balance_negative_cancel_first_productfirstreal. (((((ge_representation_real_code_cancel_first_productfirst) = 2 * (ge_balance_positive_cancel_first_productfirstreal) /\ (ge_balance_negative_cancel_first_productfirstreal) = 0) \/ exists ge_signed_half_cancel_first_productfirstrealdecode. (((ge_representation_real_code_cancel_first_productfirst) = 2 * ge_signed_half_cancel_first_productfirstrealdecode + 1 /\ (ge_balance_positive_cancel_first_productfirstreal) = 0) /\ (ge_balance_negative_cancel_first_productfirstreal) = S ge_signed_half_cancel_first_productfirstrealdecode))) /\ ((ge_first_rp_cancel_first_product) + ge_balance_negative_cancel_first_productfirstreal = (ge_first_rn_cancel_first_product) + ge_balance_positive_cancel_first_productfirstreal))) /\ (exists ge_balance_positive_cancel_first_productfirstimaginary ge_balance_negative_cancel_first_productfirstimaginary. (((((ge_representation_imaginary_code_cancel_first_productfirst) = 2 * (ge_balance_positive_cancel_first_productfirstimaginary) /\ (ge_balance_negative_cancel_first_productfirstimaginary) = 0) \/ exists ge_signed_half_cancel_first_productfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_first_productfirst) = 2 * ge_signed_half_cancel_first_productfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_first_productfirstimaginary) = 0) /\ (ge_balance_negative_cancel_first_productfirstimaginary) = S ge_signed_half_cancel_first_productfirstimaginarydecode))) /\ ((ge_first_ip_cancel_first_product) + ge_balance_negative_cancel_first_productfirstimaginary = (ge_first_in_cancel_first_product) + ge_balance_positive_cancel_first_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_first_productsecond ge_representation_imaginary_code_cancel_first_productsecond. (((p) = ((ge_representation_real_code_cancel_first_productsecond) + (ge_representation_imaginary_code_cancel_first_productsecond)) * S ((ge_representation_real_code_cancel_first_productsecond) + (ge_representation_imaginary_code_cancel_first_productsecond)) + ((ge_representation_imaginary_code_cancel_first_productsecond) + (ge_representation_imaginary_code_cancel_first_productsecond))) /\ ((exists ge_balance_positive_cancel_first_productsecondreal ge_balance_negative_cancel_first_productsecondreal. (((((ge_representation_real_code_cancel_first_productsecond) = 2 * (ge_balance_positive_cancel_first_productsecondreal) /\ (ge_balance_negative_cancel_first_productsecondreal) = 0) \/ exists ge_signed_half_cancel_first_productsecondrealdecode. (((ge_representation_real_code_cancel_first_productsecond) = 2 * ge_signed_half_cancel_first_productsecondrealdecode + 1 /\ (ge_balance_positive_cancel_first_productsecondreal) = 0) /\ (ge_balance_negative_cancel_first_productsecondreal) = S ge_signed_half_cancel_first_productsecondrealdecode))) /\ ((ge_second_rp_cancel_first_product) + ge_balance_negative_cancel_first_productsecondreal = (ge_second_rn_cancel_first_product) + ge_balance_positive_cancel_first_productsecondreal))) /\ (exists ge_balance_positive_cancel_first_productsecondimaginary ge_balance_negative_cancel_first_productsecondimaginary. (((((ge_representation_imaginary_code_cancel_first_productsecond) = 2 * (ge_balance_positive_cancel_first_productsecondimaginary) /\ (ge_balance_negative_cancel_first_productsecondimaginary) = 0) \/ exists ge_signed_half_cancel_first_productsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_first_productsecond) = 2 * ge_signed_half_cancel_first_productsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_first_productsecondimaginary) = 0) /\ (ge_balance_negative_cancel_first_productsecondimaginary) = S ge_signed_half_cancel_first_productsecondimaginarydecode))) /\ ((ge_second_ip_cancel_first_product) + ge_balance_negative_cancel_first_productsecondimaginary = (ge_second_in_cancel_first_product) + ge_balance_positive_cancel_first_productsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_first_productoutput ge_representation_imaginary_code_cancel_first_productoutput. (((P) = ((ge_representation_real_code_cancel_first_productoutput) + (ge_representation_imaginary_code_cancel_first_productoutput)) * S ((ge_representation_real_code_cancel_first_productoutput) + (ge_representation_imaginary_code_cancel_first_productoutput)) + ((ge_representation_imaginary_code_cancel_first_productoutput) + (ge_representation_imaginary_code_cancel_first_productoutput))) /\ ((exists ge_balance_positive_cancel_first_productoutputreal ge_balance_negative_cancel_first_productoutputreal. (((((ge_representation_real_code_cancel_first_productoutput) = 2 * (ge_balance_positive_cancel_first_productoutputreal) /\ (ge_balance_negative_cancel_first_productoutputreal) = 0) \/ exists ge_signed_half_cancel_first_productoutputrealdecode. (((ge_representation_real_code_cancel_first_productoutput) = 2 * ge_signed_half_cancel_first_productoutputrealdecode + 1 /\ (ge_balance_positive_cancel_first_productoutputreal) = 0) /\ (ge_balance_negative_cancel_first_productoutputreal) = S ge_signed_half_cancel_first_productoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_first_product) * (ge_second_rp_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_rn_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_in_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_ip_cancel_first_product))))))) + ge_balance_negative_cancel_first_productoutputreal = (((((((ge_first_rp_cancel_first_product) * (ge_second_rn_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_rp_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_ip_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_in_cancel_first_product))))))) + ge_balance_positive_cancel_first_productoutputreal))) /\ (exists ge_balance_positive_cancel_first_productoutputimaginary ge_balance_negative_cancel_first_productoutputimaginary. (((((ge_representation_imaginary_code_cancel_first_productoutput) = 2 * (ge_balance_positive_cancel_first_productoutputimaginary) /\ (ge_balance_negative_cancel_first_productoutputimaginary) = 0) \/ exists ge_signed_half_cancel_first_productoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_first_productoutput) = 2 * ge_signed_half_cancel_first_productoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_first_productoutputimaginary) = 0) /\ (ge_balance_negative_cancel_first_productoutputimaginary) = S ge_signed_half_cancel_first_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_first_product) * (ge_second_ip_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_in_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_rp_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_rn_cancel_first_product))))))) + ge_balance_negative_cancel_first_productoutputimaginary = (((((((ge_first_rp_cancel_first_product) * (ge_second_in_cancel_first_product))) + (((ge_first_rn_cancel_first_product) * (ge_second_ip_cancel_first_product))))) + (((((ge_first_ip_cancel_first_product) * (ge_second_rn_cancel_first_product))) + (((ge_first_in_cancel_first_product) * (ge_second_rp_cancel_first_product))))))) + ge_balance_positive_cancel_first_productoutputimaginary))))))))) -> (exists ge_first_rp_cancel_second_product ge_first_rn_cancel_second_product ge_first_ip_cancel_second_product ge_first_in_cancel_second_product ge_second_rp_cancel_second_product ge_second_rn_cancel_second_product ge_second_ip_cancel_second_product ge_second_in_cancel_second_product. ((exists ge_representation_real_code_cancel_second_productfirst ge_representation_imaginary_code_cancel_second_productfirst. (((T) = ((ge_representation_real_code_cancel_second_productfirst) + (ge_representation_imaginary_code_cancel_second_productfirst)) * S ((ge_representation_real_code_cancel_second_productfirst) + (ge_representation_imaginary_code_cancel_second_productfirst)) + ((ge_representation_imaginary_code_cancel_second_productfirst) + (ge_representation_imaginary_code_cancel_second_productfirst))) /\ ((exists ge_balance_positive_cancel_second_productfirstreal ge_balance_negative_cancel_second_productfirstreal. (((((ge_representation_real_code_cancel_second_productfirst) = 2 * (ge_balance_positive_cancel_second_productfirstreal) /\ (ge_balance_negative_cancel_second_productfirstreal) = 0) \/ exists ge_signed_half_cancel_second_productfirstrealdecode. (((ge_representation_real_code_cancel_second_productfirst) = 2 * ge_signed_half_cancel_second_productfirstrealdecode + 1 /\ (ge_balance_positive_cancel_second_productfirstreal) = 0) /\ (ge_balance_negative_cancel_second_productfirstreal) = S ge_signed_half_cancel_second_productfirstrealdecode))) /\ ((ge_first_rp_cancel_second_product) + ge_balance_negative_cancel_second_productfirstreal = (ge_first_rn_cancel_second_product) + ge_balance_positive_cancel_second_productfirstreal))) /\ (exists ge_balance_positive_cancel_second_productfirstimaginary ge_balance_negative_cancel_second_productfirstimaginary. (((((ge_representation_imaginary_code_cancel_second_productfirst) = 2 * (ge_balance_positive_cancel_second_productfirstimaginary) /\ (ge_balance_negative_cancel_second_productfirstimaginary) = 0) \/ exists ge_signed_half_cancel_second_productfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_second_productfirst) = 2 * ge_signed_half_cancel_second_productfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_second_productfirstimaginary) = 0) /\ (ge_balance_negative_cancel_second_productfirstimaginary) = S ge_signed_half_cancel_second_productfirstimaginarydecode))) /\ ((ge_first_ip_cancel_second_product) + ge_balance_negative_cancel_second_productfirstimaginary = (ge_first_in_cancel_second_product) + ge_balance_positive_cancel_second_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_second_productsecond ge_representation_imaginary_code_cancel_second_productsecond. (((q) = ((ge_representation_real_code_cancel_second_productsecond) + (ge_representation_imaginary_code_cancel_second_productsecond)) * S ((ge_representation_real_code_cancel_second_productsecond) + (ge_representation_imaginary_code_cancel_second_productsecond)) + ((ge_representation_imaginary_code_cancel_second_productsecond) + (ge_representation_imaginary_code_cancel_second_productsecond))) /\ ((exists ge_balance_positive_cancel_second_productsecondreal ge_balance_negative_cancel_second_productsecondreal. (((((ge_representation_real_code_cancel_second_productsecond) = 2 * (ge_balance_positive_cancel_second_productsecondreal) /\ (ge_balance_negative_cancel_second_productsecondreal) = 0) \/ exists ge_signed_half_cancel_second_productsecondrealdecode. (((ge_representation_real_code_cancel_second_productsecond) = 2 * ge_signed_half_cancel_second_productsecondrealdecode + 1 /\ (ge_balance_positive_cancel_second_productsecondreal) = 0) /\ (ge_balance_negative_cancel_second_productsecondreal) = S ge_signed_half_cancel_second_productsecondrealdecode))) /\ ((ge_second_rp_cancel_second_product) + ge_balance_negative_cancel_second_productsecondreal = (ge_second_rn_cancel_second_product) + ge_balance_positive_cancel_second_productsecondreal))) /\ (exists ge_balance_positive_cancel_second_productsecondimaginary ge_balance_negative_cancel_second_productsecondimaginary. (((((ge_representation_imaginary_code_cancel_second_productsecond) = 2 * (ge_balance_positive_cancel_second_productsecondimaginary) /\ (ge_balance_negative_cancel_second_productsecondimaginary) = 0) \/ exists ge_signed_half_cancel_second_productsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_second_productsecond) = 2 * ge_signed_half_cancel_second_productsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_second_productsecondimaginary) = 0) /\ (ge_balance_negative_cancel_second_productsecondimaginary) = S ge_signed_half_cancel_second_productsecondimaginarydecode))) /\ ((ge_second_ip_cancel_second_product) + ge_balance_negative_cancel_second_productsecondimaginary = (ge_second_in_cancel_second_product) + ge_balance_positive_cancel_second_productsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_second_productoutput ge_representation_imaginary_code_cancel_second_productoutput. (((Q) = ((ge_representation_real_code_cancel_second_productoutput) + (ge_representation_imaginary_code_cancel_second_productoutput)) * S ((ge_representation_real_code_cancel_second_productoutput) + (ge_representation_imaginary_code_cancel_second_productoutput)) + ((ge_representation_imaginary_code_cancel_second_productoutput) + (ge_representation_imaginary_code_cancel_second_productoutput))) /\ ((exists ge_balance_positive_cancel_second_productoutputreal ge_balance_negative_cancel_second_productoutputreal. (((((ge_representation_real_code_cancel_second_productoutput) = 2 * (ge_balance_positive_cancel_second_productoutputreal) /\ (ge_balance_negative_cancel_second_productoutputreal) = 0) \/ exists ge_signed_half_cancel_second_productoutputrealdecode. (((ge_representation_real_code_cancel_second_productoutput) = 2 * ge_signed_half_cancel_second_productoutputrealdecode + 1 /\ (ge_balance_positive_cancel_second_productoutputreal) = 0) /\ (ge_balance_negative_cancel_second_productoutputreal) = S ge_signed_half_cancel_second_productoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_second_product) * (ge_second_rp_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_rn_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_in_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_ip_cancel_second_product))))))) + ge_balance_negative_cancel_second_productoutputreal = (((((((ge_first_rp_cancel_second_product) * (ge_second_rn_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_rp_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_ip_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_in_cancel_second_product))))))) + ge_balance_positive_cancel_second_productoutputreal))) /\ (exists ge_balance_positive_cancel_second_productoutputimaginary ge_balance_negative_cancel_second_productoutputimaginary. (((((ge_representation_imaginary_code_cancel_second_productoutput) = 2 * (ge_balance_positive_cancel_second_productoutputimaginary) /\ (ge_balance_negative_cancel_second_productoutputimaginary) = 0) \/ exists ge_signed_half_cancel_second_productoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_second_productoutput) = 2 * ge_signed_half_cancel_second_productoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_second_productoutputimaginary) = 0) /\ (ge_balance_negative_cancel_second_productoutputimaginary) = S ge_signed_half_cancel_second_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_second_product) * (ge_second_ip_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_in_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_rp_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_rn_cancel_second_product))))))) + ge_balance_negative_cancel_second_productoutputimaginary = (((((((ge_first_rp_cancel_second_product) * (ge_second_in_cancel_second_product))) + (((ge_first_rn_cancel_second_product) * (ge_second_ip_cancel_second_product))))) + (((((ge_first_ip_cancel_second_product) * (ge_second_rn_cancel_second_product))) + (((ge_first_in_cancel_second_product) * (ge_second_rp_cancel_second_product))))))) + ge_balance_positive_cancel_second_productoutputimaginary))))))))) -> (exists gr_unit_cancel_total_associate. ((exists gr_inverse_cancel_total_associateunit. (exists ge_first_rp_cancel_total_associateunitidentity ge_first_rn_cancel_total_associateunitidentity ge_first_ip_cancel_total_associateunitidentity ge_first_in_cancel_total_associateunitidentity ge_second_rp_cancel_total_associateunitidentity ge_second_rn_cancel_total_associateunitidentity ge_second_ip_cancel_total_associateunitidentity ge_second_in_cancel_total_associateunitidentity. ((exists ge_representation_real_code_cancel_total_associateunitidentityfirst ge_representation_imaginary_code_cancel_total_associateunitidentityfirst. (((gr_unit_cancel_total_associate) = ((ge_representation_real_code_cancel_total_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_total_associateunitidentityfirst)) * S ((ge_representation_real_code_cancel_total_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_total_associateunitidentityfirst)) + ((ge_representation_imaginary_code_cancel_total_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_total_associateunitidentityfirst))) /\ ((exists ge_balance_positive_cancel_total_associateunitidentityfirstreal ge_balance_negative_cancel_total_associateunitidentityfirstreal. (((((ge_representation_real_code_cancel_total_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_total_associateunitidentityfirstreal) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityfirstrealdecode. (((ge_representation_real_code_cancel_total_associateunitidentityfirst) = 2 * ge_signed_half_cancel_total_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstreal) = S ge_signed_half_cancel_total_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentityfirstreal = (ge_first_rn_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_cancel_total_associateunitidentityfirstimaginary ge_balance_negative_cancel_total_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_cancel_total_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_total_associateunitidentityfirstimaginary) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associateunitidentityfirst) = 2 * ge_signed_half_cancel_total_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityfirstimaginary) = S ge_signed_half_cancel_total_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentityfirstimaginary = (ge_first_in_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_total_associateunitidentitysecond ge_representation_imaginary_code_cancel_total_associateunitidentitysecond. (((gr_inverse_cancel_total_associateunit) = ((ge_representation_real_code_cancel_total_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_total_associateunitidentitysecond)) * S ((ge_representation_real_code_cancel_total_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_total_associateunitidentitysecond)) + ((ge_representation_imaginary_code_cancel_total_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_total_associateunitidentitysecond))) /\ ((exists ge_balance_positive_cancel_total_associateunitidentitysecondreal ge_balance_negative_cancel_total_associateunitidentitysecondreal. (((((ge_representation_real_code_cancel_total_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_total_associateunitidentitysecondreal) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentitysecondrealdecode. (((ge_representation_real_code_cancel_total_associateunitidentitysecond) = 2 * ge_signed_half_cancel_total_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondreal) = S ge_signed_half_cancel_total_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentitysecondreal = (ge_second_rn_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_cancel_total_associateunitidentitysecondimaginary ge_balance_negative_cancel_total_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_cancel_total_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_total_associateunitidentitysecondimaginary) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associateunitidentitysecond) = 2 * ge_signed_half_cancel_total_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentitysecondimaginary) = S ge_signed_half_cancel_total_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cancel_total_associateunitidentity) + ge_balance_negative_cancel_total_associateunitidentitysecondimaginary = (ge_second_in_cancel_total_associateunitidentity) + ge_balance_positive_cancel_total_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_total_associateunitidentityoutput ge_representation_imaginary_code_cancel_total_associateunitidentityoutput. (((6) = ((ge_representation_real_code_cancel_total_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_total_associateunitidentityoutput)) * S ((ge_representation_real_code_cancel_total_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_total_associateunitidentityoutput)) + ((ge_representation_imaginary_code_cancel_total_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_total_associateunitidentityoutput))) /\ ((exists ge_balance_positive_cancel_total_associateunitidentityoutputreal ge_balance_negative_cancel_total_associateunitidentityoutputreal. (((((ge_representation_real_code_cancel_total_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_total_associateunitidentityoutputreal) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityoutputrealdecode. (((ge_representation_real_code_cancel_total_associateunitidentityoutput) = 2 * ge_signed_half_cancel_total_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputreal) = S ge_signed_half_cancel_total_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))))))) + ge_balance_negative_cancel_total_associateunitidentityoutputreal = (((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))))))) + ge_balance_positive_cancel_total_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_cancel_total_associateunitidentityoutputimaginary ge_balance_negative_cancel_total_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_cancel_total_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_total_associateunitidentityoutputimaginary) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cancel_total_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associateunitidentityoutput) = 2 * ge_signed_half_cancel_total_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cancel_total_associateunitidentityoutputimaginary) = S ge_signed_half_cancel_total_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))))))) + ge_balance_negative_cancel_total_associateunitidentityoutputimaginary = (((((((ge_first_rp_cancel_total_associateunitidentity) * (ge_second_in_cancel_total_associateunitidentity))) + (((ge_first_rn_cancel_total_associateunitidentity) * (ge_second_ip_cancel_total_associateunitidentity))))) + (((((ge_first_ip_cancel_total_associateunitidentity) * (ge_second_rn_cancel_total_associateunitidentity))) + (((ge_first_in_cancel_total_associateunitidentity) * (ge_second_rp_cancel_total_associateunitidentity))))))) + ge_balance_positive_cancel_total_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_cancel_total_associatetransport ge_first_rn_cancel_total_associatetransport ge_first_ip_cancel_total_associatetransport ge_first_in_cancel_total_associatetransport ge_second_rp_cancel_total_associatetransport ge_second_rn_cancel_total_associatetransport ge_second_ip_cancel_total_associatetransport ge_second_in_cancel_total_associatetransport. ((exists ge_representation_real_code_cancel_total_associatetransportfirst ge_representation_imaginary_code_cancel_total_associatetransportfirst. (((gr_unit_cancel_total_associate) = ((ge_representation_real_code_cancel_total_associatetransportfirst) + (ge_representation_imaginary_code_cancel_total_associatetransportfirst)) * S ((ge_representation_real_code_cancel_total_associatetransportfirst) + (ge_representation_imaginary_code_cancel_total_associatetransportfirst)) + ((ge_representation_imaginary_code_cancel_total_associatetransportfirst) + (ge_representation_imaginary_code_cancel_total_associatetransportfirst))) /\ ((exists ge_balance_positive_cancel_total_associatetransportfirstreal ge_balance_negative_cancel_total_associatetransportfirstreal. (((((ge_representation_real_code_cancel_total_associatetransportfirst) = 2 * (ge_balance_positive_cancel_total_associatetransportfirstreal) /\ (ge_balance_negative_cancel_total_associatetransportfirstreal) = 0) \/ exists ge_signed_half_cancel_total_associatetransportfirstrealdecode. (((ge_representation_real_code_cancel_total_associatetransportfirst) = 2 * ge_signed_half_cancel_total_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportfirstreal) = 0) /\ (ge_balance_negative_cancel_total_associatetransportfirstreal) = S ge_signed_half_cancel_total_associatetransportfirstrealdecode))) /\ ((ge_first_rp_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportfirstreal = (ge_first_rn_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportfirstreal))) /\ (exists ge_balance_positive_cancel_total_associatetransportfirstimaginary ge_balance_negative_cancel_total_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_cancel_total_associatetransportfirst) = 2 * (ge_balance_positive_cancel_total_associatetransportfirstimaginary) /\ (ge_balance_negative_cancel_total_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_cancel_total_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associatetransportfirst) = 2 * ge_signed_half_cancel_total_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_cancel_total_associatetransportfirstimaginary) = S ge_signed_half_cancel_total_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportfirstimaginary = (ge_first_in_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_total_associatetransportsecond ge_representation_imaginary_code_cancel_total_associatetransportsecond. (((P) = ((ge_representation_real_code_cancel_total_associatetransportsecond) + (ge_representation_imaginary_code_cancel_total_associatetransportsecond)) * S ((ge_representation_real_code_cancel_total_associatetransportsecond) + (ge_representation_imaginary_code_cancel_total_associatetransportsecond)) + ((ge_representation_imaginary_code_cancel_total_associatetransportsecond) + (ge_representation_imaginary_code_cancel_total_associatetransportsecond))) /\ ((exists ge_balance_positive_cancel_total_associatetransportsecondreal ge_balance_negative_cancel_total_associatetransportsecondreal. (((((ge_representation_real_code_cancel_total_associatetransportsecond) = 2 * (ge_balance_positive_cancel_total_associatetransportsecondreal) /\ (ge_balance_negative_cancel_total_associatetransportsecondreal) = 0) \/ exists ge_signed_half_cancel_total_associatetransportsecondrealdecode. (((ge_representation_real_code_cancel_total_associatetransportsecond) = 2 * ge_signed_half_cancel_total_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportsecondreal) = 0) /\ (ge_balance_negative_cancel_total_associatetransportsecondreal) = S ge_signed_half_cancel_total_associatetransportsecondrealdecode))) /\ ((ge_second_rp_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportsecondreal = (ge_second_rn_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportsecondreal))) /\ (exists ge_balance_positive_cancel_total_associatetransportsecondimaginary ge_balance_negative_cancel_total_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_cancel_total_associatetransportsecond) = 2 * (ge_balance_positive_cancel_total_associatetransportsecondimaginary) /\ (ge_balance_negative_cancel_total_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_cancel_total_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associatetransportsecond) = 2 * ge_signed_half_cancel_total_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_cancel_total_associatetransportsecondimaginary) = S ge_signed_half_cancel_total_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_cancel_total_associatetransport) + ge_balance_negative_cancel_total_associatetransportsecondimaginary = (ge_second_in_cancel_total_associatetransport) + ge_balance_positive_cancel_total_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_total_associatetransportoutput ge_representation_imaginary_code_cancel_total_associatetransportoutput. (((Q) = ((ge_representation_real_code_cancel_total_associatetransportoutput) + (ge_representation_imaginary_code_cancel_total_associatetransportoutput)) * S ((ge_representation_real_code_cancel_total_associatetransportoutput) + (ge_representation_imaginary_code_cancel_total_associatetransportoutput)) + ((ge_representation_imaginary_code_cancel_total_associatetransportoutput) + (ge_representation_imaginary_code_cancel_total_associatetransportoutput))) /\ ((exists ge_balance_positive_cancel_total_associatetransportoutputreal ge_balance_negative_cancel_total_associatetransportoutputreal. (((((ge_representation_real_code_cancel_total_associatetransportoutput) = 2 * (ge_balance_positive_cancel_total_associatetransportoutputreal) /\ (ge_balance_negative_cancel_total_associatetransportoutputreal) = 0) \/ exists ge_signed_half_cancel_total_associatetransportoutputrealdecode. (((ge_representation_real_code_cancel_total_associatetransportoutput) = 2 * ge_signed_half_cancel_total_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportoutputreal) = 0) /\ (ge_balance_negative_cancel_total_associatetransportoutputreal) = S ge_signed_half_cancel_total_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))))))) + ge_balance_negative_cancel_total_associatetransportoutputreal = (((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))))))) + ge_balance_positive_cancel_total_associatetransportoutputreal))) /\ (exists ge_balance_positive_cancel_total_associatetransportoutputimaginary ge_balance_negative_cancel_total_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_cancel_total_associatetransportoutput) = 2 * (ge_balance_positive_cancel_total_associatetransportoutputimaginary) /\ (ge_balance_negative_cancel_total_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_cancel_total_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_total_associatetransportoutput) = 2 * ge_signed_half_cancel_total_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_total_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_cancel_total_associatetransportoutputimaginary) = S ge_signed_half_cancel_total_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))))))) + ge_balance_negative_cancel_total_associatetransportoutputimaginary = (((((((ge_first_rp_cancel_total_associatetransport) * (ge_second_in_cancel_total_associatetransport))) + (((ge_first_rn_cancel_total_associatetransport) * (ge_second_ip_cancel_total_associatetransport))))) + (((((ge_first_ip_cancel_total_associatetransport) * (ge_second_rn_cancel_total_associatetransport))) + (((ge_first_in_cancel_total_associatetransport) * (ge_second_rp_cancel_total_associatetransport))))))) + ge_balance_positive_cancel_total_associatetransportoutputimaginary))))))))))) -> (exists gr_unit_cancel_factor_associate. ((exists gr_inverse_cancel_factor_associateunit. (exists ge_first_rp_cancel_factor_associateunitidentity ge_first_rn_cancel_factor_associateunitidentity ge_first_ip_cancel_factor_associateunitidentity ge_first_in_cancel_factor_associateunitidentity ge_second_rp_cancel_factor_associateunitidentity ge_second_rn_cancel_factor_associateunitidentity ge_second_ip_cancel_factor_associateunitidentity ge_second_in_cancel_factor_associateunitidentity. ((exists ge_representation_real_code_cancel_factor_associateunitidentityfirst ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst. (((gr_unit_cancel_factor_associate) = ((ge_representation_real_code_cancel_factor_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst)) * S ((ge_representation_real_code_cancel_factor_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst)) + ((ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst))) /\ ((exists ge_balance_positive_cancel_factor_associateunitidentityfirstreal ge_balance_negative_cancel_factor_associateunitidentityfirstreal. (((((ge_representation_real_code_cancel_factor_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityfirstreal) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityfirstrealdecode. (((ge_representation_real_code_cancel_factor_associateunitidentityfirst) = 2 * ge_signed_half_cancel_factor_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstreal) = S ge_signed_half_cancel_factor_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentityfirstreal = (ge_first_rn_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associateunitidentityfirst) = 2 * ge_signed_half_cancel_factor_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary) = S ge_signed_half_cancel_factor_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentityfirstimaginary = (ge_first_in_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_factor_associateunitidentitysecond ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond. (((gr_inverse_cancel_factor_associateunit) = ((ge_representation_real_code_cancel_factor_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond)) * S ((ge_representation_real_code_cancel_factor_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond)) + ((ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond))) /\ ((exists ge_balance_positive_cancel_factor_associateunitidentitysecondreal ge_balance_negative_cancel_factor_associateunitidentitysecondreal. (((((ge_representation_real_code_cancel_factor_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_factor_associateunitidentitysecondreal) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentitysecondrealdecode. (((ge_representation_real_code_cancel_factor_associateunitidentitysecond) = 2 * ge_signed_half_cancel_factor_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondreal) = S ge_signed_half_cancel_factor_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentitysecondreal = (ge_second_rn_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associateunitidentitysecond) = 2 * ge_signed_half_cancel_factor_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary) = S ge_signed_half_cancel_factor_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cancel_factor_associateunitidentity) + ge_balance_negative_cancel_factor_associateunitidentitysecondimaginary = (ge_second_in_cancel_factor_associateunitidentity) + ge_balance_positive_cancel_factor_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_factor_associateunitidentityoutput ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput. (((6) = ((ge_representation_real_code_cancel_factor_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput)) * S ((ge_representation_real_code_cancel_factor_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput)) + ((ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput))) /\ ((exists ge_balance_positive_cancel_factor_associateunitidentityoutputreal ge_balance_negative_cancel_factor_associateunitidentityoutputreal. (((((ge_representation_real_code_cancel_factor_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityoutputreal) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityoutputrealdecode. (((ge_representation_real_code_cancel_factor_associateunitidentityoutput) = 2 * ge_signed_half_cancel_factor_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputreal) = S ge_signed_half_cancel_factor_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))))))) + ge_balance_negative_cancel_factor_associateunitidentityoutputreal = (((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))))))) + ge_balance_positive_cancel_factor_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associateunitidentityoutput) = 2 * ge_signed_half_cancel_factor_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary) = S ge_signed_half_cancel_factor_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))))))) + ge_balance_negative_cancel_factor_associateunitidentityoutputimaginary = (((((((ge_first_rp_cancel_factor_associateunitidentity) * (ge_second_in_cancel_factor_associateunitidentity))) + (((ge_first_rn_cancel_factor_associateunitidentity) * (ge_second_ip_cancel_factor_associateunitidentity))))) + (((((ge_first_ip_cancel_factor_associateunitidentity) * (ge_second_rn_cancel_factor_associateunitidentity))) + (((ge_first_in_cancel_factor_associateunitidentity) * (ge_second_rp_cancel_factor_associateunitidentity))))))) + ge_balance_positive_cancel_factor_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_cancel_factor_associatetransport ge_first_rn_cancel_factor_associatetransport ge_first_ip_cancel_factor_associatetransport ge_first_in_cancel_factor_associatetransport ge_second_rp_cancel_factor_associatetransport ge_second_rn_cancel_factor_associatetransport ge_second_ip_cancel_factor_associatetransport ge_second_in_cancel_factor_associatetransport. ((exists ge_representation_real_code_cancel_factor_associatetransportfirst ge_representation_imaginary_code_cancel_factor_associatetransportfirst. (((gr_unit_cancel_factor_associate) = ((ge_representation_real_code_cancel_factor_associatetransportfirst) + (ge_representation_imaginary_code_cancel_factor_associatetransportfirst)) * S ((ge_representation_real_code_cancel_factor_associatetransportfirst) + (ge_representation_imaginary_code_cancel_factor_associatetransportfirst)) + ((ge_representation_imaginary_code_cancel_factor_associatetransportfirst) + (ge_representation_imaginary_code_cancel_factor_associatetransportfirst))) /\ ((exists ge_balance_positive_cancel_factor_associatetransportfirstreal ge_balance_negative_cancel_factor_associatetransportfirstreal. (((((ge_representation_real_code_cancel_factor_associatetransportfirst) = 2 * (ge_balance_positive_cancel_factor_associatetransportfirstreal) /\ (ge_balance_negative_cancel_factor_associatetransportfirstreal) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportfirstrealdecode. (((ge_representation_real_code_cancel_factor_associatetransportfirst) = 2 * ge_signed_half_cancel_factor_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportfirstreal) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportfirstreal) = S ge_signed_half_cancel_factor_associatetransportfirstrealdecode))) /\ ((ge_first_rp_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportfirstreal = (ge_first_rn_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportfirstreal))) /\ (exists ge_balance_positive_cancel_factor_associatetransportfirstimaginary ge_balance_negative_cancel_factor_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_cancel_factor_associatetransportfirst) = 2 * (ge_balance_positive_cancel_factor_associatetransportfirstimaginary) /\ (ge_balance_negative_cancel_factor_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associatetransportfirst) = 2 * ge_signed_half_cancel_factor_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportfirstimaginary) = S ge_signed_half_cancel_factor_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportfirstimaginary = (ge_first_in_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_factor_associatetransportsecond ge_representation_imaginary_code_cancel_factor_associatetransportsecond. (((p) = ((ge_representation_real_code_cancel_factor_associatetransportsecond) + (ge_representation_imaginary_code_cancel_factor_associatetransportsecond)) * S ((ge_representation_real_code_cancel_factor_associatetransportsecond) + (ge_representation_imaginary_code_cancel_factor_associatetransportsecond)) + ((ge_representation_imaginary_code_cancel_factor_associatetransportsecond) + (ge_representation_imaginary_code_cancel_factor_associatetransportsecond))) /\ ((exists ge_balance_positive_cancel_factor_associatetransportsecondreal ge_balance_negative_cancel_factor_associatetransportsecondreal. (((((ge_representation_real_code_cancel_factor_associatetransportsecond) = 2 * (ge_balance_positive_cancel_factor_associatetransportsecondreal) /\ (ge_balance_negative_cancel_factor_associatetransportsecondreal) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportsecondrealdecode. (((ge_representation_real_code_cancel_factor_associatetransportsecond) = 2 * ge_signed_half_cancel_factor_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportsecondreal) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportsecondreal) = S ge_signed_half_cancel_factor_associatetransportsecondrealdecode))) /\ ((ge_second_rp_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportsecondreal = (ge_second_rn_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportsecondreal))) /\ (exists ge_balance_positive_cancel_factor_associatetransportsecondimaginary ge_balance_negative_cancel_factor_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_cancel_factor_associatetransportsecond) = 2 * (ge_balance_positive_cancel_factor_associatetransportsecondimaginary) /\ (ge_balance_negative_cancel_factor_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associatetransportsecond) = 2 * ge_signed_half_cancel_factor_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportsecondimaginary) = S ge_signed_half_cancel_factor_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_cancel_factor_associatetransport) + ge_balance_negative_cancel_factor_associatetransportsecondimaginary = (ge_second_in_cancel_factor_associatetransport) + ge_balance_positive_cancel_factor_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_factor_associatetransportoutput ge_representation_imaginary_code_cancel_factor_associatetransportoutput. (((q) = ((ge_representation_real_code_cancel_factor_associatetransportoutput) + (ge_representation_imaginary_code_cancel_factor_associatetransportoutput)) * S ((ge_representation_real_code_cancel_factor_associatetransportoutput) + (ge_representation_imaginary_code_cancel_factor_associatetransportoutput)) + ((ge_representation_imaginary_code_cancel_factor_associatetransportoutput) + (ge_representation_imaginary_code_cancel_factor_associatetransportoutput))) /\ ((exists ge_balance_positive_cancel_factor_associatetransportoutputreal ge_balance_negative_cancel_factor_associatetransportoutputreal. (((((ge_representation_real_code_cancel_factor_associatetransportoutput) = 2 * (ge_balance_positive_cancel_factor_associatetransportoutputreal) /\ (ge_balance_negative_cancel_factor_associatetransportoutputreal) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportoutputrealdecode. (((ge_representation_real_code_cancel_factor_associatetransportoutput) = 2 * ge_signed_half_cancel_factor_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportoutputreal) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportoutputreal) = S ge_signed_half_cancel_factor_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))))))) + ge_balance_negative_cancel_factor_associatetransportoutputreal = (((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))))))) + ge_balance_positive_cancel_factor_associatetransportoutputreal))) /\ (exists ge_balance_positive_cancel_factor_associatetransportoutputimaginary ge_balance_negative_cancel_factor_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_cancel_factor_associatetransportoutput) = 2 * (ge_balance_positive_cancel_factor_associatetransportoutputimaginary) /\ (ge_balance_negative_cancel_factor_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_cancel_factor_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_factor_associatetransportoutput) = 2 * ge_signed_half_cancel_factor_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_factor_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_cancel_factor_associatetransportoutputimaginary) = S ge_signed_half_cancel_factor_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))))))) + ge_balance_negative_cancel_factor_associatetransportoutputimaginary = (((((((ge_first_rp_cancel_factor_associatetransport) * (ge_second_in_cancel_factor_associatetransport))) + (((ge_first_rn_cancel_factor_associatetransport) * (ge_second_ip_cancel_factor_associatetransport))))) + (((((ge_first_ip_cancel_factor_associatetransport) * (ge_second_rn_cancel_factor_associatetransport))) + (((ge_first_in_cancel_factor_associatetransport) * (ge_second_rp_cancel_factor_associatetransport))))))) + ge_balance_positive_cancel_factor_associatetransportoutputimaginary))))))))))) -> ~(p=0) -> (exists gr_unit_cancel_prefix_associate. ((exists gr_inverse_cancel_prefix_associateunit. (exists ge_first_rp_cancel_prefix_associateunitidentity ge_first_rn_cancel_prefix_associateunitidentity ge_first_ip_cancel_prefix_associateunitidentity ge_first_in_cancel_prefix_associateunitidentity ge_second_rp_cancel_prefix_associateunitidentity ge_second_rn_cancel_prefix_associateunitidentity ge_second_ip_cancel_prefix_associateunitidentity ge_second_in_cancel_prefix_associateunitidentity. ((exists ge_representation_real_code_cancel_prefix_associateunitidentityfirst ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst. (((gr_unit_cancel_prefix_associate) = ((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst)) * S ((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst)) + ((ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst))) /\ ((exists ge_balance_positive_cancel_prefix_associateunitidentityfirstreal ge_balance_negative_cancel_prefix_associateunitidentityfirstreal. (((((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityfirstreal) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityfirstrealdecode. (((ge_representation_real_code_cancel_prefix_associateunitidentityfirst) = 2 * ge_signed_half_cancel_prefix_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstreal) = S ge_signed_half_cancel_prefix_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentityfirstreal = (ge_first_rn_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associateunitidentityfirst) = 2 * ge_signed_half_cancel_prefix_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary) = S ge_signed_half_cancel_prefix_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentityfirstimaginary = (ge_first_in_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_prefix_associateunitidentitysecond ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond. (((gr_inverse_cancel_prefix_associateunit) = ((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond)) * S ((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond)) + ((ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond))) /\ ((exists ge_balance_positive_cancel_prefix_associateunitidentitysecondreal ge_balance_negative_cancel_prefix_associateunitidentitysecondreal. (((((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentitysecondreal) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentitysecondrealdecode. (((ge_representation_real_code_cancel_prefix_associateunitidentitysecond) = 2 * ge_signed_half_cancel_prefix_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondreal) = S ge_signed_half_cancel_prefix_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentitysecondreal = (ge_second_rn_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associateunitidentitysecond) = 2 * ge_signed_half_cancel_prefix_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary) = S ge_signed_half_cancel_prefix_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_cancel_prefix_associateunitidentity) + ge_balance_negative_cancel_prefix_associateunitidentitysecondimaginary = (ge_second_in_cancel_prefix_associateunitidentity) + ge_balance_positive_cancel_prefix_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_prefix_associateunitidentityoutput ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput. (((6) = ((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput)) * S ((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput)) + ((ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput) + (ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput))) /\ ((exists ge_balance_positive_cancel_prefix_associateunitidentityoutputreal ge_balance_negative_cancel_prefix_associateunitidentityoutputreal. (((((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityoutputreal) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityoutputrealdecode. (((ge_representation_real_code_cancel_prefix_associateunitidentityoutput) = 2 * ge_signed_half_cancel_prefix_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputreal) = S ge_signed_half_cancel_prefix_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))))))) + ge_balance_negative_cancel_prefix_associateunitidentityoutputreal = (((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))))))) + ge_balance_positive_cancel_prefix_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput) = 2 * (ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associateunitidentityoutput) = 2 * ge_signed_half_cancel_prefix_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary) = S ge_signed_half_cancel_prefix_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))))))) + ge_balance_negative_cancel_prefix_associateunitidentityoutputimaginary = (((((((ge_first_rp_cancel_prefix_associateunitidentity) * (ge_second_in_cancel_prefix_associateunitidentity))) + (((ge_first_rn_cancel_prefix_associateunitidentity) * (ge_second_ip_cancel_prefix_associateunitidentity))))) + (((((ge_first_ip_cancel_prefix_associateunitidentity) * (ge_second_rn_cancel_prefix_associateunitidentity))) + (((ge_first_in_cancel_prefix_associateunitidentity) * (ge_second_rp_cancel_prefix_associateunitidentity))))))) + ge_balance_positive_cancel_prefix_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_cancel_prefix_associatetransport ge_first_rn_cancel_prefix_associatetransport ge_first_ip_cancel_prefix_associatetransport ge_first_in_cancel_prefix_associatetransport ge_second_rp_cancel_prefix_associatetransport ge_second_rn_cancel_prefix_associatetransport ge_second_ip_cancel_prefix_associatetransport ge_second_in_cancel_prefix_associatetransport. ((exists ge_representation_real_code_cancel_prefix_associatetransportfirst ge_representation_imaginary_code_cancel_prefix_associatetransportfirst. (((gr_unit_cancel_prefix_associate) = ((ge_representation_real_code_cancel_prefix_associatetransportfirst) + (ge_representation_imaginary_code_cancel_prefix_associatetransportfirst)) * S ((ge_representation_real_code_cancel_prefix_associatetransportfirst) + (ge_representation_imaginary_code_cancel_prefix_associatetransportfirst)) + ((ge_representation_imaginary_code_cancel_prefix_associatetransportfirst) + (ge_representation_imaginary_code_cancel_prefix_associatetransportfirst))) /\ ((exists ge_balance_positive_cancel_prefix_associatetransportfirstreal ge_balance_negative_cancel_prefix_associatetransportfirstreal. (((((ge_representation_real_code_cancel_prefix_associatetransportfirst) = 2 * (ge_balance_positive_cancel_prefix_associatetransportfirstreal) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstreal) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportfirstrealdecode. (((ge_representation_real_code_cancel_prefix_associatetransportfirst) = 2 * ge_signed_half_cancel_prefix_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportfirstreal) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstreal) = S ge_signed_half_cancel_prefix_associatetransportfirstrealdecode))) /\ ((ge_first_rp_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportfirstreal = (ge_first_rn_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportfirstreal))) /\ (exists ge_balance_positive_cancel_prefix_associatetransportfirstimaginary ge_balance_negative_cancel_prefix_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associatetransportfirst) = 2 * (ge_balance_positive_cancel_prefix_associatetransportfirstimaginary) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associatetransportfirst) = 2 * ge_signed_half_cancel_prefix_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportfirstimaginary) = S ge_signed_half_cancel_prefix_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportfirstimaginary = (ge_first_in_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_prefix_associatetransportsecond ge_representation_imaginary_code_cancel_prefix_associatetransportsecond. (((R) = ((ge_representation_real_code_cancel_prefix_associatetransportsecond) + (ge_representation_imaginary_code_cancel_prefix_associatetransportsecond)) * S ((ge_representation_real_code_cancel_prefix_associatetransportsecond) + (ge_representation_imaginary_code_cancel_prefix_associatetransportsecond)) + ((ge_representation_imaginary_code_cancel_prefix_associatetransportsecond) + (ge_representation_imaginary_code_cancel_prefix_associatetransportsecond))) /\ ((exists ge_balance_positive_cancel_prefix_associatetransportsecondreal ge_balance_negative_cancel_prefix_associatetransportsecondreal. (((((ge_representation_real_code_cancel_prefix_associatetransportsecond) = 2 * (ge_balance_positive_cancel_prefix_associatetransportsecondreal) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondreal) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportsecondrealdecode. (((ge_representation_real_code_cancel_prefix_associatetransportsecond) = 2 * ge_signed_half_cancel_prefix_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportsecondreal) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondreal) = S ge_signed_half_cancel_prefix_associatetransportsecondrealdecode))) /\ ((ge_second_rp_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportsecondreal = (ge_second_rn_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportsecondreal))) /\ (exists ge_balance_positive_cancel_prefix_associatetransportsecondimaginary ge_balance_negative_cancel_prefix_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associatetransportsecond) = 2 * (ge_balance_positive_cancel_prefix_associatetransportsecondimaginary) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associatetransportsecond) = 2 * ge_signed_half_cancel_prefix_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportsecondimaginary) = S ge_signed_half_cancel_prefix_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_cancel_prefix_associatetransport) + ge_balance_negative_cancel_prefix_associatetransportsecondimaginary = (ge_second_in_cancel_prefix_associatetransport) + ge_balance_positive_cancel_prefix_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_prefix_associatetransportoutput ge_representation_imaginary_code_cancel_prefix_associatetransportoutput. (((T) = ((ge_representation_real_code_cancel_prefix_associatetransportoutput) + (ge_representation_imaginary_code_cancel_prefix_associatetransportoutput)) * S ((ge_representation_real_code_cancel_prefix_associatetransportoutput) + (ge_representation_imaginary_code_cancel_prefix_associatetransportoutput)) + ((ge_representation_imaginary_code_cancel_prefix_associatetransportoutput) + (ge_representation_imaginary_code_cancel_prefix_associatetransportoutput))) /\ ((exists ge_balance_positive_cancel_prefix_associatetransportoutputreal ge_balance_negative_cancel_prefix_associatetransportoutputreal. (((((ge_representation_real_code_cancel_prefix_associatetransportoutput) = 2 * (ge_balance_positive_cancel_prefix_associatetransportoutputreal) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputreal) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportoutputrealdecode. (((ge_representation_real_code_cancel_prefix_associatetransportoutput) = 2 * ge_signed_half_cancel_prefix_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportoutputreal) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputreal) = S ge_signed_half_cancel_prefix_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))))))) + ge_balance_negative_cancel_prefix_associatetransportoutputreal = (((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))))))) + ge_balance_positive_cancel_prefix_associatetransportoutputreal))) /\ (exists ge_balance_positive_cancel_prefix_associatetransportoutputimaginary ge_balance_negative_cancel_prefix_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_cancel_prefix_associatetransportoutput) = 2 * (ge_balance_positive_cancel_prefix_associatetransportoutputimaginary) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_cancel_prefix_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_prefix_associatetransportoutput) = 2 * ge_signed_half_cancel_prefix_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_prefix_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_cancel_prefix_associatetransportoutputimaginary) = S ge_signed_half_cancel_prefix_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))))))) + ge_balance_negative_cancel_prefix_associatetransportoutputimaginary = (((((((ge_first_rp_cancel_prefix_associatetransport) * (ge_second_in_cancel_prefix_associatetransport))) + (((ge_first_rn_cancel_prefix_associatetransport) * (ge_second_ip_cancel_prefix_associatetransport))))) + (((((ge_first_ip_cancel_prefix_associatetransport) * (ge_second_rn_cancel_prefix_associatetransport))) + (((ge_first_in_cancel_prefix_associatetransport) * (ge_second_rp_cancel_prefix_associatetransport))))))) + ge_balance_positive_cancel_prefix_associatetransportoutputimaginary)))))))))))

Complete tactic proof in conservative notation

All 94 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

94 script commands · 21 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (8)

gaussian unit valid gaussian multiply input left valid gaussian multiply cancel right gaussian multiply associative reverse gaussian multiply commutative gaussian associate transitive gaussian factor associate code transport gaussian associate symmetric

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

L1
intro R
L2
intro p
L3
intro P
L4
intro T
L5
intro q
L6
intro Q
L7
intro hRP
L8
intro hTQ
L9
intro hPQ
L10
intro hpq

02Fix variables and assumptionsL11–11

Work with arbitrary variables or the premises of the current implication.

L11
intro hp

03Separate the logical casesL12–15

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L12
cases hPQ
L13
cases hPQ_witness
L14
cases hpq
L15
cases hpq_witness

04Establish hCL16–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply exists.

L16
have hC : ∃ C. GMul(x,R,C)Definitions: GMul(x,R,C)Original native command in the exact edition
L17
specialize gaussian_multiply_exists (x)
L18
specialize gaussian_multiply_exists (R)
L19
apply gaussian_multiply_exists
L20
specialize gaussian_unit_valid (x)
L21
apply gaussian_unit_valid
L22
exact hPQ_witness_left
L23
specialize gaussian_multiply_input_left_valid (R)
L24
specialize gaussian_multiply_input_left_valid (p)
L25
specialize gaussian_multiply_input_left_valid (P)

05Use earlier factsL26–27

Instantiate or apply named facts and discharge the corresponding proof obligations.

L26
apply gaussian_multiply_input_left_valid
L27
exact hRP

06Separate the logical casesL28–28

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L28
cases hC

07Establish hDL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply exists.

L29
have hD : ∃ D. GMul(x1,T,D)Definitions: GMul(x1,T,D)Original native command in the exact edition
L30
specialize gaussian_multiply_exists (x1)
L31
specialize gaussian_multiply_exists (T)
L32
apply gaussian_multiply_exists
L33
specialize gaussian_unit_valid (x1)
L34
apply gaussian_unit_valid
L35
exact hpq_witness_left
L36
specialize gaussian_multiply_input_left_valid (T)
L37
specialize gaussian_multiply_input_left_valid (q)
L38
specialize gaussian_multiply_input_left_valid (Q)

08Use earlier factsL39–40

Instantiate or apply named facts and discharge the corresponding proof obligations.

L39
apply gaussian_multiply_input_left_valid
L40
exact hTQ

09Separate the logical casesL41–41

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L41
cases hD

10Establish heqL42–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply cancel right.

L42
have heq : x2=x3
L43
specialize gaussian_multiply_cancel_right (x2)
L44
specialize gaussian_multiply_cancel_right (x3)
L45
specialize gaussian_multiply_cancel_right (p)
L46
specialize gaussian_multiply_cancel_right (Q)
L47
apply gaussian_multiply_cancel_right
L48
exact hp
L49
specialize gaussian_multiply_associative_reverse (x)
L50
specialize gaussian_multiply_associative_reverse (R)
L51
specialize gaussian_multiply_associative_reverse (p)

11Use earlier factsL52–61

Instantiate or apply named facts and discharge the corresponding proof obligations.

L52
specialize gaussian_multiply_associative_reverse (x2)
L53
specialize gaussian_multiply_associative_reverse (P)
L54
specialize gaussian_multiply_associative_reverse (Q)
L55
apply gaussian_multiply_associative_reverse
L56
exact hC_witness
L57
exact hRP
L58
exact hPQ_witness_right
L59
specialize gaussian_multiply_associative_reverse (T)
L60
specialize gaussian_multiply_associative_reverse (x1)
L61
specialize gaussian_multiply_associative_reverse (p)

12Use earlier factsL62–71

Instantiate or apply named facts and discharge the corresponding proof obligations.

L62
specialize gaussian_multiply_associative_reverse (x3)
L63
specialize gaussian_multiply_associative_reverse (q)
L64
specialize gaussian_multiply_associative_reverse (Q)
L65
apply gaussian_multiply_associative_reverse
L66
specialize gaussian_multiply_commutative (x1)
L67
specialize gaussian_multiply_commutative (T)
L68
specialize gaussian_multiply_commutative (x3)
L69
apply gaussian_multiply_commutative
L70
exact hD_witness
L71
exact hpq_witness_right

13Use earlier factsL72–81

Instantiate or apply named facts and discharge the corresponding proof obligations.

L72
exact hTQ
L73
specialize gaussian_associate_transitive (R)
L74
specialize gaussian_associate_transitive (x3)
L75
specialize gaussian_associate_transitive (T)
L76
apply gaussian_associate_transitive
L77
specialize gaussian_factor_associate_code_transport (R)
L78
specialize gaussian_factor_associate_code_transport (x2)
L79
specialize gaussian_factor_associate_code_transport (R)
L80
specialize gaussian_factor_associate_code_transport (x3)
L81
apply gaussian_factor_associate_code_transport

14Calculate and transport equalitiesL82–82

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

L82
refl

15Use earlier factsL83–83

Instantiate or apply named facts and discharge the corresponding proof obligations.

L83
exact heq

16Construct an explicit witnessL84–84

Supply the displayed value, then prove that it has the required property.

L84
exists (x)

17Separate the logical casesL85–85

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L85
split

18Use earlier factsL86–90

Instantiate or apply named facts and discharge the corresponding proof obligations.

L86
exact hPQ_witness_left
L87
exact hC_witness
L88
specialize gaussian_associate_symmetric (T)
L89
specialize gaussian_associate_symmetric (x3)
L90
apply gaussian_associate_symmetric

19Construct an explicit witnessL91–91

Supply the displayed value, then prove that it has the required property.

L91
exists (x1)

20Separate the logical casesL92–92

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L92
split

21Use earlier factsL93–94

Instantiate or apply named facts and discharge the corresponding proof obligations.

L93
exact hpq_witness_left
L94
exact hD_witness

Library-wide reading audit

Original defined command ledger · 94 lines

0001intro R
0002intro p
0003intro P
0004intro T
0005intro q
0006intro Q
0007intro hRP
0008intro hTQ
0009intro hPQ
0010intro hpq
0011intro hp
0012cases hPQ
0013cases hPQ_witness
0014cases hpq
0015cases hpq_witness
0016have hC : ∃ C. GMul(x,R,C)
0017specialize gaussian_multiply_exists (x)
0018specialize gaussian_multiply_exists (R)
0019apply gaussian_multiply_exists
0020specialize gaussian_unit_valid (x)
0021apply gaussian_unit_valid
0022exact hPQ_witness_left
0023specialize gaussian_multiply_input_left_valid (R)
0024specialize gaussian_multiply_input_left_valid (p)
0025specialize gaussian_multiply_input_left_valid (P)
0026apply gaussian_multiply_input_left_valid
0027exact hRP
0028cases hC
0029have hD : ∃ D. GMul(x1,T,D)
0030specialize gaussian_multiply_exists (x1)
0031specialize gaussian_multiply_exists (T)
0032apply gaussian_multiply_exists
0033specialize gaussian_unit_valid (x1)
0034apply gaussian_unit_valid
0035exact hpq_witness_left
0036specialize gaussian_multiply_input_left_valid (T)
0037specialize gaussian_multiply_input_left_valid (q)
0038specialize gaussian_multiply_input_left_valid (Q)
0039apply gaussian_multiply_input_left_valid
0040exact hTQ
0041cases hD
0042have heq : x2=x3
0043specialize gaussian_multiply_cancel_right (x2)
0044specialize gaussian_multiply_cancel_right (x3)
0045specialize gaussian_multiply_cancel_right (p)
0046specialize gaussian_multiply_cancel_right (Q)
0047apply gaussian_multiply_cancel_right
0048exact hp
0049specialize gaussian_multiply_associative_reverse (x)
0050specialize gaussian_multiply_associative_reverse (R)
0051specialize gaussian_multiply_associative_reverse (p)
0052specialize gaussian_multiply_associative_reverse (x2)
0053specialize gaussian_multiply_associative_reverse (P)
0054specialize gaussian_multiply_associative_reverse (Q)
0055apply gaussian_multiply_associative_reverse
0056exact hC_witness
0057exact hRP
0058exact hPQ_witness_right
0059specialize gaussian_multiply_associative_reverse (T)
0060specialize gaussian_multiply_associative_reverse (x1)
0061specialize gaussian_multiply_associative_reverse (p)
0062specialize gaussian_multiply_associative_reverse (x3)
0063specialize gaussian_multiply_associative_reverse (q)
0064specialize gaussian_multiply_associative_reverse (Q)
0065apply gaussian_multiply_associative_reverse
0066specialize gaussian_multiply_commutative (x1)
0067specialize gaussian_multiply_commutative (T)
0068specialize gaussian_multiply_commutative (x3)
0069apply gaussian_multiply_commutative
0070exact hD_witness
0071exact hpq_witness_right
0072exact hTQ
0073specialize gaussian_associate_transitive (R)
0074specialize gaussian_associate_transitive (x3)
0075specialize gaussian_associate_transitive (T)
0076apply gaussian_associate_transitive
0077specialize gaussian_factor_associate_code_transport (R)
0078specialize gaussian_factor_associate_code_transport (x2)
0079specialize gaussian_factor_associate_code_transport (R)
0080specialize gaussian_factor_associate_code_transport (x3)
0081apply gaussian_factor_associate_code_transport
0082refl
0083exact heq
0084exists (x)
0085split
0086exact hPQ_witness_left
0087exact hC_witness
0088specialize gaussian_associate_symmetric (T)
0089specialize gaussian_associate_symmetric (x3)
0090apply gaussian_associate_symmetric
0091exists (x1)
0092split
0093exact hpq_witness_left
0094exact hD_witness