dirichlet_convolution_prefix_first_input_transport

forall F G H n k l M. (exists dst_positive_code_prefix_valid dst_positive_scale_prefix_valid dst_negative_code_prefix_valid dst_negative_scale_prefix_valid. (((H) = (((((dst_positive_code_prefix_valid) + (dst_positive_scale_prefix_valid)) * S ((dst_positive_code_prefix_valid) + (dst_positive_scale_prefix_valid)) + ((dst_positive_scale_prefix_valid) + (dst_positive_scale_prefix_valid))) + (((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) * S ((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) + ((dst_negative_scale_prefix_valid) + (dst_negative_scale_prefix_valid)))) * S ((((dst_positive_code_prefix_valid) + (dst_positive_scale_prefix_valid)) * S ((dst_positive_code_prefix_valid) + (dst_positive_scale_prefix_valid)) + ((dst_positive_scale_prefix_valid) + (dst_positive_scale_prefix_valid))) + (((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) * S ((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) + ((dst_negative_scale_prefix_valid) + (dst_negative_scale_prefix_valid)))) + ((((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) * S ((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) + ((dst_negative_scale_prefix_valid) + (dst_negative_scale_prefix_valid))) + (((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) * S ((dst_negative_code_prefix_valid) + (dst_negative_scale_prefix_valid)) + ((dst_negative_scale_prefix_valid) + (dst_negative_scale_prefix_valid)))))) /\ (forall dst_index_prefix_valid. (exists pvs_le_gap_prefix_validdomain. pvs_le_gap_prefix_validdomain + (dst_index_prefix_valid) = (k)) -> exists dst_positive_prefix_valid dst_negative_prefix_valid dst_value_prefix_valid. ((((exists ff_h_pvs_prefix_validentrypositive. ff_h_pvs_prefix_validentrypositive + S (dst_positive_prefix_valid) = S ((S (dst_index_prefix_valid)) * dst_positive_scale_prefix_valid)) /\ exists ff_q_pvs_prefix_validentrypositive. dst_positive_code_prefix_valid = ff_q_pvs_prefix_validentrypositive * S ((S (dst_index_prefix_valid)) * dst_positive_scale_prefix_valid) + (dst_positive_prefix_valid))) /\ (((((exists ff_h_pvs_prefix_validentrynegative. ff_h_pvs_prefix_validentrynegative + S (dst_negative_prefix_valid) = S ((S (dst_index_prefix_valid)) * dst_negative_scale_prefix_valid)) /\ exists ff_q_pvs_prefix_validentrynegative. dst_negative_code_prefix_valid = ff_q_pvs_prefix_validentrynegative * S ((S (dst_index_prefix_valid)) * dst_negative_scale_prefix_valid) + (dst_negative_prefix_valid))) /\ (exists ge_balance_positive_prefix_validentryvalue ge_balance_negative_prefix_validentryvalue. (((((dst_value_prefix_valid) = 2 * (ge_balance_positive_prefix_validentryvalue) /\ (ge_balance_negative_prefix_validentryvalue) = 0) \/ exists ge_signed_half_prefix_validentryvaluedecode. (((dst_value_prefix_valid) = 2 * ge_signed_half_prefix_validentryvaluedecode + 1 /\ (ge_balance_positive_prefix_validentryvalue) = 0) /\ (ge_balance_negative_prefix_validentryvalue) = S ge_signed_half_prefix_validentryvaluedecode))) /\ ((dst_positive_prefix_valid) + ge_balance_negative_prefix_validentryvalue = (dst_negative_prefix_valid) + ge_balance_positive_prefix_validentryvalue))))))))) -> (forall dst_index_prefix_equal dst_first_prefix_equal dst_second_prefix_equal. (exists pvs_gap_prefix_equalbound. pvs_gap_prefix_equalbound + S (dst_index_prefix_equal) = (l)) -> (exists dst_positive_code_prefix_equalfirst dst_positive_scale_prefix_equalfirst dst_negative_code_prefix_equalfirst dst_negative_scale_prefix_equalfirst dst_positive_prefix_equalfirst dst_negative_prefix_equalfirst. (((F) = (((((dst_positive_code_prefix_equalfirst) + (dst_positive_scale_prefix_equalfirst)) * S ((dst_positive_code_prefix_equalfirst) + (dst_positive_scale_prefix_equalfirst)) + ((dst_positive_scale_prefix_equalfirst) + (dst_positive_scale_prefix_equalfirst))) + (((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) * S ((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) + ((dst_negative_scale_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)))) * S ((((dst_positive_code_prefix_equalfirst) + (dst_positive_scale_prefix_equalfirst)) * S ((dst_positive_code_prefix_equalfirst) + (dst_positive_scale_prefix_equalfirst)) + ((dst_positive_scale_prefix_equalfirst) + (dst_positive_scale_prefix_equalfirst))) + (((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) * S ((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) + ((dst_negative_scale_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)))) + ((((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) * S ((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) + ((dst_negative_scale_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst))) + (((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) * S ((dst_negative_code_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)) + ((dst_negative_scale_prefix_equalfirst) + (dst_negative_scale_prefix_equalfirst)))))) /\ (((((exists ff_h_pvs_prefix_equalfirstpositive. ff_h_pvs_prefix_equalfirstpositive + S (dst_positive_prefix_equalfirst) = S ((S (dst_index_prefix_equal)) * dst_positive_scale_prefix_equalfirst)) /\ exists ff_q_pvs_prefix_equalfirstpositive. dst_positive_code_prefix_equalfirst = ff_q_pvs_prefix_equalfirstpositive * S ((S (dst_index_prefix_equal)) * dst_positive_scale_prefix_equalfirst) + (dst_positive_prefix_equalfirst))) /\ (((((exists ff_h_pvs_prefix_equalfirstnegative. ff_h_pvs_prefix_equalfirstnegative + S (dst_negative_prefix_equalfirst) = S ((S (dst_index_prefix_equal)) * dst_negative_scale_prefix_equalfirst)) /\ exists ff_q_pvs_prefix_equalfirstnegative. dst_negative_code_prefix_equalfirst = ff_q_pvs_prefix_equalfirstnegative * S ((S (dst_index_prefix_equal)) * dst_negative_scale_prefix_equalfirst) + (dst_negative_prefix_equalfirst))) /\ (exists ge_balance_positive_prefix_equalfirstvalue ge_balance_negative_prefix_equalfirstvalue. (((((dst_first_prefix_equal) = 2 * (ge_balance_positive_prefix_equalfirstvalue) /\ (ge_balance_negative_prefix_equalfirstvalue) = 0) \/ exists ge_signed_half_prefix_equalfirstvaluedecode. (((dst_first_prefix_equal) = 2 * ge_signed_half_prefix_equalfirstvaluedecode + 1 /\ (ge_balance_positive_prefix_equalfirstvalue) = 0) /\ (ge_balance_negative_prefix_equalfirstvalue) = S ge_signed_half_prefix_equalfirstvaluedecode))) /\ ((dst_positive_prefix_equalfirst) + ge_balance_negative_prefix_equalfirstvalue = (dst_negative_prefix_equalfirst) + ge_balance_positive_prefix_equalfirstvalue))))))))) -> (exists dst_positive_code_prefix_equalsecond dst_positive_scale_prefix_equalsecond dst_negative_code_prefix_equalsecond dst_negative_scale_prefix_equalsecond dst_positive_prefix_equalsecond dst_negative_prefix_equalsecond. (((H) = (((((dst_positive_code_prefix_equalsecond) + (dst_positive_scale_prefix_equalsecond)) * S ((dst_positive_code_prefix_equalsecond) + (dst_positive_scale_prefix_equalsecond)) + ((dst_positive_scale_prefix_equalsecond) + (dst_positive_scale_prefix_equalsecond))) + (((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) * S ((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) + ((dst_negative_scale_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)))) * S ((((dst_positive_code_prefix_equalsecond) + (dst_positive_scale_prefix_equalsecond)) * S ((dst_positive_code_prefix_equalsecond) + (dst_positive_scale_prefix_equalsecond)) + ((dst_positive_scale_prefix_equalsecond) + (dst_positive_scale_prefix_equalsecond))) + (((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) * S ((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) + ((dst_negative_scale_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)))) + ((((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) * S ((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) + ((dst_negative_scale_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond))) + (((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) * S ((dst_negative_code_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)) + ((dst_negative_scale_prefix_equalsecond) + (dst_negative_scale_prefix_equalsecond)))))) /\ (((((exists ff_h_pvs_prefix_equalsecondpositive. ff_h_pvs_prefix_equalsecondpositive + S (dst_positive_prefix_equalsecond) = S ((S (dst_index_prefix_equal)) * dst_positive_scale_prefix_equalsecond)) /\ exists ff_q_pvs_prefix_equalsecondpositive. dst_positive_code_prefix_equalsecond = ff_q_pvs_prefix_equalsecondpositive * S ((S (dst_index_prefix_equal)) * dst_positive_scale_prefix_equalsecond) + (dst_positive_prefix_equalsecond))) /\ (((((exists ff_h_pvs_prefix_equalsecondnegative. ff_h_pvs_prefix_equalsecondnegative + S (dst_negative_prefix_equalsecond) = S ((S (dst_index_prefix_equal)) * dst_negative_scale_prefix_equalsecond)) /\ exists ff_q_pvs_prefix_equalsecondnegative. dst_negative_code_prefix_equalsecond = ff_q_pvs_prefix_equalsecondnegative * S ((S (dst_index_prefix_equal)) * dst_negative_scale_prefix_equalsecond) + (dst_negative_prefix_equalsecond))) /\ (exists ge_balance_positive_prefix_equalsecondvalue ge_balance_negative_prefix_equalsecondvalue. (((((dst_second_prefix_equal) = 2 * (ge_balance_positive_prefix_equalsecondvalue) /\ (ge_balance_negative_prefix_equalsecondvalue) = 0) \/ exists ge_signed_half_prefix_equalsecondvaluedecode. (((dst_second_prefix_equal) = 2 * ge_signed_half_prefix_equalsecondvaluedecode + 1 /\ (ge_balance_positive_prefix_equalsecondvalue) = 0) /\ (ge_balance_negative_prefix_equalsecondvalue) = S ge_signed_half_prefix_equalsecondvaluedecode))) /\ ((dst_positive_prefix_equalsecond) + ge_balance_negative_prefix_equalsecondvalue = (dst_negative_prefix_equalsecond) + ge_balance_positive_prefix_equalsecondvalue))))))))) -> dst_first_prefix_equal = dst_second_prefix_equal) -> (exists pvs_gap_prefix_strict. pvs_gap_prefix_strict + S (k) = (l)) -> (((exists dst_positive_code_prefix_sourcetable dst_positive_scale_prefix_sourcetable dst_negative_code_prefix_sourcetable dst_negative_scale_prefix_sourcetable. (((M) = (((((dst_positive_code_prefix_sourcetable) + (dst_positive_scale_prefix_sourcetable)) * S ((dst_positive_code_prefix_sourcetable) + (dst_positive_scale_prefix_sourcetable)) + ((dst_positive_scale_prefix_sourcetable) + (dst_positive_scale_prefix_sourcetable))) + (((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) * S ((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) + ((dst_negative_scale_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)))) * S ((((dst_positive_code_prefix_sourcetable) + (dst_positive_scale_prefix_sourcetable)) * S ((dst_positive_code_prefix_sourcetable) + (dst_positive_scale_prefix_sourcetable)) + ((dst_positive_scale_prefix_sourcetable) + (dst_positive_scale_prefix_sourcetable))) + (((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) * S ((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) + ((dst_negative_scale_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)))) + ((((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) * S ((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) + ((dst_negative_scale_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable))) + (((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) * S ((dst_negative_code_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)) + ((dst_negative_scale_prefix_sourcetable) + (dst_negative_scale_prefix_sourcetable)))))) /\ (forall dst_index_prefix_sourcetable. (exists pvs_le_gap_prefix_sourcetabledomain. pvs_le_gap_prefix_sourcetabledomain + (dst_index_prefix_sourcetable) = (k)) -> exists dst_positive_prefix_sourcetable dst_negative_prefix_sourcetable dst_value_prefix_sourcetable. ((((exists ff_h_pvs_prefix_sourcetableentrypositive. ff_h_pvs_prefix_sourcetableentrypositive + S (dst_positive_prefix_sourcetable) = S ((S (dst_index_prefix_sourcetable)) * dst_positive_scale_prefix_sourcetable)) /\ exists ff_q_pvs_prefix_sourcetableentrypositive. dst_positive_code_prefix_sourcetable = ff_q_pvs_prefix_sourcetableentrypositive * S ((S (dst_index_prefix_sourcetable)) * dst_positive_scale_prefix_sourcetable) + (dst_positive_prefix_sourcetable))) /\ (((((exists ff_h_pvs_prefix_sourcetableentrynegative. ff_h_pvs_prefix_sourcetableentrynegative + S (dst_negative_prefix_sourcetable) = S ((S (dst_index_prefix_sourcetable)) * dst_negative_scale_prefix_sourcetable)) /\ exists ff_q_pvs_prefix_sourcetableentrynegative. dst_negative_code_prefix_sourcetable = ff_q_pvs_prefix_sourcetableentrynegative * S ((S (dst_index_prefix_sourcetable)) * dst_negative_scale_prefix_sourcetable) + (dst_negative_prefix_sourcetable))) /\ (exists ge_balance_positive_prefix_sourcetableentryvalue ge_balance_negative_prefix_sourcetableentryvalue. (((((dst_value_prefix_sourcetable) = 2 * (ge_balance_positive_prefix_sourcetableentryvalue) /\ (ge_balance_negative_prefix_sourcetableentryvalue) = 0) \/ exists ge_signed_half_prefix_sourcetableentryvaluedecode. (((dst_value_prefix_sourcetable) = 2 * ge_signed_half_prefix_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_sourcetableentryvalue) = 0) /\ (ge_balance_negative_prefix_sourcetableentryvalue) = S ge_signed_half_prefix_sourcetableentryvaluedecode))) /\ ((dst_positive_prefix_sourcetable) + ge_balance_negative_prefix_sourcetableentryvalue = (dst_negative_prefix_sourcetable) + ge_balance_positive_prefix_sourcetableentryvalue))))))))) /\ (forall dc_index_prefix_source dc_value_prefix_source. (exists pvs_le_gap_prefix_sourcedomain. pvs_le_gap_prefix_sourcedomain + (dc_index_prefix_source) = (k)) -> (exists dst_positive_code_prefix_sourcelookup dst_positive_scale_prefix_sourcelookup dst_negative_code_prefix_sourcelookup dst_negative_scale_prefix_sourcelookup dst_positive_prefix_sourcelookup dst_negative_prefix_sourcelookup. (((M) = (((((dst_positive_code_prefix_sourcelookup) + (dst_positive_scale_prefix_sourcelookup)) * S ((dst_positive_code_prefix_sourcelookup) + (dst_positive_scale_prefix_sourcelookup)) + ((dst_positive_scale_prefix_sourcelookup) + (dst_positive_scale_prefix_sourcelookup))) + (((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) * S ((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) + ((dst_negative_scale_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)))) * S ((((dst_positive_code_prefix_sourcelookup) + (dst_positive_scale_prefix_sourcelookup)) * S ((dst_positive_code_prefix_sourcelookup) + (dst_positive_scale_prefix_sourcelookup)) + ((dst_positive_scale_prefix_sourcelookup) + (dst_positive_scale_prefix_sourcelookup))) + (((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) * S ((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) + ((dst_negative_scale_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)))) + ((((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) * S ((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) + ((dst_negative_scale_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup))) + (((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) * S ((dst_negative_code_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)) + ((dst_negative_scale_prefix_sourcelookup) + (dst_negative_scale_prefix_sourcelookup)))))) /\ (((((exists ff_h_pvs_prefix_sourcelookuppositive. ff_h_pvs_prefix_sourcelookuppositive + S (dst_positive_prefix_sourcelookup) = S ((S (dc_index_prefix_source)) * dst_positive_scale_prefix_sourcelookup)) /\ exists ff_q_pvs_prefix_sourcelookuppositive. dst_positive_code_prefix_sourcelookup = ff_q_pvs_prefix_sourcelookuppositive * S ((S (dc_index_prefix_source)) * dst_positive_scale_prefix_sourcelookup) + (dst_positive_prefix_sourcelookup))) /\ (((((exists ff_h_pvs_prefix_sourcelookupnegative. ff_h_pvs_prefix_sourcelookupnegative + S (dst_negative_prefix_sourcelookup) = S ((S (dc_index_prefix_source)) * dst_negative_scale_prefix_sourcelookup)) /\ exists ff_q_pvs_prefix_sourcelookupnegative. dst_negative_code_prefix_sourcelookup = ff_q_pvs_prefix_sourcelookupnegative * S ((S (dc_index_prefix_source)) * dst_negative_scale_prefix_sourcelookup) + (dst_negative_prefix_sourcelookup))) /\ (exists ge_balance_positive_prefix_sourcelookupvalue ge_balance_negative_prefix_sourcelookupvalue. (((((dc_value_prefix_source) = 2 * (ge_balance_positive_prefix_sourcelookupvalue) /\ (ge_balance_negative_prefix_sourcelookupvalue) = 0) \/ exists ge_signed_half_prefix_sourcelookupvaluedecode. (((dc_value_prefix_source) = 2 * ge_signed_half_prefix_sourcelookupvaluedecode + 1 /\ (ge_balance_positive_prefix_sourcelookupvalue) = 0) /\ (ge_balance_negative_prefix_sourcelookupvalue) = S ge_signed_half_prefix_sourcelookupvaluedecode))) /\ ((dst_positive_prefix_sourcelookup) + ge_balance_negative_prefix_sourcelookupvalue = (dst_negative_prefix_sourcelookup) + ge_balance_positive_prefix_sourcelookupvalue))))))))) -> ((((~((dc_index_prefix_source)=0)) /\ (exists dc_quotient_prefix_sourceentry dc_left_prefix_sourceentry dc_right_prefix_sourceentry. (((n)=(dc_index_prefix_source)*dc_quotient_prefix_sourceentry) /\ (((exists dst_positive_code_prefix_sourceentryleft dst_positive_scale_prefix_sourceentryleft dst_negative_code_prefix_sourceentryleft dst_negative_scale_prefix_sourceentryleft dst_positive_prefix_sourceentryleft dst_negative_prefix_sourceentryleft. (((F) = (((((dst_positive_code_prefix_sourceentryleft) + (dst_positive_scale_prefix_sourceentryleft)) * S ((dst_positive_code_prefix_sourceentryleft) + (dst_positive_scale_prefix_sourceentryleft)) + ((dst_positive_scale_prefix_sourceentryleft) + (dst_positive_scale_prefix_sourceentryleft))) + (((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) * S ((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) + ((dst_negative_scale_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)))) * S ((((dst_positive_code_prefix_sourceentryleft) + (dst_positive_scale_prefix_sourceentryleft)) * S ((dst_positive_code_prefix_sourceentryleft) + (dst_positive_scale_prefix_sourceentryleft)) + ((dst_positive_scale_prefix_sourceentryleft) + (dst_positive_scale_prefix_sourceentryleft))) + (((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) * S ((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) + ((dst_negative_scale_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)))) + ((((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) * S ((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) + ((dst_negative_scale_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft))) + (((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) * S ((dst_negative_code_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)) + ((dst_negative_scale_prefix_sourceentryleft) + (dst_negative_scale_prefix_sourceentryleft)))))) /\ (((((exists ff_h_pvs_prefix_sourceentryleftpositive. ff_h_pvs_prefix_sourceentryleftpositive + S (dst_positive_prefix_sourceentryleft) = S ((S (dc_index_prefix_source)) * dst_positive_scale_prefix_sourceentryleft)) /\ exists ff_q_pvs_prefix_sourceentryleftpositive. dst_positive_code_prefix_sourceentryleft = ff_q_pvs_prefix_sourceentryleftpositive * S ((S (dc_index_prefix_source)) * dst_positive_scale_prefix_sourceentryleft) + (dst_positive_prefix_sourceentryleft))) /\ (((((exists ff_h_pvs_prefix_sourceentryleftnegative. ff_h_pvs_prefix_sourceentryleftnegative + S (dst_negative_prefix_sourceentryleft) = S ((S (dc_index_prefix_source)) * dst_negative_scale_prefix_sourceentryleft)) /\ exists ff_q_pvs_prefix_sourceentryleftnegative. dst_negative_code_prefix_sourceentryleft = ff_q_pvs_prefix_sourceentryleftnegative * S ((S (dc_index_prefix_source)) * dst_negative_scale_prefix_sourceentryleft) + (dst_negative_prefix_sourceentryleft))) /\ (exists ge_balance_positive_prefix_sourceentryleftvalue ge_balance_negative_prefix_sourceentryleftvalue. (((((dc_left_prefix_sourceentry) = 2 * (ge_balance_positive_prefix_sourceentryleftvalue) /\ (ge_balance_negative_prefix_sourceentryleftvalue) = 0) \/ exists ge_signed_half_prefix_sourceentryleftvaluedecode. (((dc_left_prefix_sourceentry) = 2 * ge_signed_half_prefix_sourceentryleftvaluedecode + 1 /\ (ge_balance_positive_prefix_sourceentryleftvalue) = 0) /\ (ge_balance_negative_prefix_sourceentryleftvalue) = S ge_signed_half_prefix_sourceentryleftvaluedecode))) /\ ((dst_positive_prefix_sourceentryleft) + ge_balance_negative_prefix_sourceentryleftvalue = (dst_negative_prefix_sourceentryleft) + ge_balance_positive_prefix_sourceentryleftvalue))))))))) /\ (((exists dst_positive_code_prefix_sourceentryright dst_positive_scale_prefix_sourceentryright dst_negative_code_prefix_sourceentryright dst_negative_scale_prefix_sourceentryright dst_positive_prefix_sourceentryright dst_negative_prefix_sourceentryright. (((G) = (((((dst_positive_code_prefix_sourceentryright) + (dst_positive_scale_prefix_sourceentryright)) * S ((dst_positive_code_prefix_sourceentryright) + (dst_positive_scale_prefix_sourceentryright)) + ((dst_positive_scale_prefix_sourceentryright) + (dst_positive_scale_prefix_sourceentryright))) + (((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) * S ((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) + ((dst_negative_scale_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)))) * S ((((dst_positive_code_prefix_sourceentryright) + (dst_positive_scale_prefix_sourceentryright)) * S ((dst_positive_code_prefix_sourceentryright) + (dst_positive_scale_prefix_sourceentryright)) + ((dst_positive_scale_prefix_sourceentryright) + (dst_positive_scale_prefix_sourceentryright))) + (((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) * S ((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) + ((dst_negative_scale_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)))) + ((((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) * S ((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) + ((dst_negative_scale_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright))) + (((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) * S ((dst_negative_code_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)) + ((dst_negative_scale_prefix_sourceentryright) + (dst_negative_scale_prefix_sourceentryright)))))) /\ (((((exists ff_h_pvs_prefix_sourceentryrightpositive. ff_h_pvs_prefix_sourceentryrightpositive + S (dst_positive_prefix_sourceentryright) = S ((S (dc_quotient_prefix_sourceentry)) * dst_positive_scale_prefix_sourceentryright)) /\ exists ff_q_pvs_prefix_sourceentryrightpositive. dst_positive_code_prefix_sourceentryright = ff_q_pvs_prefix_sourceentryrightpositive * S ((S (dc_quotient_prefix_sourceentry)) * dst_positive_scale_prefix_sourceentryright) + (dst_positive_prefix_sourceentryright))) /\ (((((exists ff_h_pvs_prefix_sourceentryrightnegative. ff_h_pvs_prefix_sourceentryrightnegative + S (dst_negative_prefix_sourceentryright) = S ((S (dc_quotient_prefix_sourceentry)) * dst_negative_scale_prefix_sourceentryright)) /\ exists ff_q_pvs_prefix_sourceentryrightnegative. dst_negative_code_prefix_sourceentryright = ff_q_pvs_prefix_sourceentryrightnegative * S ((S (dc_quotient_prefix_sourceentry)) * dst_negative_scale_prefix_sourceentryright) + (dst_negative_prefix_sourceentryright))) /\ (exists ge_balance_positive_prefix_sourceentryrightvalue ge_balance_negative_prefix_sourceentryrightvalue. (((((dc_right_prefix_sourceentry) = 2 * (ge_balance_positive_prefix_sourceentryrightvalue) /\ (ge_balance_negative_prefix_sourceentryrightvalue) = 0) \/ exists ge_signed_half_prefix_sourceentryrightvaluedecode. (((dc_right_prefix_sourceentry) = 2 * ge_signed_half_prefix_sourceentryrightvaluedecode + 1 /\ (ge_balance_positive_prefix_sourceentryrightvalue) = 0) /\ (ge_balance_negative_prefix_sourceentryrightvalue) = S ge_signed_half_prefix_sourceentryrightvaluedecode))) /\ ((dst_positive_prefix_sourceentryright) + ge_balance_negative_prefix_sourceentryrightvalue = (dst_negative_prefix_sourceentryright) + ge_balance_positive_prefix_sourceentryrightvalue))))))))) /\ (exists sto_ap_prefix_sourceentryproduct sto_an_prefix_sourceentryproduct sto_bp_prefix_sourceentryproduct sto_bn_prefix_sourceentryproduct sto_cp_prefix_sourceentryproduct sto_cn_prefix_sourceentryproduct. (((((dc_left_prefix_sourceentry) = 2 * (sto_ap_prefix_sourceentryproduct) /\ (sto_an_prefix_sourceentryproduct) = 0) \/ exists ge_signed_half_prefix_sourceentryproductleft. (((dc_left_prefix_sourceentry) = 2 * ge_signed_half_prefix_sourceentryproductleft + 1 /\ (sto_ap_prefix_sourceentryproduct) = 0) /\ (sto_an_prefix_sourceentryproduct) = S ge_signed_half_prefix_sourceentryproductleft))) /\ ((((((dc_right_prefix_sourceentry) = 2 * (sto_bp_prefix_sourceentryproduct) /\ (sto_bn_prefix_sourceentryproduct) = 0) \/ exists ge_signed_half_prefix_sourceentryproductright. (((dc_right_prefix_sourceentry) = 2 * ge_signed_half_prefix_sourceentryproductright + 1 /\ (sto_bp_prefix_sourceentryproduct) = 0) /\ (sto_bn_prefix_sourceentryproduct) = S ge_signed_half_prefix_sourceentryproductright))) /\ ((((((dc_value_prefix_source) = 2 * (sto_cp_prefix_sourceentryproduct) /\ (sto_cn_prefix_sourceentryproduct) = 0) \/ exists ge_signed_half_prefix_sourceentryproductoutput. (((dc_value_prefix_source) = 2 * ge_signed_half_prefix_sourceentryproductoutput + 1 /\ (sto_cp_prefix_sourceentryproduct) = 0) /\ (sto_cn_prefix_sourceentryproduct) = S ge_signed_half_prefix_sourceentryproductoutput))) /\ ((sto_ap_prefix_sourceentryproduct * sto_bp_prefix_sourceentryproduct + sto_an_prefix_sourceentryproduct * sto_bn_prefix_sourceentryproduct) + sto_cn_prefix_sourceentryproduct = (sto_ap_prefix_sourceentryproduct * sto_bn_prefix_sourceentryproduct + sto_an_prefix_sourceentryproduct * sto_bp_prefix_sourceentryproduct) + sto_cp_prefix_sourceentryproduct))))))))))))))) \/ ((((dc_index_prefix_source)=0 \/ ~(exists pvs_factor_prefix_sourceentrynondivisor. (n) = (dc_index_prefix_source) * pvs_factor_prefix_sourceentrynondivisor)) /\ ((dc_value_prefix_source)=0))))))) -> (((exists dst_positive_code_prefix_resulttable dst_positive_scale_prefix_resulttable dst_negative_code_prefix_resulttable dst_negative_scale_prefix_resulttable. (((M) = (((((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) * S ((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) + ((dst_positive_scale_prefix_resulttable) + (dst_positive_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))) * S ((((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) * S ((dst_positive_code_prefix_resulttable) + (dst_positive_scale_prefix_resulttable)) + ((dst_positive_scale_prefix_resulttable) + (dst_positive_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))) + ((((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable))) + (((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) * S ((dst_negative_code_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)) + ((dst_negative_scale_prefix_resulttable) + (dst_negative_scale_prefix_resulttable)))))) /\ (forall dst_index_prefix_resulttable. (exists pvs_le_gap_prefix_resulttabledomain. pvs_le_gap_prefix_resulttabledomain + (dst_index_prefix_resulttable) = (k)) -> exists dst_positive_prefix_resulttable dst_negative_prefix_resulttable dst_value_prefix_resulttable. ((((exists ff_h_pvs_prefix_resulttableentrypositive. ff_h_pvs_prefix_resulttableentrypositive + S (dst_positive_prefix_resulttable) = S ((S (dst_index_prefix_resulttable)) * dst_positive_scale_prefix_resulttable)) /\ exists ff_q_pvs_prefix_resulttableentrypositive. dst_positive_code_prefix_resulttable = ff_q_pvs_prefix_resulttableentrypositive * S ((S (dst_index_prefix_resulttable)) * dst_positive_scale_prefix_resulttable) + (dst_positive_prefix_resulttable))) /\ (((((exists ff_h_pvs_prefix_resulttableentrynegative. ff_h_pvs_prefix_resulttableentrynegative + S (dst_negative_prefix_resulttable) = S ((S (dst_index_prefix_resulttable)) * dst_negative_scale_prefix_resulttable)) /\ exists ff_q_pvs_prefix_resulttableentrynegative. dst_negative_code_prefix_resulttable = ff_q_pvs_prefix_resulttableentrynegative * S ((S (dst_index_prefix_resulttable)) * dst_negative_scale_prefix_resulttable) + (dst_negative_prefix_resulttable))) /\ (exists ge_balance_positive_prefix_resulttableentryvalue ge_balance_negative_prefix_resulttableentryvalue. (((((dst_value_prefix_resulttable) = 2 * (ge_balance_positive_prefix_resulttableentryvalue) /\ (ge_balance_negative_prefix_resulttableentryvalue) = 0) \/ exists ge_signed_half_prefix_resulttableentryvaluedecode. (((dst_value_prefix_resulttable) = 2 * ge_signed_half_prefix_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_prefix_resulttableentryvalue) = 0) /\ (ge_balance_negative_prefix_resulttableentryvalue) = S ge_signed_half_prefix_resulttableentryvaluedecode))) /\ ((dst_positive_prefix_resulttable) + ge_balance_negative_prefix_resulttableentryvalue = (dst_negative_prefix_resulttable) + ge_balance_positive_prefix_resulttableentryvalue))))))))) /\ (forall dc_index_prefix_result dc_value_prefix_result. (exists pvs_le_gap_prefix_resultdomain. pvs_le_gap_prefix_resultdomain + (dc_index_prefix_result) = (k)) -> (exists dst_positive_code_prefix_resultlookup dst_positive_scale_prefix_resultlookup dst_negative_code_prefix_resultlookup dst_negative_scale_prefix_resultlookup dst_positive_prefix_resultlookup dst_negative_prefix_resultlookup. (((M) = (((((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) * S ((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) + ((dst_positive_scale_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))) * S ((((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) * S ((dst_positive_code_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup)) + ((dst_positive_scale_prefix_resultlookup) + (dst_positive_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))) + ((((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup))) + (((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) * S ((dst_negative_code_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)) + ((dst_negative_scale_prefix_resultlookup) + (dst_negative_scale_prefix_resultlookup)))))) /\ (((((exists ff_h_pvs_prefix_resultlookuppositive. ff_h_pvs_prefix_resultlookuppositive + S (dst_positive_prefix_resultlookup) = S ((S (dc_index_prefix_result)) * dst_positive_scale_prefix_resultlookup)) /\ exists ff_q_pvs_prefix_resultlookuppositive. dst_positive_code_prefix_resultlookup = ff_q_pvs_prefix_resultlookuppositive * S ((S (dc_index_prefix_result)) * dst_positive_scale_prefix_resultlookup) + (dst_positive_prefix_resultlookup))) /\ (((((exists ff_h_pvs_prefix_resultlookupnegative. ff_h_pvs_prefix_resultlookupnegative + S (dst_negative_prefix_resultlookup) = S ((S (dc_index_prefix_result)) * dst_negative_scale_prefix_resultlookup)) /\ exists ff_q_pvs_prefix_resultlookupnegative. dst_negative_code_prefix_resultlookup = ff_q_pvs_prefix_resultlookupnegative * S ((S (dc_index_prefix_result)) * dst_negative_scale_prefix_resultlookup) + (dst_negative_prefix_resultlookup))) /\ (exists ge_balance_positive_prefix_resultlookupvalue ge_balance_negative_prefix_resultlookupvalue. (((((dc_value_prefix_result) = 2 * (ge_balance_positive_prefix_resultlookupvalue) /\ (ge_balance_negative_prefix_resultlookupvalue) = 0) \/ exists ge_signed_half_prefix_resultlookupvaluedecode. (((dc_value_prefix_result) = 2 * ge_signed_half_prefix_resultlookupvaluedecode + 1 /\ (ge_balance_positive_prefix_resultlookupvalue) = 0) /\ (ge_balance_negative_prefix_resultlookupvalue) = S ge_signed_half_prefix_resultlookupvaluedecode))) /\ ((dst_positive_prefix_resultlookup) + ge_balance_negative_prefix_resultlookupvalue = (dst_negative_prefix_resultlookup) + ge_balance_positive_prefix_resultlookupvalue))))))))) -> ((((~((dc_index_prefix_result)=0)) /\ (exists dc_quotient_prefix_resultentry dc_left_prefix_resultentry dc_right_prefix_resultentry. (((n)=(dc_index_prefix_result)*dc_quotient_prefix_resultentry) /\ (((exists dst_positive_code_prefix_resultentryleft dst_positive_scale_prefix_resultentryleft dst_negative_code_prefix_resultentryleft dst_negative_scale_prefix_resultentryleft dst_positive_prefix_resultentryleft dst_negative_prefix_resultentryleft. (((H) = (((((dst_positive_code_prefix_resultentryleft) + (dst_positive_scale_prefix_resultentryleft)) * S ((dst_positive_code_prefix_resultentryleft) + (dst_positive_scale_prefix_resultentryleft)) + ((dst_positive_scale_prefix_resultentryleft) + (dst_positive_scale_prefix_resultentryleft))) + (((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) * S ((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) + ((dst_negative_scale_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)))) * S ((((dst_positive_code_prefix_resultentryleft) + (dst_positive_scale_prefix_resultentryleft)) * S ((dst_positive_code_prefix_resultentryleft) + (dst_positive_scale_prefix_resultentryleft)) + ((dst_positive_scale_prefix_resultentryleft) + (dst_positive_scale_prefix_resultentryleft))) + (((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) * S ((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) + ((dst_negative_scale_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)))) + ((((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) * S ((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) + ((dst_negative_scale_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft))) + (((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) * S ((dst_negative_code_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)) + ((dst_negative_scale_prefix_resultentryleft) + (dst_negative_scale_prefix_resultentryleft)))))) /\ (((((exists ff_h_pvs_prefix_resultentryleftpositive. ff_h_pvs_prefix_resultentryleftpositive + S (dst_positive_prefix_resultentryleft) = S ((S (dc_index_prefix_result)) * dst_positive_scale_prefix_resultentryleft)) /\ exists ff_q_pvs_prefix_resultentryleftpositive. dst_positive_code_prefix_resultentryleft = ff_q_pvs_prefix_resultentryleftpositive * S ((S (dc_index_prefix_result)) * dst_positive_scale_prefix_resultentryleft) + (dst_positive_prefix_resultentryleft))) /\ (((((exists ff_h_pvs_prefix_resultentryleftnegative. ff_h_pvs_prefix_resultentryleftnegative + S (dst_negative_prefix_resultentryleft) = S ((S (dc_index_prefix_result)) * dst_negative_scale_prefix_resultentryleft)) /\ exists ff_q_pvs_prefix_resultentryleftnegative. dst_negative_code_prefix_resultentryleft = ff_q_pvs_prefix_resultentryleftnegative * S ((S (dc_index_prefix_result)) * dst_negative_scale_prefix_resultentryleft) + (dst_negative_prefix_resultentryleft))) /\ (exists ge_balance_positive_prefix_resultentryleftvalue ge_balance_negative_prefix_resultentryleftvalue. (((((dc_left_prefix_resultentry) = 2 * (ge_balance_positive_prefix_resultentryleftvalue) /\ (ge_balance_negative_prefix_resultentryleftvalue) = 0) \/ exists ge_signed_half_prefix_resultentryleftvaluedecode. (((dc_left_prefix_resultentry) = 2 * ge_signed_half_prefix_resultentryleftvaluedecode + 1 /\ (ge_balance_positive_prefix_resultentryleftvalue) = 0) /\ (ge_balance_negative_prefix_resultentryleftvalue) = S ge_signed_half_prefix_resultentryleftvaluedecode))) /\ ((dst_positive_prefix_resultentryleft) + ge_balance_negative_prefix_resultentryleftvalue = (dst_negative_prefix_resultentryleft) + ge_balance_positive_prefix_resultentryleftvalue))))))))) /\ (((exists dst_positive_code_prefix_resultentryright dst_positive_scale_prefix_resultentryright dst_negative_code_prefix_resultentryright dst_negative_scale_prefix_resultentryright dst_positive_prefix_resultentryright dst_negative_prefix_resultentryright. (((G) = (((((dst_positive_code_prefix_resultentryright) + (dst_positive_scale_prefix_resultentryright)) * S ((dst_positive_code_prefix_resultentryright) + (dst_positive_scale_prefix_resultentryright)) + ((dst_positive_scale_prefix_resultentryright) + (dst_positive_scale_prefix_resultentryright))) + (((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) * S ((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) + ((dst_negative_scale_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)))) * S ((((dst_positive_code_prefix_resultentryright) + (dst_positive_scale_prefix_resultentryright)) * S ((dst_positive_code_prefix_resultentryright) + (dst_positive_scale_prefix_resultentryright)) + ((dst_positive_scale_prefix_resultentryright) + (dst_positive_scale_prefix_resultentryright))) + (((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) * S ((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) + ((dst_negative_scale_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)))) + ((((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) * S ((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) + ((dst_negative_scale_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright))) + (((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) * S ((dst_negative_code_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)) + ((dst_negative_scale_prefix_resultentryright) + (dst_negative_scale_prefix_resultentryright)))))) /\ (((((exists ff_h_pvs_prefix_resultentryrightpositive. ff_h_pvs_prefix_resultentryrightpositive + S (dst_positive_prefix_resultentryright) = S ((S (dc_quotient_prefix_resultentry)) * dst_positive_scale_prefix_resultentryright)) /\ exists ff_q_pvs_prefix_resultentryrightpositive. dst_positive_code_prefix_resultentryright = ff_q_pvs_prefix_resultentryrightpositive * S ((S (dc_quotient_prefix_resultentry)) * dst_positive_scale_prefix_resultentryright) + (dst_positive_prefix_resultentryright))) /\ (((((exists ff_h_pvs_prefix_resultentryrightnegative. ff_h_pvs_prefix_resultentryrightnegative + S (dst_negative_prefix_resultentryright) = S ((S (dc_quotient_prefix_resultentry)) * dst_negative_scale_prefix_resultentryright)) /\ exists ff_q_pvs_prefix_resultentryrightnegative. dst_negative_code_prefix_resultentryright = ff_q_pvs_prefix_resultentryrightnegative * S ((S (dc_quotient_prefix_resultentry)) * dst_negative_scale_prefix_resultentryright) + (dst_negative_prefix_resultentryright))) /\ (exists ge_balance_positive_prefix_resultentryrightvalue ge_balance_negative_prefix_resultentryrightvalue. (((((dc_right_prefix_resultentry) = 2 * (ge_balance_positive_prefix_resultentryrightvalue) /\ (ge_balance_negative_prefix_resultentryrightvalue) = 0) \/ exists ge_signed_half_prefix_resultentryrightvaluedecode. (((dc_right_prefix_resultentry) = 2 * ge_signed_half_prefix_resultentryrightvaluedecode + 1 /\ (ge_balance_positive_prefix_resultentryrightvalue) = 0) /\ (ge_balance_negative_prefix_resultentryrightvalue) = S ge_signed_half_prefix_resultentryrightvaluedecode))) /\ ((dst_positive_prefix_resultentryright) + ge_balance_negative_prefix_resultentryrightvalue = (dst_negative_prefix_resultentryright) + ge_balance_positive_prefix_resultentryrightvalue))))))))) /\ (exists sto_ap_prefix_resultentryproduct sto_an_prefix_resultentryproduct sto_bp_prefix_resultentryproduct sto_bn_prefix_resultentryproduct sto_cp_prefix_resultentryproduct sto_cn_prefix_resultentryproduct. (((((dc_left_prefix_resultentry) = 2 * (sto_ap_prefix_resultentryproduct) /\ (sto_an_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_prefix_resultentryproductleft. (((dc_left_prefix_resultentry) = 2 * ge_signed_half_prefix_resultentryproductleft + 1 /\ (sto_ap_prefix_resultentryproduct) = 0) /\ (sto_an_prefix_resultentryproduct) = S ge_signed_half_prefix_resultentryproductleft))) /\ ((((((dc_right_prefix_resultentry) = 2 * (sto_bp_prefix_resultentryproduct) /\ (sto_bn_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_prefix_resultentryproductright. (((dc_right_prefix_resultentry) = 2 * ge_signed_half_prefix_resultentryproductright + 1 /\ (sto_bp_prefix_resultentryproduct) = 0) /\ (sto_bn_prefix_resultentryproduct) = S ge_signed_half_prefix_resultentryproductright))) /\ ((((((dc_value_prefix_result) = 2 * (sto_cp_prefix_resultentryproduct) /\ (sto_cn_prefix_resultentryproduct) = 0) \/ exists ge_signed_half_prefix_resultentryproductoutput. (((dc_value_prefix_result) = 2 * ge_signed_half_prefix_resultentryproductoutput + 1 /\ (sto_cp_prefix_resultentryproduct) = 0) /\ (sto_cn_prefix_resultentryproduct) = S ge_signed_half_prefix_resultentryproductoutput))) /\ ((sto_ap_prefix_resultentryproduct * sto_bp_prefix_resultentryproduct + sto_an_prefix_resultentryproduct * sto_bn_prefix_resultentryproduct) + sto_cn_prefix_resultentryproduct = (sto_ap_prefix_resultentryproduct * sto_bn_prefix_resultentryproduct + sto_an_prefix_resultentryproduct * sto_bp_prefix_resultentryproduct) + sto_cp_prefix_resultentryproduct))))))))))))))) \/ ((((dc_index_prefix_result)=0 \/ ~(exists pvs_factor_prefix_resultentrynondivisor. (n) = (dc_index_prefix_result) * pvs_factor_prefix_resultentrynondivisor)) /\ ((dc_value_prefix_result)=0)))))))