dirichlet_delta_right_sum_value

Exact expanded first-order arithmetic statement

forall N F E n a z. (((exists dst_positive_code_unit_value_deltatable dst_positive_scale_unit_value_deltatable dst_negative_code_unit_value_deltatable dst_negative_scale_unit_value_deltatable. (((E) = (((((dst_positive_code_unit_value_deltatable) + (dst_positive_scale_unit_value_deltatable)) * S ((dst_positive_code_unit_value_deltatable) + (dst_positive_scale_unit_value_deltatable)) + ((dst_positive_scale_unit_value_deltatable) + (dst_positive_scale_unit_value_deltatable))) + (((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) * S ((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) + ((dst_negative_scale_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)))) * S ((((dst_positive_code_unit_value_deltatable) + (dst_positive_scale_unit_value_deltatable)) * S ((dst_positive_code_unit_value_deltatable) + (dst_positive_scale_unit_value_deltatable)) + ((dst_positive_scale_unit_value_deltatable) + (dst_positive_scale_unit_value_deltatable))) + (((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) * S ((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) + ((dst_negative_scale_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)))) + ((((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) * S ((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) + ((dst_negative_scale_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable))) + (((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) * S ((dst_negative_code_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)) + ((dst_negative_scale_unit_value_deltatable) + (dst_negative_scale_unit_value_deltatable)))))) /\ (forall dst_index_unit_value_deltatable. (exists pvs_le_gap_unit_value_deltatabledomain. pvs_le_gap_unit_value_deltatabledomain + (dst_index_unit_value_deltatable) = (N)) -> exists dst_positive_unit_value_deltatable dst_negative_unit_value_deltatable dst_value_unit_value_deltatable. ((((exists ff_h_pvs_unit_value_deltatableentrypositive. ff_h_pvs_unit_value_deltatableentrypositive + S (dst_positive_unit_value_deltatable) = S ((S (dst_index_unit_value_deltatable)) * dst_positive_scale_unit_value_deltatable)) /\ exists ff_q_pvs_unit_value_deltatableentrypositive. dst_positive_code_unit_value_deltatable = ff_q_pvs_unit_value_deltatableentrypositive * S ((S (dst_index_unit_value_deltatable)) * dst_positive_scale_unit_value_deltatable) + (dst_positive_unit_value_deltatable))) /\ (((((exists ff_h_pvs_unit_value_deltatableentrynegative. ff_h_pvs_unit_value_deltatableentrynegative + S (dst_negative_unit_value_deltatable) = S ((S (dst_index_unit_value_deltatable)) * dst_negative_scale_unit_value_deltatable)) /\ exists ff_q_pvs_unit_value_deltatableentrynegative. dst_negative_code_unit_value_deltatable = ff_q_pvs_unit_value_deltatableentrynegative * S ((S (dst_index_unit_value_deltatable)) * dst_negative_scale_unit_value_deltatable) + (dst_negative_unit_value_deltatable))) /\ (exists ge_balance_positive_unit_value_deltatableentryvalue ge_balance_negative_unit_value_deltatableentryvalue. (((((dst_value_unit_value_deltatable) = 2 * (ge_balance_positive_unit_value_deltatableentryvalue) /\ (ge_balance_negative_unit_value_deltatableentryvalue) = 0) \/ exists ge_signed_half_unit_value_deltatableentryvaluedecode. (((dst_value_unit_value_deltatable) = 2 * ge_signed_half_unit_value_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_unit_value_deltatableentryvalue) = 0) /\ (ge_balance_negative_unit_value_deltatableentryvalue) = S ge_signed_half_unit_value_deltatableentryvaluedecode))) /\ ((dst_positive_unit_value_deltatable) + ge_balance_negative_unit_value_deltatableentryvalue = (dst_negative_unit_value_deltatable) + ge_balance_positive_unit_value_deltatableentryvalue))))))))) /\ (forall du_index_unit_value_delta du_value_unit_value_delta. ~(du_index_unit_value_delta=0) -> (exists pvs_le_gap_unit_value_deltabound. pvs_le_gap_unit_value_deltabound + (du_index_unit_value_delta) = (N)) -> (exists dst_positive_code_unit_value_deltaentry dst_positive_scale_unit_value_deltaentry dst_negative_code_unit_value_deltaentry dst_negative_scale_unit_value_deltaentry dst_positive_unit_value_deltaentry dst_negative_unit_value_deltaentry. (((E) = (((((dst_positive_code_unit_value_deltaentry) + (dst_positive_scale_unit_value_deltaentry)) * S ((dst_positive_code_unit_value_deltaentry) + (dst_positive_scale_unit_value_deltaentry)) + ((dst_positive_scale_unit_value_deltaentry) + (dst_positive_scale_unit_value_deltaentry))) + (((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) * S ((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) + ((dst_negative_scale_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)))) * S ((((dst_positive_code_unit_value_deltaentry) + (dst_positive_scale_unit_value_deltaentry)) * S ((dst_positive_code_unit_value_deltaentry) + (dst_positive_scale_unit_value_deltaentry)) + ((dst_positive_scale_unit_value_deltaentry) + (dst_positive_scale_unit_value_deltaentry))) + (((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) * S ((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) + ((dst_negative_scale_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)))) + ((((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) * S ((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) + ((dst_negative_scale_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry))) + (((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) * S ((dst_negative_code_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)) + ((dst_negative_scale_unit_value_deltaentry) + (dst_negative_scale_unit_value_deltaentry)))))) /\ (((((exists ff_h_pvs_unit_value_deltaentrypositive. ff_h_pvs_unit_value_deltaentrypositive + S (dst_positive_unit_value_deltaentry) = S ((S (du_index_unit_value_delta)) * dst_positive_scale_unit_value_deltaentry)) /\ exists ff_q_pvs_unit_value_deltaentrypositive. dst_positive_code_unit_value_deltaentry = ff_q_pvs_unit_value_deltaentrypositive * S ((S (du_index_unit_value_delta)) * dst_positive_scale_unit_value_deltaentry) + (dst_positive_unit_value_deltaentry))) /\ (((((exists ff_h_pvs_unit_value_deltaentrynegative. ff_h_pvs_unit_value_deltaentrynegative + S (dst_negative_unit_value_deltaentry) = S ((S (du_index_unit_value_delta)) * dst_negative_scale_unit_value_deltaentry)) /\ exists ff_q_pvs_unit_value_deltaentrynegative. dst_negative_code_unit_value_deltaentry = ff_q_pvs_unit_value_deltaentrynegative * S ((S (du_index_unit_value_delta)) * dst_negative_scale_unit_value_deltaentry) + (dst_negative_unit_value_deltaentry))) /\ (exists ge_balance_positive_unit_value_deltaentryvalue ge_balance_negative_unit_value_deltaentryvalue. (((((du_value_unit_value_delta) = 2 * (ge_balance_positive_unit_value_deltaentryvalue) /\ (ge_balance_negative_unit_value_deltaentryvalue) = 0) \/ exists ge_signed_half_unit_value_deltaentryvaluedecode. (((du_value_unit_value_delta) = 2 * ge_signed_half_unit_value_deltaentryvaluedecode + 1 /\ (ge_balance_positive_unit_value_deltaentryvalue) = 0) /\ (ge_balance_negative_unit_value_deltaentryvalue) = S ge_signed_half_unit_value_deltaentryvaluedecode))) /\ ((dst_positive_unit_value_deltaentry) + ge_balance_negative_unit_value_deltaentryvalue = (dst_negative_unit_value_deltaentry) + ge_balance_positive_unit_value_deltaentryvalue))))))))) -> ((((du_index_unit_value_delta)=1 -> (du_value_unit_value_delta)=2) /\ (~((du_index_unit_value_delta)=1) -> (du_value_unit_value_delta)=0)))))) -> (exists pvs_le_gap_unit_value_bound. pvs_le_gap_unit_value_bound + (n) = (N)) -> (exists dst_positive_code_unit_value_source dst_positive_scale_unit_value_source dst_negative_code_unit_value_source dst_negative_scale_unit_value_source dst_positive_unit_value_source dst_negative_unit_value_source. (((F) = (((((dst_positive_code_unit_value_source) + (dst_positive_scale_unit_value_source)) * S ((dst_positive_code_unit_value_source) + (dst_positive_scale_unit_value_source)) + ((dst_positive_scale_unit_value_source) + (dst_positive_scale_unit_value_source))) + (((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) * S ((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) + ((dst_negative_scale_unit_value_source) + (dst_negative_scale_unit_value_source)))) * S ((((dst_positive_code_unit_value_source) + (dst_positive_scale_unit_value_source)) * S ((dst_positive_code_unit_value_source) + (dst_positive_scale_unit_value_source)) + ((dst_positive_scale_unit_value_source) + (dst_positive_scale_unit_value_source))) + (((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) * S ((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) + ((dst_negative_scale_unit_value_source) + (dst_negative_scale_unit_value_source)))) + ((((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) * S ((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) + ((dst_negative_scale_unit_value_source) + (dst_negative_scale_unit_value_source))) + (((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) * S ((dst_negative_code_unit_value_source) + (dst_negative_scale_unit_value_source)) + ((dst_negative_scale_unit_value_source) + (dst_negative_scale_unit_value_source)))))) /\ (((((exists ff_h_pvs_unit_value_sourcepositive. ff_h_pvs_unit_value_sourcepositive + S (dst_positive_unit_value_source) = S ((S (n)) * dst_positive_scale_unit_value_source)) /\ exists ff_q_pvs_unit_value_sourcepositive. dst_positive_code_unit_value_source = ff_q_pvs_unit_value_sourcepositive * S ((S (n)) * dst_positive_scale_unit_value_source) + (dst_positive_unit_value_source))) /\ (((((exists ff_h_pvs_unit_value_sourcenegative. ff_h_pvs_unit_value_sourcenegative + S (dst_negative_unit_value_source) = S ((S (n)) * dst_negative_scale_unit_value_source)) /\ exists ff_q_pvs_unit_value_sourcenegative. dst_negative_code_unit_value_source = ff_q_pvs_unit_value_sourcenegative * S ((S (n)) * dst_negative_scale_unit_value_source) + (dst_negative_unit_value_source))) /\ (exists ge_balance_positive_unit_value_sourcevalue ge_balance_negative_unit_value_sourcevalue. (((((a) = 2 * (ge_balance_positive_unit_value_sourcevalue) /\ (ge_balance_negative_unit_value_sourcevalue) = 0) \/ exists ge_signed_half_unit_value_sourcevaluedecode. (((a) = 2 * ge_signed_half_unit_value_sourcevaluedecode + 1 /\ (ge_balance_positive_unit_value_sourcevalue) = 0) /\ (ge_balance_negative_unit_value_sourcevalue) = S ge_signed_half_unit_value_sourcevaluedecode))) /\ ((dst_positive_unit_value_source) + ge_balance_negative_unit_value_sourcevalue = (dst_negative_unit_value_source) + ge_balance_positive_unit_value_sourcevalue))))))))) -> (((~((n)=0)) /\ (exists dc_mask_unit_value_convolution. ((((exists dst_positive_code_unit_value_convolutionmasktable dst_positive_scale_unit_value_convolutionmasktable dst_negative_code_unit_value_convolutionmasktable dst_negative_scale_unit_value_convolutionmasktable. (((dc_mask_unit_value_convolution) = (((((dst_positive_code_unit_value_convolutionmasktable) + (dst_positive_scale_unit_value_convolutionmasktable)) * S ((dst_positive_code_unit_value_convolutionmasktable) + (dst_positive_scale_unit_value_convolutionmasktable)) + ((dst_positive_scale_unit_value_convolutionmasktable) + (dst_positive_scale_unit_value_convolutionmasktable))) + (((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) * S ((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) + ((dst_negative_scale_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)))) * S ((((dst_positive_code_unit_value_convolutionmasktable) + (dst_positive_scale_unit_value_convolutionmasktable)) * S ((dst_positive_code_unit_value_convolutionmasktable) + (dst_positive_scale_unit_value_convolutionmasktable)) + ((dst_positive_scale_unit_value_convolutionmasktable) + (dst_positive_scale_unit_value_convolutionmasktable))) + (((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) * S ((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) + ((dst_negative_scale_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)))) + ((((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) * S ((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) + ((dst_negative_scale_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable))) + (((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) * S ((dst_negative_code_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)) + ((dst_negative_scale_unit_value_convolutionmasktable) + (dst_negative_scale_unit_value_convolutionmasktable)))))) /\ (forall dst_index_unit_value_convolutionmasktable. (exists pvs_le_gap_unit_value_convolutionmasktabledomain. pvs_le_gap_unit_value_convolutionmasktabledomain + (dst_index_unit_value_convolutionmasktable) = (n)) -> exists dst_positive_unit_value_convolutionmasktable dst_negative_unit_value_convolutionmasktable dst_value_unit_value_convolutionmasktable. ((((exists ff_h_pvs_unit_value_convolutionmasktableentrypositive. ff_h_pvs_unit_value_convolutionmasktableentrypositive + S (dst_positive_unit_value_convolutionmasktable) = S ((S (dst_index_unit_value_convolutionmasktable)) * dst_positive_scale_unit_value_convolutionmasktable)) /\ exists ff_q_pvs_unit_value_convolutionmasktableentrypositive. dst_positive_code_unit_value_convolutionmasktable = ff_q_pvs_unit_value_convolutionmasktableentrypositive * S ((S (dst_index_unit_value_convolutionmasktable)) * dst_positive_scale_unit_value_convolutionmasktable) + (dst_positive_unit_value_convolutionmasktable))) /\ (((((exists ff_h_pvs_unit_value_convolutionmasktableentrynegative. ff_h_pvs_unit_value_convolutionmasktableentrynegative + S (dst_negative_unit_value_convolutionmasktable) = S ((S (dst_index_unit_value_convolutionmasktable)) * dst_negative_scale_unit_value_convolutionmasktable)) /\ exists ff_q_pvs_unit_value_convolutionmasktableentrynegative. dst_negative_code_unit_value_convolutionmasktable = ff_q_pvs_unit_value_convolutionmasktableentrynegative * S ((S (dst_index_unit_value_convolutionmasktable)) * dst_negative_scale_unit_value_convolutionmasktable) + (dst_negative_unit_value_convolutionmasktable))) /\ (exists ge_balance_positive_unit_value_convolutionmasktableentryvalue ge_balance_negative_unit_value_convolutionmasktableentryvalue. (((((dst_value_unit_value_convolutionmasktable) = 2 * (ge_balance_positive_unit_value_convolutionmasktableentryvalue) /\ (ge_balance_negative_unit_value_convolutionmasktableentryvalue) = 0) \/ exists ge_signed_half_unit_value_convolutionmasktableentryvaluedecode. (((dst_value_unit_value_convolutionmasktable) = 2 * ge_signed_half_unit_value_convolutionmasktableentryvaluedecode + 1 /\ (ge_balance_positive_unit_value_convolutionmasktableentryvalue) = 0) /\ (ge_balance_negative_unit_value_convolutionmasktableentryvalue) = S ge_signed_half_unit_value_convolutionmasktableentryvaluedecode))) /\ ((dst_positive_unit_value_convolutionmasktable) + ge_balance_negative_unit_value_convolutionmasktableentryvalue = (dst_negative_unit_value_convolutionmasktable) + ge_balance_positive_unit_value_convolutionmasktableentryvalue))))))))) /\ (forall dc_index_unit_value_convolutionmask dc_value_unit_value_convolutionmask. (exists pvs_le_gap_unit_value_convolutionmaskdomain. pvs_le_gap_unit_value_convolutionmaskdomain + (dc_index_unit_value_convolutionmask) = (n)) -> (exists dst_positive_code_unit_value_convolutionmasklookup dst_positive_scale_unit_value_convolutionmasklookup dst_negative_code_unit_value_convolutionmasklookup dst_negative_scale_unit_value_convolutionmasklookup dst_positive_unit_value_convolutionmasklookup dst_negative_unit_value_convolutionmasklookup. (((dc_mask_unit_value_convolution) = (((((dst_positive_code_unit_value_convolutionmasklookup) + (dst_positive_scale_unit_value_convolutionmasklookup)) * S ((dst_positive_code_unit_value_convolutionmasklookup) + (dst_positive_scale_unit_value_convolutionmasklookup)) + ((dst_positive_scale_unit_value_convolutionmasklookup) + (dst_positive_scale_unit_value_convolutionmasklookup))) + (((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) * S ((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) + ((dst_negative_scale_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)))) * S ((((dst_positive_code_unit_value_convolutionmasklookup) + (dst_positive_scale_unit_value_convolutionmasklookup)) * S ((dst_positive_code_unit_value_convolutionmasklookup) + (dst_positive_scale_unit_value_convolutionmasklookup)) + ((dst_positive_scale_unit_value_convolutionmasklookup) + (dst_positive_scale_unit_value_convolutionmasklookup))) + (((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) * S ((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) + ((dst_negative_scale_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)))) + ((((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) * S ((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) + ((dst_negative_scale_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup))) + (((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) * S ((dst_negative_code_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)) + ((dst_negative_scale_unit_value_convolutionmasklookup) + (dst_negative_scale_unit_value_convolutionmasklookup)))))) /\ (((((exists ff_h_pvs_unit_value_convolutionmasklookuppositive. ff_h_pvs_unit_value_convolutionmasklookuppositive + S (dst_positive_unit_value_convolutionmasklookup) = S ((S (dc_index_unit_value_convolutionmask)) * dst_positive_scale_unit_value_convolutionmasklookup)) /\ exists ff_q_pvs_unit_value_convolutionmasklookuppositive. dst_positive_code_unit_value_convolutionmasklookup = ff_q_pvs_unit_value_convolutionmasklookuppositive * S ((S (dc_index_unit_value_convolutionmask)) * dst_positive_scale_unit_value_convolutionmasklookup) + (dst_positive_unit_value_convolutionmasklookup))) /\ (((((exists ff_h_pvs_unit_value_convolutionmasklookupnegative. ff_h_pvs_unit_value_convolutionmasklookupnegative + S (dst_negative_unit_value_convolutionmasklookup) = S ((S (dc_index_unit_value_convolutionmask)) * dst_negative_scale_unit_value_convolutionmasklookup)) /\ exists ff_q_pvs_unit_value_convolutionmasklookupnegative. dst_negative_code_unit_value_convolutionmasklookup = ff_q_pvs_unit_value_convolutionmasklookupnegative * S ((S (dc_index_unit_value_convolutionmask)) * dst_negative_scale_unit_value_convolutionmasklookup) + (dst_negative_unit_value_convolutionmasklookup))) /\ (exists ge_balance_positive_unit_value_convolutionmasklookupvalue ge_balance_negative_unit_value_convolutionmasklookupvalue. (((((dc_value_unit_value_convolutionmask) = 2 * (ge_balance_positive_unit_value_convolutionmasklookupvalue) /\ (ge_balance_negative_unit_value_convolutionmasklookupvalue) = 0) \/ exists ge_signed_half_unit_value_convolutionmasklookupvaluedecode. (((dc_value_unit_value_convolutionmask) = 2 * ge_signed_half_unit_value_convolutionmasklookupvaluedecode + 1 /\ (ge_balance_positive_unit_value_convolutionmasklookupvalue) = 0) /\ (ge_balance_negative_unit_value_convolutionmasklookupvalue) = S ge_signed_half_unit_value_convolutionmasklookupvaluedecode))) /\ ((dst_positive_unit_value_convolutionmasklookup) + ge_balance_negative_unit_value_convolutionmasklookupvalue = (dst_negative_unit_value_convolutionmasklookup) + ge_balance_positive_unit_value_convolutionmasklookupvalue))))))))) -> ((((~((dc_index_unit_value_convolutionmask)=0)) /\ (exists dc_quotient_unit_value_convolutionmaskentry dc_left_unit_value_convolutionmaskentry dc_right_unit_value_convolutionmaskentry. (((n)=(dc_index_unit_value_convolutionmask)*dc_quotient_unit_value_convolutionmaskentry) /\ (((exists dst_positive_code_unit_value_convolutionmaskentryleft dst_positive_scale_unit_value_convolutionmaskentryleft dst_negative_code_unit_value_convolutionmaskentryleft dst_negative_scale_unit_value_convolutionmaskentryleft dst_positive_unit_value_convolutionmaskentryleft dst_negative_unit_value_convolutionmaskentryleft. (((F) = (((((dst_positive_code_unit_value_convolutionmaskentryleft) + (dst_positive_scale_unit_value_convolutionmaskentryleft)) * S ((dst_positive_code_unit_value_convolutionmaskentryleft) + (dst_positive_scale_unit_value_convolutionmaskentryleft)) + ((dst_positive_scale_unit_value_convolutionmaskentryleft) + (dst_positive_scale_unit_value_convolutionmaskentryleft))) + (((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) * S ((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) + ((dst_negative_scale_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)))) * S ((((dst_positive_code_unit_value_convolutionmaskentryleft) + (dst_positive_scale_unit_value_convolutionmaskentryleft)) * S ((dst_positive_code_unit_value_convolutionmaskentryleft) + (dst_positive_scale_unit_value_convolutionmaskentryleft)) + ((dst_positive_scale_unit_value_convolutionmaskentryleft) + (dst_positive_scale_unit_value_convolutionmaskentryleft))) + (((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) * S ((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) + ((dst_negative_scale_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)))) + ((((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) * S ((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) + ((dst_negative_scale_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft))) + (((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) * S ((dst_negative_code_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)) + ((dst_negative_scale_unit_value_convolutionmaskentryleft) + (dst_negative_scale_unit_value_convolutionmaskentryleft)))))) /\ (((((exists ff_h_pvs_unit_value_convolutionmaskentryleftpositive. ff_h_pvs_unit_value_convolutionmaskentryleftpositive + S (dst_positive_unit_value_convolutionmaskentryleft) = S ((S (dc_index_unit_value_convolutionmask)) * dst_positive_scale_unit_value_convolutionmaskentryleft)) /\ exists ff_q_pvs_unit_value_convolutionmaskentryleftpositive. dst_positive_code_unit_value_convolutionmaskentryleft = ff_q_pvs_unit_value_convolutionmaskentryleftpositive * S ((S (dc_index_unit_value_convolutionmask)) * dst_positive_scale_unit_value_convolutionmaskentryleft) + (dst_positive_unit_value_convolutionmaskentryleft))) /\ (((((exists ff_h_pvs_unit_value_convolutionmaskentryleftnegative. ff_h_pvs_unit_value_convolutionmaskentryleftnegative + S (dst_negative_unit_value_convolutionmaskentryleft) = S ((S (dc_index_unit_value_convolutionmask)) * dst_negative_scale_unit_value_convolutionmaskentryleft)) /\ exists ff_q_pvs_unit_value_convolutionmaskentryleftnegative. dst_negative_code_unit_value_convolutionmaskentryleft = ff_q_pvs_unit_value_convolutionmaskentryleftnegative * S ((S (dc_index_unit_value_convolutionmask)) * dst_negative_scale_unit_value_convolutionmaskentryleft) + (dst_negative_unit_value_convolutionmaskentryleft))) /\ (exists ge_balance_positive_unit_value_convolutionmaskentryleftvalue ge_balance_negative_unit_value_convolutionmaskentryleftvalue. (((((dc_left_unit_value_convolutionmaskentry) = 2 * (ge_balance_positive_unit_value_convolutionmaskentryleftvalue) /\ (ge_balance_negative_unit_value_convolutionmaskentryleftvalue) = 0) \/ exists ge_signed_half_unit_value_convolutionmaskentryleftvaluedecode. (((dc_left_unit_value_convolutionmaskentry) = 2 * ge_signed_half_unit_value_convolutionmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_unit_value_convolutionmaskentryleftvalue) = 0) /\ (ge_balance_negative_unit_value_convolutionmaskentryleftvalue) = S ge_signed_half_unit_value_convolutionmaskentryleftvaluedecode))) /\ ((dst_positive_unit_value_convolutionmaskentryleft) + ge_balance_negative_unit_value_convolutionmaskentryleftvalue = (dst_negative_unit_value_convolutionmaskentryleft) + ge_balance_positive_unit_value_convolutionmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_unit_value_convolutionmaskentryright dst_positive_scale_unit_value_convolutionmaskentryright dst_negative_code_unit_value_convolutionmaskentryright dst_negative_scale_unit_value_convolutionmaskentryright dst_positive_unit_value_convolutionmaskentryright dst_negative_unit_value_convolutionmaskentryright. (((E) = (((((dst_positive_code_unit_value_convolutionmaskentryright) + (dst_positive_scale_unit_value_convolutionmaskentryright)) * S ((dst_positive_code_unit_value_convolutionmaskentryright) + (dst_positive_scale_unit_value_convolutionmaskentryright)) + ((dst_positive_scale_unit_value_convolutionmaskentryright) + (dst_positive_scale_unit_value_convolutionmaskentryright))) + (((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) * S ((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) + ((dst_negative_scale_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)))) * S ((((dst_positive_code_unit_value_convolutionmaskentryright) + (dst_positive_scale_unit_value_convolutionmaskentryright)) * S ((dst_positive_code_unit_value_convolutionmaskentryright) + (dst_positive_scale_unit_value_convolutionmaskentryright)) + ((dst_positive_scale_unit_value_convolutionmaskentryright) + (dst_positive_scale_unit_value_convolutionmaskentryright))) + (((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) * S ((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) + ((dst_negative_scale_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)))) + ((((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) * S ((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) + ((dst_negative_scale_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright))) + (((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) * S ((dst_negative_code_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)) + ((dst_negative_scale_unit_value_convolutionmaskentryright) + (dst_negative_scale_unit_value_convolutionmaskentryright)))))) /\ (((((exists ff_h_pvs_unit_value_convolutionmaskentryrightpositive. ff_h_pvs_unit_value_convolutionmaskentryrightpositive + S (dst_positive_unit_value_convolutionmaskentryright) = S ((S (dc_quotient_unit_value_convolutionmaskentry)) * dst_positive_scale_unit_value_convolutionmaskentryright)) /\ exists ff_q_pvs_unit_value_convolutionmaskentryrightpositive. dst_positive_code_unit_value_convolutionmaskentryright = ff_q_pvs_unit_value_convolutionmaskentryrightpositive * S ((S (dc_quotient_unit_value_convolutionmaskentry)) * dst_positive_scale_unit_value_convolutionmaskentryright) + (dst_positive_unit_value_convolutionmaskentryright))) /\ (((((exists ff_h_pvs_unit_value_convolutionmaskentryrightnegative. ff_h_pvs_unit_value_convolutionmaskentryrightnegative + S (dst_negative_unit_value_convolutionmaskentryright) = S ((S (dc_quotient_unit_value_convolutionmaskentry)) * dst_negative_scale_unit_value_convolutionmaskentryright)) /\ exists ff_q_pvs_unit_value_convolutionmaskentryrightnegative. dst_negative_code_unit_value_convolutionmaskentryright = ff_q_pvs_unit_value_convolutionmaskentryrightnegative * S ((S (dc_quotient_unit_value_convolutionmaskentry)) * dst_negative_scale_unit_value_convolutionmaskentryright) + (dst_negative_unit_value_convolutionmaskentryright))) /\ (exists ge_balance_positive_unit_value_convolutionmaskentryrightvalue ge_balance_negative_unit_value_convolutionmaskentryrightvalue. (((((dc_right_unit_value_convolutionmaskentry) = 2 * (ge_balance_positive_unit_value_convolutionmaskentryrightvalue) /\ (ge_balance_negative_unit_value_convolutionmaskentryrightvalue) = 0) \/ exists ge_signed_half_unit_value_convolutionmaskentryrightvaluedecode. (((dc_right_unit_value_convolutionmaskentry) = 2 * ge_signed_half_unit_value_convolutionmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_unit_value_convolutionmaskentryrightvalue) = 0) /\ (ge_balance_negative_unit_value_convolutionmaskentryrightvalue) = S ge_signed_half_unit_value_convolutionmaskentryrightvaluedecode))) /\ ((dst_positive_unit_value_convolutionmaskentryright) + ge_balance_negative_unit_value_convolutionmaskentryrightvalue = (dst_negative_unit_value_convolutionmaskentryright) + ge_balance_positive_unit_value_convolutionmaskentryrightvalue))))))))) /\ (exists sto_ap_unit_value_convolutionmaskentryproduct sto_an_unit_value_convolutionmaskentryproduct sto_bp_unit_value_convolutionmaskentryproduct sto_bn_unit_value_convolutionmaskentryproduct sto_cp_unit_value_convolutionmaskentryproduct sto_cn_unit_value_convolutionmaskentryproduct. (((((dc_left_unit_value_convolutionmaskentry) = 2 * (sto_ap_unit_value_convolutionmaskentryproduct) /\ (sto_an_unit_value_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_unit_value_convolutionmaskentryproductleft. (((dc_left_unit_value_convolutionmaskentry) = 2 * ge_signed_half_unit_value_convolutionmaskentryproductleft + 1 /\ (sto_ap_unit_value_convolutionmaskentryproduct) = 0) /\ (sto_an_unit_value_convolutionmaskentryproduct) = S ge_signed_half_unit_value_convolutionmaskentryproductleft))) /\ ((((((dc_right_unit_value_convolutionmaskentry) = 2 * (sto_bp_unit_value_convolutionmaskentryproduct) /\ (sto_bn_unit_value_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_unit_value_convolutionmaskentryproductright. (((dc_right_unit_value_convolutionmaskentry) = 2 * ge_signed_half_unit_value_convolutionmaskentryproductright + 1 /\ (sto_bp_unit_value_convolutionmaskentryproduct) = 0) /\ (sto_bn_unit_value_convolutionmaskentryproduct) = S ge_signed_half_unit_value_convolutionmaskentryproductright))) /\ ((((((dc_value_unit_value_convolutionmask) = 2 * (sto_cp_unit_value_convolutionmaskentryproduct) /\ (sto_cn_unit_value_convolutionmaskentryproduct) = 0) \/ exists ge_signed_half_unit_value_convolutionmaskentryproductoutput. (((dc_value_unit_value_convolutionmask) = 2 * ge_signed_half_unit_value_convolutionmaskentryproductoutput + 1 /\ (sto_cp_unit_value_convolutionmaskentryproduct) = 0) /\ (sto_cn_unit_value_convolutionmaskentryproduct) = S ge_signed_half_unit_value_convolutionmaskentryproductoutput))) /\ ((sto_ap_unit_value_convolutionmaskentryproduct * sto_bp_unit_value_convolutionmaskentryproduct + sto_an_unit_value_convolutionmaskentryproduct * sto_bn_unit_value_convolutionmaskentryproduct) + sto_cn_unit_value_convolutionmaskentryproduct = (sto_ap_unit_value_convolutionmaskentryproduct * sto_bn_unit_value_convolutionmaskentryproduct + sto_an_unit_value_convolutionmaskentryproduct * sto_bp_unit_value_convolutionmaskentryproduct) + sto_cp_unit_value_convolutionmaskentryproduct))))))))))))))) \/ ((((dc_index_unit_value_convolutionmask)=0 \/ ~(exists pvs_factor_unit_value_convolutionmaskentrynondivisor. (n) = (dc_index_unit_value_convolutionmask) * pvs_factor_unit_value_convolutionmaskentrynondivisor)) /\ ((dc_value_unit_value_convolutionmask)=0))))))) /\ (exists dst_positive_code_unit_value_convolutionfold dst_positive_scale_unit_value_convolutionfold dst_negative_code_unit_value_convolutionfold dst_negative_scale_unit_value_convolutionfold dst_positive_sum_unit_value_convolutionfold dst_negative_sum_unit_value_convolutionfold. (((dc_mask_unit_value_convolution) = (((((dst_positive_code_unit_value_convolutionfold) + (dst_positive_scale_unit_value_convolutionfold)) * S ((dst_positive_code_unit_value_convolutionfold) + (dst_positive_scale_unit_value_convolutionfold)) + ((dst_positive_scale_unit_value_convolutionfold) + (dst_positive_scale_unit_value_convolutionfold))) + (((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) * S ((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) + ((dst_negative_scale_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)))) * S ((((dst_positive_code_unit_value_convolutionfold) + (dst_positive_scale_unit_value_convolutionfold)) * S ((dst_positive_code_unit_value_convolutionfold) + (dst_positive_scale_unit_value_convolutionfold)) + ((dst_positive_scale_unit_value_convolutionfold) + (dst_positive_scale_unit_value_convolutionfold))) + (((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) * S ((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) + ((dst_negative_scale_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)))) + ((((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) * S ((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) + ((dst_negative_scale_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold))) + (((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) * S ((dst_negative_code_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)) + ((dst_negative_scale_unit_value_convolutionfold) + (dst_negative_scale_unit_value_convolutionfold)))))) /\ (((exists fs_u_dst_unit_value_convolutionfoldpositive fs_v_dst_unit_value_convolutionfoldpositive. ((((exists fs_h_dst_unit_value_convolutionfoldpositive_body_start. fs_h_dst_unit_value_convolutionfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_value_convolutionfoldpositive)) /\ exists fs_q_dst_unit_value_convolutionfoldpositive_body_start. fs_u_dst_unit_value_convolutionfoldpositive = fs_q_dst_unit_value_convolutionfoldpositive_body_start * S ((S (0)) * fs_v_dst_unit_value_convolutionfoldpositive) + (0))) /\ ((((exists fs_h_dst_unit_value_convolutionfoldpositive_body_terminal. fs_h_dst_unit_value_convolutionfoldpositive_body_terminal + S (dst_positive_sum_unit_value_convolutionfold) = S ((S (S (n))) * fs_v_dst_unit_value_convolutionfoldpositive)) /\ exists fs_q_dst_unit_value_convolutionfoldpositive_body_terminal. fs_u_dst_unit_value_convolutionfoldpositive = fs_q_dst_unit_value_convolutionfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_unit_value_convolutionfoldpositive) + (dst_positive_sum_unit_value_convolutionfold))) /\ forall fs_i_dst_unit_value_convolutionfoldpositive_body_steps. (exists fs_lt_dst_unit_value_convolutionfoldpositive_body_steps_bound. fs_lt_dst_unit_value_convolutionfoldpositive_body_steps_bound + S fs_i_dst_unit_value_convolutionfoldpositive_body_steps = S (n)) -> exists fs_a_dst_unit_value_convolutionfoldpositive_body_steps fs_r_dst_unit_value_convolutionfoldpositive_body_steps fs_s_dst_unit_value_convolutionfoldpositive_body_steps. ((((exists fs_h_dst_unit_value_convolutionfoldpositive_body_steps_summand. fs_h_dst_unit_value_convolutionfoldpositive_body_steps_summand + S (fs_a_dst_unit_value_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_unit_value_convolutionfoldpositive_body_steps)) * dst_positive_scale_unit_value_convolutionfold)) /\ exists fs_q_dst_unit_value_convolutionfoldpositive_body_steps_summand. dst_positive_code_unit_value_convolutionfold = fs_q_dst_unit_value_convolutionfoldpositive_body_steps_summand * S ((S (fs_i_dst_unit_value_convolutionfoldpositive_body_steps)) * dst_positive_scale_unit_value_convolutionfold) + (fs_a_dst_unit_value_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_value_convolutionfoldpositive_body_steps_partial. fs_h_dst_unit_value_convolutionfoldpositive_body_steps_partial + S (fs_r_dst_unit_value_convolutionfoldpositive_body_steps) = S ((S (fs_i_dst_unit_value_convolutionfoldpositive_body_steps)) * fs_v_dst_unit_value_convolutionfoldpositive)) /\ exists fs_q_dst_unit_value_convolutionfoldpositive_body_steps_partial. fs_u_dst_unit_value_convolutionfoldpositive = fs_q_dst_unit_value_convolutionfoldpositive_body_steps_partial * S ((S (fs_i_dst_unit_value_convolutionfoldpositive_body_steps)) * fs_v_dst_unit_value_convolutionfoldpositive) + (fs_r_dst_unit_value_convolutionfoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_value_convolutionfoldpositive_body_steps_successor. fs_h_dst_unit_value_convolutionfoldpositive_body_steps_successor + S (fs_s_dst_unit_value_convolutionfoldpositive_body_steps) = S ((S (S fs_i_dst_unit_value_convolutionfoldpositive_body_steps)) * fs_v_dst_unit_value_convolutionfoldpositive)) /\ exists fs_q_dst_unit_value_convolutionfoldpositive_body_steps_successor. fs_u_dst_unit_value_convolutionfoldpositive = fs_q_dst_unit_value_convolutionfoldpositive_body_steps_successor * S ((S (S fs_i_dst_unit_value_convolutionfoldpositive_body_steps)) * fs_v_dst_unit_value_convolutionfoldpositive) + (fs_s_dst_unit_value_convolutionfoldpositive_body_steps))) /\ fs_s_dst_unit_value_convolutionfoldpositive_body_steps = fs_r_dst_unit_value_convolutionfoldpositive_body_steps + fs_a_dst_unit_value_convolutionfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_value_convolutionfoldnegative fs_v_dst_unit_value_convolutionfoldnegative. ((((exists fs_h_dst_unit_value_convolutionfoldnegative_body_start. fs_h_dst_unit_value_convolutionfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_value_convolutionfoldnegative)) /\ exists fs_q_dst_unit_value_convolutionfoldnegative_body_start. fs_u_dst_unit_value_convolutionfoldnegative = fs_q_dst_unit_value_convolutionfoldnegative_body_start * S ((S (0)) * fs_v_dst_unit_value_convolutionfoldnegative) + (0))) /\ ((((exists fs_h_dst_unit_value_convolutionfoldnegative_body_terminal. fs_h_dst_unit_value_convolutionfoldnegative_body_terminal + S (dst_negative_sum_unit_value_convolutionfold) = S ((S (S (n))) * fs_v_dst_unit_value_convolutionfoldnegative)) /\ exists fs_q_dst_unit_value_convolutionfoldnegative_body_terminal. fs_u_dst_unit_value_convolutionfoldnegative = fs_q_dst_unit_value_convolutionfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_unit_value_convolutionfoldnegative) + (dst_negative_sum_unit_value_convolutionfold))) /\ forall fs_i_dst_unit_value_convolutionfoldnegative_body_steps. (exists fs_lt_dst_unit_value_convolutionfoldnegative_body_steps_bound. fs_lt_dst_unit_value_convolutionfoldnegative_body_steps_bound + S fs_i_dst_unit_value_convolutionfoldnegative_body_steps = S (n)) -> exists fs_a_dst_unit_value_convolutionfoldnegative_body_steps fs_r_dst_unit_value_convolutionfoldnegative_body_steps fs_s_dst_unit_value_convolutionfoldnegative_body_steps. ((((exists fs_h_dst_unit_value_convolutionfoldnegative_body_steps_summand. fs_h_dst_unit_value_convolutionfoldnegative_body_steps_summand + S (fs_a_dst_unit_value_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_unit_value_convolutionfoldnegative_body_steps)) * dst_negative_scale_unit_value_convolutionfold)) /\ exists fs_q_dst_unit_value_convolutionfoldnegative_body_steps_summand. dst_negative_code_unit_value_convolutionfold = fs_q_dst_unit_value_convolutionfoldnegative_body_steps_summand * S ((S (fs_i_dst_unit_value_convolutionfoldnegative_body_steps)) * dst_negative_scale_unit_value_convolutionfold) + (fs_a_dst_unit_value_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_value_convolutionfoldnegative_body_steps_partial. fs_h_dst_unit_value_convolutionfoldnegative_body_steps_partial + S (fs_r_dst_unit_value_convolutionfoldnegative_body_steps) = S ((S (fs_i_dst_unit_value_convolutionfoldnegative_body_steps)) * fs_v_dst_unit_value_convolutionfoldnegative)) /\ exists fs_q_dst_unit_value_convolutionfoldnegative_body_steps_partial. fs_u_dst_unit_value_convolutionfoldnegative = fs_q_dst_unit_value_convolutionfoldnegative_body_steps_partial * S ((S (fs_i_dst_unit_value_convolutionfoldnegative_body_steps)) * fs_v_dst_unit_value_convolutionfoldnegative) + (fs_r_dst_unit_value_convolutionfoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_value_convolutionfoldnegative_body_steps_successor. fs_h_dst_unit_value_convolutionfoldnegative_body_steps_successor + S (fs_s_dst_unit_value_convolutionfoldnegative_body_steps) = S ((S (S fs_i_dst_unit_value_convolutionfoldnegative_body_steps)) * fs_v_dst_unit_value_convolutionfoldnegative)) /\ exists fs_q_dst_unit_value_convolutionfoldnegative_body_steps_successor. fs_u_dst_unit_value_convolutionfoldnegative = fs_q_dst_unit_value_convolutionfoldnegative_body_steps_successor * S ((S (S fs_i_dst_unit_value_convolutionfoldnegative_body_steps)) * fs_v_dst_unit_value_convolutionfoldnegative) + (fs_s_dst_unit_value_convolutionfoldnegative_body_steps))) /\ fs_s_dst_unit_value_convolutionfoldnegative_body_steps = fs_r_dst_unit_value_convolutionfoldnegative_body_steps + fs_a_dst_unit_value_convolutionfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_value_convolutionfoldresult ge_balance_negative_unit_value_convolutionfoldresult. (((((z) = 2 * (ge_balance_positive_unit_value_convolutionfoldresult) /\ (ge_balance_negative_unit_value_convolutionfoldresult) = 0) \/ exists ge_signed_half_unit_value_convolutionfoldresultdecode. (((z) = 2 * ge_signed_half_unit_value_convolutionfoldresultdecode + 1 /\ (ge_balance_positive_unit_value_convolutionfoldresult) = 0) /\ (ge_balance_negative_unit_value_convolutionfoldresult) = S ge_signed_half_unit_value_convolutionfoldresultdecode))) /\ ((dst_positive_sum_unit_value_convolutionfold) + ge_balance_negative_unit_value_convolutionfoldresult = (dst_negative_sum_unit_value_convolutionfold) + ge_balance_positive_unit_value_convolutionfoldresult))))))))))))) -> z=a