dirichlet_convolution_zero_prefix_sum

Exact expanded first-order arithmetic statement

forall F G n M. (((exists dst_positive_code_zero_prefixtable dst_positive_scale_zero_prefixtable dst_negative_code_zero_prefixtable dst_negative_scale_zero_prefixtable. (((M) = (((((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) * S ((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) + ((dst_positive_scale_zero_prefixtable) + (dst_positive_scale_zero_prefixtable))) + (((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)))) * S ((((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) * S ((dst_positive_code_zero_prefixtable) + (dst_positive_scale_zero_prefixtable)) + ((dst_positive_scale_zero_prefixtable) + (dst_positive_scale_zero_prefixtable))) + (((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)))) + ((((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable))) + (((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) * S ((dst_negative_code_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)) + ((dst_negative_scale_zero_prefixtable) + (dst_negative_scale_zero_prefixtable)))))) /\ (forall dst_index_zero_prefixtable. (exists pvs_le_gap_zero_prefixtabledomain. pvs_le_gap_zero_prefixtabledomain + (dst_index_zero_prefixtable) = (0)) -> exists dst_positive_zero_prefixtable dst_negative_zero_prefixtable dst_value_zero_prefixtable. ((((exists ff_h_pvs_zero_prefixtableentrypositive. ff_h_pvs_zero_prefixtableentrypositive + S (dst_positive_zero_prefixtable) = S ((S (dst_index_zero_prefixtable)) * dst_positive_scale_zero_prefixtable)) /\ exists ff_q_pvs_zero_prefixtableentrypositive. dst_positive_code_zero_prefixtable = ff_q_pvs_zero_prefixtableentrypositive * S ((S (dst_index_zero_prefixtable)) * dst_positive_scale_zero_prefixtable) + (dst_positive_zero_prefixtable))) /\ (((((exists ff_h_pvs_zero_prefixtableentrynegative. ff_h_pvs_zero_prefixtableentrynegative + S (dst_negative_zero_prefixtable) = S ((S (dst_index_zero_prefixtable)) * dst_negative_scale_zero_prefixtable)) /\ exists ff_q_pvs_zero_prefixtableentrynegative. dst_negative_code_zero_prefixtable = ff_q_pvs_zero_prefixtableentrynegative * S ((S (dst_index_zero_prefixtable)) * dst_negative_scale_zero_prefixtable) + (dst_negative_zero_prefixtable))) /\ (exists ge_balance_positive_zero_prefixtableentryvalue ge_balance_negative_zero_prefixtableentryvalue. (((((dst_value_zero_prefixtable) = 2 * (ge_balance_positive_zero_prefixtableentryvalue) /\ (ge_balance_negative_zero_prefixtableentryvalue) = 0) \/ exists ge_signed_half_zero_prefixtableentryvaluedecode. (((dst_value_zero_prefixtable) = 2 * ge_signed_half_zero_prefixtableentryvaluedecode + 1 /\ (ge_balance_positive_zero_prefixtableentryvalue) = 0) /\ (ge_balance_negative_zero_prefixtableentryvalue) = S ge_signed_half_zero_prefixtableentryvaluedecode))) /\ ((dst_positive_zero_prefixtable) + ge_balance_negative_zero_prefixtableentryvalue = (dst_negative_zero_prefixtable) + ge_balance_positive_zero_prefixtableentryvalue))))))))) /\ (forall dc_index_zero_prefix dc_value_zero_prefix. (exists pvs_le_gap_zero_prefixdomain. pvs_le_gap_zero_prefixdomain + (dc_index_zero_prefix) = (0)) -> (exists dst_positive_code_zero_prefixlookup dst_positive_scale_zero_prefixlookup dst_negative_code_zero_prefixlookup dst_negative_scale_zero_prefixlookup dst_positive_zero_prefixlookup dst_negative_zero_prefixlookup. (((M) = (((((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) * S ((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) + ((dst_positive_scale_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup))) + (((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)))) * S ((((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) * S ((dst_positive_code_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup)) + ((dst_positive_scale_zero_prefixlookup) + (dst_positive_scale_zero_prefixlookup))) + (((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)))) + ((((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup))) + (((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) * S ((dst_negative_code_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)) + ((dst_negative_scale_zero_prefixlookup) + (dst_negative_scale_zero_prefixlookup)))))) /\ (((((exists ff_h_pvs_zero_prefixlookuppositive. ff_h_pvs_zero_prefixlookuppositive + S (dst_positive_zero_prefixlookup) = S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixlookup)) /\ exists ff_q_pvs_zero_prefixlookuppositive. dst_positive_code_zero_prefixlookup = ff_q_pvs_zero_prefixlookuppositive * S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixlookup) + (dst_positive_zero_prefixlookup))) /\ (((((exists ff_h_pvs_zero_prefixlookupnegative. ff_h_pvs_zero_prefixlookupnegative + S (dst_negative_zero_prefixlookup) = S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixlookup)) /\ exists ff_q_pvs_zero_prefixlookupnegative. dst_negative_code_zero_prefixlookup = ff_q_pvs_zero_prefixlookupnegative * S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixlookup) + (dst_negative_zero_prefixlookup))) /\ (exists ge_balance_positive_zero_prefixlookupvalue ge_balance_negative_zero_prefixlookupvalue. (((((dc_value_zero_prefix) = 2 * (ge_balance_positive_zero_prefixlookupvalue) /\ (ge_balance_negative_zero_prefixlookupvalue) = 0) \/ exists ge_signed_half_zero_prefixlookupvaluedecode. (((dc_value_zero_prefix) = 2 * ge_signed_half_zero_prefixlookupvaluedecode + 1 /\ (ge_balance_positive_zero_prefixlookupvalue) = 0) /\ (ge_balance_negative_zero_prefixlookupvalue) = S ge_signed_half_zero_prefixlookupvaluedecode))) /\ ((dst_positive_zero_prefixlookup) + ge_balance_negative_zero_prefixlookupvalue = (dst_negative_zero_prefixlookup) + ge_balance_positive_zero_prefixlookupvalue))))))))) -> ((((~((dc_index_zero_prefix)=0)) /\ (exists dc_quotient_zero_prefixentry dc_left_zero_prefixentry dc_right_zero_prefixentry. (((n)=(dc_index_zero_prefix)*dc_quotient_zero_prefixentry) /\ (((exists dst_positive_code_zero_prefixentryleft dst_positive_scale_zero_prefixentryleft dst_negative_code_zero_prefixentryleft dst_negative_scale_zero_prefixentryleft dst_positive_zero_prefixentryleft dst_negative_zero_prefixentryleft. (((F) = (((((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) * S ((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) + ((dst_positive_scale_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft))) + (((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)))) * S ((((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) * S ((dst_positive_code_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft)) + ((dst_positive_scale_zero_prefixentryleft) + (dst_positive_scale_zero_prefixentryleft))) + (((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)))) + ((((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft))) + (((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) * S ((dst_negative_code_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)) + ((dst_negative_scale_zero_prefixentryleft) + (dst_negative_scale_zero_prefixentryleft)))))) /\ (((((exists ff_h_pvs_zero_prefixentryleftpositive. ff_h_pvs_zero_prefixentryleftpositive + S (dst_positive_zero_prefixentryleft) = S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixentryleft)) /\ exists ff_q_pvs_zero_prefixentryleftpositive. dst_positive_code_zero_prefixentryleft = ff_q_pvs_zero_prefixentryleftpositive * S ((S (dc_index_zero_prefix)) * dst_positive_scale_zero_prefixentryleft) + (dst_positive_zero_prefixentryleft))) /\ (((((exists ff_h_pvs_zero_prefixentryleftnegative. ff_h_pvs_zero_prefixentryleftnegative + S (dst_negative_zero_prefixentryleft) = S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixentryleft)) /\ exists ff_q_pvs_zero_prefixentryleftnegative. dst_negative_code_zero_prefixentryleft = ff_q_pvs_zero_prefixentryleftnegative * S ((S (dc_index_zero_prefix)) * dst_negative_scale_zero_prefixentryleft) + (dst_negative_zero_prefixentryleft))) /\ (exists ge_balance_positive_zero_prefixentryleftvalue ge_balance_negative_zero_prefixentryleftvalue. (((((dc_left_zero_prefixentry) = 2 * (ge_balance_positive_zero_prefixentryleftvalue) /\ (ge_balance_negative_zero_prefixentryleftvalue) = 0) \/ exists ge_signed_half_zero_prefixentryleftvaluedecode. (((dc_left_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryleftvaluedecode + 1 /\ (ge_balance_positive_zero_prefixentryleftvalue) = 0) /\ (ge_balance_negative_zero_prefixentryleftvalue) = S ge_signed_half_zero_prefixentryleftvaluedecode))) /\ ((dst_positive_zero_prefixentryleft) + ge_balance_negative_zero_prefixentryleftvalue = (dst_negative_zero_prefixentryleft) + ge_balance_positive_zero_prefixentryleftvalue))))))))) /\ (((exists dst_positive_code_zero_prefixentryright dst_positive_scale_zero_prefixentryright dst_negative_code_zero_prefixentryright dst_negative_scale_zero_prefixentryright dst_positive_zero_prefixentryright dst_negative_zero_prefixentryright. (((G) = (((((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) * S ((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) + ((dst_positive_scale_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright))) + (((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)))) * S ((((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) * S ((dst_positive_code_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright)) + ((dst_positive_scale_zero_prefixentryright) + (dst_positive_scale_zero_prefixentryright))) + (((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)))) + ((((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright))) + (((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) * S ((dst_negative_code_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)) + ((dst_negative_scale_zero_prefixentryright) + (dst_negative_scale_zero_prefixentryright)))))) /\ (((((exists ff_h_pvs_zero_prefixentryrightpositive. ff_h_pvs_zero_prefixentryrightpositive + S (dst_positive_zero_prefixentryright) = S ((S (dc_quotient_zero_prefixentry)) * dst_positive_scale_zero_prefixentryright)) /\ exists ff_q_pvs_zero_prefixentryrightpositive. dst_positive_code_zero_prefixentryright = ff_q_pvs_zero_prefixentryrightpositive * S ((S (dc_quotient_zero_prefixentry)) * dst_positive_scale_zero_prefixentryright) + (dst_positive_zero_prefixentryright))) /\ (((((exists ff_h_pvs_zero_prefixentryrightnegative. ff_h_pvs_zero_prefixentryrightnegative + S (dst_negative_zero_prefixentryright) = S ((S (dc_quotient_zero_prefixentry)) * dst_negative_scale_zero_prefixentryright)) /\ exists ff_q_pvs_zero_prefixentryrightnegative. dst_negative_code_zero_prefixentryright = ff_q_pvs_zero_prefixentryrightnegative * S ((S (dc_quotient_zero_prefixentry)) * dst_negative_scale_zero_prefixentryright) + (dst_negative_zero_prefixentryright))) /\ (exists ge_balance_positive_zero_prefixentryrightvalue ge_balance_negative_zero_prefixentryrightvalue. (((((dc_right_zero_prefixentry) = 2 * (ge_balance_positive_zero_prefixentryrightvalue) /\ (ge_balance_negative_zero_prefixentryrightvalue) = 0) \/ exists ge_signed_half_zero_prefixentryrightvaluedecode. (((dc_right_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryrightvaluedecode + 1 /\ (ge_balance_positive_zero_prefixentryrightvalue) = 0) /\ (ge_balance_negative_zero_prefixentryrightvalue) = S ge_signed_half_zero_prefixentryrightvaluedecode))) /\ ((dst_positive_zero_prefixentryright) + ge_balance_negative_zero_prefixentryrightvalue = (dst_negative_zero_prefixentryright) + ge_balance_positive_zero_prefixentryrightvalue))))))))) /\ (exists sto_ap_zero_prefixentryproduct sto_an_zero_prefixentryproduct sto_bp_zero_prefixentryproduct sto_bn_zero_prefixentryproduct sto_cp_zero_prefixentryproduct sto_cn_zero_prefixentryproduct. (((((dc_left_zero_prefixentry) = 2 * (sto_ap_zero_prefixentryproduct) /\ (sto_an_zero_prefixentryproduct) = 0) \/ exists ge_signed_half_zero_prefixentryproductleft. (((dc_left_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryproductleft + 1 /\ (sto_ap_zero_prefixentryproduct) = 0) /\ (sto_an_zero_prefixentryproduct) = S ge_signed_half_zero_prefixentryproductleft))) /\ ((((((dc_right_zero_prefixentry) = 2 * (sto_bp_zero_prefixentryproduct) /\ (sto_bn_zero_prefixentryproduct) = 0) \/ exists ge_signed_half_zero_prefixentryproductright. (((dc_right_zero_prefixentry) = 2 * ge_signed_half_zero_prefixentryproductright + 1 /\ (sto_bp_zero_prefixentryproduct) = 0) /\ (sto_bn_zero_prefixentryproduct) = S ge_signed_half_zero_prefixentryproductright))) /\ ((((((dc_value_zero_prefix) = 2 * (sto_cp_zero_prefixentryproduct) /\ (sto_cn_zero_prefixentryproduct) = 0) \/ exists ge_signed_half_zero_prefixentryproductoutput. (((dc_value_zero_prefix) = 2 * ge_signed_half_zero_prefixentryproductoutput + 1 /\ (sto_cp_zero_prefixentryproduct) = 0) /\ (sto_cn_zero_prefixentryproduct) = S ge_signed_half_zero_prefixentryproductoutput))) /\ ((sto_ap_zero_prefixentryproduct * sto_bp_zero_prefixentryproduct + sto_an_zero_prefixentryproduct * sto_bn_zero_prefixentryproduct) + sto_cn_zero_prefixentryproduct = (sto_ap_zero_prefixentryproduct * sto_bn_zero_prefixentryproduct + sto_an_zero_prefixentryproduct * sto_bp_zero_prefixentryproduct) + sto_cp_zero_prefixentryproduct))))))))))))))) \/ ((((dc_index_zero_prefix)=0 \/ ~(exists pvs_factor_zero_prefixentrynondivisor. (n) = (dc_index_zero_prefix) * pvs_factor_zero_prefixentrynondivisor)) /\ ((dc_value_zero_prefix)=0))))))) -> (exists dst_positive_code_zero_fold dst_positive_scale_zero_fold dst_negative_code_zero_fold dst_negative_scale_zero_fold dst_positive_sum_zero_fold dst_negative_sum_zero_fold. (((M) = (((((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) * S ((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) + ((dst_positive_scale_zero_fold) + (dst_positive_scale_zero_fold))) + (((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold)))) * S ((((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) * S ((dst_positive_code_zero_fold) + (dst_positive_scale_zero_fold)) + ((dst_positive_scale_zero_fold) + (dst_positive_scale_zero_fold))) + (((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold)))) + ((((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold))) + (((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) * S ((dst_negative_code_zero_fold) + (dst_negative_scale_zero_fold)) + ((dst_negative_scale_zero_fold) + (dst_negative_scale_zero_fold)))))) /\ (((exists fs_u_dst_zero_foldpositive fs_v_dst_zero_foldpositive. ((((exists fs_h_dst_zero_foldpositive_body_start. fs_h_dst_zero_foldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_start. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_start * S ((S (0)) * fs_v_dst_zero_foldpositive) + (0))) /\ ((((exists fs_h_dst_zero_foldpositive_body_terminal. fs_h_dst_zero_foldpositive_body_terminal + S (dst_positive_sum_zero_fold) = S ((S (1)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_terminal. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_terminal * S ((S (1)) * fs_v_dst_zero_foldpositive) + (dst_positive_sum_zero_fold))) /\ forall fs_i_dst_zero_foldpositive_body_steps. (exists fs_lt_dst_zero_foldpositive_body_steps_bound. fs_lt_dst_zero_foldpositive_body_steps_bound + S fs_i_dst_zero_foldpositive_body_steps = 1) -> exists fs_a_dst_zero_foldpositive_body_steps fs_r_dst_zero_foldpositive_body_steps fs_s_dst_zero_foldpositive_body_steps. ((((exists fs_h_dst_zero_foldpositive_body_steps_summand. fs_h_dst_zero_foldpositive_body_steps_summand + S (fs_a_dst_zero_foldpositive_body_steps) = S ((S (fs_i_dst_zero_foldpositive_body_steps)) * dst_positive_scale_zero_fold)) /\ exists fs_q_dst_zero_foldpositive_body_steps_summand. dst_positive_code_zero_fold = fs_q_dst_zero_foldpositive_body_steps_summand * S ((S (fs_i_dst_zero_foldpositive_body_steps)) * dst_positive_scale_zero_fold) + (fs_a_dst_zero_foldpositive_body_steps))) /\ ((((exists fs_h_dst_zero_foldpositive_body_steps_partial. fs_h_dst_zero_foldpositive_body_steps_partial + S (fs_r_dst_zero_foldpositive_body_steps) = S ((S (fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_steps_partial. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_steps_partial * S ((S (fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive) + (fs_r_dst_zero_foldpositive_body_steps))) /\ ((((exists fs_h_dst_zero_foldpositive_body_steps_successor. fs_h_dst_zero_foldpositive_body_steps_successor + S (fs_s_dst_zero_foldpositive_body_steps) = S ((S (S fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive)) /\ exists fs_q_dst_zero_foldpositive_body_steps_successor. fs_u_dst_zero_foldpositive = fs_q_dst_zero_foldpositive_body_steps_successor * S ((S (S fs_i_dst_zero_foldpositive_body_steps)) * fs_v_dst_zero_foldpositive) + (fs_s_dst_zero_foldpositive_body_steps))) /\ fs_s_dst_zero_foldpositive_body_steps = fs_r_dst_zero_foldpositive_body_steps + fs_a_dst_zero_foldpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_foldnegative fs_v_dst_zero_foldnegative. ((((exists fs_h_dst_zero_foldnegative_body_start. fs_h_dst_zero_foldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_start. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_start * S ((S (0)) * fs_v_dst_zero_foldnegative) + (0))) /\ ((((exists fs_h_dst_zero_foldnegative_body_terminal. fs_h_dst_zero_foldnegative_body_terminal + S (dst_negative_sum_zero_fold) = S ((S (1)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_terminal. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_terminal * S ((S (1)) * fs_v_dst_zero_foldnegative) + (dst_negative_sum_zero_fold))) /\ forall fs_i_dst_zero_foldnegative_body_steps. (exists fs_lt_dst_zero_foldnegative_body_steps_bound. fs_lt_dst_zero_foldnegative_body_steps_bound + S fs_i_dst_zero_foldnegative_body_steps = 1) -> exists fs_a_dst_zero_foldnegative_body_steps fs_r_dst_zero_foldnegative_body_steps fs_s_dst_zero_foldnegative_body_steps. ((((exists fs_h_dst_zero_foldnegative_body_steps_summand. fs_h_dst_zero_foldnegative_body_steps_summand + S (fs_a_dst_zero_foldnegative_body_steps) = S ((S (fs_i_dst_zero_foldnegative_body_steps)) * dst_negative_scale_zero_fold)) /\ exists fs_q_dst_zero_foldnegative_body_steps_summand. dst_negative_code_zero_fold = fs_q_dst_zero_foldnegative_body_steps_summand * S ((S (fs_i_dst_zero_foldnegative_body_steps)) * dst_negative_scale_zero_fold) + (fs_a_dst_zero_foldnegative_body_steps))) /\ ((((exists fs_h_dst_zero_foldnegative_body_steps_partial. fs_h_dst_zero_foldnegative_body_steps_partial + S (fs_r_dst_zero_foldnegative_body_steps) = S ((S (fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_steps_partial. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_steps_partial * S ((S (fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative) + (fs_r_dst_zero_foldnegative_body_steps))) /\ ((((exists fs_h_dst_zero_foldnegative_body_steps_successor. fs_h_dst_zero_foldnegative_body_steps_successor + S (fs_s_dst_zero_foldnegative_body_steps) = S ((S (S fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative)) /\ exists fs_q_dst_zero_foldnegative_body_steps_successor. fs_u_dst_zero_foldnegative = fs_q_dst_zero_foldnegative_body_steps_successor * S ((S (S fs_i_dst_zero_foldnegative_body_steps)) * fs_v_dst_zero_foldnegative) + (fs_s_dst_zero_foldnegative_body_steps))) /\ fs_s_dst_zero_foldnegative_body_steps = fs_r_dst_zero_foldnegative_body_steps + fs_a_dst_zero_foldnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_foldresult ge_balance_negative_zero_foldresult. (((((0) = 2 * (ge_balance_positive_zero_foldresult) /\ (ge_balance_negative_zero_foldresult) = 0) \/ exists ge_signed_half_zero_foldresultdecode. (((0) = 2 * ge_signed_half_zero_foldresultdecode + 1 /\ (ge_balance_positive_zero_foldresult) = 0) /\ (ge_balance_negative_zero_foldresult) = S ge_signed_half_zero_foldresultdecode))) /\ ((dst_positive_sum_zero_fold) + ge_balance_negative_zero_foldresult = (dst_negative_sum_zero_fold) + ge_balance_positive_zero_foldresult)))))))))