gaussian_unit_iff_norm_one

Exact expanded first-order arithmetic statement

forall z N. (exists ge_norm_rp_unit_iff_norm ge_norm_rn_unit_iff_norm ge_norm_ip_unit_iff_norm ge_norm_in_unit_iff_norm. ((exists ge_representation_real_code_unit_iff_normrepresentation ge_representation_imaginary_code_unit_iff_normrepresentation. (((z) = ((ge_representation_real_code_unit_iff_normrepresentation) + (ge_representation_imaginary_code_unit_iff_normrepresentation)) * S ((ge_representation_real_code_unit_iff_normrepresentation) + (ge_representation_imaginary_code_unit_iff_normrepresentation)) + ((ge_representation_imaginary_code_unit_iff_normrepresentation) + (ge_representation_imaginary_code_unit_iff_normrepresentation))) /\ ((exists ge_balance_positive_unit_iff_normrepresentationreal ge_balance_negative_unit_iff_normrepresentationreal. (((((ge_representation_real_code_unit_iff_normrepresentation) = 2 * (ge_balance_positive_unit_iff_normrepresentationreal) /\ (ge_balance_negative_unit_iff_normrepresentationreal) = 0) \/ exists ge_signed_half_unit_iff_normrepresentationrealdecode. (((ge_representation_real_code_unit_iff_normrepresentation) = 2 * ge_signed_half_unit_iff_normrepresentationrealdecode + 1 /\ (ge_balance_positive_unit_iff_normrepresentationreal) = 0) /\ (ge_balance_negative_unit_iff_normrepresentationreal) = S ge_signed_half_unit_iff_normrepresentationrealdecode))) /\ ((ge_norm_rp_unit_iff_norm) + ge_balance_negative_unit_iff_normrepresentationreal = (ge_norm_rn_unit_iff_norm) + ge_balance_positive_unit_iff_normrepresentationreal))) /\ (exists ge_balance_positive_unit_iff_normrepresentationimaginary ge_balance_negative_unit_iff_normrepresentationimaginary. (((((ge_representation_imaginary_code_unit_iff_normrepresentation) = 2 * (ge_balance_positive_unit_iff_normrepresentationimaginary) /\ (ge_balance_negative_unit_iff_normrepresentationimaginary) = 0) \/ exists ge_signed_half_unit_iff_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_unit_iff_normrepresentation) = 2 * ge_signed_half_unit_iff_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_normrepresentationimaginary) = 0) /\ (ge_balance_negative_unit_iff_normrepresentationimaginary) = S ge_signed_half_unit_iff_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_unit_iff_norm) + ge_balance_negative_unit_iff_normrepresentationimaginary = (ge_norm_in_unit_iff_norm) + ge_balance_positive_unit_iff_normrepresentationimaginary)))))) /\ (exists ge_real_square_unit_iff_normsquare ge_imaginary_square_unit_iff_normsquare. ((((((ge_norm_rp_unit_iff_norm) * (ge_norm_rp_unit_iff_norm))) + (((ge_norm_rn_unit_iff_norm) * (ge_norm_rn_unit_iff_norm)))) = ((ge_real_square_unit_iff_normsquare) + (((((ge_norm_rp_unit_iff_norm) * (ge_norm_rn_unit_iff_norm))) + (((ge_norm_rn_unit_iff_norm) * (ge_norm_rp_unit_iff_norm))))))) /\ ((((((ge_norm_ip_unit_iff_norm) * (ge_norm_ip_unit_iff_norm))) + (((ge_norm_in_unit_iff_norm) * (ge_norm_in_unit_iff_norm)))) = ((ge_imaginary_square_unit_iff_normsquare) + (((((ge_norm_ip_unit_iff_norm) * (ge_norm_in_unit_iff_norm))) + (((ge_norm_in_unit_iff_norm) * (ge_norm_ip_unit_iff_norm))))))) /\ ((N) = ge_real_square_unit_iff_normsquare + ge_imaginary_square_unit_iff_normsquare)))))) -> (((exists gr_inverse_unit_iff_forward. (exists ge_first_rp_unit_iff_forwardidentity ge_first_rn_unit_iff_forwardidentity ge_first_ip_unit_iff_forwardidentity ge_first_in_unit_iff_forwardidentity ge_second_rp_unit_iff_forwardidentity ge_second_rn_unit_iff_forwardidentity ge_second_ip_unit_iff_forwardidentity ge_second_in_unit_iff_forwardidentity. ((exists ge_representation_real_code_unit_iff_forwardidentityfirst ge_representation_imaginary_code_unit_iff_forwardidentityfirst. (((z) = ((ge_representation_real_code_unit_iff_forwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_forwardidentityfirst)) * S ((ge_representation_real_code_unit_iff_forwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_forwardidentityfirst)) + ((ge_representation_imaginary_code_unit_iff_forwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_forwardidentityfirst))) /\ ((exists ge_balance_positive_unit_iff_forwardidentityfirstreal ge_balance_negative_unit_iff_forwardidentityfirstreal. (((((ge_representation_real_code_unit_iff_forwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_forwardidentityfirstreal) /\ (ge_balance_negative_unit_iff_forwardidentityfirstreal) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityfirstrealdecode. (((ge_representation_real_code_unit_iff_forwardidentityfirst) = 2 * ge_signed_half_unit_iff_forwardidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityfirstreal) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityfirstreal) = S ge_signed_half_unit_iff_forwardidentityfirstrealdecode))) /\ ((ge_first_rp_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentityfirstreal = (ge_first_rn_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentityfirstreal))) /\ (exists ge_balance_positive_unit_iff_forwardidentityfirstimaginary ge_balance_negative_unit_iff_forwardidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_iff_forwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_forwardidentityfirstimaginary) /\ (ge_balance_negative_unit_iff_forwardidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_iff_forwardidentityfirst) = 2 * ge_signed_half_unit_iff_forwardidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityfirstimaginary) = S ge_signed_half_unit_iff_forwardidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentityfirstimaginary = (ge_first_in_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_iff_forwardidentitysecond ge_representation_imaginary_code_unit_iff_forwardidentitysecond. (((gr_inverse_unit_iff_forward) = ((ge_representation_real_code_unit_iff_forwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_forwardidentitysecond)) * S ((ge_representation_real_code_unit_iff_forwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_forwardidentitysecond)) + ((ge_representation_imaginary_code_unit_iff_forwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_forwardidentitysecond))) /\ ((exists ge_balance_positive_unit_iff_forwardidentitysecondreal ge_balance_negative_unit_iff_forwardidentitysecondreal. (((((ge_representation_real_code_unit_iff_forwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_forwardidentitysecondreal) /\ (ge_balance_negative_unit_iff_forwardidentitysecondreal) = 0) \/ exists ge_signed_half_unit_iff_forwardidentitysecondrealdecode. (((ge_representation_real_code_unit_iff_forwardidentitysecond) = 2 * ge_signed_half_unit_iff_forwardidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentitysecondreal) = 0) /\ (ge_balance_negative_unit_iff_forwardidentitysecondreal) = S ge_signed_half_unit_iff_forwardidentitysecondrealdecode))) /\ ((ge_second_rp_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentitysecondreal = (ge_second_rn_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentitysecondreal))) /\ (exists ge_balance_positive_unit_iff_forwardidentitysecondimaginary ge_balance_negative_unit_iff_forwardidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_iff_forwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_forwardidentitysecondimaginary) /\ (ge_balance_negative_unit_iff_forwardidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_iff_forwardidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_iff_forwardidentitysecond) = 2 * ge_signed_half_unit_iff_forwardidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_iff_forwardidentitysecondimaginary) = S ge_signed_half_unit_iff_forwardidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentitysecondimaginary = (ge_second_in_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_iff_forwardidentityoutput ge_representation_imaginary_code_unit_iff_forwardidentityoutput. (((6) = ((ge_representation_real_code_unit_iff_forwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_forwardidentityoutput)) * S ((ge_representation_real_code_unit_iff_forwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_forwardidentityoutput)) + ((ge_representation_imaginary_code_unit_iff_forwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_forwardidentityoutput))) /\ ((exists ge_balance_positive_unit_iff_forwardidentityoutputreal ge_balance_negative_unit_iff_forwardidentityoutputreal. (((((ge_representation_real_code_unit_iff_forwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_forwardidentityoutputreal) /\ (ge_balance_negative_unit_iff_forwardidentityoutputreal) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityoutputrealdecode. (((ge_representation_real_code_unit_iff_forwardidentityoutput) = 2 * ge_signed_half_unit_iff_forwardidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityoutputreal) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityoutputreal) = S ge_signed_half_unit_iff_forwardidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))))))) + ge_balance_negative_unit_iff_forwardidentityoutputreal = (((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))))))) + ge_balance_positive_unit_iff_forwardidentityoutputreal))) /\ (exists ge_balance_positive_unit_iff_forwardidentityoutputimaginary ge_balance_negative_unit_iff_forwardidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_iff_forwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_forwardidentityoutputimaginary) /\ (ge_balance_negative_unit_iff_forwardidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_iff_forwardidentityoutput) = 2 * ge_signed_half_unit_iff_forwardidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityoutputimaginary) = S ge_signed_half_unit_iff_forwardidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))))))) + ge_balance_negative_unit_iff_forwardidentityoutputimaginary = (((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))))))) + ge_balance_positive_unit_iff_forwardidentityoutputimaginary)))))))))) -> N=1) /\ (N=1 -> (exists gr_inverse_unit_iff_backward. (exists ge_first_rp_unit_iff_backwardidentity ge_first_rn_unit_iff_backwardidentity ge_first_ip_unit_iff_backwardidentity ge_first_in_unit_iff_backwardidentity ge_second_rp_unit_iff_backwardidentity ge_second_rn_unit_iff_backwardidentity ge_second_ip_unit_iff_backwardidentity ge_second_in_unit_iff_backwardidentity. ((exists ge_representation_real_code_unit_iff_backwardidentityfirst ge_representation_imaginary_code_unit_iff_backwardidentityfirst. (((z) = ((ge_representation_real_code_unit_iff_backwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_backwardidentityfirst)) * S ((ge_representation_real_code_unit_iff_backwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_backwardidentityfirst)) + ((ge_representation_imaginary_code_unit_iff_backwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_backwardidentityfirst))) /\ ((exists ge_balance_positive_unit_iff_backwardidentityfirstreal ge_balance_negative_unit_iff_backwardidentityfirstreal. (((((ge_representation_real_code_unit_iff_backwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_backwardidentityfirstreal) /\ (ge_balance_negative_unit_iff_backwardidentityfirstreal) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityfirstrealdecode. (((ge_representation_real_code_unit_iff_backwardidentityfirst) = 2 * ge_signed_half_unit_iff_backwardidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityfirstreal) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityfirstreal) = S ge_signed_half_unit_iff_backwardidentityfirstrealdecode))) /\ ((ge_first_rp_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentityfirstreal = (ge_first_rn_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentityfirstreal))) /\ (exists ge_balance_positive_unit_iff_backwardidentityfirstimaginary ge_balance_negative_unit_iff_backwardidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_iff_backwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_backwardidentityfirstimaginary) /\ (ge_balance_negative_unit_iff_backwardidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_iff_backwardidentityfirst) = 2 * ge_signed_half_unit_iff_backwardidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityfirstimaginary) = S ge_signed_half_unit_iff_backwardidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentityfirstimaginary = (ge_first_in_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_iff_backwardidentitysecond ge_representation_imaginary_code_unit_iff_backwardidentitysecond. (((gr_inverse_unit_iff_backward) = ((ge_representation_real_code_unit_iff_backwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_backwardidentitysecond)) * S ((ge_representation_real_code_unit_iff_backwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_backwardidentitysecond)) + ((ge_representation_imaginary_code_unit_iff_backwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_backwardidentitysecond))) /\ ((exists ge_balance_positive_unit_iff_backwardidentitysecondreal ge_balance_negative_unit_iff_backwardidentitysecondreal. (((((ge_representation_real_code_unit_iff_backwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_backwardidentitysecondreal) /\ (ge_balance_negative_unit_iff_backwardidentitysecondreal) = 0) \/ exists ge_signed_half_unit_iff_backwardidentitysecondrealdecode. (((ge_representation_real_code_unit_iff_backwardidentitysecond) = 2 * ge_signed_half_unit_iff_backwardidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentitysecondreal) = 0) /\ (ge_balance_negative_unit_iff_backwardidentitysecondreal) = S ge_signed_half_unit_iff_backwardidentitysecondrealdecode))) /\ ((ge_second_rp_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentitysecondreal = (ge_second_rn_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentitysecondreal))) /\ (exists ge_balance_positive_unit_iff_backwardidentitysecondimaginary ge_balance_negative_unit_iff_backwardidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_iff_backwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_backwardidentitysecondimaginary) /\ (ge_balance_negative_unit_iff_backwardidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_iff_backwardidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_iff_backwardidentitysecond) = 2 * ge_signed_half_unit_iff_backwardidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_iff_backwardidentitysecondimaginary) = S ge_signed_half_unit_iff_backwardidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentitysecondimaginary = (ge_second_in_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_iff_backwardidentityoutput ge_representation_imaginary_code_unit_iff_backwardidentityoutput. (((6) = ((ge_representation_real_code_unit_iff_backwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_backwardidentityoutput)) * S ((ge_representation_real_code_unit_iff_backwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_backwardidentityoutput)) + ((ge_representation_imaginary_code_unit_iff_backwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_backwardidentityoutput))) /\ ((exists ge_balance_positive_unit_iff_backwardidentityoutputreal ge_balance_negative_unit_iff_backwardidentityoutputreal. (((((ge_representation_real_code_unit_iff_backwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_backwardidentityoutputreal) /\ (ge_balance_negative_unit_iff_backwardidentityoutputreal) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityoutputrealdecode. (((ge_representation_real_code_unit_iff_backwardidentityoutput) = 2 * ge_signed_half_unit_iff_backwardidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityoutputreal) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityoutputreal) = S ge_signed_half_unit_iff_backwardidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))))))) + ge_balance_negative_unit_iff_backwardidentityoutputreal = (((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))))))) + ge_balance_positive_unit_iff_backwardidentityoutputreal))) /\ (exists ge_balance_positive_unit_iff_backwardidentityoutputimaginary ge_balance_negative_unit_iff_backwardidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_iff_backwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_backwardidentityoutputimaginary) /\ (ge_balance_negative_unit_iff_backwardidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_iff_backwardidentityoutput) = 2 * ge_signed_half_unit_iff_backwardidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityoutputimaginary) = S ge_signed_half_unit_iff_backwardidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))))))) + ge_balance_negative_unit_iff_backwardidentityoutputimaginary = (((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))))))) + ge_balance_positive_unit_iff_backwardidentityoutputimaginary))))))))))))