dirichlet_convolution_at_one_iff

Exact expanded first-order arithmetic statement

forall F G a b z. (exists dst_positive_code_one_first dst_positive_scale_one_first dst_negative_code_one_first dst_negative_scale_one_first dst_positive_one_first dst_negative_one_first. (((F) = (((((dst_positive_code_one_first) + (dst_positive_scale_one_first)) * S ((dst_positive_code_one_first) + (dst_positive_scale_one_first)) + ((dst_positive_scale_one_first) + (dst_positive_scale_one_first))) + (((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first)))) * S ((((dst_positive_code_one_first) + (dst_positive_scale_one_first)) * S ((dst_positive_code_one_first) + (dst_positive_scale_one_first)) + ((dst_positive_scale_one_first) + (dst_positive_scale_one_first))) + (((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first)))) + ((((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first))) + (((dst_negative_code_one_first) + (dst_negative_scale_one_first)) * S ((dst_negative_code_one_first) + (dst_negative_scale_one_first)) + ((dst_negative_scale_one_first) + (dst_negative_scale_one_first)))))) /\ (((((exists ff_h_pvs_one_firstpositive. ff_h_pvs_one_firstpositive + S (dst_positive_one_first) = S ((S (1)) * dst_positive_scale_one_first)) /\ exists ff_q_pvs_one_firstpositive. dst_positive_code_one_first = ff_q_pvs_one_firstpositive * S ((S (1)) * dst_positive_scale_one_first) + (dst_positive_one_first))) /\ (((((exists ff_h_pvs_one_firstnegative. ff_h_pvs_one_firstnegative + S (dst_negative_one_first) = S ((S (1)) * dst_negative_scale_one_first)) /\ exists ff_q_pvs_one_firstnegative. dst_negative_code_one_first = ff_q_pvs_one_firstnegative * S ((S (1)) * dst_negative_scale_one_first) + (dst_negative_one_first))) /\ (exists ge_balance_positive_one_firstvalue ge_balance_negative_one_firstvalue. (((((a) = 2 * (ge_balance_positive_one_firstvalue) /\ (ge_balance_negative_one_firstvalue) = 0) \/ exists ge_signed_half_one_firstvaluedecode. (((a) = 2 * ge_signed_half_one_firstvaluedecode + 1 /\ (ge_balance_positive_one_firstvalue) = 0) /\ (ge_balance_negative_one_firstvalue) = S ge_signed_half_one_firstvaluedecode))) /\ ((dst_positive_one_first) + ge_balance_negative_one_firstvalue = (dst_negative_one_first) + ge_balance_positive_one_firstvalue))))))))) -> (exists dst_positive_code_one_second dst_positive_scale_one_second dst_negative_code_one_second dst_negative_scale_one_second dst_positive_one_second dst_negative_one_second. (((G) = (((((dst_positive_code_one_second) + (dst_positive_scale_one_second)) * S ((dst_positive_code_one_second) + (dst_positive_scale_one_second)) + ((dst_positive_scale_one_second) + (dst_positive_scale_one_second))) + (((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second)))) * S ((((dst_positive_code_one_second) + (dst_positive_scale_one_second)) * S ((dst_positive_code_one_second) + (dst_positive_scale_one_second)) + ((dst_positive_scale_one_second) + (dst_positive_scale_one_second))) + (((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second)))) + ((((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second))) + (((dst_negative_code_one_second) + (dst_negative_scale_one_second)) * S ((dst_negative_code_one_second) + (dst_negative_scale_one_second)) + ((dst_negative_scale_one_second) + (dst_negative_scale_one_second)))))) /\ (((((exists ff_h_pvs_one_secondpositive. ff_h_pvs_one_secondpositive + S (dst_positive_one_second) = S ((S (1)) * dst_positive_scale_one_second)) /\ exists ff_q_pvs_one_secondpositive. dst_positive_code_one_second = ff_q_pvs_one_secondpositive * S ((S (1)) * dst_positive_scale_one_second) + (dst_positive_one_second))) /\ (((((exists ff_h_pvs_one_secondnegative. ff_h_pvs_one_secondnegative + S (dst_negative_one_second) = S ((S (1)) * dst_negative_scale_one_second)) /\ exists ff_q_pvs_one_secondnegative. dst_negative_code_one_second = ff_q_pvs_one_secondnegative * S ((S (1)) * dst_negative_scale_one_second) + (dst_negative_one_second))) /\ (exists ge_balance_positive_one_secondvalue ge_balance_negative_one_secondvalue. (((((b) = 2 * (ge_balance_positive_one_secondvalue) /\ (ge_balance_negative_one_secondvalue) = 0) \/ exists ge_signed_half_one_secondvaluedecode. (((b) = 2 * ge_signed_half_one_secondvaluedecode + 1 /\ (ge_balance_positive_one_secondvalue) = 0) /\ (ge_balance_negative_one_secondvalue) = S ge_signed_half_one_secondvaluedecode))) /\ ((dst_positive_one_second) + ge_balance_negative_one_secondvalue = (dst_negative_one_second) + ge_balance_positive_one_secondvalue))))))))) -> (((((~((1)=0)) /\ (exists dc_mask_one_convolution. ((((exists dst_positive_code_one_convolutionmasktable dst_positive_scale_one_convolutionmasktable dst_negative_code_one_convolutionmasktable dst_negative_scale_one_convolutionmasktable. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) * S ((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) + ((((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))))) /\ (forall dst_index_one_convolutionmasktable. (exists pvs_le_gap_one_convolutionmasktabledomain. pvs_le_gap_one_convolutionmasktabledomain + (dst_index_one_convolutionmasktable) = (1)) -> exists dst_positive_one_convolutionmasktable dst_negative_one_convolutionmasktable dst_value_one_convolutionmasktable. ((((exists ff_h_pvs_one_convolutionmasktableentrypositive. ff_h_pvs_one_convolutionmasktableentrypositive + S (dst_positive_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrypositive. dst_positive_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrypositive * S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable) + (dst_positive_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_one_convolutionmasktableentrynegative. ff_h_pvs_one_convolutionmasktableentrynegative + S (dst_negative_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrynegative. dst_negative_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrynegative * S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable) + (dst_negative_one_convolutionmasktable))) /\ (exists ge_balance_positive_one_convolutionmasktableentryvalue ge_balance_negative_one_convolutionmasktableentryvalue. (((((dst_value_one_convolutionmasktable) = 2 * (ge_balance_positive_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_one_convolutionmasktableentryvaluedecode. (((dst_value_one_convolutionmasktable) = 2 * ge_signed_half_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = S ge_signed_half_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_one_convolutionmasktable) + ge_balance_negative_one_convolutionmasktableentryvalue = (dst_negative_one_convolutionmasktable) + ge_balance_positive_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_one_convolutionmask dc_value_one_convolutionmask. (exists pvs_le_gap_one_convolutionmaskdomain. pvs_le_gap_one_convolutionmaskdomain + (dc_index_one_convolutionmask) = (1)) -> (exists dst_positive_code_one_convolutionmasklookup dst_positive_scale_one_convolutionmasklookup dst_negative_code_one_convolutionmasklookup dst_negative_scale_one_convolutionmasklookup dst_positive_one_convolutionmasklookup dst_negative_one_convolutionmasklookup. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) * S ((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) + ((((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_one_convolutionmasklookuppositive. ff_h_pvs_one_convolutionmasklookuppositive + S (dst_positive_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookuppositive. dst_positive_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookuppositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup) + (dst_positive_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_one_convolutionmasklookupnegative. ff_h_pvs_one_convolutionmasklookupnegative + S (dst_negative_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookupnegative. dst_negative_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookupnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup) + (dst_negative_one_convolutionmasklookup))) /\ (exists ge_balance_positive_one_convolutionmasklookupvalue ge_balance_negative_one_convolutionmasklookupvalue. (((((dc_value_one_convolutionmask) = 2 * (ge_balance_positive_one_convolutionmasklookupvalue) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_one_convolutionmasklookupvaluedecode. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = S ge_signed_half_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_one_convolutionmasklookup) + ge_balance_negative_one_convolutionmasklookupvalue = (dst_negative_one_convolutionmasklookup) + ge_balance_positive_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_one_convolutionmask)=0)) /\ (exists dc_quotient_one_convolutionmaskentry dc_left_one_convolutionmaskentry dc_right_one_convolutionmaskentry. (((1)=(dc_index_one_convolutionmask)*dc_quotient_one_convolutionmaskentry) /\ (((exists dst_positive_code_one_convolutionmaskentryleft dst_positive_scale_one_convolutionmaskentryleft dst_negative_code_one_convolutionmaskentryleft dst_negative_scale_one_convolutionmaskentryleft dst_positive_one_convolutionmaskentryleft dst_negative_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) + ((((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftpositive. ff_h_pvs_one_convolutionmaskentryleftpositive + S (dst_positive_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftpositive. dst_positive_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftpositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftnegative. ff_h_pvs_one_convolutionmaskentryleftnegative + S (dst_negative_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftnegative. dst_negative_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_one_convolutionmaskentryleftvalue ge_balance_negative_one_convolutionmaskentryleftvalue. (((((dc_left_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryleftvaluedecode. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = S ge_signed_half_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryleft) + ge_balance_negative_one_convolutionmaskentryleftvalue = (dst_negative_one_convolutionmaskentryleft) + ge_balance_positive_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_one_convolutionmaskentryright dst_positive_scale_one_convolutionmaskentryright dst_negative_code_one_convolutionmaskentryright dst_negative_scale_one_convolutionmaskentryright dst_positive_one_convolutionmaskentryright dst_negative_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) * S ((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) + ((((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightpositive. ff_h_pvs_one_convolutionmaskentryrightpositive + S (dst_positive_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightpositive. dst_positive_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightnegative. ff_h_pvs_one_convolutionmaskentryrightnegative + S (dst_negative_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightnegative. dst_negative_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_one_convolutionmaskentryrightvalue ge_balance_negative_one_convolutionmaskentryrightvalue. (((((dc_right_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryrightvaluedecode. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = S ge_signed_half_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryright) + ge_balance_negative_one_convolutionmaskentryrightvalue = (dst_negative_one_convolutionmaskentryright) + ge_balance_positive_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_one_convolutionmaskentryproduct sto_an_one_convolutionmaskentryproduct sto_bp_one_convolutionmaskentryproduct sto_bn_one_convolutionmaskentryproduct sto_cp_one_convolutionmaskentryproduct sto_cn_one_convolutionmaskentryproduct. (((((dc_left_one_convolutionmaskentry) = 2 * (sto_ap_one_convolutionmaskentryproduct) /\ (sto_an_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductleft. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_one_convolutionmaskentryproduct) = 0) /\ (sto_an_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_one_convolutionmaskentry) = 2 * (sto_bp_one_convolutionmaskentryproduct) /\ (sto_bn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductright. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductright + 1 /\ (sto_bp_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductright))) /\ ((((((dc_value_one_convolutionmask) = 2 * (sto_cp_one_convolutionmaskentryproduct) /\ (sto_cn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductoutput. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct) + sto_cn_one_convolutionmaskentryproduct = (sto_ap_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct) + sto_cp_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_one_convolutionmask)=0 \/ ~(exists pvs_factor_one_convolutionmaskentrynondivisor. (1) = (dc_index_one_convolutionmask) * pvs_factor_one_convolutionmaskentrynondivisor)) /\ ((dc_value_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_one_convolutionfold dst_positive_scale_one_convolutionfold dst_negative_code_one_convolutionfold dst_negative_scale_one_convolutionfold dst_positive_sum_one_convolutionfold dst_negative_sum_one_convolutionfold. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) * S ((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) + ((((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))))) /\ (((exists fs_u_dst_one_convolutionfoldpositive fs_v_dst_one_convolutionfoldpositive. ((((exists fs_h_dst_one_convolutionfoldpositive_body_start. fs_h_dst_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_start. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_terminal. fs_h_dst_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_terminal. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive) + (dst_positive_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldpositive_body_steps fs_r_dst_one_convolutionfoldpositive_body_steps fs_s_dst_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_one_convolutionfold = fs_q_dst_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_r_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_s_dst_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_one_convolutionfoldpositive_body_steps = fs_r_dst_one_convolutionfoldpositive_body_steps + fs_a_dst_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_one_convolutionfoldnegative fs_v_dst_one_convolutionfoldnegative. ((((exists fs_h_dst_one_convolutionfoldnegative_body_start. fs_h_dst_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_start. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_terminal. fs_h_dst_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_terminal. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative) + (dst_negative_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldnegative_body_steps fs_r_dst_one_convolutionfoldnegative_body_steps fs_s_dst_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_one_convolutionfold = fs_q_dst_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_r_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_s_dst_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_one_convolutionfoldnegative_body_steps = fs_r_dst_one_convolutionfoldnegative_body_steps + fs_a_dst_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_one_convolutionfoldresult ge_balance_negative_one_convolutionfoldresult. (((((z) = 2 * (ge_balance_positive_one_convolutionfoldresult) /\ (ge_balance_negative_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_one_convolutionfoldresultdecode. (((z) = 2 * ge_signed_half_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_one_convolutionfoldresult) = S ge_signed_half_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_one_convolutionfold) + ge_balance_negative_one_convolutionfoldresult = (dst_negative_sum_one_convolutionfold) + ge_balance_positive_one_convolutionfoldresult))))))))))))) -> (exists sto_ap_one_product sto_an_one_product sto_bp_one_product sto_bn_one_product sto_cp_one_product sto_cn_one_product. (((((a) = 2 * (sto_ap_one_product) /\ (sto_an_one_product) = 0) \/ exists ge_signed_half_one_productleft. (((a) = 2 * ge_signed_half_one_productleft + 1 /\ (sto_ap_one_product) = 0) /\ (sto_an_one_product) = S ge_signed_half_one_productleft))) /\ ((((((b) = 2 * (sto_bp_one_product) /\ (sto_bn_one_product) = 0) \/ exists ge_signed_half_one_productright. (((b) = 2 * ge_signed_half_one_productright + 1 /\ (sto_bp_one_product) = 0) /\ (sto_bn_one_product) = S ge_signed_half_one_productright))) /\ ((((((z) = 2 * (sto_cp_one_product) /\ (sto_cn_one_product) = 0) \/ exists ge_signed_half_one_productoutput. (((z) = 2 * ge_signed_half_one_productoutput + 1 /\ (sto_cp_one_product) = 0) /\ (sto_cn_one_product) = S ge_signed_half_one_productoutput))) /\ ((sto_ap_one_product * sto_bp_one_product + sto_an_one_product * sto_bn_one_product) + sto_cn_one_product = (sto_ap_one_product * sto_bn_one_product + sto_an_one_product * sto_bp_one_product) + sto_cp_one_product)))))))) /\ ((exists sto_ap_one_product sto_an_one_product sto_bp_one_product sto_bn_one_product sto_cp_one_product sto_cn_one_product. (((((a) = 2 * (sto_ap_one_product) /\ (sto_an_one_product) = 0) \/ exists ge_signed_half_one_productleft. (((a) = 2 * ge_signed_half_one_productleft + 1 /\ (sto_ap_one_product) = 0) /\ (sto_an_one_product) = S ge_signed_half_one_productleft))) /\ ((((((b) = 2 * (sto_bp_one_product) /\ (sto_bn_one_product) = 0) \/ exists ge_signed_half_one_productright. (((b) = 2 * ge_signed_half_one_productright + 1 /\ (sto_bp_one_product) = 0) /\ (sto_bn_one_product) = S ge_signed_half_one_productright))) /\ ((((((z) = 2 * (sto_cp_one_product) /\ (sto_cn_one_product) = 0) \/ exists ge_signed_half_one_productoutput. (((z) = 2 * ge_signed_half_one_productoutput + 1 /\ (sto_cp_one_product) = 0) /\ (sto_cn_one_product) = S ge_signed_half_one_productoutput))) /\ ((sto_ap_one_product * sto_bp_one_product + sto_an_one_product * sto_bn_one_product) + sto_cn_one_product = (sto_ap_one_product * sto_bn_one_product + sto_an_one_product * sto_bp_one_product) + sto_cp_one_product))))))) -> (((~((1)=0)) /\ (exists dc_mask_one_convolution. ((((exists dst_positive_code_one_convolutionmasktable dst_positive_scale_one_convolutionmasktable dst_negative_code_one_convolutionmasktable dst_negative_scale_one_convolutionmasktable. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) * S ((((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) * S ((dst_positive_code_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable)) + ((dst_positive_scale_one_convolutionmasktable) + (dst_positive_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))) + ((((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable))) + (((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) * S ((dst_negative_code_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)) + ((dst_negative_scale_one_convolutionmasktable) + (dst_negative_scale_one_convolutionmasktable)))))) /\ (forall dst_index_one_convolutionmasktable. (exists pvs_le_gap_one_convolutionmasktabledomain. pvs_le_gap_one_convolutionmasktabledomain + (dst_index_one_convolutionmasktable) = (1)) -> exists dst_positive_one_convolutionmasktable dst_negative_one_convolutionmasktable dst_value_one_convolutionmasktable. ((((exists ff_h_pvs_one_convolutionmasktableentrypositive. ff_h_pvs_one_convolutionmasktableentrypositive + S (dst_positive_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrypositive. dst_positive_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrypositive * S ((S (dst_index_one_convolutionmasktable)) * dst_positive_scale_one_convolutionmasktable) + (dst_positive_one_convolutionmasktable))) /\ (((((exists ff_h_pvs_one_convolutionmasktableentrynegative. ff_h_pvs_one_convolutionmasktableentrynegative + S (dst_negative_one_convolutionmasktable) = S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable)) /\ exists ff_q_pvs_one_convolutionmasktableentrynegative. dst_negative_code_one_convolutionmasktable = ff_q_pvs_one_convolutionmasktableentrynegative * S ((S (dst_index_one_convolutionmasktable)) * dst_negative_scale_one_convolutionmasktable) + (dst_negative_one_convolutionmasktable))) /\ (exists ge_balance_positive_one_convolutionmasktableentryvalue ge_balance_negative_one_convolutionmasktableentryvalue. (((((dst_value_one_convolutionmasktable) = 2 * (ge_balance_positive_one_convolutionmasktableentryvalue) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_one_convolutionmasktableentryvaluedecode. (((dst_value_one_convolutionmasktable) = 2 * ge_signed_half_one_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_one_convolutionmasktableentryvalue) = S ge_signed_half_one_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_one_convolutionmasktable) + ge_balance_negative_one_convolutionmasktableentryvalue = (dst_negative_one_convolutionmasktable) + ge_balance_positive_one_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_one_convolutionmask dc_value_one_convolutionmask. (exists pvs_le_gap_one_convolutionmaskdomain. pvs_le_gap_one_convolutionmaskdomain + (dc_index_one_convolutionmask) = (1)) -> (exists dst_positive_code_one_convolutionmasklookup dst_positive_scale_one_convolutionmasklookup dst_negative_code_one_convolutionmasklookup dst_negative_scale_one_convolutionmasklookup dst_positive_one_convolutionmasklookup dst_negative_one_convolutionmasklookup. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) * S ((((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) * S ((dst_positive_code_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup)) + ((dst_positive_scale_one_convolutionmasklookup) + (dst_positive_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))) + ((((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup))) + (((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) * S ((dst_negative_code_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)) + ((dst_negative_scale_one_convolutionmasklookup) + (dst_negative_scale_one_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_one_convolutionmasklookuppositive. ff_h_pvs_one_convolutionmasklookuppositive + S (dst_positive_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookuppositive. dst_positive_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookuppositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmasklookup) + (dst_positive_one_convolutionmasklookup))) /\ (((((exists ff_h_pvs_one_convolutionmasklookupnegative. ff_h_pvs_one_convolutionmasklookupnegative + S (dst_negative_one_convolutionmasklookup) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup)) /\ exists ff_q_pvs_one_convolutionmasklookupnegative. dst_negative_code_one_convolutionmasklookup = ff_q_pvs_one_convolutionmasklookupnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmasklookup) + (dst_negative_one_convolutionmasklookup))) /\ (exists ge_balance_positive_one_convolutionmasklookupvalue ge_balance_negative_one_convolutionmasklookupvalue. (((((dc_value_one_convolutionmask) = 2 * (ge_balance_positive_one_convolutionmasklookupvalue) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_one_convolutionmasklookupvaluedecode. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_one_convolutionmasklookupvalue) = S ge_signed_half_one_convolutionmasklookupvaluedecode))) /\ ((dst_positive_one_convolutionmasklookup) + ge_balance_negative_one_convolutionmasklookupvalue = (dst_negative_one_convolutionmasklookup) + ge_balance_positive_one_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_one_convolutionmask)=0)) /\ (exists dc_quotient_one_convolutionmaskentry dc_left_one_convolutionmaskentry dc_right_one_convolutionmaskentry. (((1)=(dc_index_one_convolutionmask)*dc_quotient_one_convolutionmaskentry) /\ (((exists dst_positive_code_one_convolutionmaskentryleft dst_positive_scale_one_convolutionmaskentryleft dst_negative_code_one_convolutionmaskentryleft dst_negative_scale_one_convolutionmaskentryleft dst_positive_one_convolutionmaskentryleft dst_negative_one_convolutionmaskentryleft. (((F) = (((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) * S ((((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) * S ((dst_positive_code_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft)) + ((dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))) + ((((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft))) + (((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) * S ((dst_negative_code_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)) + ((dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_scale_one_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftpositive. ff_h_pvs_one_convolutionmaskentryleftpositive + S (dst_positive_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftpositive. dst_positive_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftpositive * S ((S (dc_index_one_convolutionmask)) * dst_positive_scale_one_convolutionmaskentryleft) + (dst_positive_one_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryleftnegative. ff_h_pvs_one_convolutionmaskentryleftnegative + S (dst_negative_one_convolutionmaskentryleft) = S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft)) /\ exists ff_q_pvs_one_convolutionmaskentryleftnegative. dst_negative_code_one_convolutionmaskentryleft = ff_q_pvs_one_convolutionmaskentryleftnegative * S ((S (dc_index_one_convolutionmask)) * dst_negative_scale_one_convolutionmaskentryleft) + (dst_negative_one_convolutionmaskentryleft))) /\ (exists ge_balance_positive_one_convolutionmaskentryleftvalue ge_balance_negative_one_convolutionmaskentryleftvalue. (((((dc_left_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryleftvalue) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryleftvaluedecode. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryleftvalue) = S ge_signed_half_one_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryleft) + ge_balance_negative_one_convolutionmaskentryleftvalue = (dst_negative_one_convolutionmaskentryleft) + ge_balance_positive_one_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_one_convolutionmaskentryright dst_positive_scale_one_convolutionmaskentryright dst_negative_code_one_convolutionmaskentryright dst_negative_scale_one_convolutionmaskentryright dst_positive_one_convolutionmaskentryright dst_negative_one_convolutionmaskentryright. (((G) = (((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) * S ((((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) * S ((dst_positive_code_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright)) + ((dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))) + ((((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright))) + (((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) * S ((dst_negative_code_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)) + ((dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_scale_one_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightpositive. ff_h_pvs_one_convolutionmaskentryrightpositive + S (dst_positive_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightpositive. dst_positive_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightpositive * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_positive_scale_one_convolutionmaskentryright) + (dst_positive_one_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_one_convolutionmaskentryrightnegative. ff_h_pvs_one_convolutionmaskentryrightnegative + S (dst_negative_one_convolutionmaskentryright) = S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright)) /\ exists ff_q_pvs_one_convolutionmaskentryrightnegative. dst_negative_code_one_convolutionmaskentryright = ff_q_pvs_one_convolutionmaskentryrightnegative * S ((S (dc_quotient_one_convolutionmaskentry)) * dst_negative_scale_one_convolutionmaskentryright) + (dst_negative_one_convolutionmaskentryright))) /\ (exists ge_balance_positive_one_convolutionmaskentryrightvalue ge_balance_negative_one_convolutionmaskentryrightvalue. (((((dc_right_one_convolutionmaskentry) = 2 * (ge_balance_positive_one_convolutionmaskentryrightvalue) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_one_convolutionmaskentryrightvaluedecode. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_one_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_one_convolutionmaskentryrightvalue) = S ge_signed_half_one_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_one_convolutionmaskentryright) + ge_balance_negative_one_convolutionmaskentryrightvalue = (dst_negative_one_convolutionmaskentryright) + ge_balance_positive_one_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_one_convolutionmaskentryproduct sto_an_one_convolutionmaskentryproduct sto_bp_one_convolutionmaskentryproduct sto_bn_one_convolutionmaskentryproduct sto_cp_one_convolutionmaskentryproduct sto_cn_one_convolutionmaskentryproduct. (((((dc_left_one_convolutionmaskentry) = 2 * (sto_ap_one_convolutionmaskentryproduct) /\ (sto_an_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductleft. (((dc_left_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductleft + 1 /\ (sto_ap_one_convolutionmaskentryproduct) = 0) /\ (sto_an_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductleft))) /\ ((((((dc_right_one_convolutionmaskentry) = 2 * (sto_bp_one_convolutionmaskentryproduct) /\ (sto_bn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductright. (((dc_right_one_convolutionmaskentry) = 2 * ge_signed_half_one_convolutionmaskentryproductright + 1 /\ (sto_bp_one_convolutionmaskentryproduct) = 0) /\ (sto_bn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductright))) /\ ((((((dc_value_one_convolutionmask) = 2 * (sto_cp_one_convolutionmaskentryproduct) /\ (sto_cn_one_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_one_convolutionmaskentryproductoutput. (((dc_value_one_convolutionmask) = 2 * ge_signed_half_one_convolutionmaskentryproductoutput + 1 /\ (sto_cp_one_convolutionmaskentryproduct) = 0) /\ (sto_cn_one_convolutionmaskentryproduct) = S ge_signed_half_one_convolutionmaskentryproductoutput))) /\ ((sto_ap_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct) + sto_cn_one_convolutionmaskentryproduct = (sto_ap_one_convolutionmaskentryproduct * sto_bn_one_convolutionmaskentryproduct + sto_an_one_convolutionmaskentryproduct * sto_bp_one_convolutionmaskentryproduct) + sto_cp_one_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_one_convolutionmask)=0 \/ ~(exists pvs_factor_one_convolutionmaskentrynondivisor. (1) = (dc_index_one_convolutionmask) * pvs_factor_one_convolutionmaskentrynondivisor)) /\ ((dc_value_one_convolutionmask)=0))))))) /\ (exists dst_positive_code_one_convolutionfold dst_positive_scale_one_convolutionfold dst_negative_code_one_convolutionfold dst_negative_scale_one_convolutionfold dst_positive_sum_one_convolutionfold dst_negative_sum_one_convolutionfold. (((dc_mask_one_convolution) = (((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) * S ((((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) * S ((dst_positive_code_one_convolutionfold) + (dst_positive_scale_one_convolutionfold)) + ((dst_positive_scale_one_convolutionfold) + (dst_positive_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))) + ((((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold))) + (((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) * S ((dst_negative_code_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)) + ((dst_negative_scale_one_convolutionfold) + (dst_negative_scale_one_convolutionfold)))))) /\ (((exists fs_u_dst_one_convolutionfoldpositive fs_v_dst_one_convolutionfoldpositive. ((((exists fs_h_dst_one_convolutionfoldpositive_body_start. fs_h_dst_one_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_start. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_terminal. fs_h_dst_one_convolutionfoldpositive_body_terminal + S (dst_positive_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_terminal. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldpositive) + (dst_positive_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldpositive_body_steps. (exists fs_lt_dst_one_convolutionfoldpositive_body_steps_bound. fs_lt_dst_one_convolutionfoldpositive_body_steps_bound + S fs_i_dst_one_convolutionfoldpositive_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldpositive_body_steps fs_r_dst_one_convolutionfoldpositive_body_steps fs_s_dst_one_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_summand. fs_h_dst_one_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_summand. dst_positive_code_one_convolutionfold = fs_q_dst_one_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * dst_positive_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_partial. fs_h_dst_one_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_one_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_partial. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_r_dst_one_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldpositive_body_steps_successor. fs_h_dst_one_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_one_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive)) /\ exists fs_q_dst_one_convolutionfoldpositive_body_steps_successor. fs_u_dst_one_convolutionfoldpositive = fs_q_dst_one_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldpositive_body_steps)) * fs_v_dst_one_convolutionfoldpositive) + (fs_s_dst_one_convolutionfoldpositive_body_steps))) /\ fs_s_dst_one_convolutionfoldpositive_body_steps = fs_r_dst_one_convolutionfoldpositive_body_steps + fs_a_dst_one_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_one_convolutionfoldnegative fs_v_dst_one_convolutionfoldnegative. ((((exists fs_h_dst_one_convolutionfoldnegative_body_start. fs_h_dst_one_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_start. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_one_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_terminal. fs_h_dst_one_convolutionfoldnegative_body_terminal + S (dst_negative_sum_one_convolutionfold) = S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_terminal. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_one_convolutionfoldnegative) + (dst_negative_sum_one_convolutionfold))) /\ forall fs_i_dst_one_convolutionfoldnegative_body_steps. (exists fs_lt_dst_one_convolutionfoldnegative_body_steps_bound. fs_lt_dst_one_convolutionfoldnegative_body_steps_bound + S fs_i_dst_one_convolutionfoldnegative_body_steps = S (1)) -> exists fs_a_dst_one_convolutionfoldnegative_body_steps fs_r_dst_one_convolutionfoldnegative_body_steps fs_s_dst_one_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_summand. fs_h_dst_one_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_summand. dst_negative_code_one_convolutionfold = fs_q_dst_one_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * dst_negative_scale_one_convolutionfold) + (fs_a_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_partial. fs_h_dst_one_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_one_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_partial. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_r_dst_one_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_one_convolutionfoldnegative_body_steps_successor. fs_h_dst_one_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_one_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative)) /\ exists fs_q_dst_one_convolutionfoldnegative_body_steps_successor. fs_u_dst_one_convolutionfoldnegative = fs_q_dst_one_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_one_convolutionfoldnegative_body_steps)) * fs_v_dst_one_convolutionfoldnegative) + (fs_s_dst_one_convolutionfoldnegative_body_steps))) /\ fs_s_dst_one_convolutionfoldnegative_body_steps = fs_r_dst_one_convolutionfoldnegative_body_steps + fs_a_dst_one_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_one_convolutionfoldresult ge_balance_negative_one_convolutionfoldresult. (((((z) = 2 * (ge_balance_positive_one_convolutionfoldresult) /\ (ge_balance_negative_one_convolutionfoldresult) = 0) \/ exists ge_signed_half_one_convolutionfoldresultdecode. (((z) = 2 * ge_signed_half_one_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_one_convolutionfoldresult) = 0) /\ (ge_balance_negative_one_convolutionfoldresult) = S ge_signed_half_one_convolutionfoldresultdecode))) /\ ((dst_positive_sum_one_convolutionfold) + ge_balance_negative_one_convolutionfoldresult = (dst_negative_sum_one_convolutionfold) + ge_balance_positive_one_convolutionfoldresult)))))))))))))))