dirichlet_convolution_entry_first_input_transport

Exact expanded first-order arithmetic statement

forall F G H N l n d z. (exists dst_positive_code_entry_valid dst_positive_scale_entry_valid dst_negative_code_entry_valid dst_negative_scale_entry_valid. (((H) = (((((dst_positive_code_entry_valid) + (dst_positive_scale_entry_valid)) * S ((dst_positive_code_entry_valid) + (dst_positive_scale_entry_valid)) + ((dst_positive_scale_entry_valid) + (dst_positive_scale_entry_valid))) + (((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) * S ((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) + ((dst_negative_scale_entry_valid) + (dst_negative_scale_entry_valid)))) * S ((((dst_positive_code_entry_valid) + (dst_positive_scale_entry_valid)) * S ((dst_positive_code_entry_valid) + (dst_positive_scale_entry_valid)) + ((dst_positive_scale_entry_valid) + (dst_positive_scale_entry_valid))) + (((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) * S ((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) + ((dst_negative_scale_entry_valid) + (dst_negative_scale_entry_valid)))) + ((((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) * S ((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) + ((dst_negative_scale_entry_valid) + (dst_negative_scale_entry_valid))) + (((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) * S ((dst_negative_code_entry_valid) + (dst_negative_scale_entry_valid)) + ((dst_negative_scale_entry_valid) + (dst_negative_scale_entry_valid)))))) /\ (forall dst_index_entry_valid. (exists pvs_le_gap_entry_validdomain. pvs_le_gap_entry_validdomain + (dst_index_entry_valid) = (N)) -> exists dst_positive_entry_valid dst_negative_entry_valid dst_value_entry_valid. ((((exists ff_h_pvs_entry_validentrypositive. ff_h_pvs_entry_validentrypositive + S (dst_positive_entry_valid) = S ((S (dst_index_entry_valid)) * dst_positive_scale_entry_valid)) /\ exists ff_q_pvs_entry_validentrypositive. dst_positive_code_entry_valid = ff_q_pvs_entry_validentrypositive * S ((S (dst_index_entry_valid)) * dst_positive_scale_entry_valid) + (dst_positive_entry_valid))) /\ (((((exists ff_h_pvs_entry_validentrynegative. ff_h_pvs_entry_validentrynegative + S (dst_negative_entry_valid) = S ((S (dst_index_entry_valid)) * dst_negative_scale_entry_valid)) /\ exists ff_q_pvs_entry_validentrynegative. dst_negative_code_entry_valid = ff_q_pvs_entry_validentrynegative * S ((S (dst_index_entry_valid)) * dst_negative_scale_entry_valid) + (dst_negative_entry_valid))) /\ (exists ge_balance_positive_entry_validentryvalue ge_balance_negative_entry_validentryvalue. (((((dst_value_entry_valid) = 2 * (ge_balance_positive_entry_validentryvalue) /\ (ge_balance_negative_entry_validentryvalue) = 0) \/ exists ge_signed_half_entry_validentryvaluedecode. (((dst_value_entry_valid) = 2 * ge_signed_half_entry_validentryvaluedecode + 1 /\ (ge_balance_positive_entry_validentryvalue) = 0) /\ (ge_balance_negative_entry_validentryvalue) = S ge_signed_half_entry_validentryvaluedecode))) /\ ((dst_positive_entry_valid) + ge_balance_negative_entry_validentryvalue = (dst_negative_entry_valid) + ge_balance_positive_entry_validentryvalue))))))))) -> (forall dst_index_entry_equal dst_first_entry_equal dst_second_entry_equal. (exists pvs_gap_entry_equalbound. pvs_gap_entry_equalbound + S (dst_index_entry_equal) = (l)) -> (exists dst_positive_code_entry_equalfirst dst_positive_scale_entry_equalfirst dst_negative_code_entry_equalfirst dst_negative_scale_entry_equalfirst dst_positive_entry_equalfirst dst_negative_entry_equalfirst. (((F) = (((((dst_positive_code_entry_equalfirst) + (dst_positive_scale_entry_equalfirst)) * S ((dst_positive_code_entry_equalfirst) + (dst_positive_scale_entry_equalfirst)) + ((dst_positive_scale_entry_equalfirst) + (dst_positive_scale_entry_equalfirst))) + (((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) * S ((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) + ((dst_negative_scale_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)))) * S ((((dst_positive_code_entry_equalfirst) + (dst_positive_scale_entry_equalfirst)) * S ((dst_positive_code_entry_equalfirst) + (dst_positive_scale_entry_equalfirst)) + ((dst_positive_scale_entry_equalfirst) + (dst_positive_scale_entry_equalfirst))) + (((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) * S ((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) + ((dst_negative_scale_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)))) + ((((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) * S ((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) + ((dst_negative_scale_entry_equalfirst) + (dst_negative_scale_entry_equalfirst))) + (((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) * S ((dst_negative_code_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)) + ((dst_negative_scale_entry_equalfirst) + (dst_negative_scale_entry_equalfirst)))))) /\ (((((exists ff_h_pvs_entry_equalfirstpositive. ff_h_pvs_entry_equalfirstpositive + S (dst_positive_entry_equalfirst) = S ((S (dst_index_entry_equal)) * dst_positive_scale_entry_equalfirst)) /\ exists ff_q_pvs_entry_equalfirstpositive. dst_positive_code_entry_equalfirst = ff_q_pvs_entry_equalfirstpositive * S ((S (dst_index_entry_equal)) * dst_positive_scale_entry_equalfirst) + (dst_positive_entry_equalfirst))) /\ (((((exists ff_h_pvs_entry_equalfirstnegative. ff_h_pvs_entry_equalfirstnegative + S (dst_negative_entry_equalfirst) = S ((S (dst_index_entry_equal)) * dst_negative_scale_entry_equalfirst)) /\ exists ff_q_pvs_entry_equalfirstnegative. dst_negative_code_entry_equalfirst = ff_q_pvs_entry_equalfirstnegative * S ((S (dst_index_entry_equal)) * dst_negative_scale_entry_equalfirst) + (dst_negative_entry_equalfirst))) /\ (exists ge_balance_positive_entry_equalfirstvalue ge_balance_negative_entry_equalfirstvalue. (((((dst_first_entry_equal) = 2 * (ge_balance_positive_entry_equalfirstvalue) /\ (ge_balance_negative_entry_equalfirstvalue) = 0) \/ exists ge_signed_half_entry_equalfirstvaluedecode. (((dst_first_entry_equal) = 2 * ge_signed_half_entry_equalfirstvaluedecode + 1 /\ (ge_balance_positive_entry_equalfirstvalue) = 0) /\ (ge_balance_negative_entry_equalfirstvalue) = S ge_signed_half_entry_equalfirstvaluedecode))) /\ ((dst_positive_entry_equalfirst) + ge_balance_negative_entry_equalfirstvalue = (dst_negative_entry_equalfirst) + ge_balance_positive_entry_equalfirstvalue))))))))) -> (exists dst_positive_code_entry_equalsecond dst_positive_scale_entry_equalsecond dst_negative_code_entry_equalsecond dst_negative_scale_entry_equalsecond dst_positive_entry_equalsecond dst_negative_entry_equalsecond. (((H) = (((((dst_positive_code_entry_equalsecond) + (dst_positive_scale_entry_equalsecond)) * S ((dst_positive_code_entry_equalsecond) + (dst_positive_scale_entry_equalsecond)) + ((dst_positive_scale_entry_equalsecond) + (dst_positive_scale_entry_equalsecond))) + (((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) * S ((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) + ((dst_negative_scale_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)))) * S ((((dst_positive_code_entry_equalsecond) + (dst_positive_scale_entry_equalsecond)) * S ((dst_positive_code_entry_equalsecond) + (dst_positive_scale_entry_equalsecond)) + ((dst_positive_scale_entry_equalsecond) + (dst_positive_scale_entry_equalsecond))) + (((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) * S ((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) + ((dst_negative_scale_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)))) + ((((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) * S ((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) + ((dst_negative_scale_entry_equalsecond) + (dst_negative_scale_entry_equalsecond))) + (((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) * S ((dst_negative_code_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)) + ((dst_negative_scale_entry_equalsecond) + (dst_negative_scale_entry_equalsecond)))))) /\ (((((exists ff_h_pvs_entry_equalsecondpositive. ff_h_pvs_entry_equalsecondpositive + S (dst_positive_entry_equalsecond) = S ((S (dst_index_entry_equal)) * dst_positive_scale_entry_equalsecond)) /\ exists ff_q_pvs_entry_equalsecondpositive. dst_positive_code_entry_equalsecond = ff_q_pvs_entry_equalsecondpositive * S ((S (dst_index_entry_equal)) * dst_positive_scale_entry_equalsecond) + (dst_positive_entry_equalsecond))) /\ (((((exists ff_h_pvs_entry_equalsecondnegative. ff_h_pvs_entry_equalsecondnegative + S (dst_negative_entry_equalsecond) = S ((S (dst_index_entry_equal)) * dst_negative_scale_entry_equalsecond)) /\ exists ff_q_pvs_entry_equalsecondnegative. dst_negative_code_entry_equalsecond = ff_q_pvs_entry_equalsecondnegative * S ((S (dst_index_entry_equal)) * dst_negative_scale_entry_equalsecond) + (dst_negative_entry_equalsecond))) /\ (exists ge_balance_positive_entry_equalsecondvalue ge_balance_negative_entry_equalsecondvalue. (((((dst_second_entry_equal) = 2 * (ge_balance_positive_entry_equalsecondvalue) /\ (ge_balance_negative_entry_equalsecondvalue) = 0) \/ exists ge_signed_half_entry_equalsecondvaluedecode. (((dst_second_entry_equal) = 2 * ge_signed_half_entry_equalsecondvaluedecode + 1 /\ (ge_balance_positive_entry_equalsecondvalue) = 0) /\ (ge_balance_negative_entry_equalsecondvalue) = S ge_signed_half_entry_equalsecondvaluedecode))) /\ ((dst_positive_entry_equalsecond) + ge_balance_negative_entry_equalsecondvalue = (dst_negative_entry_equalsecond) + ge_balance_positive_entry_equalsecondvalue))))))))) -> dst_first_entry_equal = dst_second_entry_equal) -> (exists pvs_le_gap_entry_domain. pvs_le_gap_entry_domain + (d) = (N)) -> (exists pvs_gap_entry_preserved. pvs_gap_entry_preserved + S (d) = (l)) -> ((((~((d)=0)) /\ (exists dc_quotient_entry_source dc_left_entry_source dc_right_entry_source. (((n)=(d)*dc_quotient_entry_source) /\ (((exists dst_positive_code_entry_sourceleft dst_positive_scale_entry_sourceleft dst_negative_code_entry_sourceleft dst_negative_scale_entry_sourceleft dst_positive_entry_sourceleft dst_negative_entry_sourceleft. (((F) = (((((dst_positive_code_entry_sourceleft) + (dst_positive_scale_entry_sourceleft)) * S ((dst_positive_code_entry_sourceleft) + (dst_positive_scale_entry_sourceleft)) + ((dst_positive_scale_entry_sourceleft) + (dst_positive_scale_entry_sourceleft))) + (((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) * S ((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) + ((dst_negative_scale_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)))) * S ((((dst_positive_code_entry_sourceleft) + (dst_positive_scale_entry_sourceleft)) * S ((dst_positive_code_entry_sourceleft) + (dst_positive_scale_entry_sourceleft)) + ((dst_positive_scale_entry_sourceleft) + (dst_positive_scale_entry_sourceleft))) + (((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) * S ((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) + ((dst_negative_scale_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)))) + ((((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) * S ((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) + ((dst_negative_scale_entry_sourceleft) + (dst_negative_scale_entry_sourceleft))) + (((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) * S ((dst_negative_code_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)) + ((dst_negative_scale_entry_sourceleft) + (dst_negative_scale_entry_sourceleft)))))) /\ (((((exists ff_h_pvs_entry_sourceleftpositive. ff_h_pvs_entry_sourceleftpositive + S (dst_positive_entry_sourceleft) = S ((S (d)) * dst_positive_scale_entry_sourceleft)) /\ exists ff_q_pvs_entry_sourceleftpositive. dst_positive_code_entry_sourceleft = ff_q_pvs_entry_sourceleftpositive * S ((S (d)) * dst_positive_scale_entry_sourceleft) + (dst_positive_entry_sourceleft))) /\ (((((exists ff_h_pvs_entry_sourceleftnegative. ff_h_pvs_entry_sourceleftnegative + S (dst_negative_entry_sourceleft) = S ((S (d)) * dst_negative_scale_entry_sourceleft)) /\ exists ff_q_pvs_entry_sourceleftnegative. dst_negative_code_entry_sourceleft = ff_q_pvs_entry_sourceleftnegative * S ((S (d)) * dst_negative_scale_entry_sourceleft) + (dst_negative_entry_sourceleft))) /\ (exists ge_balance_positive_entry_sourceleftvalue ge_balance_negative_entry_sourceleftvalue. (((((dc_left_entry_source) = 2 * (ge_balance_positive_entry_sourceleftvalue) /\ (ge_balance_negative_entry_sourceleftvalue) = 0) \/ exists ge_signed_half_entry_sourceleftvaluedecode. (((dc_left_entry_source) = 2 * ge_signed_half_entry_sourceleftvaluedecode + 1 /\ (ge_balance_positive_entry_sourceleftvalue) = 0) /\ (ge_balance_negative_entry_sourceleftvalue) = S ge_signed_half_entry_sourceleftvaluedecode))) /\ ((dst_positive_entry_sourceleft) + ge_balance_negative_entry_sourceleftvalue = (dst_negative_entry_sourceleft) + ge_balance_positive_entry_sourceleftvalue))))))))) /\ (((exists dst_positive_code_entry_sourceright dst_positive_scale_entry_sourceright dst_negative_code_entry_sourceright dst_negative_scale_entry_sourceright dst_positive_entry_sourceright dst_negative_entry_sourceright. (((G) = (((((dst_positive_code_entry_sourceright) + (dst_positive_scale_entry_sourceright)) * S ((dst_positive_code_entry_sourceright) + (dst_positive_scale_entry_sourceright)) + ((dst_positive_scale_entry_sourceright) + (dst_positive_scale_entry_sourceright))) + (((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) * S ((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) + ((dst_negative_scale_entry_sourceright) + (dst_negative_scale_entry_sourceright)))) * S ((((dst_positive_code_entry_sourceright) + (dst_positive_scale_entry_sourceright)) * S ((dst_positive_code_entry_sourceright) + (dst_positive_scale_entry_sourceright)) + ((dst_positive_scale_entry_sourceright) + (dst_positive_scale_entry_sourceright))) + (((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) * S ((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) + ((dst_negative_scale_entry_sourceright) + (dst_negative_scale_entry_sourceright)))) + ((((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) * S ((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) + ((dst_negative_scale_entry_sourceright) + (dst_negative_scale_entry_sourceright))) + (((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) * S ((dst_negative_code_entry_sourceright) + (dst_negative_scale_entry_sourceright)) + ((dst_negative_scale_entry_sourceright) + (dst_negative_scale_entry_sourceright)))))) /\ (((((exists ff_h_pvs_entry_sourcerightpositive. ff_h_pvs_entry_sourcerightpositive + S (dst_positive_entry_sourceright) = S ((S (dc_quotient_entry_source)) * dst_positive_scale_entry_sourceright)) /\ exists ff_q_pvs_entry_sourcerightpositive. dst_positive_code_entry_sourceright = ff_q_pvs_entry_sourcerightpositive * S ((S (dc_quotient_entry_source)) * dst_positive_scale_entry_sourceright) + (dst_positive_entry_sourceright))) /\ (((((exists ff_h_pvs_entry_sourcerightnegative. ff_h_pvs_entry_sourcerightnegative + S (dst_negative_entry_sourceright) = S ((S (dc_quotient_entry_source)) * dst_negative_scale_entry_sourceright)) /\ exists ff_q_pvs_entry_sourcerightnegative. dst_negative_code_entry_sourceright = ff_q_pvs_entry_sourcerightnegative * S ((S (dc_quotient_entry_source)) * dst_negative_scale_entry_sourceright) + (dst_negative_entry_sourceright))) /\ (exists ge_balance_positive_entry_sourcerightvalue ge_balance_negative_entry_sourcerightvalue. (((((dc_right_entry_source) = 2 * (ge_balance_positive_entry_sourcerightvalue) /\ (ge_balance_negative_entry_sourcerightvalue) = 0) \/ exists ge_signed_half_entry_sourcerightvaluedecode. (((dc_right_entry_source) = 2 * ge_signed_half_entry_sourcerightvaluedecode + 1 /\ (ge_balance_positive_entry_sourcerightvalue) = 0) /\ (ge_balance_negative_entry_sourcerightvalue) = S ge_signed_half_entry_sourcerightvaluedecode))) /\ ((dst_positive_entry_sourceright) + ge_balance_negative_entry_sourcerightvalue = (dst_negative_entry_sourceright) + ge_balance_positive_entry_sourcerightvalue))))))))) /\ (exists sto_ap_entry_sourceproduct sto_an_entry_sourceproduct sto_bp_entry_sourceproduct sto_bn_entry_sourceproduct sto_cp_entry_sourceproduct sto_cn_entry_sourceproduct. (((((dc_left_entry_source) = 2 * (sto_ap_entry_sourceproduct) /\ (sto_an_entry_sourceproduct) = 0) \/ exists ge_signed_half_entry_sourceproductleft. (((dc_left_entry_source) = 2 * ge_signed_half_entry_sourceproductleft + 1 /\ (sto_ap_entry_sourceproduct) = 0) /\ (sto_an_entry_sourceproduct) = S ge_signed_half_entry_sourceproductleft))) /\ ((((((dc_right_entry_source) = 2 * (sto_bp_entry_sourceproduct) /\ (sto_bn_entry_sourceproduct) = 0) \/ exists ge_signed_half_entry_sourceproductright. (((dc_right_entry_source) = 2 * ge_signed_half_entry_sourceproductright + 1 /\ (sto_bp_entry_sourceproduct) = 0) /\ (sto_bn_entry_sourceproduct) = S ge_signed_half_entry_sourceproductright))) /\ ((((((z) = 2 * (sto_cp_entry_sourceproduct) /\ (sto_cn_entry_sourceproduct) = 0) \/ exists ge_signed_half_entry_sourceproductoutput. (((z) = 2 * ge_signed_half_entry_sourceproductoutput + 1 /\ (sto_cp_entry_sourceproduct) = 0) /\ (sto_cn_entry_sourceproduct) = S ge_signed_half_entry_sourceproductoutput))) /\ ((sto_ap_entry_sourceproduct * sto_bp_entry_sourceproduct + sto_an_entry_sourceproduct * sto_bn_entry_sourceproduct) + sto_cn_entry_sourceproduct = (sto_ap_entry_sourceproduct * sto_bn_entry_sourceproduct + sto_an_entry_sourceproduct * sto_bp_entry_sourceproduct) + sto_cp_entry_sourceproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_entry_sourcenondivisor. (n) = (d) * pvs_factor_entry_sourcenondivisor)) /\ ((z)=0)))) -> ((((~((d)=0)) /\ (exists dc_quotient_entry_result dc_left_entry_result dc_right_entry_result. (((n)=(d)*dc_quotient_entry_result) /\ (((exists dst_positive_code_entry_resultleft dst_positive_scale_entry_resultleft dst_negative_code_entry_resultleft dst_negative_scale_entry_resultleft dst_positive_entry_resultleft dst_negative_entry_resultleft. (((H) = (((((dst_positive_code_entry_resultleft) + (dst_positive_scale_entry_resultleft)) * S ((dst_positive_code_entry_resultleft) + (dst_positive_scale_entry_resultleft)) + ((dst_positive_scale_entry_resultleft) + (dst_positive_scale_entry_resultleft))) + (((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) * S ((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) + ((dst_negative_scale_entry_resultleft) + (dst_negative_scale_entry_resultleft)))) * S ((((dst_positive_code_entry_resultleft) + (dst_positive_scale_entry_resultleft)) * S ((dst_positive_code_entry_resultleft) + (dst_positive_scale_entry_resultleft)) + ((dst_positive_scale_entry_resultleft) + (dst_positive_scale_entry_resultleft))) + (((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) * S ((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) + ((dst_negative_scale_entry_resultleft) + (dst_negative_scale_entry_resultleft)))) + ((((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) * S ((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) + ((dst_negative_scale_entry_resultleft) + (dst_negative_scale_entry_resultleft))) + (((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) * S ((dst_negative_code_entry_resultleft) + (dst_negative_scale_entry_resultleft)) + ((dst_negative_scale_entry_resultleft) + (dst_negative_scale_entry_resultleft)))))) /\ (((((exists ff_h_pvs_entry_resultleftpositive. ff_h_pvs_entry_resultleftpositive + S (dst_positive_entry_resultleft) = S ((S (d)) * dst_positive_scale_entry_resultleft)) /\ exists ff_q_pvs_entry_resultleftpositive. dst_positive_code_entry_resultleft = ff_q_pvs_entry_resultleftpositive * S ((S (d)) * dst_positive_scale_entry_resultleft) + (dst_positive_entry_resultleft))) /\ (((((exists ff_h_pvs_entry_resultleftnegative. ff_h_pvs_entry_resultleftnegative + S (dst_negative_entry_resultleft) = S ((S (d)) * dst_negative_scale_entry_resultleft)) /\ exists ff_q_pvs_entry_resultleftnegative. dst_negative_code_entry_resultleft = ff_q_pvs_entry_resultleftnegative * S ((S (d)) * dst_negative_scale_entry_resultleft) + (dst_negative_entry_resultleft))) /\ (exists ge_balance_positive_entry_resultleftvalue ge_balance_negative_entry_resultleftvalue. (((((dc_left_entry_result) = 2 * (ge_balance_positive_entry_resultleftvalue) /\ (ge_balance_negative_entry_resultleftvalue) = 0) \/ exists ge_signed_half_entry_resultleftvaluedecode. (((dc_left_entry_result) = 2 * ge_signed_half_entry_resultleftvaluedecode + 1 /\ (ge_balance_positive_entry_resultleftvalue) = 0) /\ (ge_balance_negative_entry_resultleftvalue) = S ge_signed_half_entry_resultleftvaluedecode))) /\ ((dst_positive_entry_resultleft) + ge_balance_negative_entry_resultleftvalue = (dst_negative_entry_resultleft) + ge_balance_positive_entry_resultleftvalue))))))))) /\ (((exists dst_positive_code_entry_resultright dst_positive_scale_entry_resultright dst_negative_code_entry_resultright dst_negative_scale_entry_resultright dst_positive_entry_resultright dst_negative_entry_resultright. (((G) = (((((dst_positive_code_entry_resultright) + (dst_positive_scale_entry_resultright)) * S ((dst_positive_code_entry_resultright) + (dst_positive_scale_entry_resultright)) + ((dst_positive_scale_entry_resultright) + (dst_positive_scale_entry_resultright))) + (((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) * S ((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) + ((dst_negative_scale_entry_resultright) + (dst_negative_scale_entry_resultright)))) * S ((((dst_positive_code_entry_resultright) + (dst_positive_scale_entry_resultright)) * S ((dst_positive_code_entry_resultright) + (dst_positive_scale_entry_resultright)) + ((dst_positive_scale_entry_resultright) + (dst_positive_scale_entry_resultright))) + (((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) * S ((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) + ((dst_negative_scale_entry_resultright) + (dst_negative_scale_entry_resultright)))) + ((((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) * S ((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) + ((dst_negative_scale_entry_resultright) + (dst_negative_scale_entry_resultright))) + (((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) * S ((dst_negative_code_entry_resultright) + (dst_negative_scale_entry_resultright)) + ((dst_negative_scale_entry_resultright) + (dst_negative_scale_entry_resultright)))))) /\ (((((exists ff_h_pvs_entry_resultrightpositive. ff_h_pvs_entry_resultrightpositive + S (dst_positive_entry_resultright) = S ((S (dc_quotient_entry_result)) * dst_positive_scale_entry_resultright)) /\ exists ff_q_pvs_entry_resultrightpositive. dst_positive_code_entry_resultright = ff_q_pvs_entry_resultrightpositive * S ((S (dc_quotient_entry_result)) * dst_positive_scale_entry_resultright) + (dst_positive_entry_resultright))) /\ (((((exists ff_h_pvs_entry_resultrightnegative. ff_h_pvs_entry_resultrightnegative + S (dst_negative_entry_resultright) = S ((S (dc_quotient_entry_result)) * dst_negative_scale_entry_resultright)) /\ exists ff_q_pvs_entry_resultrightnegative. dst_negative_code_entry_resultright = ff_q_pvs_entry_resultrightnegative * S ((S (dc_quotient_entry_result)) * dst_negative_scale_entry_resultright) + (dst_negative_entry_resultright))) /\ (exists ge_balance_positive_entry_resultrightvalue ge_balance_negative_entry_resultrightvalue. (((((dc_right_entry_result) = 2 * (ge_balance_positive_entry_resultrightvalue) /\ (ge_balance_negative_entry_resultrightvalue) = 0) \/ exists ge_signed_half_entry_resultrightvaluedecode. (((dc_right_entry_result) = 2 * ge_signed_half_entry_resultrightvaluedecode + 1 /\ (ge_balance_positive_entry_resultrightvalue) = 0) /\ (ge_balance_negative_entry_resultrightvalue) = S ge_signed_half_entry_resultrightvaluedecode))) /\ ((dst_positive_entry_resultright) + ge_balance_negative_entry_resultrightvalue = (dst_negative_entry_resultright) + ge_balance_positive_entry_resultrightvalue))))))))) /\ (exists sto_ap_entry_resultproduct sto_an_entry_resultproduct sto_bp_entry_resultproduct sto_bn_entry_resultproduct sto_cp_entry_resultproduct sto_cn_entry_resultproduct. (((((dc_left_entry_result) = 2 * (sto_ap_entry_resultproduct) /\ (sto_an_entry_resultproduct) = 0) \/ exists ge_signed_half_entry_resultproductleft. (((dc_left_entry_result) = 2 * ge_signed_half_entry_resultproductleft + 1 /\ (sto_ap_entry_resultproduct) = 0) /\ (sto_an_entry_resultproduct) = S ge_signed_half_entry_resultproductleft))) /\ ((((((dc_right_entry_result) = 2 * (sto_bp_entry_resultproduct) /\ (sto_bn_entry_resultproduct) = 0) \/ exists ge_signed_half_entry_resultproductright. (((dc_right_entry_result) = 2 * ge_signed_half_entry_resultproductright + 1 /\ (sto_bp_entry_resultproduct) = 0) /\ (sto_bn_entry_resultproduct) = S ge_signed_half_entry_resultproductright))) /\ ((((((z) = 2 * (sto_cp_entry_resultproduct) /\ (sto_cn_entry_resultproduct) = 0) \/ exists ge_signed_half_entry_resultproductoutput. (((z) = 2 * ge_signed_half_entry_resultproductoutput + 1 /\ (sto_cp_entry_resultproduct) = 0) /\ (sto_cn_entry_resultproduct) = S ge_signed_half_entry_resultproductoutput))) /\ ((sto_ap_entry_resultproduct * sto_bp_entry_resultproduct + sto_an_entry_resultproduct * sto_bn_entry_resultproduct) + sto_cn_entry_resultproduct = (sto_ap_entry_resultproduct * sto_bn_entry_resultproduct + sto_an_entry_resultproduct * sto_bp_entry_resultproduct) + sto_cp_entry_resultproduct))))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_entry_resultnondivisor. (n) = (d) * pvs_factor_entry_resultnondivisor)) /\ ((z)=0))))