dirichlet_constant_one_sum_iff

forall N F U n z. (exists dst_positive_code_ones_sum_input dst_positive_scale_ones_sum_input dst_negative_code_ones_sum_input dst_negative_scale_ones_sum_input. (((F) = (((((dst_positive_code_ones_sum_input) + (dst_positive_scale_ones_sum_input)) * S ((dst_positive_code_ones_sum_input) + (dst_positive_scale_ones_sum_input)) + ((dst_positive_scale_ones_sum_input) + (dst_positive_scale_ones_sum_input))) + (((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) * S ((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) + ((dst_negative_scale_ones_sum_input) + (dst_negative_scale_ones_sum_input)))) * S ((((dst_positive_code_ones_sum_input) + (dst_positive_scale_ones_sum_input)) * S ((dst_positive_code_ones_sum_input) + (dst_positive_scale_ones_sum_input)) + ((dst_positive_scale_ones_sum_input) + (dst_positive_scale_ones_sum_input))) + (((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) * S ((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) + ((dst_negative_scale_ones_sum_input) + (dst_negative_scale_ones_sum_input)))) + ((((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) * S ((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) + ((dst_negative_scale_ones_sum_input) + (dst_negative_scale_ones_sum_input))) + (((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) * S ((dst_negative_code_ones_sum_input) + (dst_negative_scale_ones_sum_input)) + ((dst_negative_scale_ones_sum_input) + (dst_negative_scale_ones_sum_input)))))) /\ (forall dst_index_ones_sum_input. (exists pvs_le_gap_ones_sum_inputdomain. pvs_le_gap_ones_sum_inputdomain + (dst_index_ones_sum_input) = (N)) -> exists dst_positive_ones_sum_input dst_negative_ones_sum_input dst_value_ones_sum_input. ((((exists ff_h_pvs_ones_sum_inputentrypositive. ff_h_pvs_ones_sum_inputentrypositive + S (dst_positive_ones_sum_input) = S ((S (dst_index_ones_sum_input)) * dst_positive_scale_ones_sum_input)) /\ exists ff_q_pvs_ones_sum_inputentrypositive. dst_positive_code_ones_sum_input = ff_q_pvs_ones_sum_inputentrypositive * S ((S (dst_index_ones_sum_input)) * dst_positive_scale_ones_sum_input) + (dst_positive_ones_sum_input))) /\ (((((exists ff_h_pvs_ones_sum_inputentrynegative. ff_h_pvs_ones_sum_inputentrynegative + S (dst_negative_ones_sum_input) = S ((S (dst_index_ones_sum_input)) * dst_negative_scale_ones_sum_input)) /\ exists ff_q_pvs_ones_sum_inputentrynegative. dst_negative_code_ones_sum_input = ff_q_pvs_ones_sum_inputentrynegative * S ((S (dst_index_ones_sum_input)) * dst_negative_scale_ones_sum_input) + (dst_negative_ones_sum_input))) /\ (exists ge_balance_positive_ones_sum_inputentryvalue ge_balance_negative_ones_sum_inputentryvalue. (((((dst_value_ones_sum_input) = 2 * (ge_balance_positive_ones_sum_inputentryvalue) /\ (ge_balance_negative_ones_sum_inputentryvalue) = 0) \/ exists ge_signed_half_ones_sum_inputentryvaluedecode. (((dst_value_ones_sum_input) = 2 * ge_signed_half_ones_sum_inputentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_inputentryvalue) = 0) /\ (ge_balance_negative_ones_sum_inputentryvalue) = S ge_signed_half_ones_sum_inputentryvaluedecode))) /\ ((dst_positive_ones_sum_input) + ge_balance_negative_ones_sum_inputentryvalue = (dst_negative_ones_sum_input) + ge_balance_positive_ones_sum_inputentryvalue))))))))) -> (((exists dst_positive_code_ones_sum_onestable dst_positive_scale_ones_sum_onestable dst_negative_code_ones_sum_onestable dst_negative_scale_ones_sum_onestable. (((U) = (((((dst_positive_code_ones_sum_onestable) + (dst_positive_scale_ones_sum_onestable)) * S ((dst_positive_code_ones_sum_onestable) + (dst_positive_scale_ones_sum_onestable)) + ((dst_positive_scale_ones_sum_onestable) + (dst_positive_scale_ones_sum_onestable))) + (((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) * S ((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) + ((dst_negative_scale_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)))) * S ((((dst_positive_code_ones_sum_onestable) + (dst_positive_scale_ones_sum_onestable)) * S ((dst_positive_code_ones_sum_onestable) + (dst_positive_scale_ones_sum_onestable)) + ((dst_positive_scale_ones_sum_onestable) + (dst_positive_scale_ones_sum_onestable))) + (((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) * S ((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) + ((dst_negative_scale_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)))) + ((((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) * S ((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) + ((dst_negative_scale_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable))) + (((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) * S ((dst_negative_code_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)) + ((dst_negative_scale_ones_sum_onestable) + (dst_negative_scale_ones_sum_onestable)))))) /\ (forall dst_index_ones_sum_onestable. (exists pvs_le_gap_ones_sum_onestabledomain. pvs_le_gap_ones_sum_onestabledomain + (dst_index_ones_sum_onestable) = (N)) -> exists dst_positive_ones_sum_onestable dst_negative_ones_sum_onestable dst_value_ones_sum_onestable. ((((exists ff_h_pvs_ones_sum_onestableentrypositive. ff_h_pvs_ones_sum_onestableentrypositive + S (dst_positive_ones_sum_onestable) = S ((S (dst_index_ones_sum_onestable)) * dst_positive_scale_ones_sum_onestable)) /\ exists ff_q_pvs_ones_sum_onestableentrypositive. dst_positive_code_ones_sum_onestable = ff_q_pvs_ones_sum_onestableentrypositive * S ((S (dst_index_ones_sum_onestable)) * dst_positive_scale_ones_sum_onestable) + (dst_positive_ones_sum_onestable))) /\ (((((exists ff_h_pvs_ones_sum_onestableentrynegative. ff_h_pvs_ones_sum_onestableentrynegative + S (dst_negative_ones_sum_onestable) = S ((S (dst_index_ones_sum_onestable)) * dst_negative_scale_ones_sum_onestable)) /\ exists ff_q_pvs_ones_sum_onestableentrynegative. dst_negative_code_ones_sum_onestable = ff_q_pvs_ones_sum_onestableentrynegative * S ((S (dst_index_ones_sum_onestable)) * dst_negative_scale_ones_sum_onestable) + (dst_negative_ones_sum_onestable))) /\ (exists ge_balance_positive_ones_sum_onestableentryvalue ge_balance_negative_ones_sum_onestableentryvalue. (((((dst_value_ones_sum_onestable) = 2 * (ge_balance_positive_ones_sum_onestableentryvalue) /\ (ge_balance_negative_ones_sum_onestableentryvalue) = 0) \/ exists ge_signed_half_ones_sum_onestableentryvaluedecode. (((dst_value_ones_sum_onestable) = 2 * ge_signed_half_ones_sum_onestableentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_onestableentryvalue) = 0) /\ (ge_balance_negative_ones_sum_onestableentryvalue) = S ge_signed_half_ones_sum_onestableentryvaluedecode))) /\ ((dst_positive_ones_sum_onestable) + ge_balance_negative_ones_sum_onestableentryvalue = (dst_negative_ones_sum_onestable) + ge_balance_positive_ones_sum_onestableentryvalue))))))))) /\ (forall du_index_ones_sum_ones du_value_ones_sum_ones. ~(du_index_ones_sum_ones=0) -> (exists pvs_le_gap_ones_sum_onesbound. pvs_le_gap_ones_sum_onesbound + (du_index_ones_sum_ones) = (N)) -> (exists dst_positive_code_ones_sum_onesentry dst_positive_scale_ones_sum_onesentry dst_negative_code_ones_sum_onesentry dst_negative_scale_ones_sum_onesentry dst_positive_ones_sum_onesentry dst_negative_ones_sum_onesentry. (((U) = (((((dst_positive_code_ones_sum_onesentry) + (dst_positive_scale_ones_sum_onesentry)) * S ((dst_positive_code_ones_sum_onesentry) + (dst_positive_scale_ones_sum_onesentry)) + ((dst_positive_scale_ones_sum_onesentry) + (dst_positive_scale_ones_sum_onesentry))) + (((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) * S ((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) + ((dst_negative_scale_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)))) * S ((((dst_positive_code_ones_sum_onesentry) + (dst_positive_scale_ones_sum_onesentry)) * S ((dst_positive_code_ones_sum_onesentry) + (dst_positive_scale_ones_sum_onesentry)) + ((dst_positive_scale_ones_sum_onesentry) + (dst_positive_scale_ones_sum_onesentry))) + (((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) * S ((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) + ((dst_negative_scale_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)))) + ((((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) * S ((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) + ((dst_negative_scale_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry))) + (((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) * S ((dst_negative_code_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)) + ((dst_negative_scale_ones_sum_onesentry) + (dst_negative_scale_ones_sum_onesentry)))))) /\ (((((exists ff_h_pvs_ones_sum_onesentrypositive. ff_h_pvs_ones_sum_onesentrypositive + S (dst_positive_ones_sum_onesentry) = S ((S (du_index_ones_sum_ones)) * dst_positive_scale_ones_sum_onesentry)) /\ exists ff_q_pvs_ones_sum_onesentrypositive. dst_positive_code_ones_sum_onesentry = ff_q_pvs_ones_sum_onesentrypositive * S ((S (du_index_ones_sum_ones)) * dst_positive_scale_ones_sum_onesentry) + (dst_positive_ones_sum_onesentry))) /\ (((((exists ff_h_pvs_ones_sum_onesentrynegative. ff_h_pvs_ones_sum_onesentrynegative + S (dst_negative_ones_sum_onesentry) = S ((S (du_index_ones_sum_ones)) * dst_negative_scale_ones_sum_onesentry)) /\ exists ff_q_pvs_ones_sum_onesentrynegative. dst_negative_code_ones_sum_onesentry = ff_q_pvs_ones_sum_onesentrynegative * S ((S (du_index_ones_sum_ones)) * dst_negative_scale_ones_sum_onesentry) + (dst_negative_ones_sum_onesentry))) /\ (exists ge_balance_positive_ones_sum_onesentryvalue ge_balance_negative_ones_sum_onesentryvalue. (((((du_value_ones_sum_ones) = 2 * (ge_balance_positive_ones_sum_onesentryvalue) /\ (ge_balance_negative_ones_sum_onesentryvalue) = 0) \/ exists ge_signed_half_ones_sum_onesentryvaluedecode. (((du_value_ones_sum_ones) = 2 * ge_signed_half_ones_sum_onesentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_onesentryvalue) = 0) /\ (ge_balance_negative_ones_sum_onesentryvalue) = S ge_signed_half_ones_sum_onesentryvaluedecode))) /\ ((dst_positive_ones_sum_onesentry) + ge_balance_negative_ones_sum_onesentryvalue = (dst_negative_ones_sum_onesentry) + ge_balance_positive_ones_sum_onesentryvalue))))))))) -> du_value_ones_sum_ones=2))) -> ~(n=0) -> (exists pvs_le_gap_ones_sum_bound. pvs_le_gap_ones_sum_bound + (n) = (N)) -> ((((((~((n)=0)) /\ (exists dc_mask_ones_sum_resultconvolution. ((((exists dst_positive_code_ones_sum_resultconvolutionmasktable dst_positive_scale_ones_sum_resultconvolutionmasktable dst_negative_code_ones_sum_resultconvolutionmasktable dst_negative_scale_ones_sum_resultconvolutionmasktable. (((dc_mask_ones_sum_resultconvolution) = (((((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) + ((dst_positive_scale_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable))) + (((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) + ((dst_positive_scale_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable))) + (((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)))) + ((((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable))) + (((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)))))) /\ (forall dst_index_ones_sum_resultconvolutionmasktable. (exists pvs_le_gap_ones_sum_resultconvolutionmasktabledomain. pvs_le_gap_ones_sum_resultconvolutionmasktabledomain + (dst_index_ones_sum_resultconvolutionmasktable) = (n)) -> exists dst_positive_ones_sum_resultconvolutionmasktable dst_negative_ones_sum_resultconvolutionmasktable dst_value_ones_sum_resultconvolutionmasktable. ((((exists ff_h_pvs_ones_sum_resultconvolutionmasktableentrypositive. ff_h_pvs_ones_sum_resultconvolutionmasktableentrypositive + S (dst_positive_ones_sum_resultconvolutionmasktable) = S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_positive_scale_ones_sum_resultconvolutionmasktable)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasktableentrypositive. dst_positive_code_ones_sum_resultconvolutionmasktable = ff_q_pvs_ones_sum_resultconvolutionmasktableentrypositive * S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_positive_scale_ones_sum_resultconvolutionmasktable) + (dst_positive_ones_sum_resultconvolutionmasktable))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmasktableentrynegative. ff_h_pvs_ones_sum_resultconvolutionmasktableentrynegative + S (dst_negative_ones_sum_resultconvolutionmasktable) = S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_negative_scale_ones_sum_resultconvolutionmasktable)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasktableentrynegative. dst_negative_code_ones_sum_resultconvolutionmasktable = ff_q_pvs_ones_sum_resultconvolutionmasktableentrynegative * S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_ones_sum_resultconvolutionmasktable))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue. (((((dst_value_ones_sum_resultconvolutionmasktable) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmasktableentryvaluedecode. (((dst_value_ones_sum_resultconvolutionmasktable) = 2 * ge_signed_half_ones_sum_resultconvolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue) = S ge_signed_half_ones_sum_resultconvolutionmasktableentryvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmasktable) + ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue = (dst_negative_ones_sum_resultconvolutionmasktable) + ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue))))))))) /\ (forall dc_index_ones_sum_resultconvolutionmask dc_value_ones_sum_resultconvolutionmask. (exists pvs_le_gap_ones_sum_resultconvolutionmaskdomain. pvs_le_gap_ones_sum_resultconvolutionmaskdomain + (dc_index_ones_sum_resultconvolutionmask) = (n)) -> (exists dst_positive_code_ones_sum_resultconvolutionmasklookup dst_positive_scale_ones_sum_resultconvolutionmasklookup dst_negative_code_ones_sum_resultconvolutionmasklookup dst_negative_scale_ones_sum_resultconvolutionmasklookup dst_positive_ones_sum_resultconvolutionmasklookup dst_negative_ones_sum_resultconvolutionmasklookup. (((dc_mask_ones_sum_resultconvolution) = (((((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_positive_scale_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup))) + (((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_positive_scale_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup))) + (((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)))) + ((((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup))) + (((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)))))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmasklookuppositive. ff_h_pvs_ones_sum_resultconvolutionmasklookuppositive + S (dst_positive_ones_sum_resultconvolutionmasklookup) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmasklookup)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasklookuppositive. dst_positive_code_ones_sum_resultconvolutionmasklookup = ff_q_pvs_ones_sum_resultconvolutionmasklookuppositive * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmasklookup) + (dst_positive_ones_sum_resultconvolutionmasklookup))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmasklookupnegative. ff_h_pvs_ones_sum_resultconvolutionmasklookupnegative + S (dst_negative_ones_sum_resultconvolutionmasklookup) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmasklookup)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasklookupnegative. dst_negative_code_ones_sum_resultconvolutionmasklookup = ff_q_pvs_ones_sum_resultconvolutionmasklookupnegative * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_ones_sum_resultconvolutionmasklookup))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue. (((((dc_value_ones_sum_resultconvolutionmask) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmasklookupvaluedecode. (((dc_value_ones_sum_resultconvolutionmask) = 2 * ge_signed_half_ones_sum_resultconvolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue) = S ge_signed_half_ones_sum_resultconvolutionmasklookupvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmasklookup) + ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue = (dst_negative_ones_sum_resultconvolutionmasklookup) + ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue))))))))) -> ((((~((dc_index_ones_sum_resultconvolutionmask)=0)) /\ (exists dc_quotient_ones_sum_resultconvolutionmaskentry dc_left_ones_sum_resultconvolutionmaskentry dc_right_ones_sum_resultconvolutionmaskentry. (((n)=(dc_index_ones_sum_resultconvolutionmask)*dc_quotient_ones_sum_resultconvolutionmaskentry) /\ (((exists dst_positive_code_ones_sum_resultconvolutionmaskentryleft dst_positive_scale_ones_sum_resultconvolutionmaskentryleft dst_negative_code_ones_sum_resultconvolutionmaskentryleft dst_negative_scale_ones_sum_resultconvolutionmaskentryleft dst_positive_ones_sum_resultconvolutionmaskentryleft dst_negative_ones_sum_resultconvolutionmaskentryleft. (((F) = (((((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)))) + ((((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryleftpositive. ff_h_pvs_ones_sum_resultconvolutionmaskentryleftpositive + S (dst_positive_ones_sum_resultconvolutionmaskentryleft) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryleftpositive. dst_positive_code_ones_sum_resultconvolutionmaskentryleft = ff_q_pvs_ones_sum_resultconvolutionmaskentryleftpositive * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_ones_sum_resultconvolutionmaskentryleft))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryleftnegative. ff_h_pvs_ones_sum_resultconvolutionmaskentryleftnegative + S (dst_negative_ones_sum_resultconvolutionmaskentryleft) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryleftnegative. dst_negative_code_ones_sum_resultconvolutionmaskentryleft = ff_q_pvs_ones_sum_resultconvolutionmaskentryleftnegative * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_ones_sum_resultconvolutionmaskentryleft))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue. (((((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryleftvaluedecode. (((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue) = S ge_signed_half_ones_sum_resultconvolutionmaskentryleftvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmaskentryleft) + ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue = (dst_negative_ones_sum_resultconvolutionmaskentryleft) + ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_ones_sum_resultconvolutionmaskentryright dst_positive_scale_ones_sum_resultconvolutionmaskentryright dst_negative_code_ones_sum_resultconvolutionmaskentryright dst_negative_scale_ones_sum_resultconvolutionmaskentryright dst_positive_ones_sum_resultconvolutionmaskentryright dst_negative_ones_sum_resultconvolutionmaskentryright. (((U) = (((((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)))) + ((((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryrightpositive. ff_h_pvs_ones_sum_resultconvolutionmaskentryrightpositive + S (dst_positive_ones_sum_resultconvolutionmaskentryright) = S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryrightpositive. dst_positive_code_ones_sum_resultconvolutionmaskentryright = ff_q_pvs_ones_sum_resultconvolutionmaskentryrightpositive * S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryright) + (dst_positive_ones_sum_resultconvolutionmaskentryright))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryrightnegative. ff_h_pvs_ones_sum_resultconvolutionmaskentryrightnegative + S (dst_negative_ones_sum_resultconvolutionmaskentryright) = S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryrightnegative. dst_negative_code_ones_sum_resultconvolutionmaskentryright = ff_q_pvs_ones_sum_resultconvolutionmaskentryrightnegative * S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_ones_sum_resultconvolutionmaskentryright))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue. (((((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryrightvaluedecode. (((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue) = S ge_signed_half_ones_sum_resultconvolutionmaskentryrightvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmaskentryright) + ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue = (dst_negative_ones_sum_resultconvolutionmaskentryright) + ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_ones_sum_resultconvolutionmaskentryproduct sto_an_ones_sum_resultconvolutionmaskentryproduct sto_bp_ones_sum_resultconvolutionmaskentryproduct sto_bn_ones_sum_resultconvolutionmaskentryproduct sto_cp_ones_sum_resultconvolutionmaskentryproduct sto_cn_ones_sum_resultconvolutionmaskentryproduct. (((((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * (sto_ap_ones_sum_resultconvolutionmaskentryproduct) /\ (sto_an_ones_sum_resultconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryproductleft. (((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryproductleft + 1 /\ (sto_ap_ones_sum_resultconvolutionmaskentryproduct) = 0) /\ (sto_an_ones_sum_resultconvolutionmaskentryproduct) = S ge_signed_half_ones_sum_resultconvolutionmaskentryproductleft))) /\ ((((((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * (sto_bp_ones_sum_resultconvolutionmaskentryproduct) /\ (sto_bn_ones_sum_resultconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryproductright. (((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryproductright + 1 /\ (sto_bp_ones_sum_resultconvolutionmaskentryproduct) = 0) /\ (sto_bn_ones_sum_resultconvolutionmaskentryproduct) = S ge_signed_half_ones_sum_resultconvolutionmaskentryproductright))) /\ ((((((dc_value_ones_sum_resultconvolutionmask) = 2 * (sto_cp_ones_sum_resultconvolutionmaskentryproduct) /\ (sto_cn_ones_sum_resultconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryproductoutput. (((dc_value_ones_sum_resultconvolutionmask) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryproductoutput + 1 /\ (sto_cp_ones_sum_resultconvolutionmaskentryproduct) = 0) /\ (sto_cn_ones_sum_resultconvolutionmaskentryproduct) = S ge_signed_half_ones_sum_resultconvolutionmaskentryproductoutput))) /\ ((sto_ap_ones_sum_resultconvolutionmaskentryproduct * sto_bp_ones_sum_resultconvolutionmaskentryproduct + sto_an_ones_sum_resultconvolutionmaskentryproduct * sto_bn_ones_sum_resultconvolutionmaskentryproduct) + sto_cn_ones_sum_resultconvolutionmaskentryproduct = (sto_ap_ones_sum_resultconvolutionmaskentryproduct * sto_bn_ones_sum_resultconvolutionmaskentryproduct + sto_an_ones_sum_resultconvolutionmaskentryproduct * sto_bp_ones_sum_resultconvolutionmaskentryproduct) + sto_cp_ones_sum_resultconvolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_ones_sum_resultconvolutionmask)=0 \/ ~(exists pvs_factor_ones_sum_resultconvolutionmaskentrynondivisor. (n) = (dc_index_ones_sum_resultconvolutionmask) * pvs_factor_ones_sum_resultconvolutionmaskentrynondivisor)) /\ ((dc_value_ones_sum_resultconvolutionmask)=0))))))) /\ (exists dst_positive_code_ones_sum_resultconvolutionfold dst_positive_scale_ones_sum_resultconvolutionfold dst_negative_code_ones_sum_resultconvolutionfold dst_negative_scale_ones_sum_resultconvolutionfold dst_positive_sum_ones_sum_resultconvolutionfold dst_negative_sum_ones_sum_resultconvolutionfold. (((dc_mask_ones_sum_resultconvolution) = (((((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) * S ((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) + ((dst_positive_scale_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold))) + (((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)))) * S ((((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) * S ((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) + ((dst_positive_scale_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold))) + (((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)))) + ((((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold))) + (((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)))))) /\ (((exists fs_u_dst_ones_sum_resultconvolutionfoldpositive fs_v_dst_ones_sum_resultconvolutionfoldpositive. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_start. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_start. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_terminal. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_terminal + S (dst_positive_sum_ones_sum_resultconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_terminal. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (dst_positive_sum_ones_sum_resultconvolutionfold))) /\ forall fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps. (exists fs_lt_dst_ones_sum_resultconvolutionfoldpositive_body_steps_bound. fs_lt_dst_ones_sum_resultconvolutionfoldpositive_body_steps_bound + S fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand + S (fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultconvolutionfold)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand. dst_positive_code_ones_sum_resultconvolutionfold = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultconvolutionfold) + (fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial + S (fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor + S (fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps))) /\ fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps = fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps + fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_sum_resultconvolutionfoldnegative fs_v_dst_ones_sum_resultconvolutionfoldnegative. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_start. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_start. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_terminal. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_terminal + S (dst_negative_sum_ones_sum_resultconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_terminal. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (dst_negative_sum_ones_sum_resultconvolutionfold))) /\ forall fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps. (exists fs_lt_dst_ones_sum_resultconvolutionfoldnegative_body_steps_bound. fs_lt_dst_ones_sum_resultconvolutionfoldnegative_body_steps_bound + S fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand + S (fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultconvolutionfold)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand. dst_negative_code_ones_sum_resultconvolutionfold = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultconvolutionfold) + (fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial + S (fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor + S (fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps))) /\ fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps = fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps + fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionfoldresult ge_balance_negative_ones_sum_resultconvolutionfoldresult. (((((z) = 2 * (ge_balance_positive_ones_sum_resultconvolutionfoldresult) /\ (ge_balance_negative_ones_sum_resultconvolutionfoldresult) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionfoldresultdecode. (((z) = 2 * ge_signed_half_ones_sum_resultconvolutionfoldresultdecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionfoldresult) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionfoldresult) = S ge_signed_half_ones_sum_resultconvolutionfoldresultdecode))) /\ ((dst_positive_sum_ones_sum_resultconvolutionfold) + ge_balance_negative_ones_sum_resultconvolutionfoldresult = (dst_negative_sum_ones_sum_resultconvolutionfold) + ge_balance_positive_ones_sum_resultconvolutionfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dm_mask_table_ones_sum_resultdivisor. ((((exists dst_positive_code_ones_sum_resultdivisormasktable dst_positive_scale_ones_sum_resultdivisormasktable dst_negative_code_ones_sum_resultdivisormasktable dst_negative_scale_ones_sum_resultdivisormasktable. (((dm_mask_table_ones_sum_resultdivisor) = (((((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) * S ((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) + ((dst_positive_scale_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable))) + (((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)))) * S ((((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) * S ((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) + ((dst_positive_scale_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable))) + (((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)))) + ((((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable))) + (((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)))))) /\ (forall dst_index_ones_sum_resultdivisormasktable. (exists pvs_le_gap_ones_sum_resultdivisormasktabledomain. pvs_le_gap_ones_sum_resultdivisormasktabledomain + (dst_index_ones_sum_resultdivisormasktable) = (n)) -> exists dst_positive_ones_sum_resultdivisormasktable dst_negative_ones_sum_resultdivisormasktable dst_value_ones_sum_resultdivisormasktable. ((((exists ff_h_pvs_ones_sum_resultdivisormasktableentrypositive. ff_h_pvs_ones_sum_resultdivisormasktableentrypositive + S (dst_positive_ones_sum_resultdivisormasktable) = S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_positive_scale_ones_sum_resultdivisormasktable)) /\ exists ff_q_pvs_ones_sum_resultdivisormasktableentrypositive. dst_positive_code_ones_sum_resultdivisormasktable = ff_q_pvs_ones_sum_resultdivisormasktableentrypositive * S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_positive_scale_ones_sum_resultdivisormasktable) + (dst_positive_ones_sum_resultdivisormasktable))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormasktableentrynegative. ff_h_pvs_ones_sum_resultdivisormasktableentrynegative + S (dst_negative_ones_sum_resultdivisormasktable) = S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_negative_scale_ones_sum_resultdivisormasktable)) /\ exists ff_q_pvs_ones_sum_resultdivisormasktableentrynegative. dst_negative_code_ones_sum_resultdivisormasktable = ff_q_pvs_ones_sum_resultdivisormasktableentrynegative * S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_ones_sum_resultdivisormasktable))) /\ (exists ge_balance_positive_ones_sum_resultdivisormasktableentryvalue ge_balance_negative_ones_sum_resultdivisormasktableentryvalue. (((((dst_value_ones_sum_resultdivisormasktable) = 2 * (ge_balance_positive_ones_sum_resultdivisormasktableentryvalue) /\ (ge_balance_negative_ones_sum_resultdivisormasktableentryvalue) = 0) \/ exists ge_signed_half_ones_sum_resultdivisormasktableentryvaluedecode. (((dst_value_ones_sum_resultdivisormasktable) = 2 * ge_signed_half_ones_sum_resultdivisormasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisormasktableentryvalue) = 0) /\ (ge_balance_negative_ones_sum_resultdivisormasktableentryvalue) = S ge_signed_half_ones_sum_resultdivisormasktableentryvaluedecode))) /\ ((dst_positive_ones_sum_resultdivisormasktable) + ge_balance_negative_ones_sum_resultdivisormasktableentryvalue = (dst_negative_ones_sum_resultdivisormasktable) + ge_balance_positive_ones_sum_resultdivisormasktableentryvalue))))))))) /\ (forall dm_index_ones_sum_resultdivisormask dm_value_ones_sum_resultdivisormask. (exists pvs_le_gap_ones_sum_resultdivisormaskdomain. pvs_le_gap_ones_sum_resultdivisormaskdomain + (dm_index_ones_sum_resultdivisormask) = (n)) -> (exists dst_positive_code_ones_sum_resultdivisormasklookup dst_positive_scale_ones_sum_resultdivisormasklookup dst_negative_code_ones_sum_resultdivisormasklookup dst_negative_scale_ones_sum_resultdivisormasklookup dst_positive_ones_sum_resultdivisormasklookup dst_negative_ones_sum_resultdivisormasklookup. (((dm_mask_table_ones_sum_resultdivisor) = (((((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) * S ((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) + ((dst_positive_scale_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup))) + (((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)))) * S ((((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) * S ((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) + ((dst_positive_scale_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup))) + (((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)))) + ((((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup))) + (((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)))))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormasklookuppositive. ff_h_pvs_ones_sum_resultdivisormasklookuppositive + S (dst_positive_ones_sum_resultdivisormasklookup) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormasklookup)) /\ exists ff_q_pvs_ones_sum_resultdivisormasklookuppositive. dst_positive_code_ones_sum_resultdivisormasklookup = ff_q_pvs_ones_sum_resultdivisormasklookuppositive * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormasklookup) + (dst_positive_ones_sum_resultdivisormasklookup))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormasklookupnegative. ff_h_pvs_ones_sum_resultdivisormasklookupnegative + S (dst_negative_ones_sum_resultdivisormasklookup) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormasklookup)) /\ exists ff_q_pvs_ones_sum_resultdivisormasklookupnegative. dst_negative_code_ones_sum_resultdivisormasklookup = ff_q_pvs_ones_sum_resultdivisormasklookupnegative * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_ones_sum_resultdivisormasklookup))) /\ (exists ge_balance_positive_ones_sum_resultdivisormasklookupvalue ge_balance_negative_ones_sum_resultdivisormasklookupvalue. (((((dm_value_ones_sum_resultdivisormask) = 2 * (ge_balance_positive_ones_sum_resultdivisormasklookupvalue) /\ (ge_balance_negative_ones_sum_resultdivisormasklookupvalue) = 0) \/ exists ge_signed_half_ones_sum_resultdivisormasklookupvaluedecode. (((dm_value_ones_sum_resultdivisormask) = 2 * ge_signed_half_ones_sum_resultdivisormasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisormasklookupvalue) = 0) /\ (ge_balance_negative_ones_sum_resultdivisormasklookupvalue) = S ge_signed_half_ones_sum_resultdivisormasklookupvaluedecode))) /\ ((dst_positive_ones_sum_resultdivisormasklookup) + ge_balance_negative_ones_sum_resultdivisormasklookupvalue = (dst_negative_ones_sum_resultdivisormasklookup) + ge_balance_positive_ones_sum_resultdivisormasklookupvalue))))))))) -> ((((~((dm_index_ones_sum_resultdivisormask)=0)) /\ (exists dm_quotient_ones_sum_resultdivisormaskentry. (((n)=(dm_index_ones_sum_resultdivisormask)*dm_quotient_ones_sum_resultdivisormaskentry) /\ (exists dst_positive_code_ones_sum_resultdivisormaskentryinput dst_positive_scale_ones_sum_resultdivisormaskentryinput dst_negative_code_ones_sum_resultdivisormaskentryinput dst_negative_scale_ones_sum_resultdivisormaskentryinput dst_positive_ones_sum_resultdivisormaskentryinput dst_negative_ones_sum_resultdivisormaskentryinput. (((F) = (((((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_positive_scale_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput))) + (((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)))) * S ((((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_positive_scale_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput))) + (((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)))) + ((((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput))) + (((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)))))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormaskentryinputpositive. ff_h_pvs_ones_sum_resultdivisormaskentryinputpositive + S (dst_positive_ones_sum_resultdivisormaskentryinput) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormaskentryinput)) /\ exists ff_q_pvs_ones_sum_resultdivisormaskentryinputpositive. dst_positive_code_ones_sum_resultdivisormaskentryinput = ff_q_pvs_ones_sum_resultdivisormaskentryinputpositive * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormaskentryinput) + (dst_positive_ones_sum_resultdivisormaskentryinput))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormaskentryinputnegative. ff_h_pvs_ones_sum_resultdivisormaskentryinputnegative + S (dst_negative_ones_sum_resultdivisormaskentryinput) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormaskentryinput)) /\ exists ff_q_pvs_ones_sum_resultdivisormaskentryinputnegative. dst_negative_code_ones_sum_resultdivisormaskentryinput = ff_q_pvs_ones_sum_resultdivisormaskentryinputnegative * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_ones_sum_resultdivisormaskentryinput))) /\ (exists ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue. (((((dm_value_ones_sum_resultdivisormask) = 2 * (ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue) /\ (ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue) = 0) \/ exists ge_signed_half_ones_sum_resultdivisormaskentryinputvaluedecode. (((dm_value_ones_sum_resultdivisormask) = 2 * ge_signed_half_ones_sum_resultdivisormaskentryinputvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue) = 0) /\ (ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue) = S ge_signed_half_ones_sum_resultdivisormaskentryinputvaluedecode))) /\ ((dst_positive_ones_sum_resultdivisormaskentryinput) + ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue = (dst_negative_ones_sum_resultdivisormaskentryinput) + ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue))))))))))))) \/ ((((dm_index_ones_sum_resultdivisormask)=0 \/ ~(exists pvs_factor_ones_sum_resultdivisormaskentrynondivisor. (n) = (dm_index_ones_sum_resultdivisormask) * pvs_factor_ones_sum_resultdivisormaskentrynondivisor)) /\ ((dm_value_ones_sum_resultdivisormask)=0))))))) /\ (exists dst_positive_code_ones_sum_resultdivisorfold dst_positive_scale_ones_sum_resultdivisorfold dst_negative_code_ones_sum_resultdivisorfold dst_negative_scale_ones_sum_resultdivisorfold dst_positive_sum_ones_sum_resultdivisorfold dst_negative_sum_ones_sum_resultdivisorfold. (((dm_mask_table_ones_sum_resultdivisor) = (((((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) * S ((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) + ((dst_positive_scale_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold))) + (((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)))) * S ((((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) * S ((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) + ((dst_positive_scale_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold))) + (((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)))) + ((((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold))) + (((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)))))) /\ (((exists fs_u_dst_ones_sum_resultdivisorfoldpositive fs_v_dst_ones_sum_resultdivisorfoldpositive. ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_start. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_start. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_terminal. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_terminal + S (dst_positive_sum_ones_sum_resultdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_terminal. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (dst_positive_sum_ones_sum_resultdivisorfold))) /\ forall fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps. (exists fs_lt_dst_ones_sum_resultdivisorfoldpositive_body_steps_bound. fs_lt_dst_ones_sum_resultdivisorfoldpositive_body_steps_bound + S fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps. ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand + S (fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultdivisorfold)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand. dst_positive_code_ones_sum_resultdivisorfold = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultdivisorfold) + (fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial + S (fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor + S (fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps))) /\ fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps = fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps + fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_sum_resultdivisorfoldnegative fs_v_dst_ones_sum_resultdivisorfoldnegative. ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_start. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_start. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_terminal. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_terminal + S (dst_negative_sum_ones_sum_resultdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_terminal. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (dst_negative_sum_ones_sum_resultdivisorfold))) /\ forall fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps. (exists fs_lt_dst_ones_sum_resultdivisorfoldnegative_body_steps_bound. fs_lt_dst_ones_sum_resultdivisorfoldnegative_body_steps_bound + S fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps. ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand + S (fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultdivisorfold)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand. dst_negative_code_ones_sum_resultdivisorfold = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultdivisorfold) + (fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial + S (fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor + S (fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps))) /\ fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps = fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps + fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_sum_resultdivisorfoldresult ge_balance_negative_ones_sum_resultdivisorfoldresult. (((((z) = 2 * (ge_balance_positive_ones_sum_resultdivisorfoldresult) /\ (ge_balance_negative_ones_sum_resultdivisorfoldresult) = 0) \/ exists ge_signed_half_ones_sum_resultdivisorfoldresultdecode. (((z) = 2 * ge_signed_half_ones_sum_resultdivisorfoldresultdecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisorfoldresult) = 0) /\ (ge_balance_negative_ones_sum_resultdivisorfoldresult) = S ge_signed_half_ones_sum_resultdivisorfoldresultdecode))) /\ ((dst_positive_sum_ones_sum_resultdivisorfold) + ge_balance_negative_ones_sum_resultdivisorfoldresult = (dst_negative_sum_ones_sum_resultdivisorfold) + ge_balance_positive_ones_sum_resultdivisorfoldresult)))))))))))))) /\ ((((~((n)=0)) /\ (exists dm_mask_table_ones_sum_resultdivisor. ((((exists dst_positive_code_ones_sum_resultdivisormasktable dst_positive_scale_ones_sum_resultdivisormasktable dst_negative_code_ones_sum_resultdivisormasktable dst_negative_scale_ones_sum_resultdivisormasktable. (((dm_mask_table_ones_sum_resultdivisor) = (((((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) * S ((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) + ((dst_positive_scale_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable))) + (((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)))) * S ((((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) * S ((dst_positive_code_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable)) + ((dst_positive_scale_ones_sum_resultdivisormasktable) + (dst_positive_scale_ones_sum_resultdivisormasktable))) + (((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)))) + ((((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable))) + (((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) * S ((dst_negative_code_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)) + ((dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_scale_ones_sum_resultdivisormasktable)))))) /\ (forall dst_index_ones_sum_resultdivisormasktable. (exists pvs_le_gap_ones_sum_resultdivisormasktabledomain. pvs_le_gap_ones_sum_resultdivisormasktabledomain + (dst_index_ones_sum_resultdivisormasktable) = (n)) -> exists dst_positive_ones_sum_resultdivisormasktable dst_negative_ones_sum_resultdivisormasktable dst_value_ones_sum_resultdivisormasktable. ((((exists ff_h_pvs_ones_sum_resultdivisormasktableentrypositive. ff_h_pvs_ones_sum_resultdivisormasktableentrypositive + S (dst_positive_ones_sum_resultdivisormasktable) = S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_positive_scale_ones_sum_resultdivisormasktable)) /\ exists ff_q_pvs_ones_sum_resultdivisormasktableentrypositive. dst_positive_code_ones_sum_resultdivisormasktable = ff_q_pvs_ones_sum_resultdivisormasktableentrypositive * S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_positive_scale_ones_sum_resultdivisormasktable) + (dst_positive_ones_sum_resultdivisormasktable))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormasktableentrynegative. ff_h_pvs_ones_sum_resultdivisormasktableentrynegative + S (dst_negative_ones_sum_resultdivisormasktable) = S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_negative_scale_ones_sum_resultdivisormasktable)) /\ exists ff_q_pvs_ones_sum_resultdivisormasktableentrynegative. dst_negative_code_ones_sum_resultdivisormasktable = ff_q_pvs_ones_sum_resultdivisormasktableentrynegative * S ((S (dst_index_ones_sum_resultdivisormasktable)) * dst_negative_scale_ones_sum_resultdivisormasktable) + (dst_negative_ones_sum_resultdivisormasktable))) /\ (exists ge_balance_positive_ones_sum_resultdivisormasktableentryvalue ge_balance_negative_ones_sum_resultdivisormasktableentryvalue. (((((dst_value_ones_sum_resultdivisormasktable) = 2 * (ge_balance_positive_ones_sum_resultdivisormasktableentryvalue) /\ (ge_balance_negative_ones_sum_resultdivisormasktableentryvalue) = 0) \/ exists ge_signed_half_ones_sum_resultdivisormasktableentryvaluedecode. (((dst_value_ones_sum_resultdivisormasktable) = 2 * ge_signed_half_ones_sum_resultdivisormasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisormasktableentryvalue) = 0) /\ (ge_balance_negative_ones_sum_resultdivisormasktableentryvalue) = S ge_signed_half_ones_sum_resultdivisormasktableentryvaluedecode))) /\ ((dst_positive_ones_sum_resultdivisormasktable) + ge_balance_negative_ones_sum_resultdivisormasktableentryvalue = (dst_negative_ones_sum_resultdivisormasktable) + ge_balance_positive_ones_sum_resultdivisormasktableentryvalue))))))))) /\ (forall dm_index_ones_sum_resultdivisormask dm_value_ones_sum_resultdivisormask. (exists pvs_le_gap_ones_sum_resultdivisormaskdomain. pvs_le_gap_ones_sum_resultdivisormaskdomain + (dm_index_ones_sum_resultdivisormask) = (n)) -> (exists dst_positive_code_ones_sum_resultdivisormasklookup dst_positive_scale_ones_sum_resultdivisormasklookup dst_negative_code_ones_sum_resultdivisormasklookup dst_negative_scale_ones_sum_resultdivisormasklookup dst_positive_ones_sum_resultdivisormasklookup dst_negative_ones_sum_resultdivisormasklookup. (((dm_mask_table_ones_sum_resultdivisor) = (((((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) * S ((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) + ((dst_positive_scale_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup))) + (((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)))) * S ((((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) * S ((dst_positive_code_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup)) + ((dst_positive_scale_ones_sum_resultdivisormasklookup) + (dst_positive_scale_ones_sum_resultdivisormasklookup))) + (((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)))) + ((((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup))) + (((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) * S ((dst_negative_code_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)) + ((dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_scale_ones_sum_resultdivisormasklookup)))))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormasklookuppositive. ff_h_pvs_ones_sum_resultdivisormasklookuppositive + S (dst_positive_ones_sum_resultdivisormasklookup) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormasklookup)) /\ exists ff_q_pvs_ones_sum_resultdivisormasklookuppositive. dst_positive_code_ones_sum_resultdivisormasklookup = ff_q_pvs_ones_sum_resultdivisormasklookuppositive * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormasklookup) + (dst_positive_ones_sum_resultdivisormasklookup))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormasklookupnegative. ff_h_pvs_ones_sum_resultdivisormasklookupnegative + S (dst_negative_ones_sum_resultdivisormasklookup) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormasklookup)) /\ exists ff_q_pvs_ones_sum_resultdivisormasklookupnegative. dst_negative_code_ones_sum_resultdivisormasklookup = ff_q_pvs_ones_sum_resultdivisormasklookupnegative * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormasklookup) + (dst_negative_ones_sum_resultdivisormasklookup))) /\ (exists ge_balance_positive_ones_sum_resultdivisormasklookupvalue ge_balance_negative_ones_sum_resultdivisormasklookupvalue. (((((dm_value_ones_sum_resultdivisormask) = 2 * (ge_balance_positive_ones_sum_resultdivisormasklookupvalue) /\ (ge_balance_negative_ones_sum_resultdivisormasklookupvalue) = 0) \/ exists ge_signed_half_ones_sum_resultdivisormasklookupvaluedecode. (((dm_value_ones_sum_resultdivisormask) = 2 * ge_signed_half_ones_sum_resultdivisormasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisormasklookupvalue) = 0) /\ (ge_balance_negative_ones_sum_resultdivisormasklookupvalue) = S ge_signed_half_ones_sum_resultdivisormasklookupvaluedecode))) /\ ((dst_positive_ones_sum_resultdivisormasklookup) + ge_balance_negative_ones_sum_resultdivisormasklookupvalue = (dst_negative_ones_sum_resultdivisormasklookup) + ge_balance_positive_ones_sum_resultdivisormasklookupvalue))))))))) -> ((((~((dm_index_ones_sum_resultdivisormask)=0)) /\ (exists dm_quotient_ones_sum_resultdivisormaskentry. (((n)=(dm_index_ones_sum_resultdivisormask)*dm_quotient_ones_sum_resultdivisormaskentry) /\ (exists dst_positive_code_ones_sum_resultdivisormaskentryinput dst_positive_scale_ones_sum_resultdivisormaskentryinput dst_negative_code_ones_sum_resultdivisormaskentryinput dst_negative_scale_ones_sum_resultdivisormaskentryinput dst_positive_ones_sum_resultdivisormaskentryinput dst_negative_ones_sum_resultdivisormaskentryinput. (((F) = (((((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_positive_scale_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput))) + (((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)))) * S ((((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_positive_code_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_positive_scale_ones_sum_resultdivisormaskentryinput) + (dst_positive_scale_ones_sum_resultdivisormaskentryinput))) + (((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)))) + ((((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput))) + (((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) * S ((dst_negative_code_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)) + ((dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_scale_ones_sum_resultdivisormaskentryinput)))))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormaskentryinputpositive. ff_h_pvs_ones_sum_resultdivisormaskentryinputpositive + S (dst_positive_ones_sum_resultdivisormaskentryinput) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormaskentryinput)) /\ exists ff_q_pvs_ones_sum_resultdivisormaskentryinputpositive. dst_positive_code_ones_sum_resultdivisormaskentryinput = ff_q_pvs_ones_sum_resultdivisormaskentryinputpositive * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_positive_scale_ones_sum_resultdivisormaskentryinput) + (dst_positive_ones_sum_resultdivisormaskentryinput))) /\ (((((exists ff_h_pvs_ones_sum_resultdivisormaskentryinputnegative. ff_h_pvs_ones_sum_resultdivisormaskentryinputnegative + S (dst_negative_ones_sum_resultdivisormaskentryinput) = S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormaskentryinput)) /\ exists ff_q_pvs_ones_sum_resultdivisormaskentryinputnegative. dst_negative_code_ones_sum_resultdivisormaskentryinput = ff_q_pvs_ones_sum_resultdivisormaskentryinputnegative * S ((S (dm_index_ones_sum_resultdivisormask)) * dst_negative_scale_ones_sum_resultdivisormaskentryinput) + (dst_negative_ones_sum_resultdivisormaskentryinput))) /\ (exists ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue. (((((dm_value_ones_sum_resultdivisormask) = 2 * (ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue) /\ (ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue) = 0) \/ exists ge_signed_half_ones_sum_resultdivisormaskentryinputvaluedecode. (((dm_value_ones_sum_resultdivisormask) = 2 * ge_signed_half_ones_sum_resultdivisormaskentryinputvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue) = 0) /\ (ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue) = S ge_signed_half_ones_sum_resultdivisormaskentryinputvaluedecode))) /\ ((dst_positive_ones_sum_resultdivisormaskentryinput) + ge_balance_negative_ones_sum_resultdivisormaskentryinputvalue = (dst_negative_ones_sum_resultdivisormaskentryinput) + ge_balance_positive_ones_sum_resultdivisormaskentryinputvalue))))))))))))) \/ ((((dm_index_ones_sum_resultdivisormask)=0 \/ ~(exists pvs_factor_ones_sum_resultdivisormaskentrynondivisor. (n) = (dm_index_ones_sum_resultdivisormask) * pvs_factor_ones_sum_resultdivisormaskentrynondivisor)) /\ ((dm_value_ones_sum_resultdivisormask)=0))))))) /\ (exists dst_positive_code_ones_sum_resultdivisorfold dst_positive_scale_ones_sum_resultdivisorfold dst_negative_code_ones_sum_resultdivisorfold dst_negative_scale_ones_sum_resultdivisorfold dst_positive_sum_ones_sum_resultdivisorfold dst_negative_sum_ones_sum_resultdivisorfold. (((dm_mask_table_ones_sum_resultdivisor) = (((((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) * S ((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) + ((dst_positive_scale_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold))) + (((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)))) * S ((((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) * S ((dst_positive_code_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold)) + ((dst_positive_scale_ones_sum_resultdivisorfold) + (dst_positive_scale_ones_sum_resultdivisorfold))) + (((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)))) + ((((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold))) + (((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) * S ((dst_negative_code_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)) + ((dst_negative_scale_ones_sum_resultdivisorfold) + (dst_negative_scale_ones_sum_resultdivisorfold)))))) /\ (((exists fs_u_dst_ones_sum_resultdivisorfoldpositive fs_v_dst_ones_sum_resultdivisorfoldpositive. ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_start. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_start. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_terminal. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_terminal + S (dst_positive_sum_ones_sum_resultdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_terminal. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (dst_positive_sum_ones_sum_resultdivisorfold))) /\ forall fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps. (exists fs_lt_dst_ones_sum_resultdivisorfoldpositive_body_steps_bound. fs_lt_dst_ones_sum_resultdivisorfoldpositive_body_steps_bound + S fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps. ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand + S (fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultdivisorfold)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand. dst_positive_code_ones_sum_resultdivisorfold = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultdivisorfold) + (fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial + S (fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor. fs_h_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor + S (fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor. fs_u_dst_ones_sum_resultdivisorfoldpositive = fs_q_dst_ones_sum_resultdivisorfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultdivisorfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldpositive) + (fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps))) /\ fs_s_dst_ones_sum_resultdivisorfoldpositive_body_steps = fs_r_dst_ones_sum_resultdivisorfoldpositive_body_steps + fs_a_dst_ones_sum_resultdivisorfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_sum_resultdivisorfoldnegative fs_v_dst_ones_sum_resultdivisorfoldnegative. ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_start. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_start. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_terminal. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_terminal + S (dst_negative_sum_ones_sum_resultdivisorfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_terminal. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (dst_negative_sum_ones_sum_resultdivisorfold))) /\ forall fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps. (exists fs_lt_dst_ones_sum_resultdivisorfoldnegative_body_steps_bound. fs_lt_dst_ones_sum_resultdivisorfoldnegative_body_steps_bound + S fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps. ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand + S (fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultdivisorfold)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand. dst_negative_code_ones_sum_resultdivisorfold = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultdivisorfold) + (fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial + S (fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor. fs_h_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor + S (fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative)) /\ exists fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor. fs_u_dst_ones_sum_resultdivisorfoldnegative = fs_q_dst_ones_sum_resultdivisorfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultdivisorfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultdivisorfoldnegative) + (fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps))) /\ fs_s_dst_ones_sum_resultdivisorfoldnegative_body_steps = fs_r_dst_ones_sum_resultdivisorfoldnegative_body_steps + fs_a_dst_ones_sum_resultdivisorfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_sum_resultdivisorfoldresult ge_balance_negative_ones_sum_resultdivisorfoldresult. (((((z) = 2 * (ge_balance_positive_ones_sum_resultdivisorfoldresult) /\ (ge_balance_negative_ones_sum_resultdivisorfoldresult) = 0) \/ exists ge_signed_half_ones_sum_resultdivisorfoldresultdecode. (((z) = 2 * ge_signed_half_ones_sum_resultdivisorfoldresultdecode + 1 /\ (ge_balance_positive_ones_sum_resultdivisorfoldresult) = 0) /\ (ge_balance_negative_ones_sum_resultdivisorfoldresult) = S ge_signed_half_ones_sum_resultdivisorfoldresultdecode))) /\ ((dst_positive_sum_ones_sum_resultdivisorfold) + ge_balance_negative_ones_sum_resultdivisorfoldresult = (dst_negative_sum_ones_sum_resultdivisorfold) + ge_balance_positive_ones_sum_resultdivisorfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_ones_sum_resultconvolution. ((((exists dst_positive_code_ones_sum_resultconvolutionmasktable dst_positive_scale_ones_sum_resultconvolutionmasktable dst_negative_code_ones_sum_resultconvolutionmasktable dst_negative_scale_ones_sum_resultconvolutionmasktable. (((dc_mask_ones_sum_resultconvolution) = (((((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) + ((dst_positive_scale_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable))) + (((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_positive_code_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable)) + ((dst_positive_scale_ones_sum_resultconvolutionmasktable) + (dst_positive_scale_ones_sum_resultconvolutionmasktable))) + (((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)))) + ((((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable))) + (((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) * S ((dst_negative_code_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)) + ((dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_scale_ones_sum_resultconvolutionmasktable)))))) /\ (forall dst_index_ones_sum_resultconvolutionmasktable. (exists pvs_le_gap_ones_sum_resultconvolutionmasktabledomain. pvs_le_gap_ones_sum_resultconvolutionmasktabledomain + (dst_index_ones_sum_resultconvolutionmasktable) = (n)) -> exists dst_positive_ones_sum_resultconvolutionmasktable dst_negative_ones_sum_resultconvolutionmasktable dst_value_ones_sum_resultconvolutionmasktable. ((((exists ff_h_pvs_ones_sum_resultconvolutionmasktableentrypositive. ff_h_pvs_ones_sum_resultconvolutionmasktableentrypositive + S (dst_positive_ones_sum_resultconvolutionmasktable) = S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_positive_scale_ones_sum_resultconvolutionmasktable)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasktableentrypositive. dst_positive_code_ones_sum_resultconvolutionmasktable = ff_q_pvs_ones_sum_resultconvolutionmasktableentrypositive * S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_positive_scale_ones_sum_resultconvolutionmasktable) + (dst_positive_ones_sum_resultconvolutionmasktable))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmasktableentrynegative. ff_h_pvs_ones_sum_resultconvolutionmasktableentrynegative + S (dst_negative_ones_sum_resultconvolutionmasktable) = S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_negative_scale_ones_sum_resultconvolutionmasktable)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasktableentrynegative. dst_negative_code_ones_sum_resultconvolutionmasktable = ff_q_pvs_ones_sum_resultconvolutionmasktableentrynegative * S ((S (dst_index_ones_sum_resultconvolutionmasktable)) * dst_negative_scale_ones_sum_resultconvolutionmasktable) + (dst_negative_ones_sum_resultconvolutionmasktable))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue. (((((dst_value_ones_sum_resultconvolutionmasktable) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmasktableentryvaluedecode. (((dst_value_ones_sum_resultconvolutionmasktable) = 2 * ge_signed_half_ones_sum_resultconvolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue) = S ge_signed_half_ones_sum_resultconvolutionmasktableentryvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmasktable) + ge_balance_negative_ones_sum_resultconvolutionmasktableentryvalue = (dst_negative_ones_sum_resultconvolutionmasktable) + ge_balance_positive_ones_sum_resultconvolutionmasktableentryvalue))))))))) /\ (forall dc_index_ones_sum_resultconvolutionmask dc_value_ones_sum_resultconvolutionmask. (exists pvs_le_gap_ones_sum_resultconvolutionmaskdomain. pvs_le_gap_ones_sum_resultconvolutionmaskdomain + (dc_index_ones_sum_resultconvolutionmask) = (n)) -> (exists dst_positive_code_ones_sum_resultconvolutionmasklookup dst_positive_scale_ones_sum_resultconvolutionmasklookup dst_negative_code_ones_sum_resultconvolutionmasklookup dst_negative_scale_ones_sum_resultconvolutionmasklookup dst_positive_ones_sum_resultconvolutionmasklookup dst_negative_ones_sum_resultconvolutionmasklookup. (((dc_mask_ones_sum_resultconvolution) = (((((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_positive_scale_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup))) + (((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_positive_code_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_positive_scale_ones_sum_resultconvolutionmasklookup) + (dst_positive_scale_ones_sum_resultconvolutionmasklookup))) + (((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)))) + ((((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup))) + (((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) * S ((dst_negative_code_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)) + ((dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_scale_ones_sum_resultconvolutionmasklookup)))))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmasklookuppositive. ff_h_pvs_ones_sum_resultconvolutionmasklookuppositive + S (dst_positive_ones_sum_resultconvolutionmasklookup) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmasklookup)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasklookuppositive. dst_positive_code_ones_sum_resultconvolutionmasklookup = ff_q_pvs_ones_sum_resultconvolutionmasklookuppositive * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmasklookup) + (dst_positive_ones_sum_resultconvolutionmasklookup))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmasklookupnegative. ff_h_pvs_ones_sum_resultconvolutionmasklookupnegative + S (dst_negative_ones_sum_resultconvolutionmasklookup) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmasklookup)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmasklookupnegative. dst_negative_code_ones_sum_resultconvolutionmasklookup = ff_q_pvs_ones_sum_resultconvolutionmasklookupnegative * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmasklookup) + (dst_negative_ones_sum_resultconvolutionmasklookup))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue. (((((dc_value_ones_sum_resultconvolutionmask) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmasklookupvaluedecode. (((dc_value_ones_sum_resultconvolutionmask) = 2 * ge_signed_half_ones_sum_resultconvolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue) = S ge_signed_half_ones_sum_resultconvolutionmasklookupvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmasklookup) + ge_balance_negative_ones_sum_resultconvolutionmasklookupvalue = (dst_negative_ones_sum_resultconvolutionmasklookup) + ge_balance_positive_ones_sum_resultconvolutionmasklookupvalue))))))))) -> ((((~((dc_index_ones_sum_resultconvolutionmask)=0)) /\ (exists dc_quotient_ones_sum_resultconvolutionmaskentry dc_left_ones_sum_resultconvolutionmaskentry dc_right_ones_sum_resultconvolutionmaskentry. (((n)=(dc_index_ones_sum_resultconvolutionmask)*dc_quotient_ones_sum_resultconvolutionmaskentry) /\ (((exists dst_positive_code_ones_sum_resultconvolutionmaskentryleft dst_positive_scale_ones_sum_resultconvolutionmaskentryleft dst_negative_code_ones_sum_resultconvolutionmaskentryleft dst_negative_scale_ones_sum_resultconvolutionmaskentryleft dst_positive_ones_sum_resultconvolutionmaskentryleft dst_negative_ones_sum_resultconvolutionmaskentryleft. (((F) = (((((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryleft))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)))) + ((((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryleftpositive. ff_h_pvs_ones_sum_resultconvolutionmaskentryleftpositive + S (dst_positive_ones_sum_resultconvolutionmaskentryleft) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryleftpositive. dst_positive_code_ones_sum_resultconvolutionmaskentryleft = ff_q_pvs_ones_sum_resultconvolutionmaskentryleftpositive * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_positive_ones_sum_resultconvolutionmaskentryleft))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryleftnegative. ff_h_pvs_ones_sum_resultconvolutionmaskentryleftnegative + S (dst_negative_ones_sum_resultconvolutionmaskentryleft) = S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryleft)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryleftnegative. dst_negative_code_ones_sum_resultconvolutionmaskentryleft = ff_q_pvs_ones_sum_resultconvolutionmaskentryleftnegative * S ((S (dc_index_ones_sum_resultconvolutionmask)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryleft) + (dst_negative_ones_sum_resultconvolutionmaskentryleft))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue. (((((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryleftvaluedecode. (((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue) = S ge_signed_half_ones_sum_resultconvolutionmaskentryleftvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmaskentryleft) + ge_balance_negative_ones_sum_resultconvolutionmaskentryleftvalue = (dst_negative_ones_sum_resultconvolutionmaskentryleft) + ge_balance_positive_ones_sum_resultconvolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_ones_sum_resultconvolutionmaskentryright dst_positive_scale_ones_sum_resultconvolutionmaskentryright dst_negative_code_ones_sum_resultconvolutionmaskentryright dst_negative_scale_ones_sum_resultconvolutionmaskentryright dst_positive_ones_sum_resultconvolutionmaskentryright dst_negative_ones_sum_resultconvolutionmaskentryright. (((U) = (((((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)))) * S ((((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_positive_code_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_positive_scale_ones_sum_resultconvolutionmaskentryright) + (dst_positive_scale_ones_sum_resultconvolutionmaskentryright))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)))) + ((((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright))) + (((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) * S ((dst_negative_code_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) + ((dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_scale_ones_sum_resultconvolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryrightpositive. ff_h_pvs_ones_sum_resultconvolutionmaskentryrightpositive + S (dst_positive_ones_sum_resultconvolutionmaskentryright) = S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryrightpositive. dst_positive_code_ones_sum_resultconvolutionmaskentryright = ff_q_pvs_ones_sum_resultconvolutionmaskentryrightpositive * S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_positive_scale_ones_sum_resultconvolutionmaskentryright) + (dst_positive_ones_sum_resultconvolutionmaskentryright))) /\ (((((exists ff_h_pvs_ones_sum_resultconvolutionmaskentryrightnegative. ff_h_pvs_ones_sum_resultconvolutionmaskentryrightnegative + S (dst_negative_ones_sum_resultconvolutionmaskentryright) = S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryright)) /\ exists ff_q_pvs_ones_sum_resultconvolutionmaskentryrightnegative. dst_negative_code_ones_sum_resultconvolutionmaskentryright = ff_q_pvs_ones_sum_resultconvolutionmaskentryrightnegative * S ((S (dc_quotient_ones_sum_resultconvolutionmaskentry)) * dst_negative_scale_ones_sum_resultconvolutionmaskentryright) + (dst_negative_ones_sum_resultconvolutionmaskentryright))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue. (((((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * (ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryrightvaluedecode. (((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue) = S ge_signed_half_ones_sum_resultconvolutionmaskentryrightvaluedecode))) /\ ((dst_positive_ones_sum_resultconvolutionmaskentryright) + ge_balance_negative_ones_sum_resultconvolutionmaskentryrightvalue = (dst_negative_ones_sum_resultconvolutionmaskentryright) + ge_balance_positive_ones_sum_resultconvolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_ones_sum_resultconvolutionmaskentryproduct sto_an_ones_sum_resultconvolutionmaskentryproduct sto_bp_ones_sum_resultconvolutionmaskentryproduct sto_bn_ones_sum_resultconvolutionmaskentryproduct sto_cp_ones_sum_resultconvolutionmaskentryproduct sto_cn_ones_sum_resultconvolutionmaskentryproduct. (((((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * (sto_ap_ones_sum_resultconvolutionmaskentryproduct) /\ (sto_an_ones_sum_resultconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryproductleft. (((dc_left_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryproductleft + 1 /\ (sto_ap_ones_sum_resultconvolutionmaskentryproduct) = 0) /\ (sto_an_ones_sum_resultconvolutionmaskentryproduct) = S ge_signed_half_ones_sum_resultconvolutionmaskentryproductleft))) /\ ((((((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * (sto_bp_ones_sum_resultconvolutionmaskentryproduct) /\ (sto_bn_ones_sum_resultconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryproductright. (((dc_right_ones_sum_resultconvolutionmaskentry) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryproductright + 1 /\ (sto_bp_ones_sum_resultconvolutionmaskentryproduct) = 0) /\ (sto_bn_ones_sum_resultconvolutionmaskentryproduct) = S ge_signed_half_ones_sum_resultconvolutionmaskentryproductright))) /\ ((((((dc_value_ones_sum_resultconvolutionmask) = 2 * (sto_cp_ones_sum_resultconvolutionmaskentryproduct) /\ (sto_cn_ones_sum_resultconvolutionmaskentryproduct) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionmaskentryproductoutput. (((dc_value_ones_sum_resultconvolutionmask) = 2 * ge_signed_half_ones_sum_resultconvolutionmaskentryproductoutput + 1 /\ (sto_cp_ones_sum_resultconvolutionmaskentryproduct) = 0) /\ (sto_cn_ones_sum_resultconvolutionmaskentryproduct) = S ge_signed_half_ones_sum_resultconvolutionmaskentryproductoutput))) /\ ((sto_ap_ones_sum_resultconvolutionmaskentryproduct * sto_bp_ones_sum_resultconvolutionmaskentryproduct + sto_an_ones_sum_resultconvolutionmaskentryproduct * sto_bn_ones_sum_resultconvolutionmaskentryproduct) + sto_cn_ones_sum_resultconvolutionmaskentryproduct = (sto_ap_ones_sum_resultconvolutionmaskentryproduct * sto_bn_ones_sum_resultconvolutionmaskentryproduct + sto_an_ones_sum_resultconvolutionmaskentryproduct * sto_bp_ones_sum_resultconvolutionmaskentryproduct) + sto_cp_ones_sum_resultconvolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_ones_sum_resultconvolutionmask)=0 \/ ~(exists pvs_factor_ones_sum_resultconvolutionmaskentrynondivisor. (n) = (dc_index_ones_sum_resultconvolutionmask) * pvs_factor_ones_sum_resultconvolutionmaskentrynondivisor)) /\ ((dc_value_ones_sum_resultconvolutionmask)=0))))))) /\ (exists dst_positive_code_ones_sum_resultconvolutionfold dst_positive_scale_ones_sum_resultconvolutionfold dst_negative_code_ones_sum_resultconvolutionfold dst_negative_scale_ones_sum_resultconvolutionfold dst_positive_sum_ones_sum_resultconvolutionfold dst_negative_sum_ones_sum_resultconvolutionfold. (((dc_mask_ones_sum_resultconvolution) = (((((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) * S ((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) + ((dst_positive_scale_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold))) + (((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)))) * S ((((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) * S ((dst_positive_code_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold)) + ((dst_positive_scale_ones_sum_resultconvolutionfold) + (dst_positive_scale_ones_sum_resultconvolutionfold))) + (((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)))) + ((((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold))) + (((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) * S ((dst_negative_code_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)) + ((dst_negative_scale_ones_sum_resultconvolutionfold) + (dst_negative_scale_ones_sum_resultconvolutionfold)))))) /\ (((exists fs_u_dst_ones_sum_resultconvolutionfoldpositive fs_v_dst_ones_sum_resultconvolutionfoldpositive. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_start. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_start. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_terminal. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_terminal + S (dst_positive_sum_ones_sum_resultconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_terminal. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (dst_positive_sum_ones_sum_resultconvolutionfold))) /\ forall fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps. (exists fs_lt_dst_ones_sum_resultconvolutionfoldpositive_body_steps_bound. fs_lt_dst_ones_sum_resultconvolutionfoldpositive_body_steps_bound + S fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand + S (fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultconvolutionfold)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand. dst_positive_code_ones_sum_resultconvolutionfold = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * dst_positive_scale_ones_sum_resultconvolutionfold) + (fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial + S (fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor. fs_h_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor + S (fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor. fs_u_dst_ones_sum_resultconvolutionfoldpositive = fs_q_dst_ones_sum_resultconvolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldpositive_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldpositive) + (fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps))) /\ fs_s_dst_ones_sum_resultconvolutionfoldpositive_body_steps = fs_r_dst_ones_sum_resultconvolutionfoldpositive_body_steps + fs_a_dst_ones_sum_resultconvolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_ones_sum_resultconvolutionfoldnegative fs_v_dst_ones_sum_resultconvolutionfoldnegative. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_start. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_start. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_terminal. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_terminal + S (dst_negative_sum_ones_sum_resultconvolutionfold) = S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_terminal. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (dst_negative_sum_ones_sum_resultconvolutionfold))) /\ forall fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps. (exists fs_lt_dst_ones_sum_resultconvolutionfoldnegative_body_steps_bound. fs_lt_dst_ones_sum_resultconvolutionfoldnegative_body_steps_bound + S fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps = S (n)) -> exists fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps. ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand + S (fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultconvolutionfold)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand. dst_negative_code_ones_sum_resultconvolutionfold = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * dst_negative_scale_ones_sum_resultconvolutionfold) + (fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial + S (fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps) = S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor. fs_h_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor + S (fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative)) /\ exists fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor. fs_u_dst_ones_sum_resultconvolutionfoldnegative = fs_q_dst_ones_sum_resultconvolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_ones_sum_resultconvolutionfoldnegative_body_steps)) * fs_v_dst_ones_sum_resultconvolutionfoldnegative) + (fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps))) /\ fs_s_dst_ones_sum_resultconvolutionfoldnegative_body_steps = fs_r_dst_ones_sum_resultconvolutionfoldnegative_body_steps + fs_a_dst_ones_sum_resultconvolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_ones_sum_resultconvolutionfoldresult ge_balance_negative_ones_sum_resultconvolutionfoldresult. (((((z) = 2 * (ge_balance_positive_ones_sum_resultconvolutionfoldresult) /\ (ge_balance_negative_ones_sum_resultconvolutionfoldresult) = 0) \/ exists ge_signed_half_ones_sum_resultconvolutionfoldresultdecode. (((z) = 2 * ge_signed_half_ones_sum_resultconvolutionfoldresultdecode + 1 /\ (ge_balance_positive_ones_sum_resultconvolutionfoldresult) = 0) /\ (ge_balance_negative_ones_sum_resultconvolutionfoldresult) = S ge_signed_half_ones_sum_resultconvolutionfoldresultdecode))) /\ ((dst_positive_sum_ones_sum_resultconvolutionfold) + ge_balance_negative_ones_sum_resultconvolutionfoldresult = (dst_negative_sum_ones_sum_resultconvolutionfold) + ge_balance_positive_ones_sum_resultconvolutionfoldresult))))))))))))))))