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 h z N k. (exists ge_real_positive_rectangle_target ge_real_negative_rectangle_target ge_imaginary_positive_rectangle_target ge_imaginary_negative_rectangle_target. (exists ge_real_code_rectangle_targetdecode ge_imaginary_code_rectangle_targetdecode. (((z) = ((ge_real_code_rectangle_targetdecode) + (ge_imaginary_code_rectangle_targetdecode)) * S ((ge_real_code_rectangle_targetdecode) + (ge_imaginary_code_rectangle_targetdecode)) + ((ge_imaginary_code_rectangle_targetdecode) + (ge_imaginary_code_rectangle_targetdecode))) /\ (((((ge_real_code_rectangle_targetdecode) = 2 * (ge_real_positive_rectangle_target) /\ (ge_real_negative_rectangle_target) = 0) \/ exists ge_signed_half_ge_rectangle_targetdecode_real. (((ge_real_code_rectangle_targetdecode) = 2 * ge_signed_half_ge_rectangle_targetdecode_real + 1 /\ (ge_real_positive_rectangle_target) = 0) /\ (ge_real_negative_rectangle_target) = S ge_signed_half_ge_rectangle_targetdecode_real))) /\ ((((ge_imaginary_code_rectangle_targetdecode) = 2 * (ge_imaginary_positive_rectangle_target) /\ (ge_imaginary_negative_rectangle_target) = 0) \/ exists ge_signed_half_ge_rectangle_targetdecode_imaginary. (((ge_imaginary_code_rectangle_targetdecode) = 2 * ge_signed_half_ge_rectangle_targetdecode_imaginary + 1 /\ (ge_imaginary_positive_rectangle_target) = 0) /\ (ge_imaginary_negative_rectangle_target) = S ge_signed_half_ge_rectangle_targetdecode_imaginary))))))) -> ((exists gr_rectangle_real_rectangle_scan gr_rectangle_imaginary_rectangle_scan. ((exists ge_gap_rectangle_scanfound_real. ge_gap_rectangle_scanfound_real + S (gr_rectangle_real_rectangle_scan) = (h)) /\ ((exists ge_gap_rectangle_scanfound_imaginary. ge_gap_rectangle_scanfound_imaginary + S (gr_rectangle_imaginary_rectangle_scan) = (k)) /\ (((~(exists gr_inverse_rectangle_scanfoundnonunit. (exists ge_first_rp_rectangle_scanfoundnonunitidentity ge_first_rn_rectangle_scanfoundnonunitidentity ge_first_ip_rectangle_scanfoundnonunitidentity ge_first_in_rectangle_scanfoundnonunitidentity ge_second_rp_rectangle_scanfoundnonunitidentity ge_second_rn_rectangle_scanfoundnonunitidentity ge_second_ip_rectangle_scanfoundnonunitidentity ge_second_in_rectangle_scanfoundnonunitidentity. ((exists ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_scanfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal) = S ge_signed_half_rectangle_scanfoundnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentityfirstreal = (ge_first_rn_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_scanfoundnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentityfirstimaginary = (ge_first_in_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond. (((gr_inverse_rectangle_scanfoundnonunit) = ((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_scanfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal) = S ge_signed_half_rectangle_scanfoundnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentitysecondreal = (ge_second_rn_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_scanfoundnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanfoundnonunitidentity) + ge_balance_negative_rectangle_scanfoundnonunitidentitysecondimaginary = (ge_second_in_rectangle_scanfoundnonunitidentity) + ge_balance_positive_rectangle_scanfoundnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_scanfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal) = S ge_signed_half_rectangle_scanfoundnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))))))) + ge_balance_negative_rectangle_scanfoundnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))))))) + ge_balance_positive_rectangle_scanfoundnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanfoundnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_scanfoundnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))))))) + ge_balance_negative_rectangle_scanfoundnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_scanfoundnonunitidentity) * (ge_second_in_rectangle_scanfoundnonunitidentity))) + (((ge_first_rn_rectangle_scanfoundnonunitidentity) * (ge_second_ip_rectangle_scanfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_scanfoundnonunitidentity) * (ge_second_rn_rectangle_scanfoundnonunitidentity))) + (((ge_first_in_rectangle_scanfoundnonunitidentity) * (ge_second_rp_rectangle_scanfoundnonunitidentity))))))) + ge_balance_positive_rectangle_scanfoundnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_scanfoundquotient. (exists ge_first_rp_rectangle_scanfoundquotientproduct ge_first_rn_rectangle_scanfoundquotientproduct ge_first_ip_rectangle_scanfoundquotientproduct ge_first_in_rectangle_scanfoundquotientproduct ge_second_rp_rectangle_scanfoundquotientproduct ge_second_rn_rectangle_scanfoundquotientproduct ge_second_ip_rectangle_scanfoundquotientproduct ge_second_in_rectangle_scanfoundquotientproduct. ((exists ge_representation_real_code_rectangle_scanfoundquotientproductfirst ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst)) * S ((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_scanfoundquotientproductfirstreal ge_balance_negative_rectangle_scanfoundquotientproductfirstreal. (((((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductfirstreal) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_scanfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_scanfoundquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstreal) = S ge_signed_half_rectangle_scanfoundquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductfirstreal = (ge_first_rn_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_scanfoundquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary) = S ge_signed_half_rectangle_scanfoundquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductfirstimaginary = (ge_first_in_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanfoundquotientproductsecond ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond. (((gr_quotient_rectangle_scanfoundquotient) = ((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond)) * S ((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_scanfoundquotientproductsecondreal ge_balance_negative_rectangle_scanfoundquotientproductsecondreal. (((((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductsecondreal) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_scanfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_scanfoundquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondreal) = S ge_signed_half_rectangle_scanfoundquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductsecondreal = (ge_second_rn_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_scanfoundquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary) = S ge_signed_half_rectangle_scanfoundquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanfoundquotientproduct) + ge_balance_negative_rectangle_scanfoundquotientproductsecondimaginary = (ge_second_in_rectangle_scanfoundquotientproduct) + ge_balance_positive_rectangle_scanfoundquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanfoundquotientproductoutput ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput)) * S ((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_scanfoundquotientproductoutputreal ge_balance_negative_rectangle_scanfoundquotientproductoutputreal. (((((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductoutputreal) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_scanfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_scanfoundquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputreal) = S ge_signed_half_rectangle_scanfoundquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))))))) + ge_balance_negative_rectangle_scanfoundquotientproductoutputreal = (((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))))))) + ge_balance_positive_rectangle_scanfoundquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_scanfoundquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary) = S ge_signed_half_rectangle_scanfoundquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))))))) + ge_balance_negative_rectangle_scanfoundquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_scanfoundquotientproduct) * (ge_second_in_rectangle_scanfoundquotientproduct))) + (((ge_first_rn_rectangle_scanfoundquotientproduct) * (ge_second_ip_rectangle_scanfoundquotientproduct))))) + (((((ge_first_ip_rectangle_scanfoundquotientproduct) * (ge_second_rn_rectangle_scanfoundquotientproduct))) + (((ge_first_in_rectangle_scanfoundquotientproduct) * (ge_second_rp_rectangle_scanfoundquotientproduct))))))) + ge_balance_positive_rectangle_scanfoundquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_scanfound. ((exists ge_norm_rp_rectangle_scanfoundnorm ge_norm_rn_rectangle_scanfoundnorm ge_norm_ip_rectangle_scanfoundnorm ge_norm_in_rectangle_scanfoundnorm. ((exists ge_representation_real_code_rectangle_scanfoundnormrepresentation ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation)) * S ((ge_representation_real_code_rectangle_scanfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_scanfoundnormrepresentationreal ge_balance_negative_rectangle_scanfoundnormrepresentationreal. (((((ge_representation_real_code_rectangle_scanfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanfoundnormrepresentationreal) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_scanfoundnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_scanfoundnormrepresentation) = 2 * ge_signed_half_rectangle_scanfoundnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationreal) = S ge_signed_half_rectangle_scanfoundnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_scanfoundnorm) + ge_balance_negative_rectangle_scanfoundnormrepresentationreal = (ge_norm_rn_rectangle_scanfoundnorm) + ge_balance_positive_rectangle_scanfoundnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_scanfoundnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanfoundnormrepresentation) = 2 * ge_signed_half_rectangle_scanfoundnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary) = S ge_signed_half_rectangle_scanfoundnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_scanfoundnorm) + ge_balance_negative_rectangle_scanfoundnormrepresentationimaginary = (ge_norm_in_rectangle_scanfoundnorm) + ge_balance_positive_rectangle_scanfoundnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_scanfoundnormsquare ge_imaginary_square_rectangle_scanfoundnormsquare. ((((((ge_norm_rp_rectangle_scanfoundnorm) * (ge_norm_rp_rectangle_scanfoundnorm))) + (((ge_norm_rn_rectangle_scanfoundnorm) * (ge_norm_rn_rectangle_scanfoundnorm)))) = ((ge_real_square_rectangle_scanfoundnormsquare) + (((((ge_norm_rp_rectangle_scanfoundnorm) * (ge_norm_rn_rectangle_scanfoundnorm))) + (((ge_norm_rn_rectangle_scanfoundnorm) * (ge_norm_rp_rectangle_scanfoundnorm))))))) /\ ((((((ge_norm_ip_rectangle_scanfoundnorm) * (ge_norm_ip_rectangle_scanfoundnorm))) + (((ge_norm_in_rectangle_scanfoundnorm) * (ge_norm_in_rectangle_scanfoundnorm)))) = ((ge_imaginary_square_rectangle_scanfoundnormsquare) + (((((ge_norm_ip_rectangle_scanfoundnorm) * (ge_norm_in_rectangle_scanfoundnorm))) + (((ge_norm_in_rectangle_scanfoundnorm) * (ge_norm_ip_rectangle_scanfoundnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_scanfound) = ge_real_square_rectangle_scanfoundnormsquare + ge_imaginary_square_rectangle_scanfoundnormsquare)))))) /\ (exists ge_gap_rectangle_scanfoundstrict. ge_gap_rectangle_scanfoundstrict + S (gr_proper_divisor_norm_rectangle_scanfound) = (N)))))))))) \/ (forall gr_rectangle_real_rectangle_scan gr_rectangle_imaginary_rectangle_scan. (exists ge_gap_rectangle_scanabsent_real. ge_gap_rectangle_scanabsent_real + S (gr_rectangle_real_rectangle_scan) = (h)) -> (exists ge_gap_rectangle_scanabsent_imaginary. ge_gap_rectangle_scanabsent_imaginary + S (gr_rectangle_imaginary_rectangle_scan) = (k)) -> ~(((~(exists gr_inverse_rectangle_scanabsentnonunit. (exists ge_first_rp_rectangle_scanabsentnonunitidentity ge_first_rn_rectangle_scanabsentnonunitidentity ge_first_ip_rectangle_scanabsentnonunitidentity ge_first_in_rectangle_scanabsentnonunitidentity ge_second_rp_rectangle_scanabsentnonunitidentity ge_second_rn_rectangle_scanabsentnonunitidentity ge_second_ip_rectangle_scanabsentnonunitidentity ge_second_in_rectangle_scanabsentnonunitidentity. ((exists ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_scanabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal) = S ge_signed_half_rectangle_scanabsentnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentityfirstreal = (ge_first_rn_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_scanabsentnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentityfirstimaginary = (ge_first_in_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond. (((gr_inverse_rectangle_scanabsentnonunit) = ((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_scanabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal) = S ge_signed_half_rectangle_scanabsentnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentitysecondreal = (ge_second_rn_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_scanabsentnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanabsentnonunitidentity) + ge_balance_negative_rectangle_scanabsentnonunitidentitysecondimaginary = (ge_second_in_rectangle_scanabsentnonunitidentity) + ge_balance_positive_rectangle_scanabsentnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_scanabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal) = S ge_signed_half_rectangle_scanabsentnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))))))) + ge_balance_negative_rectangle_scanabsentnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))))))) + ge_balance_positive_rectangle_scanabsentnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_scanabsentnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_scanabsentnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))))))) + ge_balance_negative_rectangle_scanabsentnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_scanabsentnonunitidentity) * (ge_second_in_rectangle_scanabsentnonunitidentity))) + (((ge_first_rn_rectangle_scanabsentnonunitidentity) * (ge_second_ip_rectangle_scanabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_scanabsentnonunitidentity) * (ge_second_rn_rectangle_scanabsentnonunitidentity))) + (((ge_first_in_rectangle_scanabsentnonunitidentity) * (ge_second_rp_rectangle_scanabsentnonunitidentity))))))) + ge_balance_positive_rectangle_scanabsentnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_scanabsentquotient. (exists ge_first_rp_rectangle_scanabsentquotientproduct ge_first_rn_rectangle_scanabsentquotientproduct ge_first_ip_rectangle_scanabsentquotientproduct ge_first_in_rectangle_scanabsentquotientproduct ge_second_rp_rectangle_scanabsentquotientproduct ge_second_rn_rectangle_scanabsentquotientproduct ge_second_ip_rectangle_scanabsentquotientproduct ge_second_in_rectangle_scanabsentquotientproduct. ((exists ge_representation_real_code_rectangle_scanabsentquotientproductfirst ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst)) * S ((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_scanabsentquotientproductfirstreal ge_balance_negative_rectangle_scanabsentquotientproductfirstreal. (((((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductfirstreal) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_scanabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_scanabsentquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstreal) = S ge_signed_half_rectangle_scanabsentquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductfirstreal = (ge_first_rn_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_scanabsentquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary) = S ge_signed_half_rectangle_scanabsentquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductfirstimaginary = (ge_first_in_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_scanabsentquotientproductsecond ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond. (((gr_quotient_rectangle_scanabsentquotient) = ((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond)) * S ((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_scanabsentquotientproductsecondreal ge_balance_negative_rectangle_scanabsentquotientproductsecondreal. (((((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductsecondreal) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_scanabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_scanabsentquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondreal) = S ge_signed_half_rectangle_scanabsentquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductsecondreal = (ge_second_rn_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_scanabsentquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary) = S ge_signed_half_rectangle_scanabsentquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_scanabsentquotientproduct) + ge_balance_negative_rectangle_scanabsentquotientproductsecondimaginary = (ge_second_in_rectangle_scanabsentquotientproduct) + ge_balance_positive_rectangle_scanabsentquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_scanabsentquotientproductoutput ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput)) * S ((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_scanabsentquotientproductoutputreal ge_balance_negative_rectangle_scanabsentquotientproductoutputreal. (((((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductoutputreal) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_scanabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_scanabsentquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputreal) = S ge_signed_half_rectangle_scanabsentquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))))))) + ge_balance_negative_rectangle_scanabsentquotientproductoutputreal = (((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))))))) + ge_balance_positive_rectangle_scanabsentquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_scanabsentquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary) = S ge_signed_half_rectangle_scanabsentquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))))))) + ge_balance_negative_rectangle_scanabsentquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_scanabsentquotientproduct) * (ge_second_in_rectangle_scanabsentquotientproduct))) + (((ge_first_rn_rectangle_scanabsentquotientproduct) * (ge_second_ip_rectangle_scanabsentquotientproduct))))) + (((((ge_first_ip_rectangle_scanabsentquotientproduct) * (ge_second_rn_rectangle_scanabsentquotientproduct))) + (((ge_first_in_rectangle_scanabsentquotientproduct) * (ge_second_rp_rectangle_scanabsentquotientproduct))))))) + ge_balance_positive_rectangle_scanabsentquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_scanabsent. ((exists ge_norm_rp_rectangle_scanabsentnorm ge_norm_rn_rectangle_scanabsentnorm ge_norm_ip_rectangle_scanabsentnorm ge_norm_in_rectangle_scanabsentnorm. ((exists ge_representation_real_code_rectangle_scanabsentnormrepresentation ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation. (((((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) * S ((gr_rectangle_real_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan)) + ((gr_rectangle_imaginary_rectangle_scan) + (gr_rectangle_imaginary_rectangle_scan))) = ((ge_representation_real_code_rectangle_scanabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation)) * S ((ge_representation_real_code_rectangle_scanabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_scanabsentnormrepresentationreal ge_balance_negative_rectangle_scanabsentnormrepresentationreal. (((((ge_representation_real_code_rectangle_scanabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanabsentnormrepresentationreal) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_scanabsentnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_scanabsentnormrepresentation) = 2 * ge_signed_half_rectangle_scanabsentnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationreal) = S ge_signed_half_rectangle_scanabsentnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_scanabsentnorm) + ge_balance_negative_rectangle_scanabsentnormrepresentationreal = (ge_norm_rn_rectangle_scanabsentnorm) + ge_balance_positive_rectangle_scanabsentnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_scanabsentnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_scanabsentnormrepresentation) = 2 * ge_signed_half_rectangle_scanabsentnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary) = S ge_signed_half_rectangle_scanabsentnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_scanabsentnorm) + ge_balance_negative_rectangle_scanabsentnormrepresentationimaginary = (ge_norm_in_rectangle_scanabsentnorm) + ge_balance_positive_rectangle_scanabsentnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_scanabsentnormsquare ge_imaginary_square_rectangle_scanabsentnormsquare. ((((((ge_norm_rp_rectangle_scanabsentnorm) * (ge_norm_rp_rectangle_scanabsentnorm))) + (((ge_norm_rn_rectangle_scanabsentnorm) * (ge_norm_rn_rectangle_scanabsentnorm)))) = ((ge_real_square_rectangle_scanabsentnormsquare) + (((((ge_norm_rp_rectangle_scanabsentnorm) * (ge_norm_rn_rectangle_scanabsentnorm))) + (((ge_norm_rn_rectangle_scanabsentnorm) * (ge_norm_rp_rectangle_scanabsentnorm))))))) /\ ((((((ge_norm_ip_rectangle_scanabsentnorm) * (ge_norm_ip_rectangle_scanabsentnorm))) + (((ge_norm_in_rectangle_scanabsentnorm) * (ge_norm_in_rectangle_scanabsentnorm)))) = ((ge_imaginary_square_rectangle_scanabsentnormsquare) + (((((ge_norm_ip_rectangle_scanabsentnorm) * (ge_norm_in_rectangle_scanabsentnorm))) + (((ge_norm_in_rectangle_scanabsentnorm) * (ge_norm_ip_rectangle_scanabsentnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_scanabsent) = ge_real_square_rectangle_scanabsentnormsquare + ge_imaginary_square_rectangle_scanabsentnormsquare)))))) /\ (exists ge_gap_rectangle_scanabsentstrict. ge_gap_rectangle_scanabsentstrict + S (gr_proper_divisor_norm_rectangle_scanabsent) = (N)))))))))Constructive proof overview
Generated structural guide
Two ordinary finite inductions exhaust the actual signed-coordinate rectangle, with a witness or an explicit absence theorem.
The unchanged tactic script uses 7 declared prerequisites and contains 92 exact native proof lines.
Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
GF0071 gaussian_search_no_index_below_zero GF0075 gaussian_factor_search_coordinate_row finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized lt_of_lt_of_le Stable theorem; checked-use authorized le_succ_self Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized GF0073 gaussian_search_proper_divisor_code_transportDirect 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 (3)
01Induction on hL1–5
02Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
right
03Fix variables and assumptionsL7–11
04Use earlier factsL12–14
05Fix variables and assumptionsL15–18
06Establish hpreviousL19–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply IH.
- L19
have hprevious : (∃ x. ∃ y. Lt(x,h) ∧ (Lt(y,k) ∧ GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))) ∨ (∀ x. ∀ y. Lt(x,h) → Lt(y,k) → ¬GProperNormDivisor((x + y) · S (x + y) + (y + y),z,N))Definitions: GProperNormDivisorLt - L20
specialize IH (z) - L21
specialize IH (N) - L22
specialize IH (k) - L23
apply IH - L24
exact hz
07Separate the logical casesL25–30
08Construct an explicit witnessL31–32
09Separate the logical casesL33–33
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L33
split
10Use earlier factsL34–40
11Separate the logical casesL41–41
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L41
split
12Use earlier factsL42–43
13Establish hlastL44–50
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian factor search coordinate row.
- L44
have hlast : (∃ x. Lt(x,k) ∧ GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N)) ∨ (∀ x. Lt(x,k) → ¬GProperNormDivisor((h + x) · S (h + x) + (x + x),z,N))Definitions: GProperNormDivisorLt - L45
specialize gaussian_factor_search_coordinate_row (k) - L46
specialize gaussian_factor_search_coordinate_row (z) - L47
specialize gaussian_factor_search_coordinate_row (N) - L48
specialize gaussian_factor_search_coordinate_row (h) - L49
apply gaussian_factor_search_coordinate_row - L50
exact hz
14Separate the logical casesL51–54
15Construct an explicit witnessL55–56
16Separate the logical casesL57–57
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L57
split
17Construct an explicit witnessL58–58
Supply the displayed value, then prove that it has the required property.
- L58
exists 0
18Use earlier factsL59–59
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L59
apply zero_add
19Separate the logical casesL60–60
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L60
split
20Use earlier factsL61–62
21Separate the logical casesL63–63
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L63
right
22Fix variables and assumptionsL64–68
23Establish hcL69–73
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
24Separate the logical casesL74–74
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L74
cases hc
25Use earlier factsL75–82
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L75
specialize hlast_right (ic) - L76
apply hlast_right - L77
exact hi - L78
specialize gaussian_search_proper_divisor_code_transport (((rc) + (ic)) * S ((rc) + (ic)) + ((ic) + (ic))) - L79
specialize gaussian_search_proper_divisor_code_transport (((h) + (ic)) * S ((h) + (ic)) + ((ic) + (ic))) - L80
specialize gaussian_search_proper_divisor_code_transport (z) - L81
specialize gaussian_search_proper_divisor_code_transport (N) - L82
apply gaussian_search_proper_divisor_code_transport
26Calculate and transport equalitiesL83–85
Original exact command ledger · 92 lines
- 0001
induction h - 0002
intro z - 0003
intro N - 0004
intro k - 0005
intro hz - 0006
right - 0007
intro rc - 0008
intro ic - 0009
intro hr - 0010
intro hi - 0011
intro hp - 0012
specialize gaussian_search_no_index_below_zero (rc) - 0013
apply gaussian_search_no_index_below_zero - 0014
exact hr - 0015
intro z - 0016
intro N - 0017
intro k - 0018
intro hz - 0019
have hprevious : ((exists gr_rectangle_real_rectangle_previous gr_rectangle_imaginary_rectangle_previous. ((exists ge_gap_rectangle_previousfound_real. ge_gap_rectangle_previousfound_real + S (gr_rectangle_real_rectangle_previous) = (h)) /\ ((exists ge_gap_rectangle_previousfound_imaginary. ge_gap_rectangle_previousfound_imaginary + S (gr_rectangle_imaginary_rectangle_previous) = (k)) /\ (((~(exists gr_inverse_rectangle_previousfoundnonunit. (exists ge_first_rp_rectangle_previousfoundnonunitidentity ge_first_rn_rectangle_previousfoundnonunitidentity ge_first_ip_rectangle_previousfoundnonunitidentity ge_first_in_rectangle_previousfoundnonunitidentity ge_second_rp_rectangle_previousfoundnonunitidentity ge_second_rn_rectangle_previousfoundnonunitidentity ge_second_ip_rectangle_previousfoundnonunitidentity ge_second_in_rectangle_previousfoundnonunitidentity. ((exists ge_representation_real_code_rectangle_previousfoundnonunitidentityfirst ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst. (((((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) * S ((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) + ((gr_rectangle_imaginary_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous))) = ((ge_representation_real_code_rectangle_previousfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_previousfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_previousfoundnonunitidentityfirstreal ge_balance_negative_rectangle_previousfoundnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_previousfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_previousfoundnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_previousfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_previousfoundnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityfirstreal) = S ge_signed_half_rectangle_previousfoundnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_previousfoundnonunitidentity) + ge_balance_negative_rectangle_previousfoundnonunitidentityfirstreal = (ge_first_rn_rectangle_previousfoundnonunitidentity) + ge_balance_positive_rectangle_previousfoundnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_previousfoundnonunitidentityfirstimaginary ge_balance_negative_rectangle_previousfoundnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_previousfoundnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_previousfoundnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_previousfoundnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_previousfoundnonunitidentity) + ge_balance_negative_rectangle_previousfoundnonunitidentityfirstimaginary = (ge_first_in_rectangle_previousfoundnonunitidentity) + ge_balance_positive_rectangle_previousfoundnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_previousfoundnonunitidentitysecond ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond. (((gr_inverse_rectangle_previousfoundnonunit) = ((ge_representation_real_code_rectangle_previousfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_previousfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_previousfoundnonunitidentitysecondreal ge_balance_negative_rectangle_previousfoundnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_previousfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_previousfoundnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_previousfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_previousfoundnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentitysecondreal) = S ge_signed_half_rectangle_previousfoundnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_previousfoundnonunitidentity) + ge_balance_negative_rectangle_previousfoundnonunitidentitysecondreal = (ge_second_rn_rectangle_previousfoundnonunitidentity) + ge_balance_positive_rectangle_previousfoundnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_previousfoundnonunitidentitysecondimaginary ge_balance_negative_rectangle_previousfoundnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_previousfoundnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_previousfoundnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_previousfoundnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_previousfoundnonunitidentity) + ge_balance_negative_rectangle_previousfoundnonunitidentitysecondimaginary = (ge_second_in_rectangle_previousfoundnonunitidentity) + ge_balance_positive_rectangle_previousfoundnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_previousfoundnonunitidentityoutput ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_previousfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_previousfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_previousfoundnonunitidentityoutputreal ge_balance_negative_rectangle_previousfoundnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_previousfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_previousfoundnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_previousfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_previousfoundnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityoutputreal) = S ge_signed_half_rectangle_previousfoundnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_previousfoundnonunitidentity) * (ge_second_rp_rectangle_previousfoundnonunitidentity))) + (((ge_first_rn_rectangle_previousfoundnonunitidentity) * (ge_second_rn_rectangle_previousfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_previousfoundnonunitidentity) * (ge_second_in_rectangle_previousfoundnonunitidentity))) + (((ge_first_in_rectangle_previousfoundnonunitidentity) * (ge_second_ip_rectangle_previousfoundnonunitidentity))))))) + ge_balance_negative_rectangle_previousfoundnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_previousfoundnonunitidentity) * (ge_second_rn_rectangle_previousfoundnonunitidentity))) + (((ge_first_rn_rectangle_previousfoundnonunitidentity) * (ge_second_rp_rectangle_previousfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_previousfoundnonunitidentity) * (ge_second_ip_rectangle_previousfoundnonunitidentity))) + (((ge_first_in_rectangle_previousfoundnonunitidentity) * (ge_second_in_rectangle_previousfoundnonunitidentity))))))) + ge_balance_positive_rectangle_previousfoundnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_previousfoundnonunitidentityoutputimaginary ge_balance_negative_rectangle_previousfoundnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_previousfoundnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_previousfoundnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_previousfoundnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_previousfoundnonunitidentity) * (ge_second_ip_rectangle_previousfoundnonunitidentity))) + (((ge_first_rn_rectangle_previousfoundnonunitidentity) * (ge_second_in_rectangle_previousfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_previousfoundnonunitidentity) * (ge_second_rp_rectangle_previousfoundnonunitidentity))) + (((ge_first_in_rectangle_previousfoundnonunitidentity) * (ge_second_rn_rectangle_previousfoundnonunitidentity))))))) + ge_balance_negative_rectangle_previousfoundnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_previousfoundnonunitidentity) * (ge_second_in_rectangle_previousfoundnonunitidentity))) + (((ge_first_rn_rectangle_previousfoundnonunitidentity) * (ge_second_ip_rectangle_previousfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_previousfoundnonunitidentity) * (ge_second_rn_rectangle_previousfoundnonunitidentity))) + (((ge_first_in_rectangle_previousfoundnonunitidentity) * (ge_second_rp_rectangle_previousfoundnonunitidentity))))))) + ge_balance_positive_rectangle_previousfoundnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_previousfoundquotient. (exists ge_first_rp_rectangle_previousfoundquotientproduct ge_first_rn_rectangle_previousfoundquotientproduct ge_first_ip_rectangle_previousfoundquotientproduct ge_first_in_rectangle_previousfoundquotientproduct ge_second_rp_rectangle_previousfoundquotientproduct ge_second_rn_rectangle_previousfoundquotientproduct ge_second_ip_rectangle_previousfoundquotientproduct ge_second_in_rectangle_previousfoundquotientproduct. ((exists ge_representation_real_code_rectangle_previousfoundquotientproductfirst ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst. (((((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) * S ((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) + ((gr_rectangle_imaginary_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous))) = ((ge_representation_real_code_rectangle_previousfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst)) * S ((ge_representation_real_code_rectangle_previousfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_previousfoundquotientproductfirstreal ge_balance_negative_rectangle_previousfoundquotientproductfirstreal. (((((ge_representation_real_code_rectangle_previousfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_previousfoundquotientproductfirstreal) /\ (ge_balance_negative_rectangle_previousfoundquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_previousfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_previousfoundquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundquotientproductfirstreal) = S ge_signed_half_rectangle_previousfoundquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_previousfoundquotientproduct) + ge_balance_negative_rectangle_previousfoundquotientproductfirstreal = (ge_first_rn_rectangle_previousfoundquotientproduct) + ge_balance_positive_rectangle_previousfoundquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_previousfoundquotientproductfirstimaginary ge_balance_negative_rectangle_previousfoundquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_previousfoundquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_previousfoundquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_previousfoundquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundquotientproductfirstimaginary) = S ge_signed_half_rectangle_previousfoundquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_previousfoundquotientproduct) + ge_balance_negative_rectangle_previousfoundquotientproductfirstimaginary = (ge_first_in_rectangle_previousfoundquotientproduct) + ge_balance_positive_rectangle_previousfoundquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_previousfoundquotientproductsecond ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond. (((gr_quotient_rectangle_previousfoundquotient) = ((ge_representation_real_code_rectangle_previousfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond)) * S ((ge_representation_real_code_rectangle_previousfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_previousfoundquotientproductsecondreal ge_balance_negative_rectangle_previousfoundquotientproductsecondreal. (((((ge_representation_real_code_rectangle_previousfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_previousfoundquotientproductsecondreal) /\ (ge_balance_negative_rectangle_previousfoundquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_previousfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_previousfoundquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundquotientproductsecondreal) = S ge_signed_half_rectangle_previousfoundquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_previousfoundquotientproduct) + ge_balance_negative_rectangle_previousfoundquotientproductsecondreal = (ge_second_rn_rectangle_previousfoundquotientproduct) + ge_balance_positive_rectangle_previousfoundquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_previousfoundquotientproductsecondimaginary ge_balance_negative_rectangle_previousfoundquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_previousfoundquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_previousfoundquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_previousfoundquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundquotientproductsecondimaginary) = S ge_signed_half_rectangle_previousfoundquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_previousfoundquotientproduct) + ge_balance_negative_rectangle_previousfoundquotientproductsecondimaginary = (ge_second_in_rectangle_previousfoundquotientproduct) + ge_balance_positive_rectangle_previousfoundquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_previousfoundquotientproductoutput ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_previousfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput)) * S ((ge_representation_real_code_rectangle_previousfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_previousfoundquotientproductoutputreal ge_balance_negative_rectangle_previousfoundquotientproductoutputreal. (((((ge_representation_real_code_rectangle_previousfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_previousfoundquotientproductoutputreal) /\ (ge_balance_negative_rectangle_previousfoundquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_previousfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_previousfoundquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundquotientproductoutputreal) = S ge_signed_half_rectangle_previousfoundquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_previousfoundquotientproduct) * (ge_second_rp_rectangle_previousfoundquotientproduct))) + (((ge_first_rn_rectangle_previousfoundquotientproduct) * (ge_second_rn_rectangle_previousfoundquotientproduct))))) + (((((ge_first_ip_rectangle_previousfoundquotientproduct) * (ge_second_in_rectangle_previousfoundquotientproduct))) + (((ge_first_in_rectangle_previousfoundquotientproduct) * (ge_second_ip_rectangle_previousfoundquotientproduct))))))) + ge_balance_negative_rectangle_previousfoundquotientproductoutputreal = (((((((ge_first_rp_rectangle_previousfoundquotientproduct) * (ge_second_rn_rectangle_previousfoundquotientproduct))) + (((ge_first_rn_rectangle_previousfoundquotientproduct) * (ge_second_rp_rectangle_previousfoundquotientproduct))))) + (((((ge_first_ip_rectangle_previousfoundquotientproduct) * (ge_second_ip_rectangle_previousfoundquotientproduct))) + (((ge_first_in_rectangle_previousfoundquotientproduct) * (ge_second_in_rectangle_previousfoundquotientproduct))))))) + ge_balance_positive_rectangle_previousfoundquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_previousfoundquotientproductoutputimaginary ge_balance_negative_rectangle_previousfoundquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_previousfoundquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_previousfoundquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_previousfoundquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundquotientproductoutputimaginary) = S ge_signed_half_rectangle_previousfoundquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_previousfoundquotientproduct) * (ge_second_ip_rectangle_previousfoundquotientproduct))) + (((ge_first_rn_rectangle_previousfoundquotientproduct) * (ge_second_in_rectangle_previousfoundquotientproduct))))) + (((((ge_first_ip_rectangle_previousfoundquotientproduct) * (ge_second_rp_rectangle_previousfoundquotientproduct))) + (((ge_first_in_rectangle_previousfoundquotientproduct) * (ge_second_rn_rectangle_previousfoundquotientproduct))))))) + ge_balance_negative_rectangle_previousfoundquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_previousfoundquotientproduct) * (ge_second_in_rectangle_previousfoundquotientproduct))) + (((ge_first_rn_rectangle_previousfoundquotientproduct) * (ge_second_ip_rectangle_previousfoundquotientproduct))))) + (((((ge_first_ip_rectangle_previousfoundquotientproduct) * (ge_second_rn_rectangle_previousfoundquotientproduct))) + (((ge_first_in_rectangle_previousfoundquotientproduct) * (ge_second_rp_rectangle_previousfoundquotientproduct))))))) + ge_balance_positive_rectangle_previousfoundquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_previousfound. ((exists ge_norm_rp_rectangle_previousfoundnorm ge_norm_rn_rectangle_previousfoundnorm ge_norm_ip_rectangle_previousfoundnorm ge_norm_in_rectangle_previousfoundnorm. ((exists ge_representation_real_code_rectangle_previousfoundnormrepresentation ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation. (((((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) * S ((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) + ((gr_rectangle_imaginary_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous))) = ((ge_representation_real_code_rectangle_previousfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation)) * S ((ge_representation_real_code_rectangle_previousfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_previousfoundnormrepresentationreal ge_balance_negative_rectangle_previousfoundnormrepresentationreal. (((((ge_representation_real_code_rectangle_previousfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_previousfoundnormrepresentationreal) /\ (ge_balance_negative_rectangle_previousfoundnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_previousfoundnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_previousfoundnormrepresentation) = 2 * ge_signed_half_rectangle_previousfoundnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_previousfoundnormrepresentationreal) = S ge_signed_half_rectangle_previousfoundnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_previousfoundnorm) + ge_balance_negative_rectangle_previousfoundnormrepresentationreal = (ge_norm_rn_rectangle_previousfoundnorm) + ge_balance_positive_rectangle_previousfoundnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_previousfoundnormrepresentationimaginary ge_balance_negative_rectangle_previousfoundnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_previousfoundnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_previousfoundnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_previousfoundnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousfoundnormrepresentation) = 2 * ge_signed_half_rectangle_previousfoundnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousfoundnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_previousfoundnormrepresentationimaginary) = S ge_signed_half_rectangle_previousfoundnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_previousfoundnorm) + ge_balance_negative_rectangle_previousfoundnormrepresentationimaginary = (ge_norm_in_rectangle_previousfoundnorm) + ge_balance_positive_rectangle_previousfoundnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_previousfoundnormsquare ge_imaginary_square_rectangle_previousfoundnormsquare. ((((((ge_norm_rp_rectangle_previousfoundnorm) * (ge_norm_rp_rectangle_previousfoundnorm))) + (((ge_norm_rn_rectangle_previousfoundnorm) * (ge_norm_rn_rectangle_previousfoundnorm)))) = ((ge_real_square_rectangle_previousfoundnormsquare) + (((((ge_norm_rp_rectangle_previousfoundnorm) * (ge_norm_rn_rectangle_previousfoundnorm))) + (((ge_norm_rn_rectangle_previousfoundnorm) * (ge_norm_rp_rectangle_previousfoundnorm))))))) /\ ((((((ge_norm_ip_rectangle_previousfoundnorm) * (ge_norm_ip_rectangle_previousfoundnorm))) + (((ge_norm_in_rectangle_previousfoundnorm) * (ge_norm_in_rectangle_previousfoundnorm)))) = ((ge_imaginary_square_rectangle_previousfoundnormsquare) + (((((ge_norm_ip_rectangle_previousfoundnorm) * (ge_norm_in_rectangle_previousfoundnorm))) + (((ge_norm_in_rectangle_previousfoundnorm) * (ge_norm_ip_rectangle_previousfoundnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_previousfound) = ge_real_square_rectangle_previousfoundnormsquare + ge_imaginary_square_rectangle_previousfoundnormsquare)))))) /\ (exists ge_gap_rectangle_previousfoundstrict. ge_gap_rectangle_previousfoundstrict + S (gr_proper_divisor_norm_rectangle_previousfound) = (N)))))))))) \/ (forall gr_rectangle_real_rectangle_previous gr_rectangle_imaginary_rectangle_previous. (exists ge_gap_rectangle_previousabsent_real. ge_gap_rectangle_previousabsent_real + S (gr_rectangle_real_rectangle_previous) = (h)) -> (exists ge_gap_rectangle_previousabsent_imaginary. ge_gap_rectangle_previousabsent_imaginary + S (gr_rectangle_imaginary_rectangle_previous) = (k)) -> ~(((~(exists gr_inverse_rectangle_previousabsentnonunit. (exists ge_first_rp_rectangle_previousabsentnonunitidentity ge_first_rn_rectangle_previousabsentnonunitidentity ge_first_ip_rectangle_previousabsentnonunitidentity ge_first_in_rectangle_previousabsentnonunitidentity ge_second_rp_rectangle_previousabsentnonunitidentity ge_second_rn_rectangle_previousabsentnonunitidentity ge_second_ip_rectangle_previousabsentnonunitidentity ge_second_in_rectangle_previousabsentnonunitidentity. ((exists ge_representation_real_code_rectangle_previousabsentnonunitidentityfirst ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst. (((((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) * S ((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) + ((gr_rectangle_imaginary_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous))) = ((ge_representation_real_code_rectangle_previousabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_previousabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_previousabsentnonunitidentityfirstreal ge_balance_negative_rectangle_previousabsentnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_previousabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_previousabsentnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_previousabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_previousabsentnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityfirstreal) = S ge_signed_half_rectangle_previousabsentnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_previousabsentnonunitidentity) + ge_balance_negative_rectangle_previousabsentnonunitidentityfirstreal = (ge_first_rn_rectangle_previousabsentnonunitidentity) + ge_balance_positive_rectangle_previousabsentnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_previousabsentnonunitidentityfirstimaginary ge_balance_negative_rectangle_previousabsentnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_previousabsentnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_previousabsentnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_previousabsentnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_previousabsentnonunitidentity) + ge_balance_negative_rectangle_previousabsentnonunitidentityfirstimaginary = (ge_first_in_rectangle_previousabsentnonunitidentity) + ge_balance_positive_rectangle_previousabsentnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_previousabsentnonunitidentitysecond ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond. (((gr_inverse_rectangle_previousabsentnonunit) = ((ge_representation_real_code_rectangle_previousabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_previousabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_previousabsentnonunitidentitysecondreal ge_balance_negative_rectangle_previousabsentnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_previousabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_previousabsentnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_previousabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_previousabsentnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentitysecondreal) = S ge_signed_half_rectangle_previousabsentnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_previousabsentnonunitidentity) + ge_balance_negative_rectangle_previousabsentnonunitidentitysecondreal = (ge_second_rn_rectangle_previousabsentnonunitidentity) + ge_balance_positive_rectangle_previousabsentnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_previousabsentnonunitidentitysecondimaginary ge_balance_negative_rectangle_previousabsentnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_previousabsentnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_previousabsentnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_previousabsentnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_previousabsentnonunitidentity) + ge_balance_negative_rectangle_previousabsentnonunitidentitysecondimaginary = (ge_second_in_rectangle_previousabsentnonunitidentity) + ge_balance_positive_rectangle_previousabsentnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_previousabsentnonunitidentityoutput ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_previousabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_previousabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_previousabsentnonunitidentityoutputreal ge_balance_negative_rectangle_previousabsentnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_previousabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_previousabsentnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_previousabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_previousabsentnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityoutputreal) = S ge_signed_half_rectangle_previousabsentnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_previousabsentnonunitidentity) * (ge_second_rp_rectangle_previousabsentnonunitidentity))) + (((ge_first_rn_rectangle_previousabsentnonunitidentity) * (ge_second_rn_rectangle_previousabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_previousabsentnonunitidentity) * (ge_second_in_rectangle_previousabsentnonunitidentity))) + (((ge_first_in_rectangle_previousabsentnonunitidentity) * (ge_second_ip_rectangle_previousabsentnonunitidentity))))))) + ge_balance_negative_rectangle_previousabsentnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_previousabsentnonunitidentity) * (ge_second_rn_rectangle_previousabsentnonunitidentity))) + (((ge_first_rn_rectangle_previousabsentnonunitidentity) * (ge_second_rp_rectangle_previousabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_previousabsentnonunitidentity) * (ge_second_ip_rectangle_previousabsentnonunitidentity))) + (((ge_first_in_rectangle_previousabsentnonunitidentity) * (ge_second_in_rectangle_previousabsentnonunitidentity))))))) + ge_balance_positive_rectangle_previousabsentnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_previousabsentnonunitidentityoutputimaginary ge_balance_negative_rectangle_previousabsentnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_previousabsentnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_previousabsentnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_previousabsentnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_previousabsentnonunitidentity) * (ge_second_ip_rectangle_previousabsentnonunitidentity))) + (((ge_first_rn_rectangle_previousabsentnonunitidentity) * (ge_second_in_rectangle_previousabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_previousabsentnonunitidentity) * (ge_second_rp_rectangle_previousabsentnonunitidentity))) + (((ge_first_in_rectangle_previousabsentnonunitidentity) * (ge_second_rn_rectangle_previousabsentnonunitidentity))))))) + ge_balance_negative_rectangle_previousabsentnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_previousabsentnonunitidentity) * (ge_second_in_rectangle_previousabsentnonunitidentity))) + (((ge_first_rn_rectangle_previousabsentnonunitidentity) * (ge_second_ip_rectangle_previousabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_previousabsentnonunitidentity) * (ge_second_rn_rectangle_previousabsentnonunitidentity))) + (((ge_first_in_rectangle_previousabsentnonunitidentity) * (ge_second_rp_rectangle_previousabsentnonunitidentity))))))) + ge_balance_positive_rectangle_previousabsentnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_previousabsentquotient. (exists ge_first_rp_rectangle_previousabsentquotientproduct ge_first_rn_rectangle_previousabsentquotientproduct ge_first_ip_rectangle_previousabsentquotientproduct ge_first_in_rectangle_previousabsentquotientproduct ge_second_rp_rectangle_previousabsentquotientproduct ge_second_rn_rectangle_previousabsentquotientproduct ge_second_ip_rectangle_previousabsentquotientproduct ge_second_in_rectangle_previousabsentquotientproduct. ((exists ge_representation_real_code_rectangle_previousabsentquotientproductfirst ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst. (((((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) * S ((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) + ((gr_rectangle_imaginary_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous))) = ((ge_representation_real_code_rectangle_previousabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst)) * S ((ge_representation_real_code_rectangle_previousabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_previousabsentquotientproductfirstreal ge_balance_negative_rectangle_previousabsentquotientproductfirstreal. (((((ge_representation_real_code_rectangle_previousabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_previousabsentquotientproductfirstreal) /\ (ge_balance_negative_rectangle_previousabsentquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_previousabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_previousabsentquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentquotientproductfirstreal) = S ge_signed_half_rectangle_previousabsentquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_previousabsentquotientproduct) + ge_balance_negative_rectangle_previousabsentquotientproductfirstreal = (ge_first_rn_rectangle_previousabsentquotientproduct) + ge_balance_positive_rectangle_previousabsentquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_previousabsentquotientproductfirstimaginary ge_balance_negative_rectangle_previousabsentquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_previousabsentquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_previousabsentquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_previousabsentquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentquotientproductfirstimaginary) = S ge_signed_half_rectangle_previousabsentquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_previousabsentquotientproduct) + ge_balance_negative_rectangle_previousabsentquotientproductfirstimaginary = (ge_first_in_rectangle_previousabsentquotientproduct) + ge_balance_positive_rectangle_previousabsentquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_previousabsentquotientproductsecond ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond. (((gr_quotient_rectangle_previousabsentquotient) = ((ge_representation_real_code_rectangle_previousabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond)) * S ((ge_representation_real_code_rectangle_previousabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_previousabsentquotientproductsecondreal ge_balance_negative_rectangle_previousabsentquotientproductsecondreal. (((((ge_representation_real_code_rectangle_previousabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_previousabsentquotientproductsecondreal) /\ (ge_balance_negative_rectangle_previousabsentquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_previousabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_previousabsentquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentquotientproductsecondreal) = S ge_signed_half_rectangle_previousabsentquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_previousabsentquotientproduct) + ge_balance_negative_rectangle_previousabsentquotientproductsecondreal = (ge_second_rn_rectangle_previousabsentquotientproduct) + ge_balance_positive_rectangle_previousabsentquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_previousabsentquotientproductsecondimaginary ge_balance_negative_rectangle_previousabsentquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_previousabsentquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_previousabsentquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_previousabsentquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentquotientproductsecondimaginary) = S ge_signed_half_rectangle_previousabsentquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_previousabsentquotientproduct) + ge_balance_negative_rectangle_previousabsentquotientproductsecondimaginary = (ge_second_in_rectangle_previousabsentquotientproduct) + ge_balance_positive_rectangle_previousabsentquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_previousabsentquotientproductoutput ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_previousabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput)) * S ((ge_representation_real_code_rectangle_previousabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_previousabsentquotientproductoutputreal ge_balance_negative_rectangle_previousabsentquotientproductoutputreal. (((((ge_representation_real_code_rectangle_previousabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_previousabsentquotientproductoutputreal) /\ (ge_balance_negative_rectangle_previousabsentquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_previousabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_previousabsentquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentquotientproductoutputreal) = S ge_signed_half_rectangle_previousabsentquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_previousabsentquotientproduct) * (ge_second_rp_rectangle_previousabsentquotientproduct))) + (((ge_first_rn_rectangle_previousabsentquotientproduct) * (ge_second_rn_rectangle_previousabsentquotientproduct))))) + (((((ge_first_ip_rectangle_previousabsentquotientproduct) * (ge_second_in_rectangle_previousabsentquotientproduct))) + (((ge_first_in_rectangle_previousabsentquotientproduct) * (ge_second_ip_rectangle_previousabsentquotientproduct))))))) + ge_balance_negative_rectangle_previousabsentquotientproductoutputreal = (((((((ge_first_rp_rectangle_previousabsentquotientproduct) * (ge_second_rn_rectangle_previousabsentquotientproduct))) + (((ge_first_rn_rectangle_previousabsentquotientproduct) * (ge_second_rp_rectangle_previousabsentquotientproduct))))) + (((((ge_first_ip_rectangle_previousabsentquotientproduct) * (ge_second_ip_rectangle_previousabsentquotientproduct))) + (((ge_first_in_rectangle_previousabsentquotientproduct) * (ge_second_in_rectangle_previousabsentquotientproduct))))))) + ge_balance_positive_rectangle_previousabsentquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_previousabsentquotientproductoutputimaginary ge_balance_negative_rectangle_previousabsentquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_previousabsentquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_previousabsentquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_previousabsentquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentquotientproductoutputimaginary) = S ge_signed_half_rectangle_previousabsentquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_previousabsentquotientproduct) * (ge_second_ip_rectangle_previousabsentquotientproduct))) + (((ge_first_rn_rectangle_previousabsentquotientproduct) * (ge_second_in_rectangle_previousabsentquotientproduct))))) + (((((ge_first_ip_rectangle_previousabsentquotientproduct) * (ge_second_rp_rectangle_previousabsentquotientproduct))) + (((ge_first_in_rectangle_previousabsentquotientproduct) * (ge_second_rn_rectangle_previousabsentquotientproduct))))))) + ge_balance_negative_rectangle_previousabsentquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_previousabsentquotientproduct) * (ge_second_in_rectangle_previousabsentquotientproduct))) + (((ge_first_rn_rectangle_previousabsentquotientproduct) * (ge_second_ip_rectangle_previousabsentquotientproduct))))) + (((((ge_first_ip_rectangle_previousabsentquotientproduct) * (ge_second_rn_rectangle_previousabsentquotientproduct))) + (((ge_first_in_rectangle_previousabsentquotientproduct) * (ge_second_rp_rectangle_previousabsentquotientproduct))))))) + ge_balance_positive_rectangle_previousabsentquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_previousabsent. ((exists ge_norm_rp_rectangle_previousabsentnorm ge_norm_rn_rectangle_previousabsentnorm ge_norm_ip_rectangle_previousabsentnorm ge_norm_in_rectangle_previousabsentnorm. ((exists ge_representation_real_code_rectangle_previousabsentnormrepresentation ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation. (((((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) * S ((gr_rectangle_real_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous)) + ((gr_rectangle_imaginary_rectangle_previous) + (gr_rectangle_imaginary_rectangle_previous))) = ((ge_representation_real_code_rectangle_previousabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation)) * S ((ge_representation_real_code_rectangle_previousabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_previousabsentnormrepresentationreal ge_balance_negative_rectangle_previousabsentnormrepresentationreal. (((((ge_representation_real_code_rectangle_previousabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_previousabsentnormrepresentationreal) /\ (ge_balance_negative_rectangle_previousabsentnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_previousabsentnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_previousabsentnormrepresentation) = 2 * ge_signed_half_rectangle_previousabsentnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_previousabsentnormrepresentationreal) = S ge_signed_half_rectangle_previousabsentnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_previousabsentnorm) + ge_balance_negative_rectangle_previousabsentnormrepresentationreal = (ge_norm_rn_rectangle_previousabsentnorm) + ge_balance_positive_rectangle_previousabsentnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_previousabsentnormrepresentationimaginary ge_balance_negative_rectangle_previousabsentnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_previousabsentnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_previousabsentnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_previousabsentnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_previousabsentnormrepresentation) = 2 * ge_signed_half_rectangle_previousabsentnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_previousabsentnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_previousabsentnormrepresentationimaginary) = S ge_signed_half_rectangle_previousabsentnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_previousabsentnorm) + ge_balance_negative_rectangle_previousabsentnormrepresentationimaginary = (ge_norm_in_rectangle_previousabsentnorm) + ge_balance_positive_rectangle_previousabsentnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_previousabsentnormsquare ge_imaginary_square_rectangle_previousabsentnormsquare. ((((((ge_norm_rp_rectangle_previousabsentnorm) * (ge_norm_rp_rectangle_previousabsentnorm))) + (((ge_norm_rn_rectangle_previousabsentnorm) * (ge_norm_rn_rectangle_previousabsentnorm)))) = ((ge_real_square_rectangle_previousabsentnormsquare) + (((((ge_norm_rp_rectangle_previousabsentnorm) * (ge_norm_rn_rectangle_previousabsentnorm))) + (((ge_norm_rn_rectangle_previousabsentnorm) * (ge_norm_rp_rectangle_previousabsentnorm))))))) /\ ((((((ge_norm_ip_rectangle_previousabsentnorm) * (ge_norm_ip_rectangle_previousabsentnorm))) + (((ge_norm_in_rectangle_previousabsentnorm) * (ge_norm_in_rectangle_previousabsentnorm)))) = ((ge_imaginary_square_rectangle_previousabsentnormsquare) + (((((ge_norm_ip_rectangle_previousabsentnorm) * (ge_norm_in_rectangle_previousabsentnorm))) + (((ge_norm_in_rectangle_previousabsentnorm) * (ge_norm_ip_rectangle_previousabsentnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_previousabsent) = ge_real_square_rectangle_previousabsentnormsquare + ge_imaginary_square_rectangle_previousabsentnormsquare)))))) /\ (exists ge_gap_rectangle_previousabsentstrict. ge_gap_rectangle_previousabsentstrict + S (gr_proper_divisor_norm_rectangle_previousabsent) = (N))))))))) - 0020
specialize IH (z) - 0021
specialize IH (N) - 0022
specialize IH (k) - 0023
apply IH - 0024
exact hz - 0025
cases hprevious - 0026
cases hprevious_left - 0027
cases hprevious_left_witness - 0028
cases hprevious_left_witness_witness - 0029
cases hprevious_left_witness_witness_right - 0030
left - 0031
exists (x) - 0032
exists (x1) - 0033
split - 0034
specialize lt_of_lt_of_le (x) - 0035
specialize lt_of_lt_of_le (h) - 0036
specialize lt_of_lt_of_le (S h) - 0037
apply lt_of_lt_of_le - 0038
exact hprevious_left_witness_witness_left - 0039
specialize le_succ_self (h) - 0040
apply le_succ_self - 0041
split - 0042
exact hprevious_left_witness_witness_right_left - 0043
exact hprevious_left_witness_witness_right_right - 0044
have hlast : ((exists gr_row_coordinate_rectangle_last_row. ((exists ge_gap_rectangle_last_rowfound_index. ge_gap_rectangle_last_rowfound_index + S (gr_row_coordinate_rectangle_last_row) = (k)) /\ (((~(exists gr_inverse_rectangle_last_rowfoundnonunit. (exists ge_first_rp_rectangle_last_rowfoundnonunitidentity ge_first_rn_rectangle_last_rowfoundnonunitidentity ge_first_ip_rectangle_last_rowfoundnonunitidentity ge_first_in_rectangle_last_rowfoundnonunitidentity ge_second_rp_rectangle_last_rowfoundnonunitidentity ge_second_rn_rectangle_last_rowfoundnonunitidentity ge_second_ip_rectangle_last_rowfoundnonunitidentity ge_second_in_rectangle_last_rowfoundnonunitidentity. ((exists ge_representation_real_code_rectangle_last_rowfoundnonunitidentityfirst ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst. (((((h) + (gr_row_coordinate_rectangle_last_row)) * S ((h) + (gr_row_coordinate_rectangle_last_row)) + ((gr_row_coordinate_rectangle_last_row) + (gr_row_coordinate_rectangle_last_row))) = ((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstreal ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_last_rowfoundnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstreal) = S ge_signed_half_rectangle_last_rowfoundnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_last_rowfoundnonunitidentity) + ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstreal = (ge_first_rn_rectangle_last_rowfoundnonunitidentity) + ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstimaginary ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityfirst) = 2 * ge_signed_half_rectangle_last_rowfoundnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_last_rowfoundnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_last_rowfoundnonunitidentity) + ge_balance_negative_rectangle_last_rowfoundnonunitidentityfirstimaginary = (ge_first_in_rectangle_last_rowfoundnonunitidentity) + ge_balance_positive_rectangle_last_rowfoundnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_last_rowfoundnonunitidentitysecond ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond. (((gr_inverse_rectangle_last_rowfoundnonunit) = ((ge_representation_real_code_rectangle_last_rowfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_last_rowfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondreal ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_last_rowfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_last_rowfoundnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondreal) = S ge_signed_half_rectangle_last_rowfoundnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_last_rowfoundnonunitidentity) + ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondreal = (ge_second_rn_rectangle_last_rowfoundnonunitidentity) + ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondimaginary ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentitysecond) = 2 * ge_signed_half_rectangle_last_rowfoundnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_last_rowfoundnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_last_rowfoundnonunitidentity) + ge_balance_negative_rectangle_last_rowfoundnonunitidentitysecondimaginary = (ge_second_in_rectangle_last_rowfoundnonunitidentity) + ge_balance_positive_rectangle_last_rowfoundnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_last_rowfoundnonunitidentityoutput ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputreal ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_last_rowfoundnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputreal) = S ge_signed_half_rectangle_last_rowfoundnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_last_rowfoundnonunitidentity) * (ge_second_rp_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_rn_rectangle_last_rowfoundnonunitidentity) * (ge_second_rn_rectangle_last_rowfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowfoundnonunitidentity) * (ge_second_in_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_in_rectangle_last_rowfoundnonunitidentity) * (ge_second_ip_rectangle_last_rowfoundnonunitidentity))))))) + ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_last_rowfoundnonunitidentity) * (ge_second_rn_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_rn_rectangle_last_rowfoundnonunitidentity) * (ge_second_rp_rectangle_last_rowfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowfoundnonunitidentity) * (ge_second_ip_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_in_rectangle_last_rowfoundnonunitidentity) * (ge_second_in_rectangle_last_rowfoundnonunitidentity))))))) + ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputimaginary ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundnonunitidentityoutput) = 2 * ge_signed_half_rectangle_last_rowfoundnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_last_rowfoundnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_last_rowfoundnonunitidentity) * (ge_second_ip_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_rn_rectangle_last_rowfoundnonunitidentity) * (ge_second_in_rectangle_last_rowfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowfoundnonunitidentity) * (ge_second_rp_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_in_rectangle_last_rowfoundnonunitidentity) * (ge_second_rn_rectangle_last_rowfoundnonunitidentity))))))) + ge_balance_negative_rectangle_last_rowfoundnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_last_rowfoundnonunitidentity) * (ge_second_in_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_rn_rectangle_last_rowfoundnonunitidentity) * (ge_second_ip_rectangle_last_rowfoundnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowfoundnonunitidentity) * (ge_second_rn_rectangle_last_rowfoundnonunitidentity))) + (((ge_first_in_rectangle_last_rowfoundnonunitidentity) * (ge_second_rp_rectangle_last_rowfoundnonunitidentity))))))) + ge_balance_positive_rectangle_last_rowfoundnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_last_rowfoundquotient. (exists ge_first_rp_rectangle_last_rowfoundquotientproduct ge_first_rn_rectangle_last_rowfoundquotientproduct ge_first_ip_rectangle_last_rowfoundquotientproduct ge_first_in_rectangle_last_rowfoundquotientproduct ge_second_rp_rectangle_last_rowfoundquotientproduct ge_second_rn_rectangle_last_rowfoundquotientproduct ge_second_ip_rectangle_last_rowfoundquotientproduct ge_second_in_rectangle_last_rowfoundquotientproduct. ((exists ge_representation_real_code_rectangle_last_rowfoundquotientproductfirst ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst. (((((h) + (gr_row_coordinate_rectangle_last_row)) * S ((h) + (gr_row_coordinate_rectangle_last_row)) + ((gr_row_coordinate_rectangle_last_row) + (gr_row_coordinate_rectangle_last_row))) = ((ge_representation_real_code_rectangle_last_rowfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst)) * S ((ge_representation_real_code_rectangle_last_rowfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundquotientproductfirstreal ge_balance_negative_rectangle_last_rowfoundquotientproductfirstreal. (((((ge_representation_real_code_rectangle_last_rowfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_last_rowfoundquotientproductfirstreal) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_last_rowfoundquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductfirstreal) = S ge_signed_half_rectangle_last_rowfoundquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_last_rowfoundquotientproduct) + ge_balance_negative_rectangle_last_rowfoundquotientproductfirstreal = (ge_first_rn_rectangle_last_rowfoundquotientproduct) + ge_balance_positive_rectangle_last_rowfoundquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundquotientproductfirstimaginary ge_balance_negative_rectangle_last_rowfoundquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst) = 2 * (ge_balance_positive_rectangle_last_rowfoundquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductfirst) = 2 * ge_signed_half_rectangle_last_rowfoundquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductfirstimaginary) = S ge_signed_half_rectangle_last_rowfoundquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_last_rowfoundquotientproduct) + ge_balance_negative_rectangle_last_rowfoundquotientproductfirstimaginary = (ge_first_in_rectangle_last_rowfoundquotientproduct) + ge_balance_positive_rectangle_last_rowfoundquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_last_rowfoundquotientproductsecond ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond. (((gr_quotient_rectangle_last_rowfoundquotient) = ((ge_representation_real_code_rectangle_last_rowfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond)) * S ((ge_representation_real_code_rectangle_last_rowfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundquotientproductsecondreal ge_balance_negative_rectangle_last_rowfoundquotientproductsecondreal. (((((ge_representation_real_code_rectangle_last_rowfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_last_rowfoundquotientproductsecondreal) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_last_rowfoundquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductsecondreal) = S ge_signed_half_rectangle_last_rowfoundquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_last_rowfoundquotientproduct) + ge_balance_negative_rectangle_last_rowfoundquotientproductsecondreal = (ge_second_rn_rectangle_last_rowfoundquotientproduct) + ge_balance_positive_rectangle_last_rowfoundquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundquotientproductsecondimaginary ge_balance_negative_rectangle_last_rowfoundquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond) = 2 * (ge_balance_positive_rectangle_last_rowfoundquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductsecond) = 2 * ge_signed_half_rectangle_last_rowfoundquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductsecondimaginary) = S ge_signed_half_rectangle_last_rowfoundquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_last_rowfoundquotientproduct) + ge_balance_negative_rectangle_last_rowfoundquotientproductsecondimaginary = (ge_second_in_rectangle_last_rowfoundquotientproduct) + ge_balance_positive_rectangle_last_rowfoundquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_last_rowfoundquotientproductoutput ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_last_rowfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput)) * S ((ge_representation_real_code_rectangle_last_rowfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput) + (ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundquotientproductoutputreal ge_balance_negative_rectangle_last_rowfoundquotientproductoutputreal. (((((ge_representation_real_code_rectangle_last_rowfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_last_rowfoundquotientproductoutputreal) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_last_rowfoundquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductoutputreal) = S ge_signed_half_rectangle_last_rowfoundquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_last_rowfoundquotientproduct) * (ge_second_rp_rectangle_last_rowfoundquotientproduct))) + (((ge_first_rn_rectangle_last_rowfoundquotientproduct) * (ge_second_rn_rectangle_last_rowfoundquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowfoundquotientproduct) * (ge_second_in_rectangle_last_rowfoundquotientproduct))) + (((ge_first_in_rectangle_last_rowfoundquotientproduct) * (ge_second_ip_rectangle_last_rowfoundquotientproduct))))))) + ge_balance_negative_rectangle_last_rowfoundquotientproductoutputreal = (((((((ge_first_rp_rectangle_last_rowfoundquotientproduct) * (ge_second_rn_rectangle_last_rowfoundquotientproduct))) + (((ge_first_rn_rectangle_last_rowfoundquotientproduct) * (ge_second_rp_rectangle_last_rowfoundquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowfoundquotientproduct) * (ge_second_ip_rectangle_last_rowfoundquotientproduct))) + (((ge_first_in_rectangle_last_rowfoundquotientproduct) * (ge_second_in_rectangle_last_rowfoundquotientproduct))))))) + ge_balance_positive_rectangle_last_rowfoundquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundquotientproductoutputimaginary ge_balance_negative_rectangle_last_rowfoundquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput) = 2 * (ge_balance_positive_rectangle_last_rowfoundquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundquotientproductoutput) = 2 * ge_signed_half_rectangle_last_rowfoundquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundquotientproductoutputimaginary) = S ge_signed_half_rectangle_last_rowfoundquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_last_rowfoundquotientproduct) * (ge_second_ip_rectangle_last_rowfoundquotientproduct))) + (((ge_first_rn_rectangle_last_rowfoundquotientproduct) * (ge_second_in_rectangle_last_rowfoundquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowfoundquotientproduct) * (ge_second_rp_rectangle_last_rowfoundquotientproduct))) + (((ge_first_in_rectangle_last_rowfoundquotientproduct) * (ge_second_rn_rectangle_last_rowfoundquotientproduct))))))) + ge_balance_negative_rectangle_last_rowfoundquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_last_rowfoundquotientproduct) * (ge_second_in_rectangle_last_rowfoundquotientproduct))) + (((ge_first_rn_rectangle_last_rowfoundquotientproduct) * (ge_second_ip_rectangle_last_rowfoundquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowfoundquotientproduct) * (ge_second_rn_rectangle_last_rowfoundquotientproduct))) + (((ge_first_in_rectangle_last_rowfoundquotientproduct) * (ge_second_rp_rectangle_last_rowfoundquotientproduct))))))) + ge_balance_positive_rectangle_last_rowfoundquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_last_rowfound. ((exists ge_norm_rp_rectangle_last_rowfoundnorm ge_norm_rn_rectangle_last_rowfoundnorm ge_norm_ip_rectangle_last_rowfoundnorm ge_norm_in_rectangle_last_rowfoundnorm. ((exists ge_representation_real_code_rectangle_last_rowfoundnormrepresentation ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation. (((((h) + (gr_row_coordinate_rectangle_last_row)) * S ((h) + (gr_row_coordinate_rectangle_last_row)) + ((gr_row_coordinate_rectangle_last_row) + (gr_row_coordinate_rectangle_last_row))) = ((ge_representation_real_code_rectangle_last_rowfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation)) * S ((ge_representation_real_code_rectangle_last_rowfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation) + (ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_last_rowfoundnormrepresentationreal ge_balance_negative_rectangle_last_rowfoundnormrepresentationreal. (((((ge_representation_real_code_rectangle_last_rowfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_last_rowfoundnormrepresentationreal) /\ (ge_balance_negative_rectangle_last_rowfoundnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_last_rowfoundnormrepresentation) = 2 * ge_signed_half_rectangle_last_rowfoundnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnormrepresentationreal) = S ge_signed_half_rectangle_last_rowfoundnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_last_rowfoundnorm) + ge_balance_negative_rectangle_last_rowfoundnormrepresentationreal = (ge_norm_rn_rectangle_last_rowfoundnorm) + ge_balance_positive_rectangle_last_rowfoundnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_last_rowfoundnormrepresentationimaginary ge_balance_negative_rectangle_last_rowfoundnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation) = 2 * (ge_balance_positive_rectangle_last_rowfoundnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_last_rowfoundnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowfoundnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowfoundnormrepresentation) = 2 * ge_signed_half_rectangle_last_rowfoundnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowfoundnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowfoundnormrepresentationimaginary) = S ge_signed_half_rectangle_last_rowfoundnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_last_rowfoundnorm) + ge_balance_negative_rectangle_last_rowfoundnormrepresentationimaginary = (ge_norm_in_rectangle_last_rowfoundnorm) + ge_balance_positive_rectangle_last_rowfoundnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_last_rowfoundnormsquare ge_imaginary_square_rectangle_last_rowfoundnormsquare. ((((((ge_norm_rp_rectangle_last_rowfoundnorm) * (ge_norm_rp_rectangle_last_rowfoundnorm))) + (((ge_norm_rn_rectangle_last_rowfoundnorm) * (ge_norm_rn_rectangle_last_rowfoundnorm)))) = ((ge_real_square_rectangle_last_rowfoundnormsquare) + (((((ge_norm_rp_rectangle_last_rowfoundnorm) * (ge_norm_rn_rectangle_last_rowfoundnorm))) + (((ge_norm_rn_rectangle_last_rowfoundnorm) * (ge_norm_rp_rectangle_last_rowfoundnorm))))))) /\ ((((((ge_norm_ip_rectangle_last_rowfoundnorm) * (ge_norm_ip_rectangle_last_rowfoundnorm))) + (((ge_norm_in_rectangle_last_rowfoundnorm) * (ge_norm_in_rectangle_last_rowfoundnorm)))) = ((ge_imaginary_square_rectangle_last_rowfoundnormsquare) + (((((ge_norm_ip_rectangle_last_rowfoundnorm) * (ge_norm_in_rectangle_last_rowfoundnorm))) + (((ge_norm_in_rectangle_last_rowfoundnorm) * (ge_norm_ip_rectangle_last_rowfoundnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_last_rowfound) = ge_real_square_rectangle_last_rowfoundnormsquare + ge_imaginary_square_rectangle_last_rowfoundnormsquare)))))) /\ (exists ge_gap_rectangle_last_rowfoundstrict. ge_gap_rectangle_last_rowfoundstrict + S (gr_proper_divisor_norm_rectangle_last_rowfound) = (N))))))))) \/ (forall gr_row_coordinate_rectangle_last_row. (exists ge_gap_rectangle_last_rowabsent_index. ge_gap_rectangle_last_rowabsent_index + S (gr_row_coordinate_rectangle_last_row) = (k)) -> ~(((~(exists gr_inverse_rectangle_last_rowabsentnonunit. (exists ge_first_rp_rectangle_last_rowabsentnonunitidentity ge_first_rn_rectangle_last_rowabsentnonunitidentity ge_first_ip_rectangle_last_rowabsentnonunitidentity ge_first_in_rectangle_last_rowabsentnonunitidentity ge_second_rp_rectangle_last_rowabsentnonunitidentity ge_second_rn_rectangle_last_rowabsentnonunitidentity ge_second_ip_rectangle_last_rowabsentnonunitidentity ge_second_in_rectangle_last_rowabsentnonunitidentity. ((exists ge_representation_real_code_rectangle_last_rowabsentnonunitidentityfirst ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst. (((((h) + (gr_row_coordinate_rectangle_last_row)) * S ((h) + (gr_row_coordinate_rectangle_last_row)) + ((gr_row_coordinate_rectangle_last_row) + (gr_row_coordinate_rectangle_last_row))) = ((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst)) * S ((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstreal ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstreal. (((((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstreal) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnonunitidentityfirstrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_last_rowabsentnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstreal) = S ge_signed_half_rectangle_last_rowabsentnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_rectangle_last_rowabsentnonunitidentity) + ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstreal = (ge_first_rn_rectangle_last_rowabsentnonunitidentity) + ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstimaginary ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst) = 2 * (ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityfirst) = 2 * ge_signed_half_rectangle_last_rowabsentnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstimaginary) = S ge_signed_half_rectangle_last_rowabsentnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_last_rowabsentnonunitidentity) + ge_balance_negative_rectangle_last_rowabsentnonunitidentityfirstimaginary = (ge_first_in_rectangle_last_rowabsentnonunitidentity) + ge_balance_positive_rectangle_last_rowabsentnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_last_rowabsentnonunitidentitysecond ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond. (((gr_inverse_rectangle_last_rowabsentnonunit) = ((ge_representation_real_code_rectangle_last_rowabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond)) * S ((ge_representation_real_code_rectangle_last_rowabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondreal ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondreal. (((((ge_representation_real_code_rectangle_last_rowabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondreal) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnonunitidentitysecondrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_last_rowabsentnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondreal) = S ge_signed_half_rectangle_last_rowabsentnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_rectangle_last_rowabsentnonunitidentity) + ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondreal = (ge_second_rn_rectangle_last_rowabsentnonunitidentity) + ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondimaginary ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond) = 2 * (ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentitysecond) = 2 * ge_signed_half_rectangle_last_rowabsentnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondimaginary) = S ge_signed_half_rectangle_last_rowabsentnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_rectangle_last_rowabsentnonunitidentity) + ge_balance_negative_rectangle_last_rowabsentnonunitidentitysecondimaginary = (ge_second_in_rectangle_last_rowabsentnonunitidentity) + ge_balance_positive_rectangle_last_rowabsentnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_last_rowabsentnonunitidentityoutput ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput. (((6) = ((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput)) * S ((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput) + (ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputreal ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputreal. (((((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputreal) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnonunitidentityoutputrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_last_rowabsentnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputreal) = S ge_signed_half_rectangle_last_rowabsentnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_last_rowabsentnonunitidentity) * (ge_second_rp_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_rn_rectangle_last_rowabsentnonunitidentity) * (ge_second_rn_rectangle_last_rowabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowabsentnonunitidentity) * (ge_second_in_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_in_rectangle_last_rowabsentnonunitidentity) * (ge_second_ip_rectangle_last_rowabsentnonunitidentity))))))) + ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputreal = (((((((ge_first_rp_rectangle_last_rowabsentnonunitidentity) * (ge_second_rn_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_rn_rectangle_last_rowabsentnonunitidentity) * (ge_second_rp_rectangle_last_rowabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowabsentnonunitidentity) * (ge_second_ip_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_in_rectangle_last_rowabsentnonunitidentity) * (ge_second_in_rectangle_last_rowabsentnonunitidentity))))))) + ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputimaginary ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput) = 2 * (ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentnonunitidentityoutput) = 2 * ge_signed_half_rectangle_last_rowabsentnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputimaginary) = S ge_signed_half_rectangle_last_rowabsentnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_last_rowabsentnonunitidentity) * (ge_second_ip_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_rn_rectangle_last_rowabsentnonunitidentity) * (ge_second_in_rectangle_last_rowabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowabsentnonunitidentity) * (ge_second_rp_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_in_rectangle_last_rowabsentnonunitidentity) * (ge_second_rn_rectangle_last_rowabsentnonunitidentity))))))) + ge_balance_negative_rectangle_last_rowabsentnonunitidentityoutputimaginary = (((((((ge_first_rp_rectangle_last_rowabsentnonunitidentity) * (ge_second_in_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_rn_rectangle_last_rowabsentnonunitidentity) * (ge_second_ip_rectangle_last_rowabsentnonunitidentity))))) + (((((ge_first_ip_rectangle_last_rowabsentnonunitidentity) * (ge_second_rn_rectangle_last_rowabsentnonunitidentity))) + (((ge_first_in_rectangle_last_rowabsentnonunitidentity) * (ge_second_rp_rectangle_last_rowabsentnonunitidentity))))))) + ge_balance_positive_rectangle_last_rowabsentnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_rectangle_last_rowabsentquotient. (exists ge_first_rp_rectangle_last_rowabsentquotientproduct ge_first_rn_rectangle_last_rowabsentquotientproduct ge_first_ip_rectangle_last_rowabsentquotientproduct ge_first_in_rectangle_last_rowabsentquotientproduct ge_second_rp_rectangle_last_rowabsentquotientproduct ge_second_rn_rectangle_last_rowabsentquotientproduct ge_second_ip_rectangle_last_rowabsentquotientproduct ge_second_in_rectangle_last_rowabsentquotientproduct. ((exists ge_representation_real_code_rectangle_last_rowabsentquotientproductfirst ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst. (((((h) + (gr_row_coordinate_rectangle_last_row)) * S ((h) + (gr_row_coordinate_rectangle_last_row)) + ((gr_row_coordinate_rectangle_last_row) + (gr_row_coordinate_rectangle_last_row))) = ((ge_representation_real_code_rectangle_last_rowabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst)) * S ((ge_representation_real_code_rectangle_last_rowabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentquotientproductfirstreal ge_balance_negative_rectangle_last_rowabsentquotientproductfirstreal. (((((ge_representation_real_code_rectangle_last_rowabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_last_rowabsentquotientproductfirstreal) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductfirstreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentquotientproductfirstrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_last_rowabsentquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentquotientproductfirstreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductfirstreal) = S ge_signed_half_rectangle_last_rowabsentquotientproductfirstrealdecode))) /\ ((ge_first_rp_rectangle_last_rowabsentquotientproduct) + ge_balance_negative_rectangle_last_rowabsentquotientproductfirstreal = (ge_first_rn_rectangle_last_rowabsentquotientproduct) + ge_balance_positive_rectangle_last_rowabsentquotientproductfirstreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentquotientproductfirstimaginary ge_balance_negative_rectangle_last_rowabsentquotientproductfirstimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst) = 2 * (ge_balance_positive_rectangle_last_rowabsentquotientproductfirstimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductfirst) = 2 * ge_signed_half_rectangle_last_rowabsentquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductfirstimaginary) = S ge_signed_half_rectangle_last_rowabsentquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_rectangle_last_rowabsentquotientproduct) + ge_balance_negative_rectangle_last_rowabsentquotientproductfirstimaginary = (ge_first_in_rectangle_last_rowabsentquotientproduct) + ge_balance_positive_rectangle_last_rowabsentquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_rectangle_last_rowabsentquotientproductsecond ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond. (((gr_quotient_rectangle_last_rowabsentquotient) = ((ge_representation_real_code_rectangle_last_rowabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond)) * S ((ge_representation_real_code_rectangle_last_rowabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentquotientproductsecondreal ge_balance_negative_rectangle_last_rowabsentquotientproductsecondreal. (((((ge_representation_real_code_rectangle_last_rowabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_last_rowabsentquotientproductsecondreal) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductsecondreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentquotientproductsecondrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_last_rowabsentquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentquotientproductsecondreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductsecondreal) = S ge_signed_half_rectangle_last_rowabsentquotientproductsecondrealdecode))) /\ ((ge_second_rp_rectangle_last_rowabsentquotientproduct) + ge_balance_negative_rectangle_last_rowabsentquotientproductsecondreal = (ge_second_rn_rectangle_last_rowabsentquotientproduct) + ge_balance_positive_rectangle_last_rowabsentquotientproductsecondreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentquotientproductsecondimaginary ge_balance_negative_rectangle_last_rowabsentquotientproductsecondimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond) = 2 * (ge_balance_positive_rectangle_last_rowabsentquotientproductsecondimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductsecond) = 2 * ge_signed_half_rectangle_last_rowabsentquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductsecondimaginary) = S ge_signed_half_rectangle_last_rowabsentquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_rectangle_last_rowabsentquotientproduct) + ge_balance_negative_rectangle_last_rowabsentquotientproductsecondimaginary = (ge_second_in_rectangle_last_rowabsentquotientproduct) + ge_balance_positive_rectangle_last_rowabsentquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_rectangle_last_rowabsentquotientproductoutput ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput. (((z) = ((ge_representation_real_code_rectangle_last_rowabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput)) * S ((ge_representation_real_code_rectangle_last_rowabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput) + (ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentquotientproductoutputreal ge_balance_negative_rectangle_last_rowabsentquotientproductoutputreal. (((((ge_representation_real_code_rectangle_last_rowabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_last_rowabsentquotientproductoutputreal) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductoutputreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentquotientproductoutputrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_last_rowabsentquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentquotientproductoutputreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductoutputreal) = S ge_signed_half_rectangle_last_rowabsentquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_rectangle_last_rowabsentquotientproduct) * (ge_second_rp_rectangle_last_rowabsentquotientproduct))) + (((ge_first_rn_rectangle_last_rowabsentquotientproduct) * (ge_second_rn_rectangle_last_rowabsentquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowabsentquotientproduct) * (ge_second_in_rectangle_last_rowabsentquotientproduct))) + (((ge_first_in_rectangle_last_rowabsentquotientproduct) * (ge_second_ip_rectangle_last_rowabsentquotientproduct))))))) + ge_balance_negative_rectangle_last_rowabsentquotientproductoutputreal = (((((((ge_first_rp_rectangle_last_rowabsentquotientproduct) * (ge_second_rn_rectangle_last_rowabsentquotientproduct))) + (((ge_first_rn_rectangle_last_rowabsentquotientproduct) * (ge_second_rp_rectangle_last_rowabsentquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowabsentquotientproduct) * (ge_second_ip_rectangle_last_rowabsentquotientproduct))) + (((ge_first_in_rectangle_last_rowabsentquotientproduct) * (ge_second_in_rectangle_last_rowabsentquotientproduct))))))) + ge_balance_positive_rectangle_last_rowabsentquotientproductoutputreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentquotientproductoutputimaginary ge_balance_negative_rectangle_last_rowabsentquotientproductoutputimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput) = 2 * (ge_balance_positive_rectangle_last_rowabsentquotientproductoutputimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentquotientproductoutput) = 2 * ge_signed_half_rectangle_last_rowabsentquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentquotientproductoutputimaginary) = S ge_signed_half_rectangle_last_rowabsentquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_rectangle_last_rowabsentquotientproduct) * (ge_second_ip_rectangle_last_rowabsentquotientproduct))) + (((ge_first_rn_rectangle_last_rowabsentquotientproduct) * (ge_second_in_rectangle_last_rowabsentquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowabsentquotientproduct) * (ge_second_rp_rectangle_last_rowabsentquotientproduct))) + (((ge_first_in_rectangle_last_rowabsentquotientproduct) * (ge_second_rn_rectangle_last_rowabsentquotientproduct))))))) + ge_balance_negative_rectangle_last_rowabsentquotientproductoutputimaginary = (((((((ge_first_rp_rectangle_last_rowabsentquotientproduct) * (ge_second_in_rectangle_last_rowabsentquotientproduct))) + (((ge_first_rn_rectangle_last_rowabsentquotientproduct) * (ge_second_ip_rectangle_last_rowabsentquotientproduct))))) + (((((ge_first_ip_rectangle_last_rowabsentquotientproduct) * (ge_second_rn_rectangle_last_rowabsentquotientproduct))) + (((ge_first_in_rectangle_last_rowabsentquotientproduct) * (ge_second_rp_rectangle_last_rowabsentquotientproduct))))))) + ge_balance_positive_rectangle_last_rowabsentquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_rectangle_last_rowabsent. ((exists ge_norm_rp_rectangle_last_rowabsentnorm ge_norm_rn_rectangle_last_rowabsentnorm ge_norm_ip_rectangle_last_rowabsentnorm ge_norm_in_rectangle_last_rowabsentnorm. ((exists ge_representation_real_code_rectangle_last_rowabsentnormrepresentation ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation. (((((h) + (gr_row_coordinate_rectangle_last_row)) * S ((h) + (gr_row_coordinate_rectangle_last_row)) + ((gr_row_coordinate_rectangle_last_row) + (gr_row_coordinate_rectangle_last_row))) = ((ge_representation_real_code_rectangle_last_rowabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation)) * S ((ge_representation_real_code_rectangle_last_rowabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation)) + ((ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation) + (ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation))) /\ ((exists ge_balance_positive_rectangle_last_rowabsentnormrepresentationreal ge_balance_negative_rectangle_last_rowabsentnormrepresentationreal. (((((ge_representation_real_code_rectangle_last_rowabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_last_rowabsentnormrepresentationreal) /\ (ge_balance_negative_rectangle_last_rowabsentnormrepresentationreal) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnormrepresentationrealdecode. (((ge_representation_real_code_rectangle_last_rowabsentnormrepresentation) = 2 * ge_signed_half_rectangle_last_rowabsentnormrepresentationrealdecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnormrepresentationreal) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnormrepresentationreal) = S ge_signed_half_rectangle_last_rowabsentnormrepresentationrealdecode))) /\ ((ge_norm_rp_rectangle_last_rowabsentnorm) + ge_balance_negative_rectangle_last_rowabsentnormrepresentationreal = (ge_norm_rn_rectangle_last_rowabsentnorm) + ge_balance_positive_rectangle_last_rowabsentnormrepresentationreal))) /\ (exists ge_balance_positive_rectangle_last_rowabsentnormrepresentationimaginary ge_balance_negative_rectangle_last_rowabsentnormrepresentationimaginary. (((((ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation) = 2 * (ge_balance_positive_rectangle_last_rowabsentnormrepresentationimaginary) /\ (ge_balance_negative_rectangle_last_rowabsentnormrepresentationimaginary) = 0) \/ exists ge_signed_half_rectangle_last_rowabsentnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_rectangle_last_rowabsentnormrepresentation) = 2 * ge_signed_half_rectangle_last_rowabsentnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_rectangle_last_rowabsentnormrepresentationimaginary) = 0) /\ (ge_balance_negative_rectangle_last_rowabsentnormrepresentationimaginary) = S ge_signed_half_rectangle_last_rowabsentnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_rectangle_last_rowabsentnorm) + ge_balance_negative_rectangle_last_rowabsentnormrepresentationimaginary = (ge_norm_in_rectangle_last_rowabsentnorm) + ge_balance_positive_rectangle_last_rowabsentnormrepresentationimaginary)))))) /\ (exists ge_real_square_rectangle_last_rowabsentnormsquare ge_imaginary_square_rectangle_last_rowabsentnormsquare. ((((((ge_norm_rp_rectangle_last_rowabsentnorm) * (ge_norm_rp_rectangle_last_rowabsentnorm))) + (((ge_norm_rn_rectangle_last_rowabsentnorm) * (ge_norm_rn_rectangle_last_rowabsentnorm)))) = ((ge_real_square_rectangle_last_rowabsentnormsquare) + (((((ge_norm_rp_rectangle_last_rowabsentnorm) * (ge_norm_rn_rectangle_last_rowabsentnorm))) + (((ge_norm_rn_rectangle_last_rowabsentnorm) * (ge_norm_rp_rectangle_last_rowabsentnorm))))))) /\ ((((((ge_norm_ip_rectangle_last_rowabsentnorm) * (ge_norm_ip_rectangle_last_rowabsentnorm))) + (((ge_norm_in_rectangle_last_rowabsentnorm) * (ge_norm_in_rectangle_last_rowabsentnorm)))) = ((ge_imaginary_square_rectangle_last_rowabsentnormsquare) + (((((ge_norm_ip_rectangle_last_rowabsentnorm) * (ge_norm_in_rectangle_last_rowabsentnorm))) + (((ge_norm_in_rectangle_last_rowabsentnorm) * (ge_norm_ip_rectangle_last_rowabsentnorm))))))) /\ ((gr_proper_divisor_norm_rectangle_last_rowabsent) = ge_real_square_rectangle_last_rowabsentnormsquare + ge_imaginary_square_rectangle_last_rowabsentnormsquare)))))) /\ (exists ge_gap_rectangle_last_rowabsentstrict. ge_gap_rectangle_last_rowabsentstrict + S (gr_proper_divisor_norm_rectangle_last_rowabsent) = (N))))))))) - 0045
specialize gaussian_factor_search_coordinate_row (k) - 0046
specialize gaussian_factor_search_coordinate_row (z) - 0047
specialize gaussian_factor_search_coordinate_row (N) - 0048
specialize gaussian_factor_search_coordinate_row (h) - 0049
apply gaussian_factor_search_coordinate_row - 0050
exact hz - 0051
cases hlast - 0052
cases hlast_left - 0053
cases hlast_left_witness - 0054
left - 0055
exists (h) - 0056
exists (x) - 0057
split - 0058
exists 0 - 0059
apply zero_add - 0060
split - 0061
exact hlast_left_witness_left - 0062
exact hlast_left_witness_right - 0063
right - 0064
intro rc - 0065
intro ic - 0066
intro hr - 0067
intro hi - 0068
intro hp - 0069
have hc : rc=h \/ (exists ge_gap_rectangle_previous_index. ge_gap_rectangle_previous_index + S (rc) = (h)) - 0070
specialize finite_lt_succ_eq_or_lt (h) - 0071
specialize finite_lt_succ_eq_or_lt (rc) - 0072
apply finite_lt_succ_eq_or_lt - 0073
exact hr - 0074
cases hc - 0075
specialize hlast_right (ic) - 0076
apply hlast_right - 0077
exact hi - 0078
specialize gaussian_search_proper_divisor_code_transport (((rc) + (ic)) * S ((rc) + (ic)) + ((ic) + (ic))) - 0079
specialize gaussian_search_proper_divisor_code_transport (((h) + (ic)) * S ((h) + (ic)) + ((ic) + (ic))) - 0080
specialize gaussian_search_proper_divisor_code_transport (z) - 0081
specialize gaussian_search_proper_divisor_code_transport (N) - 0082
apply gaussian_search_proper_divisor_code_transport - 0083
rewrite hc_left - 0084
rewrite hc_left - 0085
refl - 0086
exact hp - 0087
specialize hprevious_right (rc) - 0088
specialize hprevious_right (ic) - 0089
apply hprevious_right - 0090
exact hc_right - 0091
exact hi - 0092
exact hp