dirichlet_convolution_sum_zero_excluded

Exact expanded first-order arithmetic statement

forall F G z. (((~((0)=0)) /\ (exists dc_mask_sum_zero. ((((exists dst_positive_code_sum_zeromasktable dst_positive_scale_sum_zeromasktable dst_negative_code_sum_zeromasktable dst_negative_scale_sum_zeromasktable. (((dc_mask_sum_zero) = (((((dst_positive_code_sum_zeromasktable) + (dst_positive_scale_sum_zeromasktable)) * S ((dst_positive_code_sum_zeromasktable) + (dst_positive_scale_sum_zeromasktable)) + ((dst_positive_scale_sum_zeromasktable) + (dst_positive_scale_sum_zeromasktable))) + (((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) * S ((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) + ((dst_negative_scale_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)))) * S ((((dst_positive_code_sum_zeromasktable) + (dst_positive_scale_sum_zeromasktable)) * S ((dst_positive_code_sum_zeromasktable) + (dst_positive_scale_sum_zeromasktable)) + ((dst_positive_scale_sum_zeromasktable) + (dst_positive_scale_sum_zeromasktable))) + (((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) * S ((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) + ((dst_negative_scale_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)))) + ((((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) * S ((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) + ((dst_negative_scale_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable))) + (((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) * S ((dst_negative_code_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)) + ((dst_negative_scale_sum_zeromasktable) + (dst_negative_scale_sum_zeromasktable)))))) /\ (forall dst_index_sum_zeromasktable. (exists pvs_le_gap_sum_zeromasktabledomain. pvs_le_gap_sum_zeromasktabledomain + (dst_index_sum_zeromasktable) = (0)) -> exists dst_positive_sum_zeromasktable dst_negative_sum_zeromasktable dst_value_sum_zeromasktable. ((((exists ff_h_pvs_sum_zeromasktableentrypositive. ff_h_pvs_sum_zeromasktableentrypositive + S (dst_positive_sum_zeromasktable) = S ((S (dst_index_sum_zeromasktable)) * dst_positive_scale_sum_zeromasktable)) /\ exists ff_q_pvs_sum_zeromasktableentrypositive. dst_positive_code_sum_zeromasktable = ff_q_pvs_sum_zeromasktableentrypositive * S ((S (dst_index_sum_zeromasktable)) * dst_positive_scale_sum_zeromasktable) + (dst_positive_sum_zeromasktable))) /\ (((((exists ff_h_pvs_sum_zeromasktableentrynegative. ff_h_pvs_sum_zeromasktableentrynegative + S (dst_negative_sum_zeromasktable) = S ((S (dst_index_sum_zeromasktable)) * dst_negative_scale_sum_zeromasktable)) /\ exists ff_q_pvs_sum_zeromasktableentrynegative. dst_negative_code_sum_zeromasktable = ff_q_pvs_sum_zeromasktableentrynegative * S ((S (dst_index_sum_zeromasktable)) * dst_negative_scale_sum_zeromasktable) + (dst_negative_sum_zeromasktable))) /\ (exists ge_balance_positive_sum_zeromasktableentryvalue ge_balance_negative_sum_zeromasktableentryvalue. (((((dst_value_sum_zeromasktable) = 2 * (ge_balance_positive_sum_zeromasktableentryvalue) /\ (ge_balance_negative_sum_zeromasktableentryvalue) = 0) \/ exists ge_signed_half_sum_zeromasktableentryvaluedecode. (((dst_value_sum_zeromasktable) = 2 * ge_signed_half_sum_zeromasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_zeromasktableentryvalue) = 0) /\ (ge_balance_negative_sum_zeromasktableentryvalue) = S ge_signed_half_sum_zeromasktableentryvaluedecode))) /\ ((dst_positive_sum_zeromasktable) + ge_balance_negative_sum_zeromasktableentryvalue = (dst_negative_sum_zeromasktable) + ge_balance_positive_sum_zeromasktableentryvalue))))))))) /\ (forall dc_index_sum_zeromask dc_value_sum_zeromask. (exists pvs_le_gap_sum_zeromaskdomain. pvs_le_gap_sum_zeromaskdomain + (dc_index_sum_zeromask) = (0)) -> (exists dst_positive_code_sum_zeromasklookup dst_positive_scale_sum_zeromasklookup dst_negative_code_sum_zeromasklookup dst_negative_scale_sum_zeromasklookup dst_positive_sum_zeromasklookup dst_negative_sum_zeromasklookup. (((dc_mask_sum_zero) = (((((dst_positive_code_sum_zeromasklookup) + (dst_positive_scale_sum_zeromasklookup)) * S ((dst_positive_code_sum_zeromasklookup) + (dst_positive_scale_sum_zeromasklookup)) + ((dst_positive_scale_sum_zeromasklookup) + (dst_positive_scale_sum_zeromasklookup))) + (((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) * S ((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) + ((dst_negative_scale_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)))) * S ((((dst_positive_code_sum_zeromasklookup) + (dst_positive_scale_sum_zeromasklookup)) * S ((dst_positive_code_sum_zeromasklookup) + (dst_positive_scale_sum_zeromasklookup)) + ((dst_positive_scale_sum_zeromasklookup) + (dst_positive_scale_sum_zeromasklookup))) + (((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) * S ((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) + ((dst_negative_scale_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)))) + ((((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) * S ((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) + ((dst_negative_scale_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup))) + (((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) * S ((dst_negative_code_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)) + ((dst_negative_scale_sum_zeromasklookup) + (dst_negative_scale_sum_zeromasklookup)))))) /\ (((((exists ff_h_pvs_sum_zeromasklookuppositive. ff_h_pvs_sum_zeromasklookuppositive + S (dst_positive_sum_zeromasklookup) = S ((S (dc_index_sum_zeromask)) * dst_positive_scale_sum_zeromasklookup)) /\ exists ff_q_pvs_sum_zeromasklookuppositive. dst_positive_code_sum_zeromasklookup = ff_q_pvs_sum_zeromasklookuppositive * S ((S (dc_index_sum_zeromask)) * dst_positive_scale_sum_zeromasklookup) + (dst_positive_sum_zeromasklookup))) /\ (((((exists ff_h_pvs_sum_zeromasklookupnegative. ff_h_pvs_sum_zeromasklookupnegative + S (dst_negative_sum_zeromasklookup) = S ((S (dc_index_sum_zeromask)) * dst_negative_scale_sum_zeromasklookup)) /\ exists ff_q_pvs_sum_zeromasklookupnegative. dst_negative_code_sum_zeromasklookup = ff_q_pvs_sum_zeromasklookupnegative * S ((S (dc_index_sum_zeromask)) * dst_negative_scale_sum_zeromasklookup) + (dst_negative_sum_zeromasklookup))) /\ (exists ge_balance_positive_sum_zeromasklookupvalue ge_balance_negative_sum_zeromasklookupvalue. (((((dc_value_sum_zeromask) = 2 * (ge_balance_positive_sum_zeromasklookupvalue) /\ (ge_balance_negative_sum_zeromasklookupvalue) = 0) \/ exists ge_signed_half_sum_zeromasklookupvaluedecode. (((dc_value_sum_zeromask) = 2 * ge_signed_half_sum_zeromasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_zeromasklookupvalue) = 0) /\ (ge_balance_negative_sum_zeromasklookupvalue) = S ge_signed_half_sum_zeromasklookupvaluedecode))) /\ ((dst_positive_sum_zeromasklookup) + ge_balance_negative_sum_zeromasklookupvalue = (dst_negative_sum_zeromasklookup) + ge_balance_positive_sum_zeromasklookupvalue))))))))) -> ((((~((dc_index_sum_zeromask)=0)) /\ (exists dc_quotient_sum_zeromaskentry dc_left_sum_zeromaskentry dc_right_sum_zeromaskentry. (((0)=(dc_index_sum_zeromask)*dc_quotient_sum_zeromaskentry) /\ (((exists dst_positive_code_sum_zeromaskentryleft dst_positive_scale_sum_zeromaskentryleft dst_negative_code_sum_zeromaskentryleft dst_negative_scale_sum_zeromaskentryleft dst_positive_sum_zeromaskentryleft dst_negative_sum_zeromaskentryleft. (((F) = (((((dst_positive_code_sum_zeromaskentryleft) + (dst_positive_scale_sum_zeromaskentryleft)) * S ((dst_positive_code_sum_zeromaskentryleft) + (dst_positive_scale_sum_zeromaskentryleft)) + ((dst_positive_scale_sum_zeromaskentryleft) + (dst_positive_scale_sum_zeromaskentryleft))) + (((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) * S ((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) + ((dst_negative_scale_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)))) * S ((((dst_positive_code_sum_zeromaskentryleft) + (dst_positive_scale_sum_zeromaskentryleft)) * S ((dst_positive_code_sum_zeromaskentryleft) + (dst_positive_scale_sum_zeromaskentryleft)) + ((dst_positive_scale_sum_zeromaskentryleft) + (dst_positive_scale_sum_zeromaskentryleft))) + (((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) * S ((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) + ((dst_negative_scale_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)))) + ((((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) * S ((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) + ((dst_negative_scale_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft))) + (((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) * S ((dst_negative_code_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)) + ((dst_negative_scale_sum_zeromaskentryleft) + (dst_negative_scale_sum_zeromaskentryleft)))))) /\ (((((exists ff_h_pvs_sum_zeromaskentryleftpositive. ff_h_pvs_sum_zeromaskentryleftpositive + S (dst_positive_sum_zeromaskentryleft) = S ((S (dc_index_sum_zeromask)) * dst_positive_scale_sum_zeromaskentryleft)) /\ exists ff_q_pvs_sum_zeromaskentryleftpositive. dst_positive_code_sum_zeromaskentryleft = ff_q_pvs_sum_zeromaskentryleftpositive * S ((S (dc_index_sum_zeromask)) * dst_positive_scale_sum_zeromaskentryleft) + (dst_positive_sum_zeromaskentryleft))) /\ (((((exists ff_h_pvs_sum_zeromaskentryleftnegative. ff_h_pvs_sum_zeromaskentryleftnegative + S (dst_negative_sum_zeromaskentryleft) = S ((S (dc_index_sum_zeromask)) * dst_negative_scale_sum_zeromaskentryleft)) /\ exists ff_q_pvs_sum_zeromaskentryleftnegative. dst_negative_code_sum_zeromaskentryleft = ff_q_pvs_sum_zeromaskentryleftnegative * S ((S (dc_index_sum_zeromask)) * dst_negative_scale_sum_zeromaskentryleft) + (dst_negative_sum_zeromaskentryleft))) /\ (exists ge_balance_positive_sum_zeromaskentryleftvalue ge_balance_negative_sum_zeromaskentryleftvalue. (((((dc_left_sum_zeromaskentry) = 2 * (ge_balance_positive_sum_zeromaskentryleftvalue) /\ (ge_balance_negative_sum_zeromaskentryleftvalue) = 0) \/ exists ge_signed_half_sum_zeromaskentryleftvaluedecode. (((dc_left_sum_zeromaskentry) = 2 * ge_signed_half_sum_zeromaskentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_zeromaskentryleftvalue) = 0) /\ (ge_balance_negative_sum_zeromaskentryleftvalue) = S ge_signed_half_sum_zeromaskentryleftvaluedecode))) /\ ((dst_positive_sum_zeromaskentryleft) + ge_balance_negative_sum_zeromaskentryleftvalue = (dst_negative_sum_zeromaskentryleft) + ge_balance_positive_sum_zeromaskentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_zeromaskentryright dst_positive_scale_sum_zeromaskentryright dst_negative_code_sum_zeromaskentryright dst_negative_scale_sum_zeromaskentryright dst_positive_sum_zeromaskentryright dst_negative_sum_zeromaskentryright. (((G) = (((((dst_positive_code_sum_zeromaskentryright) + (dst_positive_scale_sum_zeromaskentryright)) * S ((dst_positive_code_sum_zeromaskentryright) + (dst_positive_scale_sum_zeromaskentryright)) + ((dst_positive_scale_sum_zeromaskentryright) + (dst_positive_scale_sum_zeromaskentryright))) + (((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) * S ((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) + ((dst_negative_scale_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)))) * S ((((dst_positive_code_sum_zeromaskentryright) + (dst_positive_scale_sum_zeromaskentryright)) * S ((dst_positive_code_sum_zeromaskentryright) + (dst_positive_scale_sum_zeromaskentryright)) + ((dst_positive_scale_sum_zeromaskentryright) + (dst_positive_scale_sum_zeromaskentryright))) + (((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) * S ((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) + ((dst_negative_scale_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)))) + ((((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) * S ((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) + ((dst_negative_scale_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright))) + (((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) * S ((dst_negative_code_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)) + ((dst_negative_scale_sum_zeromaskentryright) + (dst_negative_scale_sum_zeromaskentryright)))))) /\ (((((exists ff_h_pvs_sum_zeromaskentryrightpositive. ff_h_pvs_sum_zeromaskentryrightpositive + S (dst_positive_sum_zeromaskentryright) = S ((S (dc_quotient_sum_zeromaskentry)) * dst_positive_scale_sum_zeromaskentryright)) /\ exists ff_q_pvs_sum_zeromaskentryrightpositive. dst_positive_code_sum_zeromaskentryright = ff_q_pvs_sum_zeromaskentryrightpositive * S ((S (dc_quotient_sum_zeromaskentry)) * dst_positive_scale_sum_zeromaskentryright) + (dst_positive_sum_zeromaskentryright))) /\ (((((exists ff_h_pvs_sum_zeromaskentryrightnegative. ff_h_pvs_sum_zeromaskentryrightnegative + S (dst_negative_sum_zeromaskentryright) = S ((S (dc_quotient_sum_zeromaskentry)) * dst_negative_scale_sum_zeromaskentryright)) /\ exists ff_q_pvs_sum_zeromaskentryrightnegative. dst_negative_code_sum_zeromaskentryright = ff_q_pvs_sum_zeromaskentryrightnegative * S ((S (dc_quotient_sum_zeromaskentry)) * dst_negative_scale_sum_zeromaskentryright) + (dst_negative_sum_zeromaskentryright))) /\ (exists ge_balance_positive_sum_zeromaskentryrightvalue ge_balance_negative_sum_zeromaskentryrightvalue. (((((dc_right_sum_zeromaskentry) = 2 * (ge_balance_positive_sum_zeromaskentryrightvalue) /\ (ge_balance_negative_sum_zeromaskentryrightvalue) = 0) \/ exists ge_signed_half_sum_zeromaskentryrightvaluedecode. (((dc_right_sum_zeromaskentry) = 2 * ge_signed_half_sum_zeromaskentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_zeromaskentryrightvalue) = 0) /\ (ge_balance_negative_sum_zeromaskentryrightvalue) = S ge_signed_half_sum_zeromaskentryrightvaluedecode))) /\ ((dst_positive_sum_zeromaskentryright) + ge_balance_negative_sum_zeromaskentryrightvalue = (dst_negative_sum_zeromaskentryright) + ge_balance_positive_sum_zeromaskentryrightvalue))))))))) /\ (exists sto_ap_sum_zeromaskentryproduct sto_an_sum_zeromaskentryproduct sto_bp_sum_zeromaskentryproduct sto_bn_sum_zeromaskentryproduct sto_cp_sum_zeromaskentryproduct sto_cn_sum_zeromaskentryproduct. (((((dc_left_sum_zeromaskentry) = 2 * (sto_ap_sum_zeromaskentryproduct) /\ (sto_an_sum_zeromaskentryproduct) = 0) \/ exists ge_signed_half_sum_zeromaskentryproductleft. (((dc_left_sum_zeromaskentry) = 2 * ge_signed_half_sum_zeromaskentryproductleft + 1 /\ (sto_ap_sum_zeromaskentryproduct) = 0) /\ (sto_an_sum_zeromaskentryproduct) = S ge_signed_half_sum_zeromaskentryproductleft))) /\ ((((((dc_right_sum_zeromaskentry) = 2 * (sto_bp_sum_zeromaskentryproduct) /\ (sto_bn_sum_zeromaskentryproduct) = 0) \/ exists ge_signed_half_sum_zeromaskentryproductright. (((dc_right_sum_zeromaskentry) = 2 * ge_signed_half_sum_zeromaskentryproductright + 1 /\ (sto_bp_sum_zeromaskentryproduct) = 0) /\ (sto_bn_sum_zeromaskentryproduct) = S ge_signed_half_sum_zeromaskentryproductright))) /\ ((((((dc_value_sum_zeromask) = 2 * (sto_cp_sum_zeromaskentryproduct) /\ (sto_cn_sum_zeromaskentryproduct) = 0) \/ exists ge_signed_half_sum_zeromaskentryproductoutput. (((dc_value_sum_zeromask) = 2 * ge_signed_half_sum_zeromaskentryproductoutput + 1 /\ (sto_cp_sum_zeromaskentryproduct) = 0) /\ (sto_cn_sum_zeromaskentryproduct) = S ge_signed_half_sum_zeromaskentryproductoutput))) /\ ((sto_ap_sum_zeromaskentryproduct * sto_bp_sum_zeromaskentryproduct + sto_an_sum_zeromaskentryproduct * sto_bn_sum_zeromaskentryproduct) + sto_cn_sum_zeromaskentryproduct = (sto_ap_sum_zeromaskentryproduct * sto_bn_sum_zeromaskentryproduct + sto_an_sum_zeromaskentryproduct * sto_bp_sum_zeromaskentryproduct) + sto_cp_sum_zeromaskentryproduct))))))))))))))) \/ ((((dc_index_sum_zeromask)=0 \/ ~(exists pvs_factor_sum_zeromaskentrynondivisor. (0) = (dc_index_sum_zeromask) * pvs_factor_sum_zeromaskentrynondivisor)) /\ ((dc_value_sum_zeromask)=0))))))) /\ (exists dst_positive_code_sum_zerofold dst_positive_scale_sum_zerofold dst_negative_code_sum_zerofold dst_negative_scale_sum_zerofold dst_positive_sum_sum_zerofold dst_negative_sum_sum_zerofold. (((dc_mask_sum_zero) = (((((dst_positive_code_sum_zerofold) + (dst_positive_scale_sum_zerofold)) * S ((dst_positive_code_sum_zerofold) + (dst_positive_scale_sum_zerofold)) + ((dst_positive_scale_sum_zerofold) + (dst_positive_scale_sum_zerofold))) + (((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) * S ((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) + ((dst_negative_scale_sum_zerofold) + (dst_negative_scale_sum_zerofold)))) * S ((((dst_positive_code_sum_zerofold) + (dst_positive_scale_sum_zerofold)) * S ((dst_positive_code_sum_zerofold) + (dst_positive_scale_sum_zerofold)) + ((dst_positive_scale_sum_zerofold) + (dst_positive_scale_sum_zerofold))) + (((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) * S ((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) + ((dst_negative_scale_sum_zerofold) + (dst_negative_scale_sum_zerofold)))) + ((((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) * S ((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) + ((dst_negative_scale_sum_zerofold) + (dst_negative_scale_sum_zerofold))) + (((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) * S ((dst_negative_code_sum_zerofold) + (dst_negative_scale_sum_zerofold)) + ((dst_negative_scale_sum_zerofold) + (dst_negative_scale_sum_zerofold)))))) /\ (((exists fs_u_dst_sum_zerofoldpositive fs_v_dst_sum_zerofoldpositive. ((((exists fs_h_dst_sum_zerofoldpositive_body_start. fs_h_dst_sum_zerofoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_zerofoldpositive)) /\ exists fs_q_dst_sum_zerofoldpositive_body_start. fs_u_dst_sum_zerofoldpositive = fs_q_dst_sum_zerofoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_zerofoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_zerofoldpositive_body_terminal. fs_h_dst_sum_zerofoldpositive_body_terminal + S (dst_positive_sum_sum_zerofold) = S ((S (S (0))) * fs_v_dst_sum_zerofoldpositive)) /\ exists fs_q_dst_sum_zerofoldpositive_body_terminal. fs_u_dst_sum_zerofoldpositive = fs_q_dst_sum_zerofoldpositive_body_terminal * S ((S (S (0))) * fs_v_dst_sum_zerofoldpositive) + (dst_positive_sum_sum_zerofold))) /\ forall fs_i_dst_sum_zerofoldpositive_body_steps. (exists fs_lt_dst_sum_zerofoldpositive_body_steps_bound. fs_lt_dst_sum_zerofoldpositive_body_steps_bound + S fs_i_dst_sum_zerofoldpositive_body_steps = S (0)) -> exists fs_a_dst_sum_zerofoldpositive_body_steps fs_r_dst_sum_zerofoldpositive_body_steps fs_s_dst_sum_zerofoldpositive_body_steps. ((((exists fs_h_dst_sum_zerofoldpositive_body_steps_summand. fs_h_dst_sum_zerofoldpositive_body_steps_summand + S (fs_a_dst_sum_zerofoldpositive_body_steps) = S ((S (fs_i_dst_sum_zerofoldpositive_body_steps)) * dst_positive_scale_sum_zerofold)) /\ exists fs_q_dst_sum_zerofoldpositive_body_steps_summand. dst_positive_code_sum_zerofold = fs_q_dst_sum_zerofoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_zerofoldpositive_body_steps)) * dst_positive_scale_sum_zerofold) + (fs_a_dst_sum_zerofoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_zerofoldpositive_body_steps_partial. fs_h_dst_sum_zerofoldpositive_body_steps_partial + S (fs_r_dst_sum_zerofoldpositive_body_steps) = S ((S (fs_i_dst_sum_zerofoldpositive_body_steps)) * fs_v_dst_sum_zerofoldpositive)) /\ exists fs_q_dst_sum_zerofoldpositive_body_steps_partial. fs_u_dst_sum_zerofoldpositive = fs_q_dst_sum_zerofoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_zerofoldpositive_body_steps)) * fs_v_dst_sum_zerofoldpositive) + (fs_r_dst_sum_zerofoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_zerofoldpositive_body_steps_successor. fs_h_dst_sum_zerofoldpositive_body_steps_successor + S (fs_s_dst_sum_zerofoldpositive_body_steps) = S ((S (S fs_i_dst_sum_zerofoldpositive_body_steps)) * fs_v_dst_sum_zerofoldpositive)) /\ exists fs_q_dst_sum_zerofoldpositive_body_steps_successor. fs_u_dst_sum_zerofoldpositive = fs_q_dst_sum_zerofoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_zerofoldpositive_body_steps)) * fs_v_dst_sum_zerofoldpositive) + (fs_s_dst_sum_zerofoldpositive_body_steps))) /\ fs_s_dst_sum_zerofoldpositive_body_steps = fs_r_dst_sum_zerofoldpositive_body_steps + fs_a_dst_sum_zerofoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_zerofoldnegative fs_v_dst_sum_zerofoldnegative. ((((exists fs_h_dst_sum_zerofoldnegative_body_start. fs_h_dst_sum_zerofoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_zerofoldnegative)) /\ exists fs_q_dst_sum_zerofoldnegative_body_start. fs_u_dst_sum_zerofoldnegative = fs_q_dst_sum_zerofoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_zerofoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_zerofoldnegative_body_terminal. fs_h_dst_sum_zerofoldnegative_body_terminal + S (dst_negative_sum_sum_zerofold) = S ((S (S (0))) * fs_v_dst_sum_zerofoldnegative)) /\ exists fs_q_dst_sum_zerofoldnegative_body_terminal. fs_u_dst_sum_zerofoldnegative = fs_q_dst_sum_zerofoldnegative_body_terminal * S ((S (S (0))) * fs_v_dst_sum_zerofoldnegative) + (dst_negative_sum_sum_zerofold))) /\ forall fs_i_dst_sum_zerofoldnegative_body_steps. (exists fs_lt_dst_sum_zerofoldnegative_body_steps_bound. fs_lt_dst_sum_zerofoldnegative_body_steps_bound + S fs_i_dst_sum_zerofoldnegative_body_steps = S (0)) -> exists fs_a_dst_sum_zerofoldnegative_body_steps fs_r_dst_sum_zerofoldnegative_body_steps fs_s_dst_sum_zerofoldnegative_body_steps. ((((exists fs_h_dst_sum_zerofoldnegative_body_steps_summand. fs_h_dst_sum_zerofoldnegative_body_steps_summand + S (fs_a_dst_sum_zerofoldnegative_body_steps) = S ((S (fs_i_dst_sum_zerofoldnegative_body_steps)) * dst_negative_scale_sum_zerofold)) /\ exists fs_q_dst_sum_zerofoldnegative_body_steps_summand. dst_negative_code_sum_zerofold = fs_q_dst_sum_zerofoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_zerofoldnegative_body_steps)) * dst_negative_scale_sum_zerofold) + (fs_a_dst_sum_zerofoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_zerofoldnegative_body_steps_partial. fs_h_dst_sum_zerofoldnegative_body_steps_partial + S (fs_r_dst_sum_zerofoldnegative_body_steps) = S ((S (fs_i_dst_sum_zerofoldnegative_body_steps)) * fs_v_dst_sum_zerofoldnegative)) /\ exists fs_q_dst_sum_zerofoldnegative_body_steps_partial. fs_u_dst_sum_zerofoldnegative = fs_q_dst_sum_zerofoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_zerofoldnegative_body_steps)) * fs_v_dst_sum_zerofoldnegative) + (fs_r_dst_sum_zerofoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_zerofoldnegative_body_steps_successor. fs_h_dst_sum_zerofoldnegative_body_steps_successor + S (fs_s_dst_sum_zerofoldnegative_body_steps) = S ((S (S fs_i_dst_sum_zerofoldnegative_body_steps)) * fs_v_dst_sum_zerofoldnegative)) /\ exists fs_q_dst_sum_zerofoldnegative_body_steps_successor. fs_u_dst_sum_zerofoldnegative = fs_q_dst_sum_zerofoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_zerofoldnegative_body_steps)) * fs_v_dst_sum_zerofoldnegative) + (fs_s_dst_sum_zerofoldnegative_body_steps))) /\ fs_s_dst_sum_zerofoldnegative_body_steps = fs_r_dst_sum_zerofoldnegative_body_steps + fs_a_dst_sum_zerofoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_zerofoldresult ge_balance_negative_sum_zerofoldresult. (((((z) = 2 * (ge_balance_positive_sum_zerofoldresult) /\ (ge_balance_negative_sum_zerofoldresult) = 0) \/ exists ge_signed_half_sum_zerofoldresultdecode. (((z) = 2 * ge_signed_half_sum_zerofoldresultdecode + 1 /\ (ge_balance_positive_sum_zerofoldresult) = 0) /\ (ge_balance_negative_sum_zerofoldresult) = S ge_signed_half_sum_zerofoldresultdecode))) /\ ((dst_positive_sum_sum_zerofold) + ge_balance_negative_sum_zerofoldresult = (dst_negative_sum_sum_zerofold) + ge_balance_positive_sum_zerofoldresult))))))))))))) -> false