gaussian_factor_matching_append

Exact expanded first-order arithmetic statement

forall b c d e u v U V l p q. (forall gr_match_index_append_matching_old gr_match_image_append_matching_old gr_match_source_append_matching_old gr_match_target_append_matching_old. (exists ge_gap_append_matching_oldindex. ge_gap_append_matching_oldindex + S (gr_match_index_append_matching_old) = (l)) -> (((exists ff_h_gprod_append_matching_oldmap. ff_h_gprod_append_matching_oldmap + S (gr_match_image_append_matching_old) = S ((S (gr_match_index_append_matching_old)) * v)) /\ exists ff_q_gprod_append_matching_oldmap. u = ff_q_gprod_append_matching_oldmap * S ((S (gr_match_index_append_matching_old)) * v) + (gr_match_image_append_matching_old))) -> (((exists ff_h_gprod_append_matching_oldsource. ff_h_gprod_append_matching_oldsource + S (gr_match_source_append_matching_old) = S ((S (gr_match_index_append_matching_old)) * c)) /\ exists ff_q_gprod_append_matching_oldsource. b = ff_q_gprod_append_matching_oldsource * S ((S (gr_match_index_append_matching_old)) * c) + (gr_match_source_append_matching_old))) -> (((exists ff_h_gprod_append_matching_oldtarget. ff_h_gprod_append_matching_oldtarget + S (gr_match_target_append_matching_old) = S ((S (gr_match_image_append_matching_old)) * e)) /\ exists ff_q_gprod_append_matching_oldtarget. d = ff_q_gprod_append_matching_oldtarget * S ((S (gr_match_image_append_matching_old)) * e) + (gr_match_target_append_matching_old))) -> (exists gr_unit_append_matching_oldunit_witness. ((exists gr_inverse_append_matching_oldunit_witnessunit. (exists ge_first_rp_append_matching_oldunit_witnessunitidentity ge_first_rn_append_matching_oldunit_witnessunitidentity ge_first_ip_append_matching_oldunit_witnessunitidentity ge_first_in_append_matching_oldunit_witnessunitidentity ge_second_rp_append_matching_oldunit_witnessunitidentity ge_second_rn_append_matching_oldunit_witnessunitidentity ge_second_ip_append_matching_oldunit_witnessunitidentity ge_second_in_append_matching_oldunit_witnessunitidentity. ((exists ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst. (((gr_unit_append_matching_oldunit_witness) = ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal) = S ge_signed_half_append_matching_oldunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal = (ge_first_rn_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary) = S ge_signed_half_append_matching_oldunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary = (ge_first_in_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond. (((gr_inverse_append_matching_oldunit_witnessunit) = ((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal) = S ge_signed_half_append_matching_oldunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal = (ge_second_rn_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary) = S ge_signed_half_append_matching_oldunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary = (ge_second_in_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal) = S ge_signed_half_append_matching_oldunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal = (((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary) = S ge_signed_half_append_matching_oldunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_append_matching_oldunit_witnesstransport ge_first_rn_append_matching_oldunit_witnesstransport ge_first_ip_append_matching_oldunit_witnesstransport ge_first_in_append_matching_oldunit_witnesstransport ge_second_rp_append_matching_oldunit_witnesstransport ge_second_rn_append_matching_oldunit_witnesstransport ge_second_ip_append_matching_oldunit_witnesstransport ge_second_in_append_matching_oldunit_witnesstransport. ((exists ge_representation_real_code_append_matching_oldunit_witnesstransportfirst ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst. (((gr_unit_append_matching_oldunit_witness) = ((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst)) * S ((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal. (((((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal) = S ge_signed_half_append_matching_oldunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal = (ge_first_rn_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary) = S ge_signed_half_append_matching_oldunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary = (ge_first_in_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_oldunit_witnesstransportsecond ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond. (((gr_match_source_append_matching_old) = ((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond)) * S ((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal. (((((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal) = S ge_signed_half_append_matching_oldunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal = (ge_second_rn_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary) = S ge_signed_half_append_matching_oldunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary = (ge_second_in_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_oldunit_witnesstransportoutput ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput. (((gr_match_target_append_matching_old) = ((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput)) * S ((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal. (((((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal) = S ge_signed_half_append_matching_oldunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))))))) + ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal = (((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))))))) + ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary) = S ge_signed_half_append_matching_oldunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))))))) + ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary = (((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))))))) + ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary)))))))))))) -> (((((exists ff_h_pfp_append_matching_extensionlast. ff_h_pfp_append_matching_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_append_matching_extensionlast. U = ff_q_pfp_append_matching_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_append_matching_extensionprefix pfp_a_append_matching_extensionprefix. (exists pfp_gap_append_matching_extensionprefixbound. pfp_gap_append_matching_extensionprefixbound + S (pfp_i_append_matching_extensionprefix) = (l)) -> (((exists ff_h_pfp_append_matching_extensionprefixold. ff_h_pfp_append_matching_extensionprefixold + S (pfp_a_append_matching_extensionprefix) = S ((S (pfp_i_append_matching_extensionprefix)) * v)) /\ exists ff_q_pfp_append_matching_extensionprefixold. u = ff_q_pfp_append_matching_extensionprefixold * S ((S (pfp_i_append_matching_extensionprefix)) * v) + (pfp_a_append_matching_extensionprefix))) -> (((exists ff_h_pfp_append_matching_extensionprefixnew. ff_h_pfp_append_matching_extensionprefixnew + S (pfp_a_append_matching_extensionprefix) = S ((S (pfp_i_append_matching_extensionprefix)) * V)) /\ exists ff_q_pfp_append_matching_extensionprefixnew. U = ff_q_pfp_append_matching_extensionprefixnew * S ((S (pfp_i_append_matching_extensionprefix)) * V) + (pfp_a_append_matching_extensionprefix)))))) -> (((exists ff_h_gprod_append_matching_source_last. ff_h_gprod_append_matching_source_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_gprod_append_matching_source_last. b = ff_q_gprod_append_matching_source_last * S ((S (l)) * c) + (p))) -> (((exists ff_h_gprod_append_matching_target_last. ff_h_gprod_append_matching_target_last + S (q) = S ((S (l)) * e)) /\ exists ff_q_gprod_append_matching_target_last. d = ff_q_gprod_append_matching_target_last * S ((S (l)) * e) + (q))) -> (exists gr_unit_append_matching_last_unit. ((exists gr_inverse_append_matching_last_unitunit. (exists ge_first_rp_append_matching_last_unitunitidentity ge_first_rn_append_matching_last_unitunitidentity ge_first_ip_append_matching_last_unitunitidentity ge_first_in_append_matching_last_unitunitidentity ge_second_rp_append_matching_last_unitunitidentity ge_second_rn_append_matching_last_unitunitidentity ge_second_ip_append_matching_last_unitunitidentity ge_second_in_append_matching_last_unitunitidentity. ((exists ge_representation_real_code_append_matching_last_unitunitidentityfirst ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst. (((gr_unit_append_matching_last_unit) = ((ge_representation_real_code_append_matching_last_unitunitidentityfirst) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst)) * S ((ge_representation_real_code_append_matching_last_unitunitidentityfirst) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst)) + ((ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst))) /\ ((exists ge_balance_positive_append_matching_last_unitunitidentityfirstreal ge_balance_negative_append_matching_last_unitunitidentityfirstreal. (((((ge_representation_real_code_append_matching_last_unitunitidentityfirst) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityfirstreal) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityfirstrealdecode. (((ge_representation_real_code_append_matching_last_unitunitidentityfirst) = 2 * ge_signed_half_append_matching_last_unitunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstreal) = S ge_signed_half_append_matching_last_unitunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentityfirstreal = (ge_first_rn_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentityfirstreal))) /\ (exists ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst) = 2 * ge_signed_half_append_matching_last_unitunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary) = S ge_signed_half_append_matching_last_unitunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary = (ge_first_in_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_last_unitunitidentitysecond ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond. (((gr_inverse_append_matching_last_unitunit) = ((ge_representation_real_code_append_matching_last_unitunitidentitysecond) + (ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond)) * S ((ge_representation_real_code_append_matching_last_unitunitidentitysecond) + (ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond)) + ((ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond) + (ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond))) /\ ((exists ge_balance_positive_append_matching_last_unitunitidentitysecondreal ge_balance_negative_append_matching_last_unitunitidentitysecondreal. (((((ge_representation_real_code_append_matching_last_unitunitidentitysecond) = 2 * (ge_balance_positive_append_matching_last_unitunitidentitysecondreal) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentitysecondrealdecode. (((ge_representation_real_code_append_matching_last_unitunitidentitysecond) = 2 * ge_signed_half_append_matching_last_unitunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondreal) = S ge_signed_half_append_matching_last_unitunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentitysecondreal = (ge_second_rn_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentitysecondreal))) /\ (exists ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond) = 2 * (ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond) = 2 * ge_signed_half_append_matching_last_unitunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary) = S ge_signed_half_append_matching_last_unitunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary = (ge_second_in_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_last_unitunitidentityoutput ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput. (((6) = ((ge_representation_real_code_append_matching_last_unitunitidentityoutput) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput)) * S ((ge_representation_real_code_append_matching_last_unitunitidentityoutput) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput)) + ((ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput))) /\ ((exists ge_balance_positive_append_matching_last_unitunitidentityoutputreal ge_balance_negative_append_matching_last_unitunitidentityoutputreal. (((((ge_representation_real_code_append_matching_last_unitunitidentityoutput) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityoutputreal) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityoutputrealdecode. (((ge_representation_real_code_append_matching_last_unitunitidentityoutput) = 2 * ge_signed_half_append_matching_last_unitunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputreal) = S ge_signed_half_append_matching_last_unitunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))))))) + ge_balance_negative_append_matching_last_unitunitidentityoutputreal = (((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))))))) + ge_balance_positive_append_matching_last_unitunitidentityoutputreal))) /\ (exists ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput) = 2 * ge_signed_half_append_matching_last_unitunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary) = S ge_signed_half_append_matching_last_unitunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))))))) + ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary = (((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))))))) + ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_append_matching_last_unittransport ge_first_rn_append_matching_last_unittransport ge_first_ip_append_matching_last_unittransport ge_first_in_append_matching_last_unittransport ge_second_rp_append_matching_last_unittransport ge_second_rn_append_matching_last_unittransport ge_second_ip_append_matching_last_unittransport ge_second_in_append_matching_last_unittransport. ((exists ge_representation_real_code_append_matching_last_unittransportfirst ge_representation_imaginary_code_append_matching_last_unittransportfirst. (((gr_unit_append_matching_last_unit) = ((ge_representation_real_code_append_matching_last_unittransportfirst) + (ge_representation_imaginary_code_append_matching_last_unittransportfirst)) * S ((ge_representation_real_code_append_matching_last_unittransportfirst) + (ge_representation_imaginary_code_append_matching_last_unittransportfirst)) + ((ge_representation_imaginary_code_append_matching_last_unittransportfirst) + (ge_representation_imaginary_code_append_matching_last_unittransportfirst))) /\ ((exists ge_balance_positive_append_matching_last_unittransportfirstreal ge_balance_negative_append_matching_last_unittransportfirstreal. (((((ge_representation_real_code_append_matching_last_unittransportfirst) = 2 * (ge_balance_positive_append_matching_last_unittransportfirstreal) /\ (ge_balance_negative_append_matching_last_unittransportfirstreal) = 0) \/ exists ge_signed_half_append_matching_last_unittransportfirstrealdecode. (((ge_representation_real_code_append_matching_last_unittransportfirst) = 2 * ge_signed_half_append_matching_last_unittransportfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportfirstreal) = 0) /\ (ge_balance_negative_append_matching_last_unittransportfirstreal) = S ge_signed_half_append_matching_last_unittransportfirstrealdecode))) /\ ((ge_first_rp_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportfirstreal = (ge_first_rn_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportfirstreal))) /\ (exists ge_balance_positive_append_matching_last_unittransportfirstimaginary ge_balance_negative_append_matching_last_unittransportfirstimaginary. (((((ge_representation_imaginary_code_append_matching_last_unittransportfirst) = 2 * (ge_balance_positive_append_matching_last_unittransportfirstimaginary) /\ (ge_balance_negative_append_matching_last_unittransportfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unittransportfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unittransportfirst) = 2 * ge_signed_half_append_matching_last_unittransportfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unittransportfirstimaginary) = S ge_signed_half_append_matching_last_unittransportfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportfirstimaginary = (ge_first_in_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_last_unittransportsecond ge_representation_imaginary_code_append_matching_last_unittransportsecond. (((p) = ((ge_representation_real_code_append_matching_last_unittransportsecond) + (ge_representation_imaginary_code_append_matching_last_unittransportsecond)) * S ((ge_representation_real_code_append_matching_last_unittransportsecond) + (ge_representation_imaginary_code_append_matching_last_unittransportsecond)) + ((ge_representation_imaginary_code_append_matching_last_unittransportsecond) + (ge_representation_imaginary_code_append_matching_last_unittransportsecond))) /\ ((exists ge_balance_positive_append_matching_last_unittransportsecondreal ge_balance_negative_append_matching_last_unittransportsecondreal. (((((ge_representation_real_code_append_matching_last_unittransportsecond) = 2 * (ge_balance_positive_append_matching_last_unittransportsecondreal) /\ (ge_balance_negative_append_matching_last_unittransportsecondreal) = 0) \/ exists ge_signed_half_append_matching_last_unittransportsecondrealdecode. (((ge_representation_real_code_append_matching_last_unittransportsecond) = 2 * ge_signed_half_append_matching_last_unittransportsecondrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportsecondreal) = 0) /\ (ge_balance_negative_append_matching_last_unittransportsecondreal) = S ge_signed_half_append_matching_last_unittransportsecondrealdecode))) /\ ((ge_second_rp_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportsecondreal = (ge_second_rn_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportsecondreal))) /\ (exists ge_balance_positive_append_matching_last_unittransportsecondimaginary ge_balance_negative_append_matching_last_unittransportsecondimaginary. (((((ge_representation_imaginary_code_append_matching_last_unittransportsecond) = 2 * (ge_balance_positive_append_matching_last_unittransportsecondimaginary) /\ (ge_balance_negative_append_matching_last_unittransportsecondimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unittransportsecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unittransportsecond) = 2 * ge_signed_half_append_matching_last_unittransportsecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportsecondimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unittransportsecondimaginary) = S ge_signed_half_append_matching_last_unittransportsecondimaginarydecode))) /\ ((ge_second_ip_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportsecondimaginary = (ge_second_in_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportsecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_last_unittransportoutput ge_representation_imaginary_code_append_matching_last_unittransportoutput. (((q) = ((ge_representation_real_code_append_matching_last_unittransportoutput) + (ge_representation_imaginary_code_append_matching_last_unittransportoutput)) * S ((ge_representation_real_code_append_matching_last_unittransportoutput) + (ge_representation_imaginary_code_append_matching_last_unittransportoutput)) + ((ge_representation_imaginary_code_append_matching_last_unittransportoutput) + (ge_representation_imaginary_code_append_matching_last_unittransportoutput))) /\ ((exists ge_balance_positive_append_matching_last_unittransportoutputreal ge_balance_negative_append_matching_last_unittransportoutputreal. (((((ge_representation_real_code_append_matching_last_unittransportoutput) = 2 * (ge_balance_positive_append_matching_last_unittransportoutputreal) /\ (ge_balance_negative_append_matching_last_unittransportoutputreal) = 0) \/ exists ge_signed_half_append_matching_last_unittransportoutputrealdecode. (((ge_representation_real_code_append_matching_last_unittransportoutput) = 2 * ge_signed_half_append_matching_last_unittransportoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportoutputreal) = 0) /\ (ge_balance_negative_append_matching_last_unittransportoutputreal) = S ge_signed_half_append_matching_last_unittransportoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))))))) + ge_balance_negative_append_matching_last_unittransportoutputreal = (((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))))))) + ge_balance_positive_append_matching_last_unittransportoutputreal))) /\ (exists ge_balance_positive_append_matching_last_unittransportoutputimaginary ge_balance_negative_append_matching_last_unittransportoutputimaginary. (((((ge_representation_imaginary_code_append_matching_last_unittransportoutput) = 2 * (ge_balance_positive_append_matching_last_unittransportoutputimaginary) /\ (ge_balance_negative_append_matching_last_unittransportoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unittransportoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unittransportoutput) = 2 * ge_signed_half_append_matching_last_unittransportoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unittransportoutputimaginary) = S ge_signed_half_append_matching_last_unittransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))))))) + ge_balance_negative_append_matching_last_unittransportoutputimaginary = (((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))))))) + ge_balance_positive_append_matching_last_unittransportoutputimaginary))))))))))) -> (forall gr_match_index_append_matching_new gr_match_image_append_matching_new gr_match_source_append_matching_new gr_match_target_append_matching_new. (exists ge_gap_append_matching_newindex. ge_gap_append_matching_newindex + S (gr_match_index_append_matching_new) = (S l)) -> (((exists ff_h_gprod_append_matching_newmap. ff_h_gprod_append_matching_newmap + S (gr_match_image_append_matching_new) = S ((S (gr_match_index_append_matching_new)) * V)) /\ exists ff_q_gprod_append_matching_newmap. U = ff_q_gprod_append_matching_newmap * S ((S (gr_match_index_append_matching_new)) * V) + (gr_match_image_append_matching_new))) -> (((exists ff_h_gprod_append_matching_newsource. ff_h_gprod_append_matching_newsource + S (gr_match_source_append_matching_new) = S ((S (gr_match_index_append_matching_new)) * c)) /\ exists ff_q_gprod_append_matching_newsource. b = ff_q_gprod_append_matching_newsource * S ((S (gr_match_index_append_matching_new)) * c) + (gr_match_source_append_matching_new))) -> (((exists ff_h_gprod_append_matching_newtarget. ff_h_gprod_append_matching_newtarget + S (gr_match_target_append_matching_new) = S ((S (gr_match_image_append_matching_new)) * e)) /\ exists ff_q_gprod_append_matching_newtarget. d = ff_q_gprod_append_matching_newtarget * S ((S (gr_match_image_append_matching_new)) * e) + (gr_match_target_append_matching_new))) -> (exists gr_unit_append_matching_newunit_witness. ((exists gr_inverse_append_matching_newunit_witnessunit. (exists ge_first_rp_append_matching_newunit_witnessunitidentity ge_first_rn_append_matching_newunit_witnessunitidentity ge_first_ip_append_matching_newunit_witnessunitidentity ge_first_in_append_matching_newunit_witnessunitidentity ge_second_rp_append_matching_newunit_witnessunitidentity ge_second_rn_append_matching_newunit_witnessunitidentity ge_second_ip_append_matching_newunit_witnessunitidentity ge_second_in_append_matching_newunit_witnessunitidentity. ((exists ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst. (((gr_unit_append_matching_newunit_witness) = ((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal) = S ge_signed_half_append_matching_newunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal = (ge_first_rn_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary) = S ge_signed_half_append_matching_newunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary = (ge_first_in_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond. (((gr_inverse_append_matching_newunit_witnessunit) = ((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal) = S ge_signed_half_append_matching_newunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal = (ge_second_rn_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary) = S ge_signed_half_append_matching_newunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary = (ge_second_in_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal) = S ge_signed_half_append_matching_newunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal = (((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary) = S ge_signed_half_append_matching_newunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_append_matching_newunit_witnesstransport ge_first_rn_append_matching_newunit_witnesstransport ge_first_ip_append_matching_newunit_witnesstransport ge_first_in_append_matching_newunit_witnesstransport ge_second_rp_append_matching_newunit_witnesstransport ge_second_rn_append_matching_newunit_witnesstransport ge_second_ip_append_matching_newunit_witnesstransport ge_second_in_append_matching_newunit_witnesstransport. ((exists ge_representation_real_code_append_matching_newunit_witnesstransportfirst ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst. (((gr_unit_append_matching_newunit_witness) = ((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst)) * S ((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_append_matching_newunit_witnesstransportfirstreal ge_balance_negative_append_matching_newunit_witnesstransportfirstreal. (((((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportfirstreal) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_newunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstreal) = S ge_signed_half_append_matching_newunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportfirstreal = (ge_first_rn_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_newunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary) = S ge_signed_half_append_matching_newunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary = (ge_first_in_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_newunit_witnesstransportsecond ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond. (((gr_match_source_append_matching_new) = ((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond)) * S ((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_append_matching_newunit_witnesstransportsecondreal ge_balance_negative_append_matching_newunit_witnesstransportsecondreal. (((((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportsecondreal) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_newunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondreal) = S ge_signed_half_append_matching_newunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportsecondreal = (ge_second_rn_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_newunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary) = S ge_signed_half_append_matching_newunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary = (ge_second_in_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_newunit_witnesstransportoutput ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput. (((gr_match_target_append_matching_new) = ((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput)) * S ((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_append_matching_newunit_witnesstransportoutputreal ge_balance_negative_append_matching_newunit_witnesstransportoutputreal. (((((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportoutputreal) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_newunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputreal) = S ge_signed_half_append_matching_newunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))))))) + ge_balance_negative_append_matching_newunit_witnesstransportoutputreal = (((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))))))) + ge_balance_positive_append_matching_newunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_newunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary) = S ge_signed_half_append_matching_newunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))))))) + ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary = (((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))))))) + ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary))))))))))))