dirichlet_convolution_strict_prefix_exists

forall N k F G. (exists dst_positive_code_remainder_fixed_input dst_positive_scale_remainder_fixed_input dst_negative_code_remainder_fixed_input dst_negative_scale_remainder_fixed_input. (((F) = (((((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) * S ((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) + ((dst_positive_scale_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input))) + (((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)))) * S ((((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) * S ((dst_positive_code_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input)) + ((dst_positive_scale_remainder_fixed_input) + (dst_positive_scale_remainder_fixed_input))) + (((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)))) + ((((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input))) + (((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) * S ((dst_negative_code_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)) + ((dst_negative_scale_remainder_fixed_input) + (dst_negative_scale_remainder_fixed_input)))))) /\ (forall dst_index_remainder_fixed_input. (exists pvs_le_gap_remainder_fixed_inputdomain. pvs_le_gap_remainder_fixed_inputdomain + (dst_index_remainder_fixed_input) = (N)) -> exists dst_positive_remainder_fixed_input dst_negative_remainder_fixed_input dst_value_remainder_fixed_input. ((((exists ff_h_pvs_remainder_fixed_inputentrypositive. ff_h_pvs_remainder_fixed_inputentrypositive + S (dst_positive_remainder_fixed_input) = S ((S (dst_index_remainder_fixed_input)) * dst_positive_scale_remainder_fixed_input)) /\ exists ff_q_pvs_remainder_fixed_inputentrypositive. dst_positive_code_remainder_fixed_input = ff_q_pvs_remainder_fixed_inputentrypositive * S ((S (dst_index_remainder_fixed_input)) * dst_positive_scale_remainder_fixed_input) + (dst_positive_remainder_fixed_input))) /\ (((((exists ff_h_pvs_remainder_fixed_inputentrynegative. ff_h_pvs_remainder_fixed_inputentrynegative + S (dst_negative_remainder_fixed_input) = S ((S (dst_index_remainder_fixed_input)) * dst_negative_scale_remainder_fixed_input)) /\ exists ff_q_pvs_remainder_fixed_inputentrynegative. dst_negative_code_remainder_fixed_input = ff_q_pvs_remainder_fixed_inputentrynegative * S ((S (dst_index_remainder_fixed_input)) * dst_negative_scale_remainder_fixed_input) + (dst_negative_remainder_fixed_input))) /\ (exists ge_balance_positive_remainder_fixed_inputentryvalue ge_balance_negative_remainder_fixed_inputentryvalue. (((((dst_value_remainder_fixed_input) = 2 * (ge_balance_positive_remainder_fixed_inputentryvalue) /\ (ge_balance_negative_remainder_fixed_inputentryvalue) = 0) \/ exists ge_signed_half_remainder_fixed_inputentryvaluedecode. (((dst_value_remainder_fixed_input) = 2 * ge_signed_half_remainder_fixed_inputentryvaluedecode + 1 /\ (ge_balance_positive_remainder_fixed_inputentryvalue) = 0) /\ (ge_balance_negative_remainder_fixed_inputentryvalue) = S ge_signed_half_remainder_fixed_inputentryvaluedecode))) /\ ((dst_positive_remainder_fixed_input) + ge_balance_negative_remainder_fixed_inputentryvalue = (dst_negative_remainder_fixed_input) + ge_balance_positive_remainder_fixed_inputentryvalue))))))))) -> (exists dst_positive_code_remainder_partial_input dst_positive_scale_remainder_partial_input dst_negative_code_remainder_partial_input dst_negative_scale_remainder_partial_input. (((G) = (((((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) * S ((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) + ((dst_positive_scale_remainder_partial_input) + (dst_positive_scale_remainder_partial_input))) + (((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)))) * S ((((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) * S ((dst_positive_code_remainder_partial_input) + (dst_positive_scale_remainder_partial_input)) + ((dst_positive_scale_remainder_partial_input) + (dst_positive_scale_remainder_partial_input))) + (((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)))) + ((((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input))) + (((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) * S ((dst_negative_code_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)) + ((dst_negative_scale_remainder_partial_input) + (dst_negative_scale_remainder_partial_input)))))) /\ (forall dst_index_remainder_partial_input. (exists pvs_le_gap_remainder_partial_inputdomain. pvs_le_gap_remainder_partial_inputdomain + (dst_index_remainder_partial_input) = (k)) -> exists dst_positive_remainder_partial_input dst_negative_remainder_partial_input dst_value_remainder_partial_input. ((((exists ff_h_pvs_remainder_partial_inputentrypositive. ff_h_pvs_remainder_partial_inputentrypositive + S (dst_positive_remainder_partial_input) = S ((S (dst_index_remainder_partial_input)) * dst_positive_scale_remainder_partial_input)) /\ exists ff_q_pvs_remainder_partial_inputentrypositive. dst_positive_code_remainder_partial_input = ff_q_pvs_remainder_partial_inputentrypositive * S ((S (dst_index_remainder_partial_input)) * dst_positive_scale_remainder_partial_input) + (dst_positive_remainder_partial_input))) /\ (((((exists ff_h_pvs_remainder_partial_inputentrynegative. ff_h_pvs_remainder_partial_inputentrynegative + S (dst_negative_remainder_partial_input) = S ((S (dst_index_remainder_partial_input)) * dst_negative_scale_remainder_partial_input)) /\ exists ff_q_pvs_remainder_partial_inputentrynegative. dst_negative_code_remainder_partial_input = ff_q_pvs_remainder_partial_inputentrynegative * S ((S (dst_index_remainder_partial_input)) * dst_negative_scale_remainder_partial_input) + (dst_negative_remainder_partial_input))) /\ (exists ge_balance_positive_remainder_partial_inputentryvalue ge_balance_negative_remainder_partial_inputentryvalue. (((((dst_value_remainder_partial_input) = 2 * (ge_balance_positive_remainder_partial_inputentryvalue) /\ (ge_balance_negative_remainder_partial_inputentryvalue) = 0) \/ exists ge_signed_half_remainder_partial_inputentryvaluedecode. (((dst_value_remainder_partial_input) = 2 * ge_signed_half_remainder_partial_inputentryvaluedecode + 1 /\ (ge_balance_positive_remainder_partial_inputentryvalue) = 0) /\ (ge_balance_negative_remainder_partial_inputentryvalue) = S ge_signed_half_remainder_partial_inputentryvaluedecode))) /\ ((dst_positive_remainder_partial_input) + ge_balance_negative_remainder_partial_inputentryvalue = (dst_negative_remainder_partial_input) + ge_balance_positive_remainder_partial_inputentryvalue))))))))) -> exists M r. (((exists dst_positive_code_remainder_result_prefixtable dst_positive_scale_remainder_result_prefixtable dst_negative_code_remainder_result_prefixtable dst_negative_scale_remainder_result_prefixtable. (((M) = (((((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) * S ((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) + ((dst_positive_scale_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable))) + (((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)))) * S ((((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) * S ((dst_positive_code_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable)) + ((dst_positive_scale_remainder_result_prefixtable) + (dst_positive_scale_remainder_result_prefixtable))) + (((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)))) + ((((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable))) + (((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) * S ((dst_negative_code_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)) + ((dst_negative_scale_remainder_result_prefixtable) + (dst_negative_scale_remainder_result_prefixtable)))))) /\ (forall dst_index_remainder_result_prefixtable. (exists pvs_le_gap_remainder_result_prefixtabledomain. pvs_le_gap_remainder_result_prefixtabledomain + (dst_index_remainder_result_prefixtable) = (k)) -> exists dst_positive_remainder_result_prefixtable dst_negative_remainder_result_prefixtable dst_value_remainder_result_prefixtable. ((((exists ff_h_pvs_remainder_result_prefixtableentrypositive. ff_h_pvs_remainder_result_prefixtableentrypositive + S (dst_positive_remainder_result_prefixtable) = S ((S (dst_index_remainder_result_prefixtable)) * dst_positive_scale_remainder_result_prefixtable)) /\ exists ff_q_pvs_remainder_result_prefixtableentrypositive. dst_positive_code_remainder_result_prefixtable = ff_q_pvs_remainder_result_prefixtableentrypositive * S ((S (dst_index_remainder_result_prefixtable)) * dst_positive_scale_remainder_result_prefixtable) + (dst_positive_remainder_result_prefixtable))) /\ (((((exists ff_h_pvs_remainder_result_prefixtableentrynegative. ff_h_pvs_remainder_result_prefixtableentrynegative + S (dst_negative_remainder_result_prefixtable) = S ((S (dst_index_remainder_result_prefixtable)) * dst_negative_scale_remainder_result_prefixtable)) /\ exists ff_q_pvs_remainder_result_prefixtableentrynegative. dst_negative_code_remainder_result_prefixtable = ff_q_pvs_remainder_result_prefixtableentrynegative * S ((S (dst_index_remainder_result_prefixtable)) * dst_negative_scale_remainder_result_prefixtable) + (dst_negative_remainder_result_prefixtable))) /\ (exists ge_balance_positive_remainder_result_prefixtableentryvalue ge_balance_negative_remainder_result_prefixtableentryvalue. (((((dst_value_remainder_result_prefixtable) = 2 * (ge_balance_positive_remainder_result_prefixtableentryvalue) /\ (ge_balance_negative_remainder_result_prefixtableentryvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixtableentryvaluedecode. (((dst_value_remainder_result_prefixtable) = 2 * ge_signed_half_remainder_result_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixtableentryvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixtableentryvalue) = S ge_signed_half_remainder_result_prefixtableentryvaluedecode))) /\ ((dst_positive_remainder_result_prefixtable) + ge_balance_negative_remainder_result_prefixtableentryvalue = (dst_negative_remainder_result_prefixtable) + ge_balance_positive_remainder_result_prefixtableentryvalue))))))))) /\ (forall dc_index_remainder_result_prefix dc_value_remainder_result_prefix. (exists pvs_le_gap_remainder_result_prefixdomain. pvs_le_gap_remainder_result_prefixdomain + (dc_index_remainder_result_prefix) = (k)) -> (exists dst_positive_code_remainder_result_prefixlookup dst_positive_scale_remainder_result_prefixlookup dst_negative_code_remainder_result_prefixlookup dst_negative_scale_remainder_result_prefixlookup dst_positive_remainder_result_prefixlookup dst_negative_remainder_result_prefixlookup. (((M) = (((((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) * S ((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) + ((dst_positive_scale_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup))) + (((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)))) * S ((((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) * S ((dst_positive_code_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup)) + ((dst_positive_scale_remainder_result_prefixlookup) + (dst_positive_scale_remainder_result_prefixlookup))) + (((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)))) + ((((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup))) + (((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) * S ((dst_negative_code_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)) + ((dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_scale_remainder_result_prefixlookup)))))) /\ (((((exists ff_h_pvs_remainder_result_prefixlookuppositive. ff_h_pvs_remainder_result_prefixlookuppositive + S (dst_positive_remainder_result_prefixlookup) = S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixlookup)) /\ exists ff_q_pvs_remainder_result_prefixlookuppositive. dst_positive_code_remainder_result_prefixlookup = ff_q_pvs_remainder_result_prefixlookuppositive * S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixlookup) + (dst_positive_remainder_result_prefixlookup))) /\ (((((exists ff_h_pvs_remainder_result_prefixlookupnegative. ff_h_pvs_remainder_result_prefixlookupnegative + S (dst_negative_remainder_result_prefixlookup) = S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixlookup)) /\ exists ff_q_pvs_remainder_result_prefixlookupnegative. dst_negative_code_remainder_result_prefixlookup = ff_q_pvs_remainder_result_prefixlookupnegative * S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixlookup) + (dst_negative_remainder_result_prefixlookup))) /\ (exists ge_balance_positive_remainder_result_prefixlookupvalue ge_balance_negative_remainder_result_prefixlookupvalue. (((((dc_value_remainder_result_prefix) = 2 * (ge_balance_positive_remainder_result_prefixlookupvalue) /\ (ge_balance_negative_remainder_result_prefixlookupvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixlookupvaluedecode. (((dc_value_remainder_result_prefix) = 2 * ge_signed_half_remainder_result_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixlookupvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixlookupvalue) = S ge_signed_half_remainder_result_prefixlookupvaluedecode))) /\ ((dst_positive_remainder_result_prefixlookup) + ge_balance_negative_remainder_result_prefixlookupvalue = (dst_negative_remainder_result_prefixlookup) + ge_balance_positive_remainder_result_prefixlookupvalue))))))))) -> ((((~((dc_index_remainder_result_prefix)=0)) /\ (exists dc_quotient_remainder_result_prefixentry dc_left_remainder_result_prefixentry dc_right_remainder_result_prefixentry. (((S k)=(dc_index_remainder_result_prefix)*dc_quotient_remainder_result_prefixentry) /\ (((exists dst_positive_code_remainder_result_prefixentryleft dst_positive_scale_remainder_result_prefixentryleft dst_negative_code_remainder_result_prefixentryleft dst_negative_scale_remainder_result_prefixentryleft dst_positive_remainder_result_prefixentryleft dst_negative_remainder_result_prefixentryleft. (((G) = (((((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) * S ((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) + ((dst_positive_scale_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft))) + (((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)))) * S ((((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) * S ((dst_positive_code_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft)) + ((dst_positive_scale_remainder_result_prefixentryleft) + (dst_positive_scale_remainder_result_prefixentryleft))) + (((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)))) + ((((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft))) + (((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) * S ((dst_negative_code_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)) + ((dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_scale_remainder_result_prefixentryleft)))))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryleftpositive. ff_h_pvs_remainder_result_prefixentryleftpositive + S (dst_positive_remainder_result_prefixentryleft) = S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixentryleft)) /\ exists ff_q_pvs_remainder_result_prefixentryleftpositive. dst_positive_code_remainder_result_prefixentryleft = ff_q_pvs_remainder_result_prefixentryleftpositive * S ((S (dc_index_remainder_result_prefix)) * dst_positive_scale_remainder_result_prefixentryleft) + (dst_positive_remainder_result_prefixentryleft))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryleftnegative. ff_h_pvs_remainder_result_prefixentryleftnegative + S (dst_negative_remainder_result_prefixentryleft) = S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixentryleft)) /\ exists ff_q_pvs_remainder_result_prefixentryleftnegative. dst_negative_code_remainder_result_prefixentryleft = ff_q_pvs_remainder_result_prefixentryleftnegative * S ((S (dc_index_remainder_result_prefix)) * dst_negative_scale_remainder_result_prefixentryleft) + (dst_negative_remainder_result_prefixentryleft))) /\ (exists ge_balance_positive_remainder_result_prefixentryleftvalue ge_balance_negative_remainder_result_prefixentryleftvalue. (((((dc_left_remainder_result_prefixentry) = 2 * (ge_balance_positive_remainder_result_prefixentryleftvalue) /\ (ge_balance_negative_remainder_result_prefixentryleftvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixentryleftvaluedecode. (((dc_left_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixentryleftvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixentryleftvalue) = S ge_signed_half_remainder_result_prefixentryleftvaluedecode))) /\ ((dst_positive_remainder_result_prefixentryleft) + ge_balance_negative_remainder_result_prefixentryleftvalue = (dst_negative_remainder_result_prefixentryleft) + ge_balance_positive_remainder_result_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_remainder_result_prefixentryright dst_positive_scale_remainder_result_prefixentryright dst_negative_code_remainder_result_prefixentryright dst_negative_scale_remainder_result_prefixentryright dst_positive_remainder_result_prefixentryright dst_negative_remainder_result_prefixentryright. (((F) = (((((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) * S ((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) + ((dst_positive_scale_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright))) + (((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)))) * S ((((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) * S ((dst_positive_code_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright)) + ((dst_positive_scale_remainder_result_prefixentryright) + (dst_positive_scale_remainder_result_prefixentryright))) + (((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)))) + ((((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright))) + (((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) * S ((dst_negative_code_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)) + ((dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_scale_remainder_result_prefixentryright)))))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryrightpositive. ff_h_pvs_remainder_result_prefixentryrightpositive + S (dst_positive_remainder_result_prefixentryright) = S ((S (dc_quotient_remainder_result_prefixentry)) * dst_positive_scale_remainder_result_prefixentryright)) /\ exists ff_q_pvs_remainder_result_prefixentryrightpositive. dst_positive_code_remainder_result_prefixentryright = ff_q_pvs_remainder_result_prefixentryrightpositive * S ((S (dc_quotient_remainder_result_prefixentry)) * dst_positive_scale_remainder_result_prefixentryright) + (dst_positive_remainder_result_prefixentryright))) /\ (((((exists ff_h_pvs_remainder_result_prefixentryrightnegative. ff_h_pvs_remainder_result_prefixentryrightnegative + S (dst_negative_remainder_result_prefixentryright) = S ((S (dc_quotient_remainder_result_prefixentry)) * dst_negative_scale_remainder_result_prefixentryright)) /\ exists ff_q_pvs_remainder_result_prefixentryrightnegative. dst_negative_code_remainder_result_prefixentryright = ff_q_pvs_remainder_result_prefixentryrightnegative * S ((S (dc_quotient_remainder_result_prefixentry)) * dst_negative_scale_remainder_result_prefixentryright) + (dst_negative_remainder_result_prefixentryright))) /\ (exists ge_balance_positive_remainder_result_prefixentryrightvalue ge_balance_negative_remainder_result_prefixentryrightvalue. (((((dc_right_remainder_result_prefixentry) = 2 * (ge_balance_positive_remainder_result_prefixentryrightvalue) /\ (ge_balance_negative_remainder_result_prefixentryrightvalue) = 0) \/ exists ge_signed_half_remainder_result_prefixentryrightvaluedecode. (((dc_right_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_remainder_result_prefixentryrightvalue) = 0) /\ (ge_balance_negative_remainder_result_prefixentryrightvalue) = S ge_signed_half_remainder_result_prefixentryrightvaluedecode))) /\ ((dst_positive_remainder_result_prefixentryright) + ge_balance_negative_remainder_result_prefixentryrightvalue = (dst_negative_remainder_result_prefixentryright) + ge_balance_positive_remainder_result_prefixentryrightvalue))))))))) /\ (exists sto_ap_remainder_result_prefixentryproduct sto_an_remainder_result_prefixentryproduct sto_bp_remainder_result_prefixentryproduct sto_bn_remainder_result_prefixentryproduct sto_cp_remainder_result_prefixentryproduct sto_cn_remainder_result_prefixentryproduct. (((((dc_left_remainder_result_prefixentry) = 2 * (sto_ap_remainder_result_prefixentryproduct) /\ (sto_an_remainder_result_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_result_prefixentryproductleft. (((dc_left_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryproductleft + 1 /\ (sto_ap_remainder_result_prefixentryproduct) = 0) /\ (sto_an_remainder_result_prefixentryproduct) = S ge_signed_half_remainder_result_prefixentryproductleft))) /\ ((((((dc_right_remainder_result_prefixentry) = 2 * (sto_bp_remainder_result_prefixentryproduct) /\ (sto_bn_remainder_result_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_result_prefixentryproductright. (((dc_right_remainder_result_prefixentry) = 2 * ge_signed_half_remainder_result_prefixentryproductright + 1 /\ (sto_bp_remainder_result_prefixentryproduct) = 0) /\ (sto_bn_remainder_result_prefixentryproduct) = S ge_signed_half_remainder_result_prefixentryproductright))) /\ ((((((dc_value_remainder_result_prefix) = 2 * (sto_cp_remainder_result_prefixentryproduct) /\ (sto_cn_remainder_result_prefixentryproduct) = 0) \/ exists ge_signed_half_remainder_result_prefixentryproductoutput. (((dc_value_remainder_result_prefix) = 2 * ge_signed_half_remainder_result_prefixentryproductoutput + 1 /\ (sto_cp_remainder_result_prefixentryproduct) = 0) /\ (sto_cn_remainder_result_prefixentryproduct) = S ge_signed_half_remainder_result_prefixentryproductoutput))) /\ ((sto_ap_remainder_result_prefixentryproduct * sto_bp_remainder_result_prefixentryproduct + sto_an_remainder_result_prefixentryproduct * sto_bn_remainder_result_prefixentryproduct) + sto_cn_remainder_result_prefixentryproduct = (sto_ap_remainder_result_prefixentryproduct * sto_bn_remainder_result_prefixentryproduct + sto_an_remainder_result_prefixentryproduct * sto_bp_remainder_result_prefixentryproduct) + sto_cp_remainder_result_prefixentryproduct))))))))))))))) \/ ((((dc_index_remainder_result_prefix)=0 \/ ~(exists pvs_factor_remainder_result_prefixentrynondivisor. (S k) = (dc_index_remainder_result_prefix) * pvs_factor_remainder_result_prefixentrynondivisor)) /\ ((dc_value_remainder_result_prefix)=0))))))) /\ (exists dst_positive_code_remainder_result_sum dst_positive_scale_remainder_result_sum dst_negative_code_remainder_result_sum dst_negative_scale_remainder_result_sum dst_positive_sum_remainder_result_sum dst_negative_sum_remainder_result_sum. (((M) = (((((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) * S ((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) + ((dst_positive_scale_remainder_result_sum) + (dst_positive_scale_remainder_result_sum))) + (((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)))) * S ((((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) * S ((dst_positive_code_remainder_result_sum) + (dst_positive_scale_remainder_result_sum)) + ((dst_positive_scale_remainder_result_sum) + (dst_positive_scale_remainder_result_sum))) + (((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)))) + ((((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum))) + (((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) * S ((dst_negative_code_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)) + ((dst_negative_scale_remainder_result_sum) + (dst_negative_scale_remainder_result_sum)))))) /\ (((exists fs_u_dst_remainder_result_sumpositive fs_v_dst_remainder_result_sumpositive. ((((exists fs_h_dst_remainder_result_sumpositive_body_start. fs_h_dst_remainder_result_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_start. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_start * S ((S (0)) * fs_v_dst_remainder_result_sumpositive) + (0))) /\ ((((exists fs_h_dst_remainder_result_sumpositive_body_terminal. fs_h_dst_remainder_result_sumpositive_body_terminal + S (dst_positive_sum_remainder_result_sum) = S ((S (S k)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_terminal. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_terminal * S ((S (S k)) * fs_v_dst_remainder_result_sumpositive) + (dst_positive_sum_remainder_result_sum))) /\ forall fs_i_dst_remainder_result_sumpositive_body_steps. (exists fs_lt_dst_remainder_result_sumpositive_body_steps_bound. fs_lt_dst_remainder_result_sumpositive_body_steps_bound + S fs_i_dst_remainder_result_sumpositive_body_steps = S k) -> exists fs_a_dst_remainder_result_sumpositive_body_steps fs_r_dst_remainder_result_sumpositive_body_steps fs_s_dst_remainder_result_sumpositive_body_steps. ((((exists fs_h_dst_remainder_result_sumpositive_body_steps_summand. fs_h_dst_remainder_result_sumpositive_body_steps_summand + S (fs_a_dst_remainder_result_sumpositive_body_steps) = S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * dst_positive_scale_remainder_result_sum)) /\ exists fs_q_dst_remainder_result_sumpositive_body_steps_summand. dst_positive_code_remainder_result_sum = fs_q_dst_remainder_result_sumpositive_body_steps_summand * S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * dst_positive_scale_remainder_result_sum) + (fs_a_dst_remainder_result_sumpositive_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumpositive_body_steps_partial. fs_h_dst_remainder_result_sumpositive_body_steps_partial + S (fs_r_dst_remainder_result_sumpositive_body_steps) = S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_steps_partial. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_steps_partial * S ((S (fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive) + (fs_r_dst_remainder_result_sumpositive_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumpositive_body_steps_successor. fs_h_dst_remainder_result_sumpositive_body_steps_successor + S (fs_s_dst_remainder_result_sumpositive_body_steps) = S ((S (S fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive)) /\ exists fs_q_dst_remainder_result_sumpositive_body_steps_successor. fs_u_dst_remainder_result_sumpositive = fs_q_dst_remainder_result_sumpositive_body_steps_successor * S ((S (S fs_i_dst_remainder_result_sumpositive_body_steps)) * fs_v_dst_remainder_result_sumpositive) + (fs_s_dst_remainder_result_sumpositive_body_steps))) /\ fs_s_dst_remainder_result_sumpositive_body_steps = fs_r_dst_remainder_result_sumpositive_body_steps + fs_a_dst_remainder_result_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_remainder_result_sumnegative fs_v_dst_remainder_result_sumnegative. ((((exists fs_h_dst_remainder_result_sumnegative_body_start. fs_h_dst_remainder_result_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_start. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_start * S ((S (0)) * fs_v_dst_remainder_result_sumnegative) + (0))) /\ ((((exists fs_h_dst_remainder_result_sumnegative_body_terminal. fs_h_dst_remainder_result_sumnegative_body_terminal + S (dst_negative_sum_remainder_result_sum) = S ((S (S k)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_terminal. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_terminal * S ((S (S k)) * fs_v_dst_remainder_result_sumnegative) + (dst_negative_sum_remainder_result_sum))) /\ forall fs_i_dst_remainder_result_sumnegative_body_steps. (exists fs_lt_dst_remainder_result_sumnegative_body_steps_bound. fs_lt_dst_remainder_result_sumnegative_body_steps_bound + S fs_i_dst_remainder_result_sumnegative_body_steps = S k) -> exists fs_a_dst_remainder_result_sumnegative_body_steps fs_r_dst_remainder_result_sumnegative_body_steps fs_s_dst_remainder_result_sumnegative_body_steps. ((((exists fs_h_dst_remainder_result_sumnegative_body_steps_summand. fs_h_dst_remainder_result_sumnegative_body_steps_summand + S (fs_a_dst_remainder_result_sumnegative_body_steps) = S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * dst_negative_scale_remainder_result_sum)) /\ exists fs_q_dst_remainder_result_sumnegative_body_steps_summand. dst_negative_code_remainder_result_sum = fs_q_dst_remainder_result_sumnegative_body_steps_summand * S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * dst_negative_scale_remainder_result_sum) + (fs_a_dst_remainder_result_sumnegative_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumnegative_body_steps_partial. fs_h_dst_remainder_result_sumnegative_body_steps_partial + S (fs_r_dst_remainder_result_sumnegative_body_steps) = S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_steps_partial. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_steps_partial * S ((S (fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative) + (fs_r_dst_remainder_result_sumnegative_body_steps))) /\ ((((exists fs_h_dst_remainder_result_sumnegative_body_steps_successor. fs_h_dst_remainder_result_sumnegative_body_steps_successor + S (fs_s_dst_remainder_result_sumnegative_body_steps) = S ((S (S fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative)) /\ exists fs_q_dst_remainder_result_sumnegative_body_steps_successor. fs_u_dst_remainder_result_sumnegative = fs_q_dst_remainder_result_sumnegative_body_steps_successor * S ((S (S fs_i_dst_remainder_result_sumnegative_body_steps)) * fs_v_dst_remainder_result_sumnegative) + (fs_s_dst_remainder_result_sumnegative_body_steps))) /\ fs_s_dst_remainder_result_sumnegative_body_steps = fs_r_dst_remainder_result_sumnegative_body_steps + fs_a_dst_remainder_result_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_remainder_result_sumresult ge_balance_negative_remainder_result_sumresult. (((((r) = 2 * (ge_balance_positive_remainder_result_sumresult) /\ (ge_balance_negative_remainder_result_sumresult) = 0) \/ exists ge_signed_half_remainder_result_sumresultdecode. (((r) = 2 * ge_signed_half_remainder_result_sumresultdecode + 1 /\ (ge_balance_positive_remainder_result_sumresult) = 0) /\ (ge_balance_negative_remainder_result_sumresult) = S ge_signed_half_remainder_result_sumresultdecode))) /\ ((dst_positive_sum_remainder_result_sum) + ge_balance_negative_remainder_result_sumresult = (dst_negative_sum_remainder_result_sum) + ge_balance_positive_remainder_result_sumresult)))))))))