GF0055

gaussian_associate_symmetric

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Invert the actual unit witness to reverse Gaussian association, including the zero boundary.

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.

Exact expanded first-order arithmetic statement

forall a b. (exists gr_unit_associate_forward. ((exists gr_inverse_associate_forwardunit. (exists ge_first_rp_associate_forwardunitidentity ge_first_rn_associate_forwardunitidentity ge_first_ip_associate_forwardunitidentity ge_first_in_associate_forwardunitidentity ge_second_rp_associate_forwardunitidentity ge_second_rn_associate_forwardunitidentity ge_second_ip_associate_forwardunitidentity ge_second_in_associate_forwardunitidentity. ((exists ge_representation_real_code_associate_forwardunitidentityfirst ge_representation_imaginary_code_associate_forwardunitidentityfirst. (((gr_unit_associate_forward) = ((ge_representation_real_code_associate_forwardunitidentityfirst) + (ge_representation_imaginary_code_associate_forwardunitidentityfirst)) * S ((ge_representation_real_code_associate_forwardunitidentityfirst) + (ge_representation_imaginary_code_associate_forwardunitidentityfirst)) + ((ge_representation_imaginary_code_associate_forwardunitidentityfirst) + (ge_representation_imaginary_code_associate_forwardunitidentityfirst))) /\ ((exists ge_balance_positive_associate_forwardunitidentityfirstreal ge_balance_negative_associate_forwardunitidentityfirstreal. (((((ge_representation_real_code_associate_forwardunitidentityfirst) = 2 * (ge_balance_positive_associate_forwardunitidentityfirstreal) /\ (ge_balance_negative_associate_forwardunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_forwardunitidentityfirstrealdecode. (((ge_representation_real_code_associate_forwardunitidentityfirst) = 2 * ge_signed_half_associate_forwardunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_forwardunitidentityfirstreal) = S ge_signed_half_associate_forwardunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentityfirstreal = (ge_first_rn_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_forwardunitidentityfirstimaginary ge_balance_negative_associate_forwardunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_forwardunitidentityfirst) = 2 * (ge_balance_positive_associate_forwardunitidentityfirstimaginary) /\ (ge_balance_negative_associate_forwardunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_forwardunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_forwardunitidentityfirst) = 2 * ge_signed_half_associate_forwardunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_forwardunitidentityfirstimaginary) = S ge_signed_half_associate_forwardunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentityfirstimaginary = (ge_first_in_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_forwardunitidentitysecond ge_representation_imaginary_code_associate_forwardunitidentitysecond. (((gr_inverse_associate_forwardunit) = ((ge_representation_real_code_associate_forwardunitidentitysecond) + (ge_representation_imaginary_code_associate_forwardunitidentitysecond)) * S ((ge_representation_real_code_associate_forwardunitidentitysecond) + (ge_representation_imaginary_code_associate_forwardunitidentitysecond)) + ((ge_representation_imaginary_code_associate_forwardunitidentitysecond) + (ge_representation_imaginary_code_associate_forwardunitidentitysecond))) /\ ((exists ge_balance_positive_associate_forwardunitidentitysecondreal ge_balance_negative_associate_forwardunitidentitysecondreal. (((((ge_representation_real_code_associate_forwardunitidentitysecond) = 2 * (ge_balance_positive_associate_forwardunitidentitysecondreal) /\ (ge_balance_negative_associate_forwardunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_forwardunitidentitysecondrealdecode. (((ge_representation_real_code_associate_forwardunitidentitysecond) = 2 * ge_signed_half_associate_forwardunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_forwardunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_forwardunitidentitysecondreal) = S ge_signed_half_associate_forwardunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentitysecondreal = (ge_second_rn_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_forwardunitidentitysecondimaginary ge_balance_negative_associate_forwardunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_forwardunitidentitysecond) = 2 * (ge_balance_positive_associate_forwardunitidentitysecondimaginary) /\ (ge_balance_negative_associate_forwardunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_forwardunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_forwardunitidentitysecond) = 2 * ge_signed_half_associate_forwardunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_forwardunitidentitysecondimaginary) = S ge_signed_half_associate_forwardunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentitysecondimaginary = (ge_second_in_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_forwardunitidentityoutput ge_representation_imaginary_code_associate_forwardunitidentityoutput. (((6) = ((ge_representation_real_code_associate_forwardunitidentityoutput) + (ge_representation_imaginary_code_associate_forwardunitidentityoutput)) * S ((ge_representation_real_code_associate_forwardunitidentityoutput) + (ge_representation_imaginary_code_associate_forwardunitidentityoutput)) + ((ge_representation_imaginary_code_associate_forwardunitidentityoutput) + (ge_representation_imaginary_code_associate_forwardunitidentityoutput))) /\ ((exists ge_balance_positive_associate_forwardunitidentityoutputreal ge_balance_negative_associate_forwardunitidentityoutputreal. (((((ge_representation_real_code_associate_forwardunitidentityoutput) = 2 * (ge_balance_positive_associate_forwardunitidentityoutputreal) /\ (ge_balance_negative_associate_forwardunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_forwardunitidentityoutputrealdecode. (((ge_representation_real_code_associate_forwardunitidentityoutput) = 2 * ge_signed_half_associate_forwardunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_forwardunitidentityoutputreal) = S ge_signed_half_associate_forwardunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))))))) + ge_balance_negative_associate_forwardunitidentityoutputreal = (((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))))))) + ge_balance_positive_associate_forwardunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_forwardunitidentityoutputimaginary ge_balance_negative_associate_forwardunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_forwardunitidentityoutput) = 2 * (ge_balance_positive_associate_forwardunitidentityoutputimaginary) /\ (ge_balance_negative_associate_forwardunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_forwardunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_forwardunitidentityoutput) = 2 * ge_signed_half_associate_forwardunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_forwardunitidentityoutputimaginary) = S ge_signed_half_associate_forwardunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))))))) + ge_balance_negative_associate_forwardunitidentityoutputimaginary = (((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))))))) + ge_balance_positive_associate_forwardunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_forwardtransport ge_first_rn_associate_forwardtransport ge_first_ip_associate_forwardtransport ge_first_in_associate_forwardtransport ge_second_rp_associate_forwardtransport ge_second_rn_associate_forwardtransport ge_second_ip_associate_forwardtransport ge_second_in_associate_forwardtransport. ((exists ge_representation_real_code_associate_forwardtransportfirst ge_representation_imaginary_code_associate_forwardtransportfirst. (((gr_unit_associate_forward) = ((ge_representation_real_code_associate_forwardtransportfirst) + (ge_representation_imaginary_code_associate_forwardtransportfirst)) * S ((ge_representation_real_code_associate_forwardtransportfirst) + (ge_representation_imaginary_code_associate_forwardtransportfirst)) + ((ge_representation_imaginary_code_associate_forwardtransportfirst) + (ge_representation_imaginary_code_associate_forwardtransportfirst))) /\ ((exists ge_balance_positive_associate_forwardtransportfirstreal ge_balance_negative_associate_forwardtransportfirstreal. (((((ge_representation_real_code_associate_forwardtransportfirst) = 2 * (ge_balance_positive_associate_forwardtransportfirstreal) /\ (ge_balance_negative_associate_forwardtransportfirstreal) = 0) \/ exists ge_signed_half_associate_forwardtransportfirstrealdecode. (((ge_representation_real_code_associate_forwardtransportfirst) = 2 * ge_signed_half_associate_forwardtransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_forwardtransportfirstreal) = 0) /\ (ge_balance_negative_associate_forwardtransportfirstreal) = S ge_signed_half_associate_forwardtransportfirstrealdecode))) /\ ((ge_first_rp_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportfirstreal = (ge_first_rn_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportfirstreal))) /\ (exists ge_balance_positive_associate_forwardtransportfirstimaginary ge_balance_negative_associate_forwardtransportfirstimaginary. (((((ge_representation_imaginary_code_associate_forwardtransportfirst) = 2 * (ge_balance_positive_associate_forwardtransportfirstimaginary) /\ (ge_balance_negative_associate_forwardtransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_forwardtransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_forwardtransportfirst) = 2 * ge_signed_half_associate_forwardtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardtransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_forwardtransportfirstimaginary) = S ge_signed_half_associate_forwardtransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportfirstimaginary = (ge_first_in_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_forwardtransportsecond ge_representation_imaginary_code_associate_forwardtransportsecond. (((a) = ((ge_representation_real_code_associate_forwardtransportsecond) + (ge_representation_imaginary_code_associate_forwardtransportsecond)) * S ((ge_representation_real_code_associate_forwardtransportsecond) + (ge_representation_imaginary_code_associate_forwardtransportsecond)) + ((ge_representation_imaginary_code_associate_forwardtransportsecond) + (ge_representation_imaginary_code_associate_forwardtransportsecond))) /\ ((exists ge_balance_positive_associate_forwardtransportsecondreal ge_balance_negative_associate_forwardtransportsecondreal. (((((ge_representation_real_code_associate_forwardtransportsecond) = 2 * (ge_balance_positive_associate_forwardtransportsecondreal) /\ (ge_balance_negative_associate_forwardtransportsecondreal) = 0) \/ exists ge_signed_half_associate_forwardtransportsecondrealdecode. (((ge_representation_real_code_associate_forwardtransportsecond) = 2 * ge_signed_half_associate_forwardtransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_forwardtransportsecondreal) = 0) /\ (ge_balance_negative_associate_forwardtransportsecondreal) = S ge_signed_half_associate_forwardtransportsecondrealdecode))) /\ ((ge_second_rp_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportsecondreal = (ge_second_rn_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportsecondreal))) /\ (exists ge_balance_positive_associate_forwardtransportsecondimaginary ge_balance_negative_associate_forwardtransportsecondimaginary. (((((ge_representation_imaginary_code_associate_forwardtransportsecond) = 2 * (ge_balance_positive_associate_forwardtransportsecondimaginary) /\ (ge_balance_negative_associate_forwardtransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_forwardtransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_forwardtransportsecond) = 2 * ge_signed_half_associate_forwardtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardtransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_forwardtransportsecondimaginary) = S ge_signed_half_associate_forwardtransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportsecondimaginary = (ge_second_in_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_forwardtransportoutput ge_representation_imaginary_code_associate_forwardtransportoutput. (((b) = ((ge_representation_real_code_associate_forwardtransportoutput) + (ge_representation_imaginary_code_associate_forwardtransportoutput)) * S ((ge_representation_real_code_associate_forwardtransportoutput) + (ge_representation_imaginary_code_associate_forwardtransportoutput)) + ((ge_representation_imaginary_code_associate_forwardtransportoutput) + (ge_representation_imaginary_code_associate_forwardtransportoutput))) /\ ((exists ge_balance_positive_associate_forwardtransportoutputreal ge_balance_negative_associate_forwardtransportoutputreal. (((((ge_representation_real_code_associate_forwardtransportoutput) = 2 * (ge_balance_positive_associate_forwardtransportoutputreal) /\ (ge_balance_negative_associate_forwardtransportoutputreal) = 0) \/ exists ge_signed_half_associate_forwardtransportoutputrealdecode. (((ge_representation_real_code_associate_forwardtransportoutput) = 2 * ge_signed_half_associate_forwardtransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_forwardtransportoutputreal) = 0) /\ (ge_balance_negative_associate_forwardtransportoutputreal) = S ge_signed_half_associate_forwardtransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))))))) + ge_balance_negative_associate_forwardtransportoutputreal = (((((((ge_first_rp_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))))))) + ge_balance_positive_associate_forwardtransportoutputreal))) /\ (exists ge_balance_positive_associate_forwardtransportoutputimaginary ge_balance_negative_associate_forwardtransportoutputimaginary. (((((ge_representation_imaginary_code_associate_forwardtransportoutput) = 2 * (ge_balance_positive_associate_forwardtransportoutputimaginary) /\ (ge_balance_negative_associate_forwardtransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_forwardtransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_forwardtransportoutput) = 2 * ge_signed_half_associate_forwardtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardtransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_forwardtransportoutputimaginary) = S ge_signed_half_associate_forwardtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))))))) + ge_balance_negative_associate_forwardtransportoutputimaginary = (((((((ge_first_rp_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))))))) + ge_balance_positive_associate_forwardtransportoutputimaginary))))))))))) -> (exists gr_unit_associate_reverse. ((exists gr_inverse_associate_reverseunit. (exists ge_first_rp_associate_reverseunitidentity ge_first_rn_associate_reverseunitidentity ge_first_ip_associate_reverseunitidentity ge_first_in_associate_reverseunitidentity ge_second_rp_associate_reverseunitidentity ge_second_rn_associate_reverseunitidentity ge_second_ip_associate_reverseunitidentity ge_second_in_associate_reverseunitidentity. ((exists ge_representation_real_code_associate_reverseunitidentityfirst ge_representation_imaginary_code_associate_reverseunitidentityfirst. (((gr_unit_associate_reverse) = ((ge_representation_real_code_associate_reverseunitidentityfirst) + (ge_representation_imaginary_code_associate_reverseunitidentityfirst)) * S ((ge_representation_real_code_associate_reverseunitidentityfirst) + (ge_representation_imaginary_code_associate_reverseunitidentityfirst)) + ((ge_representation_imaginary_code_associate_reverseunitidentityfirst) + (ge_representation_imaginary_code_associate_reverseunitidentityfirst))) /\ ((exists ge_balance_positive_associate_reverseunitidentityfirstreal ge_balance_negative_associate_reverseunitidentityfirstreal. (((((ge_representation_real_code_associate_reverseunitidentityfirst) = 2 * (ge_balance_positive_associate_reverseunitidentityfirstreal) /\ (ge_balance_negative_associate_reverseunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_reverseunitidentityfirstrealdecode. (((ge_representation_real_code_associate_reverseunitidentityfirst) = 2 * ge_signed_half_associate_reverseunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_reverseunitidentityfirstreal) = S ge_signed_half_associate_reverseunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentityfirstreal = (ge_first_rn_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_reverseunitidentityfirstimaginary ge_balance_negative_associate_reverseunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_reverseunitidentityfirst) = 2 * (ge_balance_positive_associate_reverseunitidentityfirstimaginary) /\ (ge_balance_negative_associate_reverseunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_reverseunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_reverseunitidentityfirst) = 2 * ge_signed_half_associate_reverseunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_reverseunitidentityfirstimaginary) = S ge_signed_half_associate_reverseunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentityfirstimaginary = (ge_first_in_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_reverseunitidentitysecond ge_representation_imaginary_code_associate_reverseunitidentitysecond. (((gr_inverse_associate_reverseunit) = ((ge_representation_real_code_associate_reverseunitidentitysecond) + (ge_representation_imaginary_code_associate_reverseunitidentitysecond)) * S ((ge_representation_real_code_associate_reverseunitidentitysecond) + (ge_representation_imaginary_code_associate_reverseunitidentitysecond)) + ((ge_representation_imaginary_code_associate_reverseunitidentitysecond) + (ge_representation_imaginary_code_associate_reverseunitidentitysecond))) /\ ((exists ge_balance_positive_associate_reverseunitidentitysecondreal ge_balance_negative_associate_reverseunitidentitysecondreal. (((((ge_representation_real_code_associate_reverseunitidentitysecond) = 2 * (ge_balance_positive_associate_reverseunitidentitysecondreal) /\ (ge_balance_negative_associate_reverseunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_reverseunitidentitysecondrealdecode. (((ge_representation_real_code_associate_reverseunitidentitysecond) = 2 * ge_signed_half_associate_reverseunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_reverseunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_reverseunitidentitysecondreal) = S ge_signed_half_associate_reverseunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentitysecondreal = (ge_second_rn_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_reverseunitidentitysecondimaginary ge_balance_negative_associate_reverseunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_reverseunitidentitysecond) = 2 * (ge_balance_positive_associate_reverseunitidentitysecondimaginary) /\ (ge_balance_negative_associate_reverseunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_reverseunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_reverseunitidentitysecond) = 2 * ge_signed_half_associate_reverseunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_reverseunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_reverseunitidentitysecondimaginary) = S ge_signed_half_associate_reverseunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentitysecondimaginary = (ge_second_in_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_reverseunitidentityoutput ge_representation_imaginary_code_associate_reverseunitidentityoutput. (((6) = ((ge_representation_real_code_associate_reverseunitidentityoutput) + (ge_representation_imaginary_code_associate_reverseunitidentityoutput)) * S ((ge_representation_real_code_associate_reverseunitidentityoutput) + (ge_representation_imaginary_code_associate_reverseunitidentityoutput)) + ((ge_representation_imaginary_code_associate_reverseunitidentityoutput) + (ge_representation_imaginary_code_associate_reverseunitidentityoutput))) /\ ((exists ge_balance_positive_associate_reverseunitidentityoutputreal ge_balance_negative_associate_reverseunitidentityoutputreal. (((((ge_representation_real_code_associate_reverseunitidentityoutput) = 2 * (ge_balance_positive_associate_reverseunitidentityoutputreal) /\ (ge_balance_negative_associate_reverseunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_reverseunitidentityoutputrealdecode. (((ge_representation_real_code_associate_reverseunitidentityoutput) = 2 * ge_signed_half_associate_reverseunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_reverseunitidentityoutputreal) = S ge_signed_half_associate_reverseunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))))))) + ge_balance_negative_associate_reverseunitidentityoutputreal = (((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))))))) + ge_balance_positive_associate_reverseunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_reverseunitidentityoutputimaginary ge_balance_negative_associate_reverseunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_reverseunitidentityoutput) = 2 * (ge_balance_positive_associate_reverseunitidentityoutputimaginary) /\ (ge_balance_negative_associate_reverseunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_reverseunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_reverseunitidentityoutput) = 2 * ge_signed_half_associate_reverseunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_reverseunitidentityoutputimaginary) = S ge_signed_half_associate_reverseunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))))))) + ge_balance_negative_associate_reverseunitidentityoutputimaginary = (((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))))))) + ge_balance_positive_associate_reverseunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_reversetransport ge_first_rn_associate_reversetransport ge_first_ip_associate_reversetransport ge_first_in_associate_reversetransport ge_second_rp_associate_reversetransport ge_second_rn_associate_reversetransport ge_second_ip_associate_reversetransport ge_second_in_associate_reversetransport. ((exists ge_representation_real_code_associate_reversetransportfirst ge_representation_imaginary_code_associate_reversetransportfirst. (((gr_unit_associate_reverse) = ((ge_representation_real_code_associate_reversetransportfirst) + (ge_representation_imaginary_code_associate_reversetransportfirst)) * S ((ge_representation_real_code_associate_reversetransportfirst) + (ge_representation_imaginary_code_associate_reversetransportfirst)) + ((ge_representation_imaginary_code_associate_reversetransportfirst) + (ge_representation_imaginary_code_associate_reversetransportfirst))) /\ ((exists ge_balance_positive_associate_reversetransportfirstreal ge_balance_negative_associate_reversetransportfirstreal. (((((ge_representation_real_code_associate_reversetransportfirst) = 2 * (ge_balance_positive_associate_reversetransportfirstreal) /\ (ge_balance_negative_associate_reversetransportfirstreal) = 0) \/ exists ge_signed_half_associate_reversetransportfirstrealdecode. (((ge_representation_real_code_associate_reversetransportfirst) = 2 * ge_signed_half_associate_reversetransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_reversetransportfirstreal) = 0) /\ (ge_balance_negative_associate_reversetransportfirstreal) = S ge_signed_half_associate_reversetransportfirstrealdecode))) /\ ((ge_first_rp_associate_reversetransport) + ge_balance_negative_associate_reversetransportfirstreal = (ge_first_rn_associate_reversetransport) + ge_balance_positive_associate_reversetransportfirstreal))) /\ (exists ge_balance_positive_associate_reversetransportfirstimaginary ge_balance_negative_associate_reversetransportfirstimaginary. (((((ge_representation_imaginary_code_associate_reversetransportfirst) = 2 * (ge_balance_positive_associate_reversetransportfirstimaginary) /\ (ge_balance_negative_associate_reversetransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_reversetransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_reversetransportfirst) = 2 * ge_signed_half_associate_reversetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_reversetransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_reversetransportfirstimaginary) = S ge_signed_half_associate_reversetransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_reversetransport) + ge_balance_negative_associate_reversetransportfirstimaginary = (ge_first_in_associate_reversetransport) + ge_balance_positive_associate_reversetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_reversetransportsecond ge_representation_imaginary_code_associate_reversetransportsecond. (((b) = ((ge_representation_real_code_associate_reversetransportsecond) + (ge_representation_imaginary_code_associate_reversetransportsecond)) * S ((ge_representation_real_code_associate_reversetransportsecond) + (ge_representation_imaginary_code_associate_reversetransportsecond)) + ((ge_representation_imaginary_code_associate_reversetransportsecond) + (ge_representation_imaginary_code_associate_reversetransportsecond))) /\ ((exists ge_balance_positive_associate_reversetransportsecondreal ge_balance_negative_associate_reversetransportsecondreal. (((((ge_representation_real_code_associate_reversetransportsecond) = 2 * (ge_balance_positive_associate_reversetransportsecondreal) /\ (ge_balance_negative_associate_reversetransportsecondreal) = 0) \/ exists ge_signed_half_associate_reversetransportsecondrealdecode. (((ge_representation_real_code_associate_reversetransportsecond) = 2 * ge_signed_half_associate_reversetransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_reversetransportsecondreal) = 0) /\ (ge_balance_negative_associate_reversetransportsecondreal) = S ge_signed_half_associate_reversetransportsecondrealdecode))) /\ ((ge_second_rp_associate_reversetransport) + ge_balance_negative_associate_reversetransportsecondreal = (ge_second_rn_associate_reversetransport) + ge_balance_positive_associate_reversetransportsecondreal))) /\ (exists ge_balance_positive_associate_reversetransportsecondimaginary ge_balance_negative_associate_reversetransportsecondimaginary. (((((ge_representation_imaginary_code_associate_reversetransportsecond) = 2 * (ge_balance_positive_associate_reversetransportsecondimaginary) /\ (ge_balance_negative_associate_reversetransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_reversetransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_reversetransportsecond) = 2 * ge_signed_half_associate_reversetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_reversetransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_reversetransportsecondimaginary) = S ge_signed_half_associate_reversetransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_reversetransport) + ge_balance_negative_associate_reversetransportsecondimaginary = (ge_second_in_associate_reversetransport) + ge_balance_positive_associate_reversetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_reversetransportoutput ge_representation_imaginary_code_associate_reversetransportoutput. (((a) = ((ge_representation_real_code_associate_reversetransportoutput) + (ge_representation_imaginary_code_associate_reversetransportoutput)) * S ((ge_representation_real_code_associate_reversetransportoutput) + (ge_representation_imaginary_code_associate_reversetransportoutput)) + ((ge_representation_imaginary_code_associate_reversetransportoutput) + (ge_representation_imaginary_code_associate_reversetransportoutput))) /\ ((exists ge_balance_positive_associate_reversetransportoutputreal ge_balance_negative_associate_reversetransportoutputreal. (((((ge_representation_real_code_associate_reversetransportoutput) = 2 * (ge_balance_positive_associate_reversetransportoutputreal) /\ (ge_balance_negative_associate_reversetransportoutputreal) = 0) \/ exists ge_signed_half_associate_reversetransportoutputrealdecode. (((ge_representation_real_code_associate_reversetransportoutput) = 2 * ge_signed_half_associate_reversetransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_reversetransportoutputreal) = 0) /\ (ge_balance_negative_associate_reversetransportoutputreal) = S ge_signed_half_associate_reversetransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_reversetransport) * (ge_second_rp_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_rn_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_in_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_ip_associate_reversetransport))))))) + ge_balance_negative_associate_reversetransportoutputreal = (((((((ge_first_rp_associate_reversetransport) * (ge_second_rn_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_rp_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_ip_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_in_associate_reversetransport))))))) + ge_balance_positive_associate_reversetransportoutputreal))) /\ (exists ge_balance_positive_associate_reversetransportoutputimaginary ge_balance_negative_associate_reversetransportoutputimaginary. (((((ge_representation_imaginary_code_associate_reversetransportoutput) = 2 * (ge_balance_positive_associate_reversetransportoutputimaginary) /\ (ge_balance_negative_associate_reversetransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_reversetransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_reversetransportoutput) = 2 * ge_signed_half_associate_reversetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_reversetransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_reversetransportoutputimaginary) = S ge_signed_half_associate_reversetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_reversetransport) * (ge_second_ip_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_in_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_rp_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_rn_associate_reversetransport))))))) + ge_balance_negative_associate_reversetransportoutputimaginary = (((((((ge_first_rp_associate_reversetransport) * (ge_second_in_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_ip_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_rn_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_rp_associate_reversetransport))))))) + ge_balance_positive_associate_reversetransportoutputimaginary)))))))))))

Constructive proof overview

Generated structural guide

Invert the actual unit witness to reverse Gaussian association, including the zero boundary.

The unchanged tactic script uses 4 declared prerequisites and contains 31 exact native proof lines.

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

GF003E gaussian_unit_inverse GF0025 gaussian_multiply_associative GF0029 gaussian_multiply_one_left GF0008 gaussian_multiply_input_right_valid

Direct dependents

GF0069 gaussian_irreducible_dvd_product GF00A5 gaussian_factor_associate_cancel_products GF00B0 gaussian_irreducible_factorizations_unique

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

31 script commands · 8 reading checkpoints · 1 local claims

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

Named ingredients (4)
gaussian unit inversegaussian multiply associativegaussian multiply one leftgaussian multiply input right valid

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
02Separate the logical casesL4–5

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

  1. L4
    cases h
  2. L5
    cases h_witness
03Establish hinverseL6–9

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

  1. L6
    have hinverse : ∃ v. GUnit(v) ∧ (GMul(x,v,6) ∧ GMul(v,x,6))Definitions: GMulGUnit
  2. L7
    specialize gaussian_unit_inverse (x)
  3. L8
    apply gaussian_unit_inverse
  4. L9
    exact h_witness_left
04Separate the logical casesL10–12

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

  1. L10
    cases hinverse
  2. L11
    cases hinverse_witness
  3. L12
    cases hinverse_witness_right
05Construct an explicit witnessL13–13

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

  1. L13
    exists (x1)
06Separate the logical casesL14–14

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

  1. L14
    split
07Use earlier factsL15–24

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

  1. L15
    exact hinverse_witness_left
  2. L16
    specialize gaussian_multiply_associative (x1)
  3. L17
    specialize gaussian_multiply_associative (x)
  4. L18
    specialize gaussian_multiply_associative (a)
  5. L19
    specialize gaussian_multiply_associative (6)
  6. L20
    specialize gaussian_multiply_associative (b)
  7. L21
    specialize gaussian_multiply_associative (a)
  8. L22
    apply gaussian_multiply_associative
  9. L23
    exact hinverse_witness_right_right
  10. L24
    specialize gaussian_multiply_one_left (a)
08Use earlier factsL25–31

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

  1. L25
    apply gaussian_multiply_one_left
  2. L26
    specialize gaussian_multiply_input_right_valid (x)
  3. L27
    specialize gaussian_multiply_input_right_valid (a)
  4. L28
    specialize gaussian_multiply_input_right_valid (b)
  5. L29
    apply gaussian_multiply_input_right_valid
  6. L30
    exact h_witness_right
  7. L31
    exact h_witness_right

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004cases h
  5. 0005cases h_witness
  6. 0006have hinverse : exists v. ((exists gr_inverse_associate_inverse_unit. (exists ge_first_rp_associate_inverse_unitidentity ge_first_rn_associate_inverse_unitidentity ge_first_ip_associate_inverse_unitidentity ge_first_in_associate_inverse_unitidentity ge_second_rp_associate_inverse_unitidentity ge_second_rn_associate_inverse_unitidentity ge_second_ip_associate_inverse_unitidentity ge_second_in_associate_inverse_unitidentity. ((exists ge_representation_real_code_associate_inverse_unitidentityfirst ge_representation_imaginary_code_associate_inverse_unitidentityfirst. (((v) = ((ge_representation_real_code_associate_inverse_unitidentityfirst) + (ge_representation_imaginary_code_associate_inverse_unitidentityfirst)) * S ((ge_representation_real_code_associate_inverse_unitidentityfirst) + (ge_representation_imaginary_code_associate_inverse_unitidentityfirst)) + ((ge_representation_imaginary_code_associate_inverse_unitidentityfirst) + (ge_representation_imaginary_code_associate_inverse_unitidentityfirst))) /\ ((exists ge_balance_positive_associate_inverse_unitidentityfirstreal ge_balance_negative_associate_inverse_unitidentityfirstreal. (((((ge_representation_real_code_associate_inverse_unitidentityfirst) = 2 * (ge_balance_positive_associate_inverse_unitidentityfirstreal) /\ (ge_balance_negative_associate_inverse_unitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_inverse_unitidentityfirstrealdecode. (((ge_representation_real_code_associate_inverse_unitidentityfirst) = 2 * ge_signed_half_associate_inverse_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_inverse_unitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_inverse_unitidentityfirstreal) = S ge_signed_half_associate_inverse_unitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_inverse_unitidentity) + ge_balance_negative_associate_inverse_unitidentityfirstreal = (ge_first_rn_associate_inverse_unitidentity) + ge_balance_positive_associate_inverse_unitidentityfirstreal))) /\ (exists ge_balance_positive_associate_inverse_unitidentityfirstimaginary ge_balance_negative_associate_inverse_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_inverse_unitidentityfirst) = 2 * (ge_balance_positive_associate_inverse_unitidentityfirstimaginary) /\ (ge_balance_negative_associate_inverse_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_inverse_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_unitidentityfirst) = 2 * ge_signed_half_associate_inverse_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_inverse_unitidentityfirstimaginary) = S ge_signed_half_associate_inverse_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_inverse_unitidentity) + ge_balance_negative_associate_inverse_unitidentityfirstimaginary = (ge_first_in_associate_inverse_unitidentity) + ge_balance_positive_associate_inverse_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_inverse_unitidentitysecond ge_representation_imaginary_code_associate_inverse_unitidentitysecond. (((gr_inverse_associate_inverse_unit) = ((ge_representation_real_code_associate_inverse_unitidentitysecond) + (ge_representation_imaginary_code_associate_inverse_unitidentitysecond)) * S ((ge_representation_real_code_associate_inverse_unitidentitysecond) + (ge_representation_imaginary_code_associate_inverse_unitidentitysecond)) + ((ge_representation_imaginary_code_associate_inverse_unitidentitysecond) + (ge_representation_imaginary_code_associate_inverse_unitidentitysecond))) /\ ((exists ge_balance_positive_associate_inverse_unitidentitysecondreal ge_balance_negative_associate_inverse_unitidentitysecondreal. (((((ge_representation_real_code_associate_inverse_unitidentitysecond) = 2 * (ge_balance_positive_associate_inverse_unitidentitysecondreal) /\ (ge_balance_negative_associate_inverse_unitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_inverse_unitidentitysecondrealdecode. (((ge_representation_real_code_associate_inverse_unitidentitysecond) = 2 * ge_signed_half_associate_inverse_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_inverse_unitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_inverse_unitidentitysecondreal) = S ge_signed_half_associate_inverse_unitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_inverse_unitidentity) + ge_balance_negative_associate_inverse_unitidentitysecondreal = (ge_second_rn_associate_inverse_unitidentity) + ge_balance_positive_associate_inverse_unitidentitysecondreal))) /\ (exists ge_balance_positive_associate_inverse_unitidentitysecondimaginary ge_balance_negative_associate_inverse_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_inverse_unitidentitysecond) = 2 * (ge_balance_positive_associate_inverse_unitidentitysecondimaginary) /\ (ge_balance_negative_associate_inverse_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_inverse_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_unitidentitysecond) = 2 * ge_signed_half_associate_inverse_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_inverse_unitidentitysecondimaginary) = S ge_signed_half_associate_inverse_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_inverse_unitidentity) + ge_balance_negative_associate_inverse_unitidentitysecondimaginary = (ge_second_in_associate_inverse_unitidentity) + ge_balance_positive_associate_inverse_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_inverse_unitidentityoutput ge_representation_imaginary_code_associate_inverse_unitidentityoutput. (((6) = ((ge_representation_real_code_associate_inverse_unitidentityoutput) + (ge_representation_imaginary_code_associate_inverse_unitidentityoutput)) * S ((ge_representation_real_code_associate_inverse_unitidentityoutput) + (ge_representation_imaginary_code_associate_inverse_unitidentityoutput)) + ((ge_representation_imaginary_code_associate_inverse_unitidentityoutput) + (ge_representation_imaginary_code_associate_inverse_unitidentityoutput))) /\ ((exists ge_balance_positive_associate_inverse_unitidentityoutputreal ge_balance_negative_associate_inverse_unitidentityoutputreal. (((((ge_representation_real_code_associate_inverse_unitidentityoutput) = 2 * (ge_balance_positive_associate_inverse_unitidentityoutputreal) /\ (ge_balance_negative_associate_inverse_unitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_inverse_unitidentityoutputrealdecode. (((ge_representation_real_code_associate_inverse_unitidentityoutput) = 2 * ge_signed_half_associate_inverse_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_inverse_unitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_inverse_unitidentityoutputreal) = S ge_signed_half_associate_inverse_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_inverse_unitidentity) * (ge_second_rp_associate_inverse_unitidentity))) + (((ge_first_rn_associate_inverse_unitidentity) * (ge_second_rn_associate_inverse_unitidentity))))) + (((((ge_first_ip_associate_inverse_unitidentity) * (ge_second_in_associate_inverse_unitidentity))) + (((ge_first_in_associate_inverse_unitidentity) * (ge_second_ip_associate_inverse_unitidentity))))))) + ge_balance_negative_associate_inverse_unitidentityoutputreal = (((((((ge_first_rp_associate_inverse_unitidentity) * (ge_second_rn_associate_inverse_unitidentity))) + (((ge_first_rn_associate_inverse_unitidentity) * (ge_second_rp_associate_inverse_unitidentity))))) + (((((ge_first_ip_associate_inverse_unitidentity) * (ge_second_ip_associate_inverse_unitidentity))) + (((ge_first_in_associate_inverse_unitidentity) * (ge_second_in_associate_inverse_unitidentity))))))) + ge_balance_positive_associate_inverse_unitidentityoutputreal))) /\ (exists ge_balance_positive_associate_inverse_unitidentityoutputimaginary ge_balance_negative_associate_inverse_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_inverse_unitidentityoutput) = 2 * (ge_balance_positive_associate_inverse_unitidentityoutputimaginary) /\ (ge_balance_negative_associate_inverse_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_inverse_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_unitidentityoutput) = 2 * ge_signed_half_associate_inverse_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_inverse_unitidentityoutputimaginary) = S ge_signed_half_associate_inverse_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_inverse_unitidentity) * (ge_second_ip_associate_inverse_unitidentity))) + (((ge_first_rn_associate_inverse_unitidentity) * (ge_second_in_associate_inverse_unitidentity))))) + (((((ge_first_ip_associate_inverse_unitidentity) * (ge_second_rp_associate_inverse_unitidentity))) + (((ge_first_in_associate_inverse_unitidentity) * (ge_second_rn_associate_inverse_unitidentity))))))) + ge_balance_negative_associate_inverse_unitidentityoutputimaginary = (((((((ge_first_rp_associate_inverse_unitidentity) * (ge_second_in_associate_inverse_unitidentity))) + (((ge_first_rn_associate_inverse_unitidentity) * (ge_second_ip_associate_inverse_unitidentity))))) + (((((ge_first_ip_associate_inverse_unitidentity) * (ge_second_rn_associate_inverse_unitidentity))) + (((ge_first_in_associate_inverse_unitidentity) * (ge_second_rp_associate_inverse_unitidentity))))))) + ge_balance_positive_associate_inverse_unitidentityoutputimaginary)))))))))) /\ ((exists ge_first_rp_associate_inverse_first ge_first_rn_associate_inverse_first ge_first_ip_associate_inverse_first ge_first_in_associate_inverse_first ge_second_rp_associate_inverse_first ge_second_rn_associate_inverse_first ge_second_ip_associate_inverse_first ge_second_in_associate_inverse_first. ((exists ge_representation_real_code_associate_inverse_firstfirst ge_representation_imaginary_code_associate_inverse_firstfirst. (((x) = ((ge_representation_real_code_associate_inverse_firstfirst) + (ge_representation_imaginary_code_associate_inverse_firstfirst)) * S ((ge_representation_real_code_associate_inverse_firstfirst) + (ge_representation_imaginary_code_associate_inverse_firstfirst)) + ((ge_representation_imaginary_code_associate_inverse_firstfirst) + (ge_representation_imaginary_code_associate_inverse_firstfirst))) /\ ((exists ge_balance_positive_associate_inverse_firstfirstreal ge_balance_negative_associate_inverse_firstfirstreal. (((((ge_representation_real_code_associate_inverse_firstfirst) = 2 * (ge_balance_positive_associate_inverse_firstfirstreal) /\ (ge_balance_negative_associate_inverse_firstfirstreal) = 0) \/ exists ge_signed_half_associate_inverse_firstfirstrealdecode. (((ge_representation_real_code_associate_inverse_firstfirst) = 2 * ge_signed_half_associate_inverse_firstfirstrealdecode + 1 /\ (ge_balance_positive_associate_inverse_firstfirstreal) = 0) /\ (ge_balance_negative_associate_inverse_firstfirstreal) = S ge_signed_half_associate_inverse_firstfirstrealdecode))) /\ ((ge_first_rp_associate_inverse_first) + ge_balance_negative_associate_inverse_firstfirstreal = (ge_first_rn_associate_inverse_first) + ge_balance_positive_associate_inverse_firstfirstreal))) /\ (exists ge_balance_positive_associate_inverse_firstfirstimaginary ge_balance_negative_associate_inverse_firstfirstimaginary. (((((ge_representation_imaginary_code_associate_inverse_firstfirst) = 2 * (ge_balance_positive_associate_inverse_firstfirstimaginary) /\ (ge_balance_negative_associate_inverse_firstfirstimaginary) = 0) \/ exists ge_signed_half_associate_inverse_firstfirstimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_firstfirst) = 2 * ge_signed_half_associate_inverse_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_firstfirstimaginary) = 0) /\ (ge_balance_negative_associate_inverse_firstfirstimaginary) = S ge_signed_half_associate_inverse_firstfirstimaginarydecode))) /\ ((ge_first_ip_associate_inverse_first) + ge_balance_negative_associate_inverse_firstfirstimaginary = (ge_first_in_associate_inverse_first) + ge_balance_positive_associate_inverse_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_inverse_firstsecond ge_representation_imaginary_code_associate_inverse_firstsecond. (((v) = ((ge_representation_real_code_associate_inverse_firstsecond) + (ge_representation_imaginary_code_associate_inverse_firstsecond)) * S ((ge_representation_real_code_associate_inverse_firstsecond) + (ge_representation_imaginary_code_associate_inverse_firstsecond)) + ((ge_representation_imaginary_code_associate_inverse_firstsecond) + (ge_representation_imaginary_code_associate_inverse_firstsecond))) /\ ((exists ge_balance_positive_associate_inverse_firstsecondreal ge_balance_negative_associate_inverse_firstsecondreal. (((((ge_representation_real_code_associate_inverse_firstsecond) = 2 * (ge_balance_positive_associate_inverse_firstsecondreal) /\ (ge_balance_negative_associate_inverse_firstsecondreal) = 0) \/ exists ge_signed_half_associate_inverse_firstsecondrealdecode. (((ge_representation_real_code_associate_inverse_firstsecond) = 2 * ge_signed_half_associate_inverse_firstsecondrealdecode + 1 /\ (ge_balance_positive_associate_inverse_firstsecondreal) = 0) /\ (ge_balance_negative_associate_inverse_firstsecondreal) = S ge_signed_half_associate_inverse_firstsecondrealdecode))) /\ ((ge_second_rp_associate_inverse_first) + ge_balance_negative_associate_inverse_firstsecondreal = (ge_second_rn_associate_inverse_first) + ge_balance_positive_associate_inverse_firstsecondreal))) /\ (exists ge_balance_positive_associate_inverse_firstsecondimaginary ge_balance_negative_associate_inverse_firstsecondimaginary. (((((ge_representation_imaginary_code_associate_inverse_firstsecond) = 2 * (ge_balance_positive_associate_inverse_firstsecondimaginary) /\ (ge_balance_negative_associate_inverse_firstsecondimaginary) = 0) \/ exists ge_signed_half_associate_inverse_firstsecondimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_firstsecond) = 2 * ge_signed_half_associate_inverse_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_firstsecondimaginary) = 0) /\ (ge_balance_negative_associate_inverse_firstsecondimaginary) = S ge_signed_half_associate_inverse_firstsecondimaginarydecode))) /\ ((ge_second_ip_associate_inverse_first) + ge_balance_negative_associate_inverse_firstsecondimaginary = (ge_second_in_associate_inverse_first) + ge_balance_positive_associate_inverse_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_inverse_firstoutput ge_representation_imaginary_code_associate_inverse_firstoutput. (((6) = ((ge_representation_real_code_associate_inverse_firstoutput) + (ge_representation_imaginary_code_associate_inverse_firstoutput)) * S ((ge_representation_real_code_associate_inverse_firstoutput) + (ge_representation_imaginary_code_associate_inverse_firstoutput)) + ((ge_representation_imaginary_code_associate_inverse_firstoutput) + (ge_representation_imaginary_code_associate_inverse_firstoutput))) /\ ((exists ge_balance_positive_associate_inverse_firstoutputreal ge_balance_negative_associate_inverse_firstoutputreal. (((((ge_representation_real_code_associate_inverse_firstoutput) = 2 * (ge_balance_positive_associate_inverse_firstoutputreal) /\ (ge_balance_negative_associate_inverse_firstoutputreal) = 0) \/ exists ge_signed_half_associate_inverse_firstoutputrealdecode. (((ge_representation_real_code_associate_inverse_firstoutput) = 2 * ge_signed_half_associate_inverse_firstoutputrealdecode + 1 /\ (ge_balance_positive_associate_inverse_firstoutputreal) = 0) /\ (ge_balance_negative_associate_inverse_firstoutputreal) = S ge_signed_half_associate_inverse_firstoutputrealdecode))) /\ ((((((((ge_first_rp_associate_inverse_first) * (ge_second_rp_associate_inverse_first))) + (((ge_first_rn_associate_inverse_first) * (ge_second_rn_associate_inverse_first))))) + (((((ge_first_ip_associate_inverse_first) * (ge_second_in_associate_inverse_first))) + (((ge_first_in_associate_inverse_first) * (ge_second_ip_associate_inverse_first))))))) + ge_balance_negative_associate_inverse_firstoutputreal = (((((((ge_first_rp_associate_inverse_first) * (ge_second_rn_associate_inverse_first))) + (((ge_first_rn_associate_inverse_first) * (ge_second_rp_associate_inverse_first))))) + (((((ge_first_ip_associate_inverse_first) * (ge_second_ip_associate_inverse_first))) + (((ge_first_in_associate_inverse_first) * (ge_second_in_associate_inverse_first))))))) + ge_balance_positive_associate_inverse_firstoutputreal))) /\ (exists ge_balance_positive_associate_inverse_firstoutputimaginary ge_balance_negative_associate_inverse_firstoutputimaginary. (((((ge_representation_imaginary_code_associate_inverse_firstoutput) = 2 * (ge_balance_positive_associate_inverse_firstoutputimaginary) /\ (ge_balance_negative_associate_inverse_firstoutputimaginary) = 0) \/ exists ge_signed_half_associate_inverse_firstoutputimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_firstoutput) = 2 * ge_signed_half_associate_inverse_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_firstoutputimaginary) = 0) /\ (ge_balance_negative_associate_inverse_firstoutputimaginary) = S ge_signed_half_associate_inverse_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_inverse_first) * (ge_second_ip_associate_inverse_first))) + (((ge_first_rn_associate_inverse_first) * (ge_second_in_associate_inverse_first))))) + (((((ge_first_ip_associate_inverse_first) * (ge_second_rp_associate_inverse_first))) + (((ge_first_in_associate_inverse_first) * (ge_second_rn_associate_inverse_first))))))) + ge_balance_negative_associate_inverse_firstoutputimaginary = (((((((ge_first_rp_associate_inverse_first) * (ge_second_in_associate_inverse_first))) + (((ge_first_rn_associate_inverse_first) * (ge_second_ip_associate_inverse_first))))) + (((((ge_first_ip_associate_inverse_first) * (ge_second_rn_associate_inverse_first))) + (((ge_first_in_associate_inverse_first) * (ge_second_rp_associate_inverse_first))))))) + ge_balance_positive_associate_inverse_firstoutputimaginary))))))))) /\ (exists ge_first_rp_associate_inverse_second ge_first_rn_associate_inverse_second ge_first_ip_associate_inverse_second ge_first_in_associate_inverse_second ge_second_rp_associate_inverse_second ge_second_rn_associate_inverse_second ge_second_ip_associate_inverse_second ge_second_in_associate_inverse_second. ((exists ge_representation_real_code_associate_inverse_secondfirst ge_representation_imaginary_code_associate_inverse_secondfirst. (((v) = ((ge_representation_real_code_associate_inverse_secondfirst) + (ge_representation_imaginary_code_associate_inverse_secondfirst)) * S ((ge_representation_real_code_associate_inverse_secondfirst) + (ge_representation_imaginary_code_associate_inverse_secondfirst)) + ((ge_representation_imaginary_code_associate_inverse_secondfirst) + (ge_representation_imaginary_code_associate_inverse_secondfirst))) /\ ((exists ge_balance_positive_associate_inverse_secondfirstreal ge_balance_negative_associate_inverse_secondfirstreal. (((((ge_representation_real_code_associate_inverse_secondfirst) = 2 * (ge_balance_positive_associate_inverse_secondfirstreal) /\ (ge_balance_negative_associate_inverse_secondfirstreal) = 0) \/ exists ge_signed_half_associate_inverse_secondfirstrealdecode. (((ge_representation_real_code_associate_inverse_secondfirst) = 2 * ge_signed_half_associate_inverse_secondfirstrealdecode + 1 /\ (ge_balance_positive_associate_inverse_secondfirstreal) = 0) /\ (ge_balance_negative_associate_inverse_secondfirstreal) = S ge_signed_half_associate_inverse_secondfirstrealdecode))) /\ ((ge_first_rp_associate_inverse_second) + ge_balance_negative_associate_inverse_secondfirstreal = (ge_first_rn_associate_inverse_second) + ge_balance_positive_associate_inverse_secondfirstreal))) /\ (exists ge_balance_positive_associate_inverse_secondfirstimaginary ge_balance_negative_associate_inverse_secondfirstimaginary. (((((ge_representation_imaginary_code_associate_inverse_secondfirst) = 2 * (ge_balance_positive_associate_inverse_secondfirstimaginary) /\ (ge_balance_negative_associate_inverse_secondfirstimaginary) = 0) \/ exists ge_signed_half_associate_inverse_secondfirstimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_secondfirst) = 2 * ge_signed_half_associate_inverse_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_secondfirstimaginary) = 0) /\ (ge_balance_negative_associate_inverse_secondfirstimaginary) = S ge_signed_half_associate_inverse_secondfirstimaginarydecode))) /\ ((ge_first_ip_associate_inverse_second) + ge_balance_negative_associate_inverse_secondfirstimaginary = (ge_first_in_associate_inverse_second) + ge_balance_positive_associate_inverse_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_inverse_secondsecond ge_representation_imaginary_code_associate_inverse_secondsecond. (((x) = ((ge_representation_real_code_associate_inverse_secondsecond) + (ge_representation_imaginary_code_associate_inverse_secondsecond)) * S ((ge_representation_real_code_associate_inverse_secondsecond) + (ge_representation_imaginary_code_associate_inverse_secondsecond)) + ((ge_representation_imaginary_code_associate_inverse_secondsecond) + (ge_representation_imaginary_code_associate_inverse_secondsecond))) /\ ((exists ge_balance_positive_associate_inverse_secondsecondreal ge_balance_negative_associate_inverse_secondsecondreal. (((((ge_representation_real_code_associate_inverse_secondsecond) = 2 * (ge_balance_positive_associate_inverse_secondsecondreal) /\ (ge_balance_negative_associate_inverse_secondsecondreal) = 0) \/ exists ge_signed_half_associate_inverse_secondsecondrealdecode. (((ge_representation_real_code_associate_inverse_secondsecond) = 2 * ge_signed_half_associate_inverse_secondsecondrealdecode + 1 /\ (ge_balance_positive_associate_inverse_secondsecondreal) = 0) /\ (ge_balance_negative_associate_inverse_secondsecondreal) = S ge_signed_half_associate_inverse_secondsecondrealdecode))) /\ ((ge_second_rp_associate_inverse_second) + ge_balance_negative_associate_inverse_secondsecondreal = (ge_second_rn_associate_inverse_second) + ge_balance_positive_associate_inverse_secondsecondreal))) /\ (exists ge_balance_positive_associate_inverse_secondsecondimaginary ge_balance_negative_associate_inverse_secondsecondimaginary. (((((ge_representation_imaginary_code_associate_inverse_secondsecond) = 2 * (ge_balance_positive_associate_inverse_secondsecondimaginary) /\ (ge_balance_negative_associate_inverse_secondsecondimaginary) = 0) \/ exists ge_signed_half_associate_inverse_secondsecondimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_secondsecond) = 2 * ge_signed_half_associate_inverse_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_secondsecondimaginary) = 0) /\ (ge_balance_negative_associate_inverse_secondsecondimaginary) = S ge_signed_half_associate_inverse_secondsecondimaginarydecode))) /\ ((ge_second_ip_associate_inverse_second) + ge_balance_negative_associate_inverse_secondsecondimaginary = (ge_second_in_associate_inverse_second) + ge_balance_positive_associate_inverse_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_inverse_secondoutput ge_representation_imaginary_code_associate_inverse_secondoutput. (((6) = ((ge_representation_real_code_associate_inverse_secondoutput) + (ge_representation_imaginary_code_associate_inverse_secondoutput)) * S ((ge_representation_real_code_associate_inverse_secondoutput) + (ge_representation_imaginary_code_associate_inverse_secondoutput)) + ((ge_representation_imaginary_code_associate_inverse_secondoutput) + (ge_representation_imaginary_code_associate_inverse_secondoutput))) /\ ((exists ge_balance_positive_associate_inverse_secondoutputreal ge_balance_negative_associate_inverse_secondoutputreal. (((((ge_representation_real_code_associate_inverse_secondoutput) = 2 * (ge_balance_positive_associate_inverse_secondoutputreal) /\ (ge_balance_negative_associate_inverse_secondoutputreal) = 0) \/ exists ge_signed_half_associate_inverse_secondoutputrealdecode. (((ge_representation_real_code_associate_inverse_secondoutput) = 2 * ge_signed_half_associate_inverse_secondoutputrealdecode + 1 /\ (ge_balance_positive_associate_inverse_secondoutputreal) = 0) /\ (ge_balance_negative_associate_inverse_secondoutputreal) = S ge_signed_half_associate_inverse_secondoutputrealdecode))) /\ ((((((((ge_first_rp_associate_inverse_second) * (ge_second_rp_associate_inverse_second))) + (((ge_first_rn_associate_inverse_second) * (ge_second_rn_associate_inverse_second))))) + (((((ge_first_ip_associate_inverse_second) * (ge_second_in_associate_inverse_second))) + (((ge_first_in_associate_inverse_second) * (ge_second_ip_associate_inverse_second))))))) + ge_balance_negative_associate_inverse_secondoutputreal = (((((((ge_first_rp_associate_inverse_second) * (ge_second_rn_associate_inverse_second))) + (((ge_first_rn_associate_inverse_second) * (ge_second_rp_associate_inverse_second))))) + (((((ge_first_ip_associate_inverse_second) * (ge_second_ip_associate_inverse_second))) + (((ge_first_in_associate_inverse_second) * (ge_second_in_associate_inverse_second))))))) + ge_balance_positive_associate_inverse_secondoutputreal))) /\ (exists ge_balance_positive_associate_inverse_secondoutputimaginary ge_balance_negative_associate_inverse_secondoutputimaginary. (((((ge_representation_imaginary_code_associate_inverse_secondoutput) = 2 * (ge_balance_positive_associate_inverse_secondoutputimaginary) /\ (ge_balance_negative_associate_inverse_secondoutputimaginary) = 0) \/ exists ge_signed_half_associate_inverse_secondoutputimaginarydecode. (((ge_representation_imaginary_code_associate_inverse_secondoutput) = 2 * ge_signed_half_associate_inverse_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_inverse_secondoutputimaginary) = 0) /\ (ge_balance_negative_associate_inverse_secondoutputimaginary) = S ge_signed_half_associate_inverse_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_inverse_second) * (ge_second_ip_associate_inverse_second))) + (((ge_first_rn_associate_inverse_second) * (ge_second_in_associate_inverse_second))))) + (((((ge_first_ip_associate_inverse_second) * (ge_second_rp_associate_inverse_second))) + (((ge_first_in_associate_inverse_second) * (ge_second_rn_associate_inverse_second))))))) + ge_balance_negative_associate_inverse_secondoutputimaginary = (((((((ge_first_rp_associate_inverse_second) * (ge_second_in_associate_inverse_second))) + (((ge_first_rn_associate_inverse_second) * (ge_second_ip_associate_inverse_second))))) + (((((ge_first_ip_associate_inverse_second) * (ge_second_rn_associate_inverse_second))) + (((ge_first_in_associate_inverse_second) * (ge_second_rp_associate_inverse_second))))))) + ge_balance_positive_associate_inverse_secondoutputimaginary)))))))))))
  7. 0007specialize gaussian_unit_inverse (x)
  8. 0008apply gaussian_unit_inverse
  9. 0009exact h_witness_left
  10. 0010cases hinverse
  11. 0011cases hinverse_witness
  12. 0012cases hinverse_witness_right
  13. 0013exists (x1)
  14. 0014split
  15. 0015exact hinverse_witness_left
  16. 0016specialize gaussian_multiply_associative (x1)
  17. 0017specialize gaussian_multiply_associative (x)
  18. 0018specialize gaussian_multiply_associative (a)
  19. 0019specialize gaussian_multiply_associative (6)
  20. 0020specialize gaussian_multiply_associative (b)
  21. 0021specialize gaussian_multiply_associative (a)
  22. 0022apply gaussian_multiply_associative
  23. 0023exact hinverse_witness_right_right
  24. 0024specialize gaussian_multiply_one_left (a)
  25. 0025apply gaussian_multiply_one_left
  26. 0026specialize gaussian_multiply_input_right_valid (x)
  27. 0027specialize gaussian_multiply_input_right_valid (a)
  28. 0028specialize gaussian_multiply_input_right_valid (b)
  29. 0029apply gaussian_multiply_input_right_valid
  30. 0030exact h_witness_right
  31. 0031exact h_witness_right