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_quotient_mutual_first. (exists ge_first_rp_mutual_firstproduct ge_first_rn_mutual_firstproduct ge_first_ip_mutual_firstproduct ge_first_in_mutual_firstproduct ge_second_rp_mutual_firstproduct ge_second_rn_mutual_firstproduct ge_second_ip_mutual_firstproduct ge_second_in_mutual_firstproduct. ((exists ge_representation_real_code_mutual_firstproductfirst ge_representation_imaginary_code_mutual_firstproductfirst. (((a) = ((ge_representation_real_code_mutual_firstproductfirst) + (ge_representation_imaginary_code_mutual_firstproductfirst)) * S ((ge_representation_real_code_mutual_firstproductfirst) + (ge_representation_imaginary_code_mutual_firstproductfirst)) + ((ge_representation_imaginary_code_mutual_firstproductfirst) + (ge_representation_imaginary_code_mutual_firstproductfirst))) /\ ((exists ge_balance_positive_mutual_firstproductfirstreal ge_balance_negative_mutual_firstproductfirstreal. (((((ge_representation_real_code_mutual_firstproductfirst) = 2 * (ge_balance_positive_mutual_firstproductfirstreal) /\ (ge_balance_negative_mutual_firstproductfirstreal) = 0) \/ exists ge_signed_half_mutual_firstproductfirstrealdecode. (((ge_representation_real_code_mutual_firstproductfirst) = 2 * ge_signed_half_mutual_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_mutual_firstproductfirstreal) = 0) /\ (ge_balance_negative_mutual_firstproductfirstreal) = S ge_signed_half_mutual_firstproductfirstrealdecode))) /\ ((ge_first_rp_mutual_firstproduct) + ge_balance_negative_mutual_firstproductfirstreal = (ge_first_rn_mutual_firstproduct) + ge_balance_positive_mutual_firstproductfirstreal))) /\ (exists ge_balance_positive_mutual_firstproductfirstimaginary ge_balance_negative_mutual_firstproductfirstimaginary. (((((ge_representation_imaginary_code_mutual_firstproductfirst) = 2 * (ge_balance_positive_mutual_firstproductfirstimaginary) /\ (ge_balance_negative_mutual_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_mutual_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_firstproductfirst) = 2 * ge_signed_half_mutual_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_mutual_firstproductfirstimaginary) = S ge_signed_half_mutual_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_mutual_firstproduct) + ge_balance_negative_mutual_firstproductfirstimaginary = (ge_first_in_mutual_firstproduct) + ge_balance_positive_mutual_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_firstproductsecond ge_representation_imaginary_code_mutual_firstproductsecond. (((gr_quotient_mutual_first) = ((ge_representation_real_code_mutual_firstproductsecond) + (ge_representation_imaginary_code_mutual_firstproductsecond)) * S ((ge_representation_real_code_mutual_firstproductsecond) + (ge_representation_imaginary_code_mutual_firstproductsecond)) + ((ge_representation_imaginary_code_mutual_firstproductsecond) + (ge_representation_imaginary_code_mutual_firstproductsecond))) /\ ((exists ge_balance_positive_mutual_firstproductsecondreal ge_balance_negative_mutual_firstproductsecondreal. (((((ge_representation_real_code_mutual_firstproductsecond) = 2 * (ge_balance_positive_mutual_firstproductsecondreal) /\ (ge_balance_negative_mutual_firstproductsecondreal) = 0) \/ exists ge_signed_half_mutual_firstproductsecondrealdecode. (((ge_representation_real_code_mutual_firstproductsecond) = 2 * ge_signed_half_mutual_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_mutual_firstproductsecondreal) = 0) /\ (ge_balance_negative_mutual_firstproductsecondreal) = S ge_signed_half_mutual_firstproductsecondrealdecode))) /\ ((ge_second_rp_mutual_firstproduct) + ge_balance_negative_mutual_firstproductsecondreal = (ge_second_rn_mutual_firstproduct) + ge_balance_positive_mutual_firstproductsecondreal))) /\ (exists ge_balance_positive_mutual_firstproductsecondimaginary ge_balance_negative_mutual_firstproductsecondimaginary. (((((ge_representation_imaginary_code_mutual_firstproductsecond) = 2 * (ge_balance_positive_mutual_firstproductsecondimaginary) /\ (ge_balance_negative_mutual_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_mutual_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_firstproductsecond) = 2 * ge_signed_half_mutual_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_mutual_firstproductsecondimaginary) = S ge_signed_half_mutual_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_mutual_firstproduct) + ge_balance_negative_mutual_firstproductsecondimaginary = (ge_second_in_mutual_firstproduct) + ge_balance_positive_mutual_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_firstproductoutput ge_representation_imaginary_code_mutual_firstproductoutput. (((b) = ((ge_representation_real_code_mutual_firstproductoutput) + (ge_representation_imaginary_code_mutual_firstproductoutput)) * S ((ge_representation_real_code_mutual_firstproductoutput) + (ge_representation_imaginary_code_mutual_firstproductoutput)) + ((ge_representation_imaginary_code_mutual_firstproductoutput) + (ge_representation_imaginary_code_mutual_firstproductoutput))) /\ ((exists ge_balance_positive_mutual_firstproductoutputreal ge_balance_negative_mutual_firstproductoutputreal. (((((ge_representation_real_code_mutual_firstproductoutput) = 2 * (ge_balance_positive_mutual_firstproductoutputreal) /\ (ge_balance_negative_mutual_firstproductoutputreal) = 0) \/ exists ge_signed_half_mutual_firstproductoutputrealdecode. (((ge_representation_real_code_mutual_firstproductoutput) = 2 * ge_signed_half_mutual_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_mutual_firstproductoutputreal) = 0) /\ (ge_balance_negative_mutual_firstproductoutputreal) = S ge_signed_half_mutual_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))))))) + ge_balance_negative_mutual_firstproductoutputreal = (((((((ge_first_rp_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))))))) + ge_balance_positive_mutual_firstproductoutputreal))) /\ (exists ge_balance_positive_mutual_firstproductoutputimaginary ge_balance_negative_mutual_firstproductoutputimaginary. (((((ge_representation_imaginary_code_mutual_firstproductoutput) = 2 * (ge_balance_positive_mutual_firstproductoutputimaginary) /\ (ge_balance_negative_mutual_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_mutual_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_firstproductoutput) = 2 * ge_signed_half_mutual_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_mutual_firstproductoutputimaginary) = S ge_signed_half_mutual_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))))))) + ge_balance_negative_mutual_firstproductoutputimaginary = (((((((ge_first_rp_mutual_firstproduct) * (ge_second_in_mutual_firstproduct))) + (((ge_first_rn_mutual_firstproduct) * (ge_second_ip_mutual_firstproduct))))) + (((((ge_first_ip_mutual_firstproduct) * (ge_second_rn_mutual_firstproduct))) + (((ge_first_in_mutual_firstproduct) * (ge_second_rp_mutual_firstproduct))))))) + ge_balance_positive_mutual_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_mutual_second. (exists ge_first_rp_mutual_secondproduct ge_first_rn_mutual_secondproduct ge_first_ip_mutual_secondproduct ge_first_in_mutual_secondproduct ge_second_rp_mutual_secondproduct ge_second_rn_mutual_secondproduct ge_second_ip_mutual_secondproduct ge_second_in_mutual_secondproduct. ((exists ge_representation_real_code_mutual_secondproductfirst ge_representation_imaginary_code_mutual_secondproductfirst. (((b) = ((ge_representation_real_code_mutual_secondproductfirst) + (ge_representation_imaginary_code_mutual_secondproductfirst)) * S ((ge_representation_real_code_mutual_secondproductfirst) + (ge_representation_imaginary_code_mutual_secondproductfirst)) + ((ge_representation_imaginary_code_mutual_secondproductfirst) + (ge_representation_imaginary_code_mutual_secondproductfirst))) /\ ((exists ge_balance_positive_mutual_secondproductfirstreal ge_balance_negative_mutual_secondproductfirstreal. (((((ge_representation_real_code_mutual_secondproductfirst) = 2 * (ge_balance_positive_mutual_secondproductfirstreal) /\ (ge_balance_negative_mutual_secondproductfirstreal) = 0) \/ exists ge_signed_half_mutual_secondproductfirstrealdecode. (((ge_representation_real_code_mutual_secondproductfirst) = 2 * ge_signed_half_mutual_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_mutual_secondproductfirstreal) = 0) /\ (ge_balance_negative_mutual_secondproductfirstreal) = S ge_signed_half_mutual_secondproductfirstrealdecode))) /\ ((ge_first_rp_mutual_secondproduct) + ge_balance_negative_mutual_secondproductfirstreal = (ge_first_rn_mutual_secondproduct) + ge_balance_positive_mutual_secondproductfirstreal))) /\ (exists ge_balance_positive_mutual_secondproductfirstimaginary ge_balance_negative_mutual_secondproductfirstimaginary. (((((ge_representation_imaginary_code_mutual_secondproductfirst) = 2 * (ge_balance_positive_mutual_secondproductfirstimaginary) /\ (ge_balance_negative_mutual_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_mutual_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_secondproductfirst) = 2 * ge_signed_half_mutual_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_mutual_secondproductfirstimaginary) = S ge_signed_half_mutual_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_mutual_secondproduct) + ge_balance_negative_mutual_secondproductfirstimaginary = (ge_first_in_mutual_secondproduct) + ge_balance_positive_mutual_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_secondproductsecond ge_representation_imaginary_code_mutual_secondproductsecond. (((gr_quotient_mutual_second) = ((ge_representation_real_code_mutual_secondproductsecond) + (ge_representation_imaginary_code_mutual_secondproductsecond)) * S ((ge_representation_real_code_mutual_secondproductsecond) + (ge_representation_imaginary_code_mutual_secondproductsecond)) + ((ge_representation_imaginary_code_mutual_secondproductsecond) + (ge_representation_imaginary_code_mutual_secondproductsecond))) /\ ((exists ge_balance_positive_mutual_secondproductsecondreal ge_balance_negative_mutual_secondproductsecondreal. (((((ge_representation_real_code_mutual_secondproductsecond) = 2 * (ge_balance_positive_mutual_secondproductsecondreal) /\ (ge_balance_negative_mutual_secondproductsecondreal) = 0) \/ exists ge_signed_half_mutual_secondproductsecondrealdecode. (((ge_representation_real_code_mutual_secondproductsecond) = 2 * ge_signed_half_mutual_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_mutual_secondproductsecondreal) = 0) /\ (ge_balance_negative_mutual_secondproductsecondreal) = S ge_signed_half_mutual_secondproductsecondrealdecode))) /\ ((ge_second_rp_mutual_secondproduct) + ge_balance_negative_mutual_secondproductsecondreal = (ge_second_rn_mutual_secondproduct) + ge_balance_positive_mutual_secondproductsecondreal))) /\ (exists ge_balance_positive_mutual_secondproductsecondimaginary ge_balance_negative_mutual_secondproductsecondimaginary. (((((ge_representation_imaginary_code_mutual_secondproductsecond) = 2 * (ge_balance_positive_mutual_secondproductsecondimaginary) /\ (ge_balance_negative_mutual_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_mutual_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_secondproductsecond) = 2 * ge_signed_half_mutual_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_mutual_secondproductsecondimaginary) = S ge_signed_half_mutual_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_mutual_secondproduct) + ge_balance_negative_mutual_secondproductsecondimaginary = (ge_second_in_mutual_secondproduct) + ge_balance_positive_mutual_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_secondproductoutput ge_representation_imaginary_code_mutual_secondproductoutput. (((a) = ((ge_representation_real_code_mutual_secondproductoutput) + (ge_representation_imaginary_code_mutual_secondproductoutput)) * S ((ge_representation_real_code_mutual_secondproductoutput) + (ge_representation_imaginary_code_mutual_secondproductoutput)) + ((ge_representation_imaginary_code_mutual_secondproductoutput) + (ge_representation_imaginary_code_mutual_secondproductoutput))) /\ ((exists ge_balance_positive_mutual_secondproductoutputreal ge_balance_negative_mutual_secondproductoutputreal. (((((ge_representation_real_code_mutual_secondproductoutput) = 2 * (ge_balance_positive_mutual_secondproductoutputreal) /\ (ge_balance_negative_mutual_secondproductoutputreal) = 0) \/ exists ge_signed_half_mutual_secondproductoutputrealdecode. (((ge_representation_real_code_mutual_secondproductoutput) = 2 * ge_signed_half_mutual_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_mutual_secondproductoutputreal) = 0) /\ (ge_balance_negative_mutual_secondproductoutputreal) = S ge_signed_half_mutual_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))))))) + ge_balance_negative_mutual_secondproductoutputreal = (((((((ge_first_rp_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))))))) + ge_balance_positive_mutual_secondproductoutputreal))) /\ (exists ge_balance_positive_mutual_secondproductoutputimaginary ge_balance_negative_mutual_secondproductoutputimaginary. (((((ge_representation_imaginary_code_mutual_secondproductoutput) = 2 * (ge_balance_positive_mutual_secondproductoutputimaginary) /\ (ge_balance_negative_mutual_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_mutual_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_secondproductoutput) = 2 * ge_signed_half_mutual_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_mutual_secondproductoutputimaginary) = S ge_signed_half_mutual_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))))))) + ge_balance_negative_mutual_secondproductoutputimaginary = (((((((ge_first_rp_mutual_secondproduct) * (ge_second_in_mutual_secondproduct))) + (((ge_first_rn_mutual_secondproduct) * (ge_second_ip_mutual_secondproduct))))) + (((((ge_first_ip_mutual_secondproduct) * (ge_second_rn_mutual_secondproduct))) + (((ge_first_in_mutual_secondproduct) * (ge_second_rp_mutual_secondproduct))))))) + ge_balance_positive_mutual_secondproductoutputimaginary)))))))))) -> (exists gr_unit_mutual_association. ((exists gr_inverse_mutual_associationunit. (exists ge_first_rp_mutual_associationunitidentity ge_first_rn_mutual_associationunitidentity ge_first_ip_mutual_associationunitidentity ge_first_in_mutual_associationunitidentity ge_second_rp_mutual_associationunitidentity ge_second_rn_mutual_associationunitidentity ge_second_ip_mutual_associationunitidentity ge_second_in_mutual_associationunitidentity. ((exists ge_representation_real_code_mutual_associationunitidentityfirst ge_representation_imaginary_code_mutual_associationunitidentityfirst. (((gr_unit_mutual_association) = ((ge_representation_real_code_mutual_associationunitidentityfirst) + (ge_representation_imaginary_code_mutual_associationunitidentityfirst)) * S ((ge_representation_real_code_mutual_associationunitidentityfirst) + (ge_representation_imaginary_code_mutual_associationunitidentityfirst)) + ((ge_representation_imaginary_code_mutual_associationunitidentityfirst) + (ge_representation_imaginary_code_mutual_associationunitidentityfirst))) /\ ((exists ge_balance_positive_mutual_associationunitidentityfirstreal ge_balance_negative_mutual_associationunitidentityfirstreal. (((((ge_representation_real_code_mutual_associationunitidentityfirst) = 2 * (ge_balance_positive_mutual_associationunitidentityfirstreal) /\ (ge_balance_negative_mutual_associationunitidentityfirstreal) = 0) \/ exists ge_signed_half_mutual_associationunitidentityfirstrealdecode. (((ge_representation_real_code_mutual_associationunitidentityfirst) = 2 * ge_signed_half_mutual_associationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityfirstreal) = 0) /\ (ge_balance_negative_mutual_associationunitidentityfirstreal) = S ge_signed_half_mutual_associationunitidentityfirstrealdecode))) /\ ((ge_first_rp_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentityfirstreal = (ge_first_rn_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentityfirstreal))) /\ (exists ge_balance_positive_mutual_associationunitidentityfirstimaginary ge_balance_negative_mutual_associationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_mutual_associationunitidentityfirst) = 2 * (ge_balance_positive_mutual_associationunitidentityfirstimaginary) /\ (ge_balance_negative_mutual_associationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_mutual_associationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_associationunitidentityfirst) = 2 * ge_signed_half_mutual_associationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_mutual_associationunitidentityfirstimaginary) = S ge_signed_half_mutual_associationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentityfirstimaginary = (ge_first_in_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_associationunitidentitysecond ge_representation_imaginary_code_mutual_associationunitidentitysecond. (((gr_inverse_mutual_associationunit) = ((ge_representation_real_code_mutual_associationunitidentitysecond) + (ge_representation_imaginary_code_mutual_associationunitidentitysecond)) * S ((ge_representation_real_code_mutual_associationunitidentitysecond) + (ge_representation_imaginary_code_mutual_associationunitidentitysecond)) + ((ge_representation_imaginary_code_mutual_associationunitidentitysecond) + (ge_representation_imaginary_code_mutual_associationunitidentitysecond))) /\ ((exists ge_balance_positive_mutual_associationunitidentitysecondreal ge_balance_negative_mutual_associationunitidentitysecondreal. (((((ge_representation_real_code_mutual_associationunitidentitysecond) = 2 * (ge_balance_positive_mutual_associationunitidentitysecondreal) /\ (ge_balance_negative_mutual_associationunitidentitysecondreal) = 0) \/ exists ge_signed_half_mutual_associationunitidentitysecondrealdecode. (((ge_representation_real_code_mutual_associationunitidentitysecond) = 2 * ge_signed_half_mutual_associationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_mutual_associationunitidentitysecondreal) = 0) /\ (ge_balance_negative_mutual_associationunitidentitysecondreal) = S ge_signed_half_mutual_associationunitidentitysecondrealdecode))) /\ ((ge_second_rp_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentitysecondreal = (ge_second_rn_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentitysecondreal))) /\ (exists ge_balance_positive_mutual_associationunitidentitysecondimaginary ge_balance_negative_mutual_associationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_mutual_associationunitidentitysecond) = 2 * (ge_balance_positive_mutual_associationunitidentitysecondimaginary) /\ (ge_balance_negative_mutual_associationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_mutual_associationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_mutual_associationunitidentitysecond) = 2 * ge_signed_half_mutual_associationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_mutual_associationunitidentitysecondimaginary) = S ge_signed_half_mutual_associationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_mutual_associationunitidentity) + ge_balance_negative_mutual_associationunitidentitysecondimaginary = (ge_second_in_mutual_associationunitidentity) + ge_balance_positive_mutual_associationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_associationunitidentityoutput ge_representation_imaginary_code_mutual_associationunitidentityoutput. (((6) = ((ge_representation_real_code_mutual_associationunitidentityoutput) + (ge_representation_imaginary_code_mutual_associationunitidentityoutput)) * S ((ge_representation_real_code_mutual_associationunitidentityoutput) + (ge_representation_imaginary_code_mutual_associationunitidentityoutput)) + ((ge_representation_imaginary_code_mutual_associationunitidentityoutput) + (ge_representation_imaginary_code_mutual_associationunitidentityoutput))) /\ ((exists ge_balance_positive_mutual_associationunitidentityoutputreal ge_balance_negative_mutual_associationunitidentityoutputreal. (((((ge_representation_real_code_mutual_associationunitidentityoutput) = 2 * (ge_balance_positive_mutual_associationunitidentityoutputreal) /\ (ge_balance_negative_mutual_associationunitidentityoutputreal) = 0) \/ exists ge_signed_half_mutual_associationunitidentityoutputrealdecode. (((ge_representation_real_code_mutual_associationunitidentityoutput) = 2 * ge_signed_half_mutual_associationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityoutputreal) = 0) /\ (ge_balance_negative_mutual_associationunitidentityoutputreal) = S ge_signed_half_mutual_associationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))))))) + ge_balance_negative_mutual_associationunitidentityoutputreal = (((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))))))) + ge_balance_positive_mutual_associationunitidentityoutputreal))) /\ (exists ge_balance_positive_mutual_associationunitidentityoutputimaginary ge_balance_negative_mutual_associationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_mutual_associationunitidentityoutput) = 2 * (ge_balance_positive_mutual_associationunitidentityoutputimaginary) /\ (ge_balance_negative_mutual_associationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_mutual_associationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_associationunitidentityoutput) = 2 * ge_signed_half_mutual_associationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_mutual_associationunitidentityoutputimaginary) = S ge_signed_half_mutual_associationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))))))) + ge_balance_negative_mutual_associationunitidentityoutputimaginary = (((((((ge_first_rp_mutual_associationunitidentity) * (ge_second_in_mutual_associationunitidentity))) + (((ge_first_rn_mutual_associationunitidentity) * (ge_second_ip_mutual_associationunitidentity))))) + (((((ge_first_ip_mutual_associationunitidentity) * (ge_second_rn_mutual_associationunitidentity))) + (((ge_first_in_mutual_associationunitidentity) * (ge_second_rp_mutual_associationunitidentity))))))) + ge_balance_positive_mutual_associationunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_mutual_associationtransport ge_first_rn_mutual_associationtransport ge_first_ip_mutual_associationtransport ge_first_in_mutual_associationtransport ge_second_rp_mutual_associationtransport ge_second_rn_mutual_associationtransport ge_second_ip_mutual_associationtransport ge_second_in_mutual_associationtransport. ((exists ge_representation_real_code_mutual_associationtransportfirst ge_representation_imaginary_code_mutual_associationtransportfirst. (((gr_unit_mutual_association) = ((ge_representation_real_code_mutual_associationtransportfirst) + (ge_representation_imaginary_code_mutual_associationtransportfirst)) * S ((ge_representation_real_code_mutual_associationtransportfirst) + (ge_representation_imaginary_code_mutual_associationtransportfirst)) + ((ge_representation_imaginary_code_mutual_associationtransportfirst) + (ge_representation_imaginary_code_mutual_associationtransportfirst))) /\ ((exists ge_balance_positive_mutual_associationtransportfirstreal ge_balance_negative_mutual_associationtransportfirstreal. (((((ge_representation_real_code_mutual_associationtransportfirst) = 2 * (ge_balance_positive_mutual_associationtransportfirstreal) /\ (ge_balance_negative_mutual_associationtransportfirstreal) = 0) \/ exists ge_signed_half_mutual_associationtransportfirstrealdecode. (((ge_representation_real_code_mutual_associationtransportfirst) = 2 * ge_signed_half_mutual_associationtransportfirstrealdecode + 1 /\ (ge_balance_positive_mutual_associationtransportfirstreal) = 0) /\ (ge_balance_negative_mutual_associationtransportfirstreal) = S ge_signed_half_mutual_associationtransportfirstrealdecode))) /\ ((ge_first_rp_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportfirstreal = (ge_first_rn_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportfirstreal))) /\ (exists ge_balance_positive_mutual_associationtransportfirstimaginary ge_balance_negative_mutual_associationtransportfirstimaginary. (((((ge_representation_imaginary_code_mutual_associationtransportfirst) = 2 * (ge_balance_positive_mutual_associationtransportfirstimaginary) /\ (ge_balance_negative_mutual_associationtransportfirstimaginary) = 0) \/ exists ge_signed_half_mutual_associationtransportfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_associationtransportfirst) = 2 * ge_signed_half_mutual_associationtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationtransportfirstimaginary) = 0) /\ (ge_balance_negative_mutual_associationtransportfirstimaginary) = S ge_signed_half_mutual_associationtransportfirstimaginarydecode))) /\ ((ge_first_ip_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportfirstimaginary = (ge_first_in_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_associationtransportsecond ge_representation_imaginary_code_mutual_associationtransportsecond. (((a) = ((ge_representation_real_code_mutual_associationtransportsecond) + (ge_representation_imaginary_code_mutual_associationtransportsecond)) * S ((ge_representation_real_code_mutual_associationtransportsecond) + (ge_representation_imaginary_code_mutual_associationtransportsecond)) + ((ge_representation_imaginary_code_mutual_associationtransportsecond) + (ge_representation_imaginary_code_mutual_associationtransportsecond))) /\ ((exists ge_balance_positive_mutual_associationtransportsecondreal ge_balance_negative_mutual_associationtransportsecondreal. (((((ge_representation_real_code_mutual_associationtransportsecond) = 2 * (ge_balance_positive_mutual_associationtransportsecondreal) /\ (ge_balance_negative_mutual_associationtransportsecondreal) = 0) \/ exists ge_signed_half_mutual_associationtransportsecondrealdecode. (((ge_representation_real_code_mutual_associationtransportsecond) = 2 * ge_signed_half_mutual_associationtransportsecondrealdecode + 1 /\ (ge_balance_positive_mutual_associationtransportsecondreal) = 0) /\ (ge_balance_negative_mutual_associationtransportsecondreal) = S ge_signed_half_mutual_associationtransportsecondrealdecode))) /\ ((ge_second_rp_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportsecondreal = (ge_second_rn_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportsecondreal))) /\ (exists ge_balance_positive_mutual_associationtransportsecondimaginary ge_balance_negative_mutual_associationtransportsecondimaginary. (((((ge_representation_imaginary_code_mutual_associationtransportsecond) = 2 * (ge_balance_positive_mutual_associationtransportsecondimaginary) /\ (ge_balance_negative_mutual_associationtransportsecondimaginary) = 0) \/ exists ge_signed_half_mutual_associationtransportsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_associationtransportsecond) = 2 * ge_signed_half_mutual_associationtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationtransportsecondimaginary) = 0) /\ (ge_balance_negative_mutual_associationtransportsecondimaginary) = S ge_signed_half_mutual_associationtransportsecondimaginarydecode))) /\ ((ge_second_ip_mutual_associationtransport) + ge_balance_negative_mutual_associationtransportsecondimaginary = (ge_second_in_mutual_associationtransport) + ge_balance_positive_mutual_associationtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_associationtransportoutput ge_representation_imaginary_code_mutual_associationtransportoutput. (((b) = ((ge_representation_real_code_mutual_associationtransportoutput) + (ge_representation_imaginary_code_mutual_associationtransportoutput)) * S ((ge_representation_real_code_mutual_associationtransportoutput) + (ge_representation_imaginary_code_mutual_associationtransportoutput)) + ((ge_representation_imaginary_code_mutual_associationtransportoutput) + (ge_representation_imaginary_code_mutual_associationtransportoutput))) /\ ((exists ge_balance_positive_mutual_associationtransportoutputreal ge_balance_negative_mutual_associationtransportoutputreal. (((((ge_representation_real_code_mutual_associationtransportoutput) = 2 * (ge_balance_positive_mutual_associationtransportoutputreal) /\ (ge_balance_negative_mutual_associationtransportoutputreal) = 0) \/ exists ge_signed_half_mutual_associationtransportoutputrealdecode. (((ge_representation_real_code_mutual_associationtransportoutput) = 2 * ge_signed_half_mutual_associationtransportoutputrealdecode + 1 /\ (ge_balance_positive_mutual_associationtransportoutputreal) = 0) /\ (ge_balance_negative_mutual_associationtransportoutputreal) = S ge_signed_half_mutual_associationtransportoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))))))) + ge_balance_negative_mutual_associationtransportoutputreal = (((((((ge_first_rp_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))))))) + ge_balance_positive_mutual_associationtransportoutputreal))) /\ (exists ge_balance_positive_mutual_associationtransportoutputimaginary ge_balance_negative_mutual_associationtransportoutputimaginary. (((((ge_representation_imaginary_code_mutual_associationtransportoutput) = 2 * (ge_balance_positive_mutual_associationtransportoutputimaginary) /\ (ge_balance_negative_mutual_associationtransportoutputimaginary) = 0) \/ exists ge_signed_half_mutual_associationtransportoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_associationtransportoutput) = 2 * ge_signed_half_mutual_associationtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_associationtransportoutputimaginary) = 0) /\ (ge_balance_negative_mutual_associationtransportoutputimaginary) = S ge_signed_half_mutual_associationtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))))))) + ge_balance_negative_mutual_associationtransportoutputimaginary = (((((((ge_first_rp_mutual_associationtransport) * (ge_second_in_mutual_associationtransport))) + (((ge_first_rn_mutual_associationtransport) * (ge_second_ip_mutual_associationtransport))))) + (((((ge_first_ip_mutual_associationtransport) * (ge_second_rn_mutual_associationtransport))) + (((ge_first_in_mutual_associationtransport) * (ge_second_rp_mutual_associationtransport))))))) + ge_balance_positive_mutual_associationtransportoutputimaginary)))))))))))Constructive proof overview
Generated structural guide
Mutual actual divisibility is witnessed association, with the all-zero case handled explicitly and the nonzero case using real multiplication cancellation.
The unchanged tactic script uses 13 declared prerequisites and contains 80 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
eq_decidable Stable theorem; checked-use authorized GF0047 gaussian_zero_divides_only_zero GF003D gaussian_one_unit GF0029 gaussian_multiply_one_left GF000C gaussian_zero_valid gaussian_multiply_exists Alpha theorem; checked-use authorized GF0008 gaussian_multiply_input_right_valid GF0007 gaussian_multiply_input_left_valid GF0025 gaussian_multiply_associative GF003B gaussian_multiply_cancel_left GF0028 gaussian_multiply_one_right GF002F gaussian_multiply_output_transport GF0014 gaussian_multiply_commutativeDirect dependents
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
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 (11)
gaussian zero divides only zerogaussian one unitgaussian multiply one leftgaussian zero validgaussian multiply input right validgaussian multiply input left validgaussian multiply associativegaussian multiply cancel leftgaussian multiply one rightgaussian multiply output transportgaussian multiply commutative
01Fix variables and assumptionsL1–4
02Establish haL5–8
03Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
cases ha
04Establish hbL10–14
05Construct an explicit witnessL15–15
Supply the displayed value, then prove that it has the required property.
- L15
exists (6)
06Separate the logical casesL16–16
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L16
split
07Use earlier factsL17–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
exact gaussian_one_unit
08Calculate and transport equalitiesL18–19
09Use earlier factsL20–22
10Separate the logical casesL23–24
11Establish hqL25–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply exists.
- L25
have hq : ∃ q. GMul(x,x1,q)Definitions: GMul - L26
specialize gaussian_multiply_exists (x) - L27
specialize gaussian_multiply_exists (x1) - L28
apply gaussian_multiply_exists - L29
specialize gaussian_multiply_input_right_valid (a) - L30
specialize gaussian_multiply_input_right_valid (x) - L31
specialize gaussian_multiply_input_right_valid (b) - L32
apply gaussian_multiply_input_right_valid - L33
exact hA_witness - L34
specialize gaussian_multiply_input_right_valid (b)
12Use earlier factsL35–38
13Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
cases hq
14Establish hselfL40–49
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply associative.
- L40
have hself : GMul(a,x2,a)Definitions: GMul - L41
specialize gaussian_multiply_associative (a) - L42
specialize gaussian_multiply_associative (x) - L43
specialize gaussian_multiply_associative (x1) - L44
specialize gaussian_multiply_associative (b) - L45
specialize gaussian_multiply_associative (x2) - L46
specialize gaussian_multiply_associative (a) - L47
apply gaussian_multiply_associative - L48
exact hA_witness - L49
exact hB_witness
15Use earlier factsL50–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L50
exact hq_witness
16Establish heqL51–60
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply cancel left.
- L51
have heq : x2=6 - L52
specialize gaussian_multiply_cancel_left (a) - L53
specialize gaussian_multiply_cancel_left (x2) - L54
specialize gaussian_multiply_cancel_left (6) - L55
specialize gaussian_multiply_cancel_left (a) - L56
apply gaussian_multiply_cancel_left - L57
exact ha_right - L58
exact hself - L59
specialize gaussian_multiply_one_right (a) - L60
apply gaussian_multiply_one_right
17Use earlier factsL61–65
Instantiate or apply named facts and discharge the corresponding proof obligations.
18Construct an explicit witnessL66–66
Supply the displayed value, then prove that it has the required property.
- L66
exists (x)
19Separate the logical casesL67–67
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L67
split
20Construct an explicit witnessL68–68
Supply the displayed value, then prove that it has the required property.
- L68
exists (x1)
21Use earlier factsL69–78
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L69
specialize gaussian_multiply_output_transport (x) - L70
specialize gaussian_multiply_output_transport (x1) - L71
specialize gaussian_multiply_output_transport (x2) - L72
specialize gaussian_multiply_output_transport (6) - L73
apply gaussian_multiply_output_transport - L74
exact heq - L75
exact hq_witness - L76
specialize gaussian_multiply_commutative (a) - L77
specialize gaussian_multiply_commutative (x) - L78
specialize gaussian_multiply_commutative (b)
Original exact command ledger · 80 lines
- 0001
intro a - 0002
intro b - 0003
intro hA - 0004
intro hB - 0005
have ha : a=0 \/ ~(a=0) - 0006
specialize eq_decidable (a) - 0007
specialize eq_decidable (0) - 0008
apply eq_decidable - 0009
cases ha - 0010
have hb : b=0 - 0011
specialize gaussian_zero_divides_only_zero (b) - 0012
apply gaussian_zero_divides_only_zero - 0013
rewrite ha_left at hA - 0014
exact hA - 0015
exists (6) - 0016
split - 0017
exact gaussian_one_unit - 0018
rewrite ha_left - 0019
rewrite hb - 0020
specialize gaussian_multiply_one_left (0) - 0021
apply gaussian_multiply_one_left - 0022
exact gaussian_zero_valid - 0023
cases hA - 0024
cases hB - 0025
have hq : exists q. (exists ge_first_rp_mutual_quotient_product ge_first_rn_mutual_quotient_product ge_first_ip_mutual_quotient_product ge_first_in_mutual_quotient_product ge_second_rp_mutual_quotient_product ge_second_rn_mutual_quotient_product ge_second_ip_mutual_quotient_product ge_second_in_mutual_quotient_product. ((exists ge_representation_real_code_mutual_quotient_productfirst ge_representation_imaginary_code_mutual_quotient_productfirst. (((x) = ((ge_representation_real_code_mutual_quotient_productfirst) + (ge_representation_imaginary_code_mutual_quotient_productfirst)) * S ((ge_representation_real_code_mutual_quotient_productfirst) + (ge_representation_imaginary_code_mutual_quotient_productfirst)) + ((ge_representation_imaginary_code_mutual_quotient_productfirst) + (ge_representation_imaginary_code_mutual_quotient_productfirst))) /\ ((exists ge_balance_positive_mutual_quotient_productfirstreal ge_balance_negative_mutual_quotient_productfirstreal. (((((ge_representation_real_code_mutual_quotient_productfirst) = 2 * (ge_balance_positive_mutual_quotient_productfirstreal) /\ (ge_balance_negative_mutual_quotient_productfirstreal) = 0) \/ exists ge_signed_half_mutual_quotient_productfirstrealdecode. (((ge_representation_real_code_mutual_quotient_productfirst) = 2 * ge_signed_half_mutual_quotient_productfirstrealdecode + 1 /\ (ge_balance_positive_mutual_quotient_productfirstreal) = 0) /\ (ge_balance_negative_mutual_quotient_productfirstreal) = S ge_signed_half_mutual_quotient_productfirstrealdecode))) /\ ((ge_first_rp_mutual_quotient_product) + ge_balance_negative_mutual_quotient_productfirstreal = (ge_first_rn_mutual_quotient_product) + ge_balance_positive_mutual_quotient_productfirstreal))) /\ (exists ge_balance_positive_mutual_quotient_productfirstimaginary ge_balance_negative_mutual_quotient_productfirstimaginary. (((((ge_representation_imaginary_code_mutual_quotient_productfirst) = 2 * (ge_balance_positive_mutual_quotient_productfirstimaginary) /\ (ge_balance_negative_mutual_quotient_productfirstimaginary) = 0) \/ exists ge_signed_half_mutual_quotient_productfirstimaginarydecode. (((ge_representation_imaginary_code_mutual_quotient_productfirst) = 2 * ge_signed_half_mutual_quotient_productfirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_quotient_productfirstimaginary) = 0) /\ (ge_balance_negative_mutual_quotient_productfirstimaginary) = S ge_signed_half_mutual_quotient_productfirstimaginarydecode))) /\ ((ge_first_ip_mutual_quotient_product) + ge_balance_negative_mutual_quotient_productfirstimaginary = (ge_first_in_mutual_quotient_product) + ge_balance_positive_mutual_quotient_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_quotient_productsecond ge_representation_imaginary_code_mutual_quotient_productsecond. (((x1) = ((ge_representation_real_code_mutual_quotient_productsecond) + (ge_representation_imaginary_code_mutual_quotient_productsecond)) * S ((ge_representation_real_code_mutual_quotient_productsecond) + (ge_representation_imaginary_code_mutual_quotient_productsecond)) + ((ge_representation_imaginary_code_mutual_quotient_productsecond) + (ge_representation_imaginary_code_mutual_quotient_productsecond))) /\ ((exists ge_balance_positive_mutual_quotient_productsecondreal ge_balance_negative_mutual_quotient_productsecondreal. (((((ge_representation_real_code_mutual_quotient_productsecond) = 2 * (ge_balance_positive_mutual_quotient_productsecondreal) /\ (ge_balance_negative_mutual_quotient_productsecondreal) = 0) \/ exists ge_signed_half_mutual_quotient_productsecondrealdecode. (((ge_representation_real_code_mutual_quotient_productsecond) = 2 * ge_signed_half_mutual_quotient_productsecondrealdecode + 1 /\ (ge_balance_positive_mutual_quotient_productsecondreal) = 0) /\ (ge_balance_negative_mutual_quotient_productsecondreal) = S ge_signed_half_mutual_quotient_productsecondrealdecode))) /\ ((ge_second_rp_mutual_quotient_product) + ge_balance_negative_mutual_quotient_productsecondreal = (ge_second_rn_mutual_quotient_product) + ge_balance_positive_mutual_quotient_productsecondreal))) /\ (exists ge_balance_positive_mutual_quotient_productsecondimaginary ge_balance_negative_mutual_quotient_productsecondimaginary. (((((ge_representation_imaginary_code_mutual_quotient_productsecond) = 2 * (ge_balance_positive_mutual_quotient_productsecondimaginary) /\ (ge_balance_negative_mutual_quotient_productsecondimaginary) = 0) \/ exists ge_signed_half_mutual_quotient_productsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_quotient_productsecond) = 2 * ge_signed_half_mutual_quotient_productsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_quotient_productsecondimaginary) = 0) /\ (ge_balance_negative_mutual_quotient_productsecondimaginary) = S ge_signed_half_mutual_quotient_productsecondimaginarydecode))) /\ ((ge_second_ip_mutual_quotient_product) + ge_balance_negative_mutual_quotient_productsecondimaginary = (ge_second_in_mutual_quotient_product) + ge_balance_positive_mutual_quotient_productsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_quotient_productoutput ge_representation_imaginary_code_mutual_quotient_productoutput. (((q) = ((ge_representation_real_code_mutual_quotient_productoutput) + (ge_representation_imaginary_code_mutual_quotient_productoutput)) * S ((ge_representation_real_code_mutual_quotient_productoutput) + (ge_representation_imaginary_code_mutual_quotient_productoutput)) + ((ge_representation_imaginary_code_mutual_quotient_productoutput) + (ge_representation_imaginary_code_mutual_quotient_productoutput))) /\ ((exists ge_balance_positive_mutual_quotient_productoutputreal ge_balance_negative_mutual_quotient_productoutputreal. (((((ge_representation_real_code_mutual_quotient_productoutput) = 2 * (ge_balance_positive_mutual_quotient_productoutputreal) /\ (ge_balance_negative_mutual_quotient_productoutputreal) = 0) \/ exists ge_signed_half_mutual_quotient_productoutputrealdecode. (((ge_representation_real_code_mutual_quotient_productoutput) = 2 * ge_signed_half_mutual_quotient_productoutputrealdecode + 1 /\ (ge_balance_positive_mutual_quotient_productoutputreal) = 0) /\ (ge_balance_negative_mutual_quotient_productoutputreal) = S ge_signed_half_mutual_quotient_productoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_quotient_product) * (ge_second_rp_mutual_quotient_product))) + (((ge_first_rn_mutual_quotient_product) * (ge_second_rn_mutual_quotient_product))))) + (((((ge_first_ip_mutual_quotient_product) * (ge_second_in_mutual_quotient_product))) + (((ge_first_in_mutual_quotient_product) * (ge_second_ip_mutual_quotient_product))))))) + ge_balance_negative_mutual_quotient_productoutputreal = (((((((ge_first_rp_mutual_quotient_product) * (ge_second_rn_mutual_quotient_product))) + (((ge_first_rn_mutual_quotient_product) * (ge_second_rp_mutual_quotient_product))))) + (((((ge_first_ip_mutual_quotient_product) * (ge_second_ip_mutual_quotient_product))) + (((ge_first_in_mutual_quotient_product) * (ge_second_in_mutual_quotient_product))))))) + ge_balance_positive_mutual_quotient_productoutputreal))) /\ (exists ge_balance_positive_mutual_quotient_productoutputimaginary ge_balance_negative_mutual_quotient_productoutputimaginary. (((((ge_representation_imaginary_code_mutual_quotient_productoutput) = 2 * (ge_balance_positive_mutual_quotient_productoutputimaginary) /\ (ge_balance_negative_mutual_quotient_productoutputimaginary) = 0) \/ exists ge_signed_half_mutual_quotient_productoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_quotient_productoutput) = 2 * ge_signed_half_mutual_quotient_productoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_quotient_productoutputimaginary) = 0) /\ (ge_balance_negative_mutual_quotient_productoutputimaginary) = S ge_signed_half_mutual_quotient_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_quotient_product) * (ge_second_ip_mutual_quotient_product))) + (((ge_first_rn_mutual_quotient_product) * (ge_second_in_mutual_quotient_product))))) + (((((ge_first_ip_mutual_quotient_product) * (ge_second_rp_mutual_quotient_product))) + (((ge_first_in_mutual_quotient_product) * (ge_second_rn_mutual_quotient_product))))))) + ge_balance_negative_mutual_quotient_productoutputimaginary = (((((((ge_first_rp_mutual_quotient_product) * (ge_second_in_mutual_quotient_product))) + (((ge_first_rn_mutual_quotient_product) * (ge_second_ip_mutual_quotient_product))))) + (((((ge_first_ip_mutual_quotient_product) * (ge_second_rn_mutual_quotient_product))) + (((ge_first_in_mutual_quotient_product) * (ge_second_rp_mutual_quotient_product))))))) + ge_balance_positive_mutual_quotient_productoutputimaginary))))))))) - 0026
specialize gaussian_multiply_exists (x) - 0027
specialize gaussian_multiply_exists (x1) - 0028
apply gaussian_multiply_exists - 0029
specialize gaussian_multiply_input_right_valid (a) - 0030
specialize gaussian_multiply_input_right_valid (x) - 0031
specialize gaussian_multiply_input_right_valid (b) - 0032
apply gaussian_multiply_input_right_valid - 0033
exact hA_witness - 0034
specialize gaussian_multiply_input_right_valid (b) - 0035
specialize gaussian_multiply_input_right_valid (x1) - 0036
specialize gaussian_multiply_input_right_valid (a) - 0037
apply gaussian_multiply_input_right_valid - 0038
exact hB_witness - 0039
cases hq - 0040
have hself : exists ge_first_rp_mutual_self ge_first_rn_mutual_self ge_first_ip_mutual_self ge_first_in_mutual_self ge_second_rp_mutual_self ge_second_rn_mutual_self ge_second_ip_mutual_self ge_second_in_mutual_self. ((exists ge_representation_real_code_mutual_selffirst ge_representation_imaginary_code_mutual_selffirst. (((a) = ((ge_representation_real_code_mutual_selffirst) + (ge_representation_imaginary_code_mutual_selffirst)) * S ((ge_representation_real_code_mutual_selffirst) + (ge_representation_imaginary_code_mutual_selffirst)) + ((ge_representation_imaginary_code_mutual_selffirst) + (ge_representation_imaginary_code_mutual_selffirst))) /\ ((exists ge_balance_positive_mutual_selffirstreal ge_balance_negative_mutual_selffirstreal. (((((ge_representation_real_code_mutual_selffirst) = 2 * (ge_balance_positive_mutual_selffirstreal) /\ (ge_balance_negative_mutual_selffirstreal) = 0) \/ exists ge_signed_half_mutual_selffirstrealdecode. (((ge_representation_real_code_mutual_selffirst) = 2 * ge_signed_half_mutual_selffirstrealdecode + 1 /\ (ge_balance_positive_mutual_selffirstreal) = 0) /\ (ge_balance_negative_mutual_selffirstreal) = S ge_signed_half_mutual_selffirstrealdecode))) /\ ((ge_first_rp_mutual_self) + ge_balance_negative_mutual_selffirstreal = (ge_first_rn_mutual_self) + ge_balance_positive_mutual_selffirstreal))) /\ (exists ge_balance_positive_mutual_selffirstimaginary ge_balance_negative_mutual_selffirstimaginary. (((((ge_representation_imaginary_code_mutual_selffirst) = 2 * (ge_balance_positive_mutual_selffirstimaginary) /\ (ge_balance_negative_mutual_selffirstimaginary) = 0) \/ exists ge_signed_half_mutual_selffirstimaginarydecode. (((ge_representation_imaginary_code_mutual_selffirst) = 2 * ge_signed_half_mutual_selffirstimaginarydecode + 1 /\ (ge_balance_positive_mutual_selffirstimaginary) = 0) /\ (ge_balance_negative_mutual_selffirstimaginary) = S ge_signed_half_mutual_selffirstimaginarydecode))) /\ ((ge_first_ip_mutual_self) + ge_balance_negative_mutual_selffirstimaginary = (ge_first_in_mutual_self) + ge_balance_positive_mutual_selffirstimaginary)))))) /\ ((exists ge_representation_real_code_mutual_selfsecond ge_representation_imaginary_code_mutual_selfsecond. (((x2) = ((ge_representation_real_code_mutual_selfsecond) + (ge_representation_imaginary_code_mutual_selfsecond)) * S ((ge_representation_real_code_mutual_selfsecond) + (ge_representation_imaginary_code_mutual_selfsecond)) + ((ge_representation_imaginary_code_mutual_selfsecond) + (ge_representation_imaginary_code_mutual_selfsecond))) /\ ((exists ge_balance_positive_mutual_selfsecondreal ge_balance_negative_mutual_selfsecondreal. (((((ge_representation_real_code_mutual_selfsecond) = 2 * (ge_balance_positive_mutual_selfsecondreal) /\ (ge_balance_negative_mutual_selfsecondreal) = 0) \/ exists ge_signed_half_mutual_selfsecondrealdecode. (((ge_representation_real_code_mutual_selfsecond) = 2 * ge_signed_half_mutual_selfsecondrealdecode + 1 /\ (ge_balance_positive_mutual_selfsecondreal) = 0) /\ (ge_balance_negative_mutual_selfsecondreal) = S ge_signed_half_mutual_selfsecondrealdecode))) /\ ((ge_second_rp_mutual_self) + ge_balance_negative_mutual_selfsecondreal = (ge_second_rn_mutual_self) + ge_balance_positive_mutual_selfsecondreal))) /\ (exists ge_balance_positive_mutual_selfsecondimaginary ge_balance_negative_mutual_selfsecondimaginary. (((((ge_representation_imaginary_code_mutual_selfsecond) = 2 * (ge_balance_positive_mutual_selfsecondimaginary) /\ (ge_balance_negative_mutual_selfsecondimaginary) = 0) \/ exists ge_signed_half_mutual_selfsecondimaginarydecode. (((ge_representation_imaginary_code_mutual_selfsecond) = 2 * ge_signed_half_mutual_selfsecondimaginarydecode + 1 /\ (ge_balance_positive_mutual_selfsecondimaginary) = 0) /\ (ge_balance_negative_mutual_selfsecondimaginary) = S ge_signed_half_mutual_selfsecondimaginarydecode))) /\ ((ge_second_ip_mutual_self) + ge_balance_negative_mutual_selfsecondimaginary = (ge_second_in_mutual_self) + ge_balance_positive_mutual_selfsecondimaginary)))))) /\ (exists ge_representation_real_code_mutual_selfoutput ge_representation_imaginary_code_mutual_selfoutput. (((a) = ((ge_representation_real_code_mutual_selfoutput) + (ge_representation_imaginary_code_mutual_selfoutput)) * S ((ge_representation_real_code_mutual_selfoutput) + (ge_representation_imaginary_code_mutual_selfoutput)) + ((ge_representation_imaginary_code_mutual_selfoutput) + (ge_representation_imaginary_code_mutual_selfoutput))) /\ ((exists ge_balance_positive_mutual_selfoutputreal ge_balance_negative_mutual_selfoutputreal. (((((ge_representation_real_code_mutual_selfoutput) = 2 * (ge_balance_positive_mutual_selfoutputreal) /\ (ge_balance_negative_mutual_selfoutputreal) = 0) \/ exists ge_signed_half_mutual_selfoutputrealdecode. (((ge_representation_real_code_mutual_selfoutput) = 2 * ge_signed_half_mutual_selfoutputrealdecode + 1 /\ (ge_balance_positive_mutual_selfoutputreal) = 0) /\ (ge_balance_negative_mutual_selfoutputreal) = S ge_signed_half_mutual_selfoutputrealdecode))) /\ ((((((((ge_first_rp_mutual_self) * (ge_second_rp_mutual_self))) + (((ge_first_rn_mutual_self) * (ge_second_rn_mutual_self))))) + (((((ge_first_ip_mutual_self) * (ge_second_in_mutual_self))) + (((ge_first_in_mutual_self) * (ge_second_ip_mutual_self))))))) + ge_balance_negative_mutual_selfoutputreal = (((((((ge_first_rp_mutual_self) * (ge_second_rn_mutual_self))) + (((ge_first_rn_mutual_self) * (ge_second_rp_mutual_self))))) + (((((ge_first_ip_mutual_self) * (ge_second_ip_mutual_self))) + (((ge_first_in_mutual_self) * (ge_second_in_mutual_self))))))) + ge_balance_positive_mutual_selfoutputreal))) /\ (exists ge_balance_positive_mutual_selfoutputimaginary ge_balance_negative_mutual_selfoutputimaginary. (((((ge_representation_imaginary_code_mutual_selfoutput) = 2 * (ge_balance_positive_mutual_selfoutputimaginary) /\ (ge_balance_negative_mutual_selfoutputimaginary) = 0) \/ exists ge_signed_half_mutual_selfoutputimaginarydecode. (((ge_representation_imaginary_code_mutual_selfoutput) = 2 * ge_signed_half_mutual_selfoutputimaginarydecode + 1 /\ (ge_balance_positive_mutual_selfoutputimaginary) = 0) /\ (ge_balance_negative_mutual_selfoutputimaginary) = S ge_signed_half_mutual_selfoutputimaginarydecode))) /\ ((((((((ge_first_rp_mutual_self) * (ge_second_ip_mutual_self))) + (((ge_first_rn_mutual_self) * (ge_second_in_mutual_self))))) + (((((ge_first_ip_mutual_self) * (ge_second_rp_mutual_self))) + (((ge_first_in_mutual_self) * (ge_second_rn_mutual_self))))))) + ge_balance_negative_mutual_selfoutputimaginary = (((((((ge_first_rp_mutual_self) * (ge_second_in_mutual_self))) + (((ge_first_rn_mutual_self) * (ge_second_ip_mutual_self))))) + (((((ge_first_ip_mutual_self) * (ge_second_rn_mutual_self))) + (((ge_first_in_mutual_self) * (ge_second_rp_mutual_self))))))) + ge_balance_positive_mutual_selfoutputimaginary)))))))) - 0041
specialize gaussian_multiply_associative (a) - 0042
specialize gaussian_multiply_associative (x) - 0043
specialize gaussian_multiply_associative (x1) - 0044
specialize gaussian_multiply_associative (b) - 0045
specialize gaussian_multiply_associative (x2) - 0046
specialize gaussian_multiply_associative (a) - 0047
apply gaussian_multiply_associative - 0048
exact hA_witness - 0049
exact hB_witness - 0050
exact hq_witness - 0051
have heq : x2=6 - 0052
specialize gaussian_multiply_cancel_left (a) - 0053
specialize gaussian_multiply_cancel_left (x2) - 0054
specialize gaussian_multiply_cancel_left (6) - 0055
specialize gaussian_multiply_cancel_left (a) - 0056
apply gaussian_multiply_cancel_left - 0057
exact ha_right - 0058
exact hself - 0059
specialize gaussian_multiply_one_right (a) - 0060
apply gaussian_multiply_one_right - 0061
specialize gaussian_multiply_input_left_valid (a) - 0062
specialize gaussian_multiply_input_left_valid (x) - 0063
specialize gaussian_multiply_input_left_valid (b) - 0064
apply gaussian_multiply_input_left_valid - 0065
exact hA_witness - 0066
exists (x) - 0067
split - 0068
exists (x1) - 0069
specialize gaussian_multiply_output_transport (x) - 0070
specialize gaussian_multiply_output_transport (x1) - 0071
specialize gaussian_multiply_output_transport (x2) - 0072
specialize gaussian_multiply_output_transport (6) - 0073
apply gaussian_multiply_output_transport - 0074
exact heq - 0075
exact hq_witness - 0076
specialize gaussian_multiply_commutative (a) - 0077
specialize gaussian_multiply_commutative (x) - 0078
specialize gaussian_multiply_commutative (b) - 0079
apply gaussian_multiply_commutative - 0080
exact hA_witness