dirichlet_convolution_first_input_append_preserves

forall F G H l a m z. (((exists dst_positive_code_earlier_extensiontable dst_positive_scale_earlier_extensiontable dst_negative_code_earlier_extensiontable dst_negative_scale_earlier_extensiontable. (((H) = (((((dst_positive_code_earlier_extensiontable) + (dst_positive_scale_earlier_extensiontable)) * S ((dst_positive_code_earlier_extensiontable) + (dst_positive_scale_earlier_extensiontable)) + ((dst_positive_scale_earlier_extensiontable) + (dst_positive_scale_earlier_extensiontable))) + (((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) * S ((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) + ((dst_negative_scale_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)))) * S ((((dst_positive_code_earlier_extensiontable) + (dst_positive_scale_earlier_extensiontable)) * S ((dst_positive_code_earlier_extensiontable) + (dst_positive_scale_earlier_extensiontable)) + ((dst_positive_scale_earlier_extensiontable) + (dst_positive_scale_earlier_extensiontable))) + (((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) * S ((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) + ((dst_negative_scale_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)))) + ((((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) * S ((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) + ((dst_negative_scale_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable))) + (((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) * S ((dst_negative_code_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)) + ((dst_negative_scale_earlier_extensiontable) + (dst_negative_scale_earlier_extensiontable)))))) /\ (forall dst_index_earlier_extensiontable. (exists pvs_le_gap_earlier_extensiontabledomain. pvs_le_gap_earlier_extensiontabledomain + (dst_index_earlier_extensiontable) = (l)) -> exists dst_positive_earlier_extensiontable dst_negative_earlier_extensiontable dst_value_earlier_extensiontable. ((((exists ff_h_pvs_earlier_extensiontableentrypositive. ff_h_pvs_earlier_extensiontableentrypositive + S (dst_positive_earlier_extensiontable) = S ((S (dst_index_earlier_extensiontable)) * dst_positive_scale_earlier_extensiontable)) /\ exists ff_q_pvs_earlier_extensiontableentrypositive. dst_positive_code_earlier_extensiontable = ff_q_pvs_earlier_extensiontableentrypositive * S ((S (dst_index_earlier_extensiontable)) * dst_positive_scale_earlier_extensiontable) + (dst_positive_earlier_extensiontable))) /\ (((((exists ff_h_pvs_earlier_extensiontableentrynegative. ff_h_pvs_earlier_extensiontableentrynegative + S (dst_negative_earlier_extensiontable) = S ((S (dst_index_earlier_extensiontable)) * dst_negative_scale_earlier_extensiontable)) /\ exists ff_q_pvs_earlier_extensiontableentrynegative. dst_negative_code_earlier_extensiontable = ff_q_pvs_earlier_extensiontableentrynegative * S ((S (dst_index_earlier_extensiontable)) * dst_negative_scale_earlier_extensiontable) + (dst_negative_earlier_extensiontable))) /\ (exists ge_balance_positive_earlier_extensiontableentryvalue ge_balance_negative_earlier_extensiontableentryvalue. (((((dst_value_earlier_extensiontable) = 2 * (ge_balance_positive_earlier_extensiontableentryvalue) /\ (ge_balance_negative_earlier_extensiontableentryvalue) = 0) \/ exists ge_signed_half_earlier_extensiontableentryvaluedecode. (((dst_value_earlier_extensiontable) = 2 * ge_signed_half_earlier_extensiontableentryvaluedecode + 1 /\ (ge_balance_positive_earlier_extensiontableentryvalue) = 0) /\ (ge_balance_negative_earlier_extensiontableentryvalue) = S ge_signed_half_earlier_extensiontableentryvaluedecode))) /\ ((dst_positive_earlier_extensiontable) + ge_balance_negative_earlier_extensiontableentryvalue = (dst_negative_earlier_extensiontable) + ge_balance_positive_earlier_extensiontableentryvalue))))))))) /\ (((forall dst_index_earlier_extensionprefix dst_first_earlier_extensionprefix dst_second_earlier_extensionprefix. (exists pvs_gap_earlier_extensionprefixbound. pvs_gap_earlier_extensionprefixbound + S (dst_index_earlier_extensionprefix) = (l)) -> (exists dst_positive_code_earlier_extensionprefixfirst dst_positive_scale_earlier_extensionprefixfirst dst_negative_code_earlier_extensionprefixfirst dst_negative_scale_earlier_extensionprefixfirst dst_positive_earlier_extensionprefixfirst dst_negative_earlier_extensionprefixfirst. (((F) = (((((dst_positive_code_earlier_extensionprefixfirst) + (dst_positive_scale_earlier_extensionprefixfirst)) * S ((dst_positive_code_earlier_extensionprefixfirst) + (dst_positive_scale_earlier_extensionprefixfirst)) + ((dst_positive_scale_earlier_extensionprefixfirst) + (dst_positive_scale_earlier_extensionprefixfirst))) + (((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) * S ((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) + ((dst_negative_scale_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)))) * S ((((dst_positive_code_earlier_extensionprefixfirst) + (dst_positive_scale_earlier_extensionprefixfirst)) * S ((dst_positive_code_earlier_extensionprefixfirst) + (dst_positive_scale_earlier_extensionprefixfirst)) + ((dst_positive_scale_earlier_extensionprefixfirst) + (dst_positive_scale_earlier_extensionprefixfirst))) + (((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) * S ((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) + ((dst_negative_scale_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)))) + ((((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) * S ((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) + ((dst_negative_scale_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst))) + (((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) * S ((dst_negative_code_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)) + ((dst_negative_scale_earlier_extensionprefixfirst) + (dst_negative_scale_earlier_extensionprefixfirst)))))) /\ (((((exists ff_h_pvs_earlier_extensionprefixfirstpositive. ff_h_pvs_earlier_extensionprefixfirstpositive + S (dst_positive_earlier_extensionprefixfirst) = S ((S (dst_index_earlier_extensionprefix)) * dst_positive_scale_earlier_extensionprefixfirst)) /\ exists ff_q_pvs_earlier_extensionprefixfirstpositive. dst_positive_code_earlier_extensionprefixfirst = ff_q_pvs_earlier_extensionprefixfirstpositive * S ((S (dst_index_earlier_extensionprefix)) * dst_positive_scale_earlier_extensionprefixfirst) + (dst_positive_earlier_extensionprefixfirst))) /\ (((((exists ff_h_pvs_earlier_extensionprefixfirstnegative. ff_h_pvs_earlier_extensionprefixfirstnegative + S (dst_negative_earlier_extensionprefixfirst) = S ((S (dst_index_earlier_extensionprefix)) * dst_negative_scale_earlier_extensionprefixfirst)) /\ exists ff_q_pvs_earlier_extensionprefixfirstnegative. dst_negative_code_earlier_extensionprefixfirst = ff_q_pvs_earlier_extensionprefixfirstnegative * S ((S (dst_index_earlier_extensionprefix)) * dst_negative_scale_earlier_extensionprefixfirst) + (dst_negative_earlier_extensionprefixfirst))) /\ (exists ge_balance_positive_earlier_extensionprefixfirstvalue ge_balance_negative_earlier_extensionprefixfirstvalue. (((((dst_first_earlier_extensionprefix) = 2 * (ge_balance_positive_earlier_extensionprefixfirstvalue) /\ (ge_balance_negative_earlier_extensionprefixfirstvalue) = 0) \/ exists ge_signed_half_earlier_extensionprefixfirstvaluedecode. (((dst_first_earlier_extensionprefix) = 2 * ge_signed_half_earlier_extensionprefixfirstvaluedecode + 1 /\ (ge_balance_positive_earlier_extensionprefixfirstvalue) = 0) /\ (ge_balance_negative_earlier_extensionprefixfirstvalue) = S ge_signed_half_earlier_extensionprefixfirstvaluedecode))) /\ ((dst_positive_earlier_extensionprefixfirst) + ge_balance_negative_earlier_extensionprefixfirstvalue = (dst_negative_earlier_extensionprefixfirst) + ge_balance_positive_earlier_extensionprefixfirstvalue))))))))) -> (exists dst_positive_code_earlier_extensionprefixsecond dst_positive_scale_earlier_extensionprefixsecond dst_negative_code_earlier_extensionprefixsecond dst_negative_scale_earlier_extensionprefixsecond dst_positive_earlier_extensionprefixsecond dst_negative_earlier_extensionprefixsecond. (((H) = (((((dst_positive_code_earlier_extensionprefixsecond) + (dst_positive_scale_earlier_extensionprefixsecond)) * S ((dst_positive_code_earlier_extensionprefixsecond) + (dst_positive_scale_earlier_extensionprefixsecond)) + ((dst_positive_scale_earlier_extensionprefixsecond) + (dst_positive_scale_earlier_extensionprefixsecond))) + (((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) * S ((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) + ((dst_negative_scale_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)))) * S ((((dst_positive_code_earlier_extensionprefixsecond) + (dst_positive_scale_earlier_extensionprefixsecond)) * S ((dst_positive_code_earlier_extensionprefixsecond) + (dst_positive_scale_earlier_extensionprefixsecond)) + ((dst_positive_scale_earlier_extensionprefixsecond) + (dst_positive_scale_earlier_extensionprefixsecond))) + (((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) * S ((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) + ((dst_negative_scale_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)))) + ((((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) * S ((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) + ((dst_negative_scale_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond))) + (((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) * S ((dst_negative_code_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)) + ((dst_negative_scale_earlier_extensionprefixsecond) + (dst_negative_scale_earlier_extensionprefixsecond)))))) /\ (((((exists ff_h_pvs_earlier_extensionprefixsecondpositive. ff_h_pvs_earlier_extensionprefixsecondpositive + S (dst_positive_earlier_extensionprefixsecond) = S ((S (dst_index_earlier_extensionprefix)) * dst_positive_scale_earlier_extensionprefixsecond)) /\ exists ff_q_pvs_earlier_extensionprefixsecondpositive. dst_positive_code_earlier_extensionprefixsecond = ff_q_pvs_earlier_extensionprefixsecondpositive * S ((S (dst_index_earlier_extensionprefix)) * dst_positive_scale_earlier_extensionprefixsecond) + (dst_positive_earlier_extensionprefixsecond))) /\ (((((exists ff_h_pvs_earlier_extensionprefixsecondnegative. ff_h_pvs_earlier_extensionprefixsecondnegative + S (dst_negative_earlier_extensionprefixsecond) = S ((S (dst_index_earlier_extensionprefix)) * dst_negative_scale_earlier_extensionprefixsecond)) /\ exists ff_q_pvs_earlier_extensionprefixsecondnegative. dst_negative_code_earlier_extensionprefixsecond = ff_q_pvs_earlier_extensionprefixsecondnegative * S ((S (dst_index_earlier_extensionprefix)) * dst_negative_scale_earlier_extensionprefixsecond) + (dst_negative_earlier_extensionprefixsecond))) /\ (exists ge_balance_positive_earlier_extensionprefixsecondvalue ge_balance_negative_earlier_extensionprefixsecondvalue. (((((dst_second_earlier_extensionprefix) = 2 * (ge_balance_positive_earlier_extensionprefixsecondvalue) /\ (ge_balance_negative_earlier_extensionprefixsecondvalue) = 0) \/ exists ge_signed_half_earlier_extensionprefixsecondvaluedecode. (((dst_second_earlier_extensionprefix) = 2 * ge_signed_half_earlier_extensionprefixsecondvaluedecode + 1 /\ (ge_balance_positive_earlier_extensionprefixsecondvalue) = 0) /\ (ge_balance_negative_earlier_extensionprefixsecondvalue) = S ge_signed_half_earlier_extensionprefixsecondvaluedecode))) /\ ((dst_positive_earlier_extensionprefixsecond) + ge_balance_negative_earlier_extensionprefixsecondvalue = (dst_negative_earlier_extensionprefixsecond) + ge_balance_positive_earlier_extensionprefixsecondvalue))))))))) -> dst_first_earlier_extensionprefix = dst_second_earlier_extensionprefix) /\ (exists dst_positive_code_earlier_extensionlast dst_positive_scale_earlier_extensionlast dst_negative_code_earlier_extensionlast dst_negative_scale_earlier_extensionlast dst_positive_earlier_extensionlast dst_negative_earlier_extensionlast. (((H) = (((((dst_positive_code_earlier_extensionlast) + (dst_positive_scale_earlier_extensionlast)) * S ((dst_positive_code_earlier_extensionlast) + (dst_positive_scale_earlier_extensionlast)) + ((dst_positive_scale_earlier_extensionlast) + (dst_positive_scale_earlier_extensionlast))) + (((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) * S ((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) + ((dst_negative_scale_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)))) * S ((((dst_positive_code_earlier_extensionlast) + (dst_positive_scale_earlier_extensionlast)) * S ((dst_positive_code_earlier_extensionlast) + (dst_positive_scale_earlier_extensionlast)) + ((dst_positive_scale_earlier_extensionlast) + (dst_positive_scale_earlier_extensionlast))) + (((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) * S ((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) + ((dst_negative_scale_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)))) + ((((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) * S ((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) + ((dst_negative_scale_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast))) + (((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) * S ((dst_negative_code_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)) + ((dst_negative_scale_earlier_extensionlast) + (dst_negative_scale_earlier_extensionlast)))))) /\ (((((exists ff_h_pvs_earlier_extensionlastpositive. ff_h_pvs_earlier_extensionlastpositive + S (dst_positive_earlier_extensionlast) = S ((S (l)) * dst_positive_scale_earlier_extensionlast)) /\ exists ff_q_pvs_earlier_extensionlastpositive. dst_positive_code_earlier_extensionlast = ff_q_pvs_earlier_extensionlastpositive * S ((S (l)) * dst_positive_scale_earlier_extensionlast) + (dst_positive_earlier_extensionlast))) /\ (((((exists ff_h_pvs_earlier_extensionlastnegative. ff_h_pvs_earlier_extensionlastnegative + S (dst_negative_earlier_extensionlast) = S ((S (l)) * dst_negative_scale_earlier_extensionlast)) /\ exists ff_q_pvs_earlier_extensionlastnegative. dst_negative_code_earlier_extensionlast = ff_q_pvs_earlier_extensionlastnegative * S ((S (l)) * dst_negative_scale_earlier_extensionlast) + (dst_negative_earlier_extensionlast))) /\ (exists ge_balance_positive_earlier_extensionlastvalue ge_balance_negative_earlier_extensionlastvalue. (((((a) = 2 * (ge_balance_positive_earlier_extensionlastvalue) /\ (ge_balance_negative_earlier_extensionlastvalue) = 0) \/ exists ge_signed_half_earlier_extensionlastvaluedecode. (((a) = 2 * ge_signed_half_earlier_extensionlastvaluedecode + 1 /\ (ge_balance_positive_earlier_extensionlastvalue) = 0) /\ (ge_balance_negative_earlier_extensionlastvalue) = S ge_signed_half_earlier_extensionlastvaluedecode))) /\ ((dst_positive_earlier_extensionlast) + ge_balance_negative_earlier_extensionlastvalue = (dst_negative_earlier_extensionlast) + ge_balance_positive_earlier_extensionlastvalue))))))))))))) -> (exists pvs_gap_earlier_strict. pvs_gap_earlier_strict + S (m) = (l)) -> (((~((m)=0)) /\ (exists dc_mask_earlier_source. ((((exists dst_positive_code_earlier_sourcemasktable dst_positive_scale_earlier_sourcemasktable dst_negative_code_earlier_sourcemasktable dst_negative_scale_earlier_sourcemasktable. (((dc_mask_earlier_source) = (((((dst_positive_code_earlier_sourcemasktable) + (dst_positive_scale_earlier_sourcemasktable)) * S ((dst_positive_code_earlier_sourcemasktable) + (dst_positive_scale_earlier_sourcemasktable)) + ((dst_positive_scale_earlier_sourcemasktable) + (dst_positive_scale_earlier_sourcemasktable))) + (((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) * S ((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) + ((dst_negative_scale_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)))) * S ((((dst_positive_code_earlier_sourcemasktable) + (dst_positive_scale_earlier_sourcemasktable)) * S ((dst_positive_code_earlier_sourcemasktable) + (dst_positive_scale_earlier_sourcemasktable)) + ((dst_positive_scale_earlier_sourcemasktable) + (dst_positive_scale_earlier_sourcemasktable))) + (((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) * S ((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) + ((dst_negative_scale_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)))) + ((((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) * S ((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) + ((dst_negative_scale_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable))) + (((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) * S ((dst_negative_code_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)) + ((dst_negative_scale_earlier_sourcemasktable) + (dst_negative_scale_earlier_sourcemasktable)))))) /\ (forall dst_index_earlier_sourcemasktable. (exists pvs_le_gap_earlier_sourcemasktabledomain. pvs_le_gap_earlier_sourcemasktabledomain + (dst_index_earlier_sourcemasktable) = (m)) -> exists dst_positive_earlier_sourcemasktable dst_negative_earlier_sourcemasktable dst_value_earlier_sourcemasktable. ((((exists ff_h_pvs_earlier_sourcemasktableentrypositive. ff_h_pvs_earlier_sourcemasktableentrypositive + S (dst_positive_earlier_sourcemasktable) = S ((S (dst_index_earlier_sourcemasktable)) * dst_positive_scale_earlier_sourcemasktable)) /\ exists ff_q_pvs_earlier_sourcemasktableentrypositive. dst_positive_code_earlier_sourcemasktable = ff_q_pvs_earlier_sourcemasktableentrypositive * S ((S (dst_index_earlier_sourcemasktable)) * dst_positive_scale_earlier_sourcemasktable) + (dst_positive_earlier_sourcemasktable))) /\ (((((exists ff_h_pvs_earlier_sourcemasktableentrynegative. ff_h_pvs_earlier_sourcemasktableentrynegative + S (dst_negative_earlier_sourcemasktable) = S ((S (dst_index_earlier_sourcemasktable)) * dst_negative_scale_earlier_sourcemasktable)) /\ exists ff_q_pvs_earlier_sourcemasktableentrynegative. dst_negative_code_earlier_sourcemasktable = ff_q_pvs_earlier_sourcemasktableentrynegative * S ((S (dst_index_earlier_sourcemasktable)) * dst_negative_scale_earlier_sourcemasktable) + (dst_negative_earlier_sourcemasktable))) /\ (exists ge_balance_positive_earlier_sourcemasktableentryvalue ge_balance_negative_earlier_sourcemasktableentryvalue. (((((dst_value_earlier_sourcemasktable) = 2 * (ge_balance_positive_earlier_sourcemasktableentryvalue) /\ (ge_balance_negative_earlier_sourcemasktableentryvalue) = 0) \/ exists ge_signed_half_earlier_sourcemasktableentryvaluedecode. (((dst_value_earlier_sourcemasktable) = 2 * ge_signed_half_earlier_sourcemasktableentryvaluedecode + 1 /\ (ge_balance_positive_earlier_sourcemasktableentryvalue) = 0) /\ (ge_balance_negative_earlier_sourcemasktableentryvalue) = S ge_signed_half_earlier_sourcemasktableentryvaluedecode))) /\ ((dst_positive_earlier_sourcemasktable) + ge_balance_negative_earlier_sourcemasktableentryvalue = (dst_negative_earlier_sourcemasktable) + ge_balance_positive_earlier_sourcemasktableentryvalue))))))))) /\ (forall dc_index_earlier_sourcemask dc_value_earlier_sourcemask. (exists pvs_le_gap_earlier_sourcemaskdomain. pvs_le_gap_earlier_sourcemaskdomain + (dc_index_earlier_sourcemask) = (m)) -> (exists dst_positive_code_earlier_sourcemasklookup dst_positive_scale_earlier_sourcemasklookup dst_negative_code_earlier_sourcemasklookup dst_negative_scale_earlier_sourcemasklookup dst_positive_earlier_sourcemasklookup dst_negative_earlier_sourcemasklookup. (((dc_mask_earlier_source) = (((((dst_positive_code_earlier_sourcemasklookup) + (dst_positive_scale_earlier_sourcemasklookup)) * S ((dst_positive_code_earlier_sourcemasklookup) + (dst_positive_scale_earlier_sourcemasklookup)) + ((dst_positive_scale_earlier_sourcemasklookup) + (dst_positive_scale_earlier_sourcemasklookup))) + (((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) * S ((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) + ((dst_negative_scale_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)))) * S ((((dst_positive_code_earlier_sourcemasklookup) + (dst_positive_scale_earlier_sourcemasklookup)) * S ((dst_positive_code_earlier_sourcemasklookup) + (dst_positive_scale_earlier_sourcemasklookup)) + ((dst_positive_scale_earlier_sourcemasklookup) + (dst_positive_scale_earlier_sourcemasklookup))) + (((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) * S ((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) + ((dst_negative_scale_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)))) + ((((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) * S ((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) + ((dst_negative_scale_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup))) + (((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) * S ((dst_negative_code_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)) + ((dst_negative_scale_earlier_sourcemasklookup) + (dst_negative_scale_earlier_sourcemasklookup)))))) /\ (((((exists ff_h_pvs_earlier_sourcemasklookuppositive. ff_h_pvs_earlier_sourcemasklookuppositive + S (dst_positive_earlier_sourcemasklookup) = S ((S (dc_index_earlier_sourcemask)) * dst_positive_scale_earlier_sourcemasklookup)) /\ exists ff_q_pvs_earlier_sourcemasklookuppositive. dst_positive_code_earlier_sourcemasklookup = ff_q_pvs_earlier_sourcemasklookuppositive * S ((S (dc_index_earlier_sourcemask)) * dst_positive_scale_earlier_sourcemasklookup) + (dst_positive_earlier_sourcemasklookup))) /\ (((((exists ff_h_pvs_earlier_sourcemasklookupnegative. ff_h_pvs_earlier_sourcemasklookupnegative + S (dst_negative_earlier_sourcemasklookup) = S ((S (dc_index_earlier_sourcemask)) * dst_negative_scale_earlier_sourcemasklookup)) /\ exists ff_q_pvs_earlier_sourcemasklookupnegative. dst_negative_code_earlier_sourcemasklookup = ff_q_pvs_earlier_sourcemasklookupnegative * S ((S (dc_index_earlier_sourcemask)) * dst_negative_scale_earlier_sourcemasklookup) + (dst_negative_earlier_sourcemasklookup))) /\ (exists ge_balance_positive_earlier_sourcemasklookupvalue ge_balance_negative_earlier_sourcemasklookupvalue. (((((dc_value_earlier_sourcemask) = 2 * (ge_balance_positive_earlier_sourcemasklookupvalue) /\ (ge_balance_negative_earlier_sourcemasklookupvalue) = 0) \/ exists ge_signed_half_earlier_sourcemasklookupvaluedecode. (((dc_value_earlier_sourcemask) = 2 * ge_signed_half_earlier_sourcemasklookupvaluedecode + 1 /\ (ge_balance_positive_earlier_sourcemasklookupvalue) = 0) /\ (ge_balance_negative_earlier_sourcemasklookupvalue) = S ge_signed_half_earlier_sourcemasklookupvaluedecode))) /\ ((dst_positive_earlier_sourcemasklookup) + ge_balance_negative_earlier_sourcemasklookupvalue = (dst_negative_earlier_sourcemasklookup) + ge_balance_positive_earlier_sourcemasklookupvalue))))))))) -> ((((~((dc_index_earlier_sourcemask)=0)) /\ (exists dc_quotient_earlier_sourcemaskentry dc_left_earlier_sourcemaskentry dc_right_earlier_sourcemaskentry. (((m)=(dc_index_earlier_sourcemask)*dc_quotient_earlier_sourcemaskentry) /\ (((exists dst_positive_code_earlier_sourcemaskentryleft dst_positive_scale_earlier_sourcemaskentryleft dst_negative_code_earlier_sourcemaskentryleft dst_negative_scale_earlier_sourcemaskentryleft dst_positive_earlier_sourcemaskentryleft dst_negative_earlier_sourcemaskentryleft. (((F) = (((((dst_positive_code_earlier_sourcemaskentryleft) + (dst_positive_scale_earlier_sourcemaskentryleft)) * S ((dst_positive_code_earlier_sourcemaskentryleft) + (dst_positive_scale_earlier_sourcemaskentryleft)) + ((dst_positive_scale_earlier_sourcemaskentryleft) + (dst_positive_scale_earlier_sourcemaskentryleft))) + (((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) * S ((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) + ((dst_negative_scale_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)))) * S ((((dst_positive_code_earlier_sourcemaskentryleft) + (dst_positive_scale_earlier_sourcemaskentryleft)) * S ((dst_positive_code_earlier_sourcemaskentryleft) + (dst_positive_scale_earlier_sourcemaskentryleft)) + ((dst_positive_scale_earlier_sourcemaskentryleft) + (dst_positive_scale_earlier_sourcemaskentryleft))) + (((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) * S ((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) + ((dst_negative_scale_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)))) + ((((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) * S ((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) + ((dst_negative_scale_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft))) + (((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) * S ((dst_negative_code_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)) + ((dst_negative_scale_earlier_sourcemaskentryleft) + (dst_negative_scale_earlier_sourcemaskentryleft)))))) /\ (((((exists ff_h_pvs_earlier_sourcemaskentryleftpositive. ff_h_pvs_earlier_sourcemaskentryleftpositive + S (dst_positive_earlier_sourcemaskentryleft) = S ((S (dc_index_earlier_sourcemask)) * dst_positive_scale_earlier_sourcemaskentryleft)) /\ exists ff_q_pvs_earlier_sourcemaskentryleftpositive. dst_positive_code_earlier_sourcemaskentryleft = ff_q_pvs_earlier_sourcemaskentryleftpositive * S ((S (dc_index_earlier_sourcemask)) * dst_positive_scale_earlier_sourcemaskentryleft) + (dst_positive_earlier_sourcemaskentryleft))) /\ (((((exists ff_h_pvs_earlier_sourcemaskentryleftnegative. ff_h_pvs_earlier_sourcemaskentryleftnegative + S (dst_negative_earlier_sourcemaskentryleft) = S ((S (dc_index_earlier_sourcemask)) * dst_negative_scale_earlier_sourcemaskentryleft)) /\ exists ff_q_pvs_earlier_sourcemaskentryleftnegative. dst_negative_code_earlier_sourcemaskentryleft = ff_q_pvs_earlier_sourcemaskentryleftnegative * S ((S (dc_index_earlier_sourcemask)) * dst_negative_scale_earlier_sourcemaskentryleft) + (dst_negative_earlier_sourcemaskentryleft))) /\ (exists ge_balance_positive_earlier_sourcemaskentryleftvalue ge_balance_negative_earlier_sourcemaskentryleftvalue. (((((dc_left_earlier_sourcemaskentry) = 2 * (ge_balance_positive_earlier_sourcemaskentryleftvalue) /\ (ge_balance_negative_earlier_sourcemaskentryleftvalue) = 0) \/ exists ge_signed_half_earlier_sourcemaskentryleftvaluedecode. (((dc_left_earlier_sourcemaskentry) = 2 * ge_signed_half_earlier_sourcemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_earlier_sourcemaskentryleftvalue) = 0) /\ (ge_balance_negative_earlier_sourcemaskentryleftvalue) = S ge_signed_half_earlier_sourcemaskentryleftvaluedecode))) /\ ((dst_positive_earlier_sourcemaskentryleft) + ge_balance_negative_earlier_sourcemaskentryleftvalue = (dst_negative_earlier_sourcemaskentryleft) + ge_balance_positive_earlier_sourcemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_earlier_sourcemaskentryright dst_positive_scale_earlier_sourcemaskentryright dst_negative_code_earlier_sourcemaskentryright dst_negative_scale_earlier_sourcemaskentryright dst_positive_earlier_sourcemaskentryright dst_negative_earlier_sourcemaskentryright. (((G) = (((((dst_positive_code_earlier_sourcemaskentryright) + (dst_positive_scale_earlier_sourcemaskentryright)) * S ((dst_positive_code_earlier_sourcemaskentryright) + (dst_positive_scale_earlier_sourcemaskentryright)) + ((dst_positive_scale_earlier_sourcemaskentryright) + (dst_positive_scale_earlier_sourcemaskentryright))) + (((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) * S ((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) + ((dst_negative_scale_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)))) * S ((((dst_positive_code_earlier_sourcemaskentryright) + (dst_positive_scale_earlier_sourcemaskentryright)) * S ((dst_positive_code_earlier_sourcemaskentryright) + (dst_positive_scale_earlier_sourcemaskentryright)) + ((dst_positive_scale_earlier_sourcemaskentryright) + (dst_positive_scale_earlier_sourcemaskentryright))) + (((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) * S ((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) + ((dst_negative_scale_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)))) + ((((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) * S ((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) + ((dst_negative_scale_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright))) + (((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) * S ((dst_negative_code_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)) + ((dst_negative_scale_earlier_sourcemaskentryright) + (dst_negative_scale_earlier_sourcemaskentryright)))))) /\ (((((exists ff_h_pvs_earlier_sourcemaskentryrightpositive. ff_h_pvs_earlier_sourcemaskentryrightpositive + S (dst_positive_earlier_sourcemaskentryright) = S ((S (dc_quotient_earlier_sourcemaskentry)) * dst_positive_scale_earlier_sourcemaskentryright)) /\ exists ff_q_pvs_earlier_sourcemaskentryrightpositive. dst_positive_code_earlier_sourcemaskentryright = ff_q_pvs_earlier_sourcemaskentryrightpositive * S ((S (dc_quotient_earlier_sourcemaskentry)) * dst_positive_scale_earlier_sourcemaskentryright) + (dst_positive_earlier_sourcemaskentryright))) /\ (((((exists ff_h_pvs_earlier_sourcemaskentryrightnegative. ff_h_pvs_earlier_sourcemaskentryrightnegative + S (dst_negative_earlier_sourcemaskentryright) = S ((S (dc_quotient_earlier_sourcemaskentry)) * dst_negative_scale_earlier_sourcemaskentryright)) /\ exists ff_q_pvs_earlier_sourcemaskentryrightnegative. dst_negative_code_earlier_sourcemaskentryright = ff_q_pvs_earlier_sourcemaskentryrightnegative * S ((S (dc_quotient_earlier_sourcemaskentry)) * dst_negative_scale_earlier_sourcemaskentryright) + (dst_negative_earlier_sourcemaskentryright))) /\ (exists ge_balance_positive_earlier_sourcemaskentryrightvalue ge_balance_negative_earlier_sourcemaskentryrightvalue. (((((dc_right_earlier_sourcemaskentry) = 2 * (ge_balance_positive_earlier_sourcemaskentryrightvalue) /\ (ge_balance_negative_earlier_sourcemaskentryrightvalue) = 0) \/ exists ge_signed_half_earlier_sourcemaskentryrightvaluedecode. (((dc_right_earlier_sourcemaskentry) = 2 * ge_signed_half_earlier_sourcemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_earlier_sourcemaskentryrightvalue) = 0) /\ (ge_balance_negative_earlier_sourcemaskentryrightvalue) = S ge_signed_half_earlier_sourcemaskentryrightvaluedecode))) /\ ((dst_positive_earlier_sourcemaskentryright) + ge_balance_negative_earlier_sourcemaskentryrightvalue = (dst_negative_earlier_sourcemaskentryright) + ge_balance_positive_earlier_sourcemaskentryrightvalue))))))))) /\ (exists sto_ap_earlier_sourcemaskentryproduct sto_an_earlier_sourcemaskentryproduct sto_bp_earlier_sourcemaskentryproduct sto_bn_earlier_sourcemaskentryproduct sto_cp_earlier_sourcemaskentryproduct sto_cn_earlier_sourcemaskentryproduct. (((((dc_left_earlier_sourcemaskentry) = 2 * (sto_ap_earlier_sourcemaskentryproduct) /\ (sto_an_earlier_sourcemaskentryproduct) = 0) \/ exists ge_signed_half_earlier_sourcemaskentryproductleft. (((dc_left_earlier_sourcemaskentry) = 2 * ge_signed_half_earlier_sourcemaskentryproductleft + 1 /\ (sto_ap_earlier_sourcemaskentryproduct) = 0) /\ (sto_an_earlier_sourcemaskentryproduct) = S ge_signed_half_earlier_sourcemaskentryproductleft))) /\ ((((((dc_right_earlier_sourcemaskentry) = 2 * (sto_bp_earlier_sourcemaskentryproduct) /\ (sto_bn_earlier_sourcemaskentryproduct) = 0) \/ exists ge_signed_half_earlier_sourcemaskentryproductright. (((dc_right_earlier_sourcemaskentry) = 2 * ge_signed_half_earlier_sourcemaskentryproductright + 1 /\ (sto_bp_earlier_sourcemaskentryproduct) = 0) /\ (sto_bn_earlier_sourcemaskentryproduct) = S ge_signed_half_earlier_sourcemaskentryproductright))) /\ ((((((dc_value_earlier_sourcemask) = 2 * (sto_cp_earlier_sourcemaskentryproduct) /\ (sto_cn_earlier_sourcemaskentryproduct) = 0) \/ exists ge_signed_half_earlier_sourcemaskentryproductoutput. (((dc_value_earlier_sourcemask) = 2 * ge_signed_half_earlier_sourcemaskentryproductoutput + 1 /\ (sto_cp_earlier_sourcemaskentryproduct) = 0) /\ (sto_cn_earlier_sourcemaskentryproduct) = S ge_signed_half_earlier_sourcemaskentryproductoutput))) /\ ((sto_ap_earlier_sourcemaskentryproduct * sto_bp_earlier_sourcemaskentryproduct + sto_an_earlier_sourcemaskentryproduct * sto_bn_earlier_sourcemaskentryproduct) + sto_cn_earlier_sourcemaskentryproduct = (sto_ap_earlier_sourcemaskentryproduct * sto_bn_earlier_sourcemaskentryproduct + sto_an_earlier_sourcemaskentryproduct * sto_bp_earlier_sourcemaskentryproduct) + sto_cp_earlier_sourcemaskentryproduct))))))))))))))) \/ ((((dc_index_earlier_sourcemask)=0 \/ ~(exists pvs_factor_earlier_sourcemaskentrynondivisor. (m) = (dc_index_earlier_sourcemask) * pvs_factor_earlier_sourcemaskentrynondivisor)) /\ ((dc_value_earlier_sourcemask)=0))))))) /\ (exists dst_positive_code_earlier_sourcefold dst_positive_scale_earlier_sourcefold dst_negative_code_earlier_sourcefold dst_negative_scale_earlier_sourcefold dst_positive_sum_earlier_sourcefold dst_negative_sum_earlier_sourcefold. (((dc_mask_earlier_source) = (((((dst_positive_code_earlier_sourcefold) + (dst_positive_scale_earlier_sourcefold)) * S ((dst_positive_code_earlier_sourcefold) + (dst_positive_scale_earlier_sourcefold)) + ((dst_positive_scale_earlier_sourcefold) + (dst_positive_scale_earlier_sourcefold))) + (((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) * S ((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) + ((dst_negative_scale_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)))) * S ((((dst_positive_code_earlier_sourcefold) + (dst_positive_scale_earlier_sourcefold)) * S ((dst_positive_code_earlier_sourcefold) + (dst_positive_scale_earlier_sourcefold)) + ((dst_positive_scale_earlier_sourcefold) + (dst_positive_scale_earlier_sourcefold))) + (((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) * S ((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) + ((dst_negative_scale_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)))) + ((((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) * S ((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) + ((dst_negative_scale_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold))) + (((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) * S ((dst_negative_code_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)) + ((dst_negative_scale_earlier_sourcefold) + (dst_negative_scale_earlier_sourcefold)))))) /\ (((exists fs_u_dst_earlier_sourcefoldpositive fs_v_dst_earlier_sourcefoldpositive. ((((exists fs_h_dst_earlier_sourcefoldpositive_body_start. fs_h_dst_earlier_sourcefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_earlier_sourcefoldpositive)) /\ exists fs_q_dst_earlier_sourcefoldpositive_body_start. fs_u_dst_earlier_sourcefoldpositive = fs_q_dst_earlier_sourcefoldpositive_body_start * S ((S (0)) * fs_v_dst_earlier_sourcefoldpositive) + (0))) /\ ((((exists fs_h_dst_earlier_sourcefoldpositive_body_terminal. fs_h_dst_earlier_sourcefoldpositive_body_terminal + S (dst_positive_sum_earlier_sourcefold) = S ((S (S (m))) * fs_v_dst_earlier_sourcefoldpositive)) /\ exists fs_q_dst_earlier_sourcefoldpositive_body_terminal. fs_u_dst_earlier_sourcefoldpositive = fs_q_dst_earlier_sourcefoldpositive_body_terminal * S ((S (S (m))) * fs_v_dst_earlier_sourcefoldpositive) + (dst_positive_sum_earlier_sourcefold))) /\ forall fs_i_dst_earlier_sourcefoldpositive_body_steps. (exists fs_lt_dst_earlier_sourcefoldpositive_body_steps_bound. fs_lt_dst_earlier_sourcefoldpositive_body_steps_bound + S fs_i_dst_earlier_sourcefoldpositive_body_steps = S (m)) -> exists fs_a_dst_earlier_sourcefoldpositive_body_steps fs_r_dst_earlier_sourcefoldpositive_body_steps fs_s_dst_earlier_sourcefoldpositive_body_steps. ((((exists fs_h_dst_earlier_sourcefoldpositive_body_steps_summand. fs_h_dst_earlier_sourcefoldpositive_body_steps_summand + S (fs_a_dst_earlier_sourcefoldpositive_body_steps) = S ((S (fs_i_dst_earlier_sourcefoldpositive_body_steps)) * dst_positive_scale_earlier_sourcefold)) /\ exists fs_q_dst_earlier_sourcefoldpositive_body_steps_summand. dst_positive_code_earlier_sourcefold = fs_q_dst_earlier_sourcefoldpositive_body_steps_summand * S ((S (fs_i_dst_earlier_sourcefoldpositive_body_steps)) * dst_positive_scale_earlier_sourcefold) + (fs_a_dst_earlier_sourcefoldpositive_body_steps))) /\ ((((exists fs_h_dst_earlier_sourcefoldpositive_body_steps_partial. fs_h_dst_earlier_sourcefoldpositive_body_steps_partial + S (fs_r_dst_earlier_sourcefoldpositive_body_steps) = S ((S (fs_i_dst_earlier_sourcefoldpositive_body_steps)) * fs_v_dst_earlier_sourcefoldpositive)) /\ exists fs_q_dst_earlier_sourcefoldpositive_body_steps_partial. fs_u_dst_earlier_sourcefoldpositive = fs_q_dst_earlier_sourcefoldpositive_body_steps_partial * S ((S (fs_i_dst_earlier_sourcefoldpositive_body_steps)) * fs_v_dst_earlier_sourcefoldpositive) + (fs_r_dst_earlier_sourcefoldpositive_body_steps))) /\ ((((exists fs_h_dst_earlier_sourcefoldpositive_body_steps_successor. fs_h_dst_earlier_sourcefoldpositive_body_steps_successor + S (fs_s_dst_earlier_sourcefoldpositive_body_steps) = S ((S (S fs_i_dst_earlier_sourcefoldpositive_body_steps)) * fs_v_dst_earlier_sourcefoldpositive)) /\ exists fs_q_dst_earlier_sourcefoldpositive_body_steps_successor. fs_u_dst_earlier_sourcefoldpositive = fs_q_dst_earlier_sourcefoldpositive_body_steps_successor * S ((S (S fs_i_dst_earlier_sourcefoldpositive_body_steps)) * fs_v_dst_earlier_sourcefoldpositive) + (fs_s_dst_earlier_sourcefoldpositive_body_steps))) /\ fs_s_dst_earlier_sourcefoldpositive_body_steps = fs_r_dst_earlier_sourcefoldpositive_body_steps + fs_a_dst_earlier_sourcefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_earlier_sourcefoldnegative fs_v_dst_earlier_sourcefoldnegative. ((((exists fs_h_dst_earlier_sourcefoldnegative_body_start. fs_h_dst_earlier_sourcefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_earlier_sourcefoldnegative)) /\ exists fs_q_dst_earlier_sourcefoldnegative_body_start. fs_u_dst_earlier_sourcefoldnegative = fs_q_dst_earlier_sourcefoldnegative_body_start * S ((S (0)) * fs_v_dst_earlier_sourcefoldnegative) + (0))) /\ ((((exists fs_h_dst_earlier_sourcefoldnegative_body_terminal. fs_h_dst_earlier_sourcefoldnegative_body_terminal + S (dst_negative_sum_earlier_sourcefold) = S ((S (S (m))) * fs_v_dst_earlier_sourcefoldnegative)) /\ exists fs_q_dst_earlier_sourcefoldnegative_body_terminal. fs_u_dst_earlier_sourcefoldnegative = fs_q_dst_earlier_sourcefoldnegative_body_terminal * S ((S (S (m))) * fs_v_dst_earlier_sourcefoldnegative) + (dst_negative_sum_earlier_sourcefold))) /\ forall fs_i_dst_earlier_sourcefoldnegative_body_steps. (exists fs_lt_dst_earlier_sourcefoldnegative_body_steps_bound. fs_lt_dst_earlier_sourcefoldnegative_body_steps_bound + S fs_i_dst_earlier_sourcefoldnegative_body_steps = S (m)) -> exists fs_a_dst_earlier_sourcefoldnegative_body_steps fs_r_dst_earlier_sourcefoldnegative_body_steps fs_s_dst_earlier_sourcefoldnegative_body_steps. ((((exists fs_h_dst_earlier_sourcefoldnegative_body_steps_summand. fs_h_dst_earlier_sourcefoldnegative_body_steps_summand + S (fs_a_dst_earlier_sourcefoldnegative_body_steps) = S ((S (fs_i_dst_earlier_sourcefoldnegative_body_steps)) * dst_negative_scale_earlier_sourcefold)) /\ exists fs_q_dst_earlier_sourcefoldnegative_body_steps_summand. dst_negative_code_earlier_sourcefold = fs_q_dst_earlier_sourcefoldnegative_body_steps_summand * S ((S (fs_i_dst_earlier_sourcefoldnegative_body_steps)) * dst_negative_scale_earlier_sourcefold) + (fs_a_dst_earlier_sourcefoldnegative_body_steps))) /\ ((((exists fs_h_dst_earlier_sourcefoldnegative_body_steps_partial. fs_h_dst_earlier_sourcefoldnegative_body_steps_partial + S (fs_r_dst_earlier_sourcefoldnegative_body_steps) = S ((S (fs_i_dst_earlier_sourcefoldnegative_body_steps)) * fs_v_dst_earlier_sourcefoldnegative)) /\ exists fs_q_dst_earlier_sourcefoldnegative_body_steps_partial. fs_u_dst_earlier_sourcefoldnegative = fs_q_dst_earlier_sourcefoldnegative_body_steps_partial * S ((S (fs_i_dst_earlier_sourcefoldnegative_body_steps)) * fs_v_dst_earlier_sourcefoldnegative) + (fs_r_dst_earlier_sourcefoldnegative_body_steps))) /\ ((((exists fs_h_dst_earlier_sourcefoldnegative_body_steps_successor. fs_h_dst_earlier_sourcefoldnegative_body_steps_successor + S (fs_s_dst_earlier_sourcefoldnegative_body_steps) = S ((S (S fs_i_dst_earlier_sourcefoldnegative_body_steps)) * fs_v_dst_earlier_sourcefoldnegative)) /\ exists fs_q_dst_earlier_sourcefoldnegative_body_steps_successor. fs_u_dst_earlier_sourcefoldnegative = fs_q_dst_earlier_sourcefoldnegative_body_steps_successor * S ((S (S fs_i_dst_earlier_sourcefoldnegative_body_steps)) * fs_v_dst_earlier_sourcefoldnegative) + (fs_s_dst_earlier_sourcefoldnegative_body_steps))) /\ fs_s_dst_earlier_sourcefoldnegative_body_steps = fs_r_dst_earlier_sourcefoldnegative_body_steps + fs_a_dst_earlier_sourcefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_earlier_sourcefoldresult ge_balance_negative_earlier_sourcefoldresult. (((((z) = 2 * (ge_balance_positive_earlier_sourcefoldresult) /\ (ge_balance_negative_earlier_sourcefoldresult) = 0) \/ exists ge_signed_half_earlier_sourcefoldresultdecode. (((z) = 2 * ge_signed_half_earlier_sourcefoldresultdecode + 1 /\ (ge_balance_positive_earlier_sourcefoldresult) = 0) /\ (ge_balance_negative_earlier_sourcefoldresult) = S ge_signed_half_earlier_sourcefoldresultdecode))) /\ ((dst_positive_sum_earlier_sourcefold) + ge_balance_negative_earlier_sourcefoldresult = (dst_negative_sum_earlier_sourcefold) + ge_balance_positive_earlier_sourcefoldresult))))))))))))) -> (((~((m)=0)) /\ (exists dc_mask_earlier_result. ((((exists dst_positive_code_earlier_resultmasktable dst_positive_scale_earlier_resultmasktable dst_negative_code_earlier_resultmasktable dst_negative_scale_earlier_resultmasktable. (((dc_mask_earlier_result) = (((((dst_positive_code_earlier_resultmasktable) + (dst_positive_scale_earlier_resultmasktable)) * S ((dst_positive_code_earlier_resultmasktable) + (dst_positive_scale_earlier_resultmasktable)) + ((dst_positive_scale_earlier_resultmasktable) + (dst_positive_scale_earlier_resultmasktable))) + (((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) * S ((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) + ((dst_negative_scale_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)))) * S ((((dst_positive_code_earlier_resultmasktable) + (dst_positive_scale_earlier_resultmasktable)) * S ((dst_positive_code_earlier_resultmasktable) + (dst_positive_scale_earlier_resultmasktable)) + ((dst_positive_scale_earlier_resultmasktable) + (dst_positive_scale_earlier_resultmasktable))) + (((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) * S ((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) + ((dst_negative_scale_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)))) + ((((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) * S ((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) + ((dst_negative_scale_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable))) + (((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) * S ((dst_negative_code_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)) + ((dst_negative_scale_earlier_resultmasktable) + (dst_negative_scale_earlier_resultmasktable)))))) /\ (forall dst_index_earlier_resultmasktable. (exists pvs_le_gap_earlier_resultmasktabledomain. pvs_le_gap_earlier_resultmasktabledomain + (dst_index_earlier_resultmasktable) = (m)) -> exists dst_positive_earlier_resultmasktable dst_negative_earlier_resultmasktable dst_value_earlier_resultmasktable. ((((exists ff_h_pvs_earlier_resultmasktableentrypositive. ff_h_pvs_earlier_resultmasktableentrypositive + S (dst_positive_earlier_resultmasktable) = S ((S (dst_index_earlier_resultmasktable)) * dst_positive_scale_earlier_resultmasktable)) /\ exists ff_q_pvs_earlier_resultmasktableentrypositive. dst_positive_code_earlier_resultmasktable = ff_q_pvs_earlier_resultmasktableentrypositive * S ((S (dst_index_earlier_resultmasktable)) * dst_positive_scale_earlier_resultmasktable) + (dst_positive_earlier_resultmasktable))) /\ (((((exists ff_h_pvs_earlier_resultmasktableentrynegative. ff_h_pvs_earlier_resultmasktableentrynegative + S (dst_negative_earlier_resultmasktable) = S ((S (dst_index_earlier_resultmasktable)) * dst_negative_scale_earlier_resultmasktable)) /\ exists ff_q_pvs_earlier_resultmasktableentrynegative. dst_negative_code_earlier_resultmasktable = ff_q_pvs_earlier_resultmasktableentrynegative * S ((S (dst_index_earlier_resultmasktable)) * dst_negative_scale_earlier_resultmasktable) + (dst_negative_earlier_resultmasktable))) /\ (exists ge_balance_positive_earlier_resultmasktableentryvalue ge_balance_negative_earlier_resultmasktableentryvalue. (((((dst_value_earlier_resultmasktable) = 2 * (ge_balance_positive_earlier_resultmasktableentryvalue) /\ (ge_balance_negative_earlier_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_earlier_resultmasktableentryvaluedecode. (((dst_value_earlier_resultmasktable) = 2 * ge_signed_half_earlier_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_earlier_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_earlier_resultmasktableentryvalue) = S ge_signed_half_earlier_resultmasktableentryvaluedecode))) /\ ((dst_positive_earlier_resultmasktable) + ge_balance_negative_earlier_resultmasktableentryvalue = (dst_negative_earlier_resultmasktable) + ge_balance_positive_earlier_resultmasktableentryvalue))))))))) /\ (forall dc_index_earlier_resultmask dc_value_earlier_resultmask. (exists pvs_le_gap_earlier_resultmaskdomain. pvs_le_gap_earlier_resultmaskdomain + (dc_index_earlier_resultmask) = (m)) -> (exists dst_positive_code_earlier_resultmasklookup dst_positive_scale_earlier_resultmasklookup dst_negative_code_earlier_resultmasklookup dst_negative_scale_earlier_resultmasklookup dst_positive_earlier_resultmasklookup dst_negative_earlier_resultmasklookup. (((dc_mask_earlier_result) = (((((dst_positive_code_earlier_resultmasklookup) + (dst_positive_scale_earlier_resultmasklookup)) * S ((dst_positive_code_earlier_resultmasklookup) + (dst_positive_scale_earlier_resultmasklookup)) + ((dst_positive_scale_earlier_resultmasklookup) + (dst_positive_scale_earlier_resultmasklookup))) + (((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) * S ((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) + ((dst_negative_scale_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)))) * S ((((dst_positive_code_earlier_resultmasklookup) + (dst_positive_scale_earlier_resultmasklookup)) * S ((dst_positive_code_earlier_resultmasklookup) + (dst_positive_scale_earlier_resultmasklookup)) + ((dst_positive_scale_earlier_resultmasklookup) + (dst_positive_scale_earlier_resultmasklookup))) + (((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) * S ((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) + ((dst_negative_scale_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)))) + ((((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) * S ((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) + ((dst_negative_scale_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup))) + (((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) * S ((dst_negative_code_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)) + ((dst_negative_scale_earlier_resultmasklookup) + (dst_negative_scale_earlier_resultmasklookup)))))) /\ (((((exists ff_h_pvs_earlier_resultmasklookuppositive. ff_h_pvs_earlier_resultmasklookuppositive + S (dst_positive_earlier_resultmasklookup) = S ((S (dc_index_earlier_resultmask)) * dst_positive_scale_earlier_resultmasklookup)) /\ exists ff_q_pvs_earlier_resultmasklookuppositive. dst_positive_code_earlier_resultmasklookup = ff_q_pvs_earlier_resultmasklookuppositive * S ((S (dc_index_earlier_resultmask)) * dst_positive_scale_earlier_resultmasklookup) + (dst_positive_earlier_resultmasklookup))) /\ (((((exists ff_h_pvs_earlier_resultmasklookupnegative. ff_h_pvs_earlier_resultmasklookupnegative + S (dst_negative_earlier_resultmasklookup) = S ((S (dc_index_earlier_resultmask)) * dst_negative_scale_earlier_resultmasklookup)) /\ exists ff_q_pvs_earlier_resultmasklookupnegative. dst_negative_code_earlier_resultmasklookup = ff_q_pvs_earlier_resultmasklookupnegative * S ((S (dc_index_earlier_resultmask)) * dst_negative_scale_earlier_resultmasklookup) + (dst_negative_earlier_resultmasklookup))) /\ (exists ge_balance_positive_earlier_resultmasklookupvalue ge_balance_negative_earlier_resultmasklookupvalue. (((((dc_value_earlier_resultmask) = 2 * (ge_balance_positive_earlier_resultmasklookupvalue) /\ (ge_balance_negative_earlier_resultmasklookupvalue) = 0) \/ exists ge_signed_half_earlier_resultmasklookupvaluedecode. (((dc_value_earlier_resultmask) = 2 * ge_signed_half_earlier_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_earlier_resultmasklookupvalue) = 0) /\ (ge_balance_negative_earlier_resultmasklookupvalue) = S ge_signed_half_earlier_resultmasklookupvaluedecode))) /\ ((dst_positive_earlier_resultmasklookup) + ge_balance_negative_earlier_resultmasklookupvalue = (dst_negative_earlier_resultmasklookup) + ge_balance_positive_earlier_resultmasklookupvalue))))))))) -> ((((~((dc_index_earlier_resultmask)=0)) /\ (exists dc_quotient_earlier_resultmaskentry dc_left_earlier_resultmaskentry dc_right_earlier_resultmaskentry. (((m)=(dc_index_earlier_resultmask)*dc_quotient_earlier_resultmaskentry) /\ (((exists dst_positive_code_earlier_resultmaskentryleft dst_positive_scale_earlier_resultmaskentryleft dst_negative_code_earlier_resultmaskentryleft dst_negative_scale_earlier_resultmaskentryleft dst_positive_earlier_resultmaskentryleft dst_negative_earlier_resultmaskentryleft. (((H) = (((((dst_positive_code_earlier_resultmaskentryleft) + (dst_positive_scale_earlier_resultmaskentryleft)) * S ((dst_positive_code_earlier_resultmaskentryleft) + (dst_positive_scale_earlier_resultmaskentryleft)) + ((dst_positive_scale_earlier_resultmaskentryleft) + (dst_positive_scale_earlier_resultmaskentryleft))) + (((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) * S ((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) + ((dst_negative_scale_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)))) * S ((((dst_positive_code_earlier_resultmaskentryleft) + (dst_positive_scale_earlier_resultmaskentryleft)) * S ((dst_positive_code_earlier_resultmaskentryleft) + (dst_positive_scale_earlier_resultmaskentryleft)) + ((dst_positive_scale_earlier_resultmaskentryleft) + (dst_positive_scale_earlier_resultmaskentryleft))) + (((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) * S ((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) + ((dst_negative_scale_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)))) + ((((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) * S ((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) + ((dst_negative_scale_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft))) + (((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) * S ((dst_negative_code_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)) + ((dst_negative_scale_earlier_resultmaskentryleft) + (dst_negative_scale_earlier_resultmaskentryleft)))))) /\ (((((exists ff_h_pvs_earlier_resultmaskentryleftpositive. ff_h_pvs_earlier_resultmaskentryleftpositive + S (dst_positive_earlier_resultmaskentryleft) = S ((S (dc_index_earlier_resultmask)) * dst_positive_scale_earlier_resultmaskentryleft)) /\ exists ff_q_pvs_earlier_resultmaskentryleftpositive. dst_positive_code_earlier_resultmaskentryleft = ff_q_pvs_earlier_resultmaskentryleftpositive * S ((S (dc_index_earlier_resultmask)) * dst_positive_scale_earlier_resultmaskentryleft) + (dst_positive_earlier_resultmaskentryleft))) /\ (((((exists ff_h_pvs_earlier_resultmaskentryleftnegative. ff_h_pvs_earlier_resultmaskentryleftnegative + S (dst_negative_earlier_resultmaskentryleft) = S ((S (dc_index_earlier_resultmask)) * dst_negative_scale_earlier_resultmaskentryleft)) /\ exists ff_q_pvs_earlier_resultmaskentryleftnegative. dst_negative_code_earlier_resultmaskentryleft = ff_q_pvs_earlier_resultmaskentryleftnegative * S ((S (dc_index_earlier_resultmask)) * dst_negative_scale_earlier_resultmaskentryleft) + (dst_negative_earlier_resultmaskentryleft))) /\ (exists ge_balance_positive_earlier_resultmaskentryleftvalue ge_balance_negative_earlier_resultmaskentryleftvalue. (((((dc_left_earlier_resultmaskentry) = 2 * (ge_balance_positive_earlier_resultmaskentryleftvalue) /\ (ge_balance_negative_earlier_resultmaskentryleftvalue) = 0) \/ exists ge_signed_half_earlier_resultmaskentryleftvaluedecode. (((dc_left_earlier_resultmaskentry) = 2 * ge_signed_half_earlier_resultmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_earlier_resultmaskentryleftvalue) = 0) /\ (ge_balance_negative_earlier_resultmaskentryleftvalue) = S ge_signed_half_earlier_resultmaskentryleftvaluedecode))) /\ ((dst_positive_earlier_resultmaskentryleft) + ge_balance_negative_earlier_resultmaskentryleftvalue = (dst_negative_earlier_resultmaskentryleft) + ge_balance_positive_earlier_resultmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_earlier_resultmaskentryright dst_positive_scale_earlier_resultmaskentryright dst_negative_code_earlier_resultmaskentryright dst_negative_scale_earlier_resultmaskentryright dst_positive_earlier_resultmaskentryright dst_negative_earlier_resultmaskentryright. (((G) = (((((dst_positive_code_earlier_resultmaskentryright) + (dst_positive_scale_earlier_resultmaskentryright)) * S ((dst_positive_code_earlier_resultmaskentryright) + (dst_positive_scale_earlier_resultmaskentryright)) + ((dst_positive_scale_earlier_resultmaskentryright) + (dst_positive_scale_earlier_resultmaskentryright))) + (((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) * S ((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) + ((dst_negative_scale_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)))) * S ((((dst_positive_code_earlier_resultmaskentryright) + (dst_positive_scale_earlier_resultmaskentryright)) * S ((dst_positive_code_earlier_resultmaskentryright) + (dst_positive_scale_earlier_resultmaskentryright)) + ((dst_positive_scale_earlier_resultmaskentryright) + (dst_positive_scale_earlier_resultmaskentryright))) + (((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) * S ((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) + ((dst_negative_scale_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)))) + ((((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) * S ((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) + ((dst_negative_scale_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright))) + (((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) * S ((dst_negative_code_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)) + ((dst_negative_scale_earlier_resultmaskentryright) + (dst_negative_scale_earlier_resultmaskentryright)))))) /\ (((((exists ff_h_pvs_earlier_resultmaskentryrightpositive. ff_h_pvs_earlier_resultmaskentryrightpositive + S (dst_positive_earlier_resultmaskentryright) = S ((S (dc_quotient_earlier_resultmaskentry)) * dst_positive_scale_earlier_resultmaskentryright)) /\ exists ff_q_pvs_earlier_resultmaskentryrightpositive. dst_positive_code_earlier_resultmaskentryright = ff_q_pvs_earlier_resultmaskentryrightpositive * S ((S (dc_quotient_earlier_resultmaskentry)) * dst_positive_scale_earlier_resultmaskentryright) + (dst_positive_earlier_resultmaskentryright))) /\ (((((exists ff_h_pvs_earlier_resultmaskentryrightnegative. ff_h_pvs_earlier_resultmaskentryrightnegative + S (dst_negative_earlier_resultmaskentryright) = S ((S (dc_quotient_earlier_resultmaskentry)) * dst_negative_scale_earlier_resultmaskentryright)) /\ exists ff_q_pvs_earlier_resultmaskentryrightnegative. dst_negative_code_earlier_resultmaskentryright = ff_q_pvs_earlier_resultmaskentryrightnegative * S ((S (dc_quotient_earlier_resultmaskentry)) * dst_negative_scale_earlier_resultmaskentryright) + (dst_negative_earlier_resultmaskentryright))) /\ (exists ge_balance_positive_earlier_resultmaskentryrightvalue ge_balance_negative_earlier_resultmaskentryrightvalue. (((((dc_right_earlier_resultmaskentry) = 2 * (ge_balance_positive_earlier_resultmaskentryrightvalue) /\ (ge_balance_negative_earlier_resultmaskentryrightvalue) = 0) \/ exists ge_signed_half_earlier_resultmaskentryrightvaluedecode. (((dc_right_earlier_resultmaskentry) = 2 * ge_signed_half_earlier_resultmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_earlier_resultmaskentryrightvalue) = 0) /\ (ge_balance_negative_earlier_resultmaskentryrightvalue) = S ge_signed_half_earlier_resultmaskentryrightvaluedecode))) /\ ((dst_positive_earlier_resultmaskentryright) + ge_balance_negative_earlier_resultmaskentryrightvalue = (dst_negative_earlier_resultmaskentryright) + ge_balance_positive_earlier_resultmaskentryrightvalue))))))))) /\ (exists sto_ap_earlier_resultmaskentryproduct sto_an_earlier_resultmaskentryproduct sto_bp_earlier_resultmaskentryproduct sto_bn_earlier_resultmaskentryproduct sto_cp_earlier_resultmaskentryproduct sto_cn_earlier_resultmaskentryproduct. (((((dc_left_earlier_resultmaskentry) = 2 * (sto_ap_earlier_resultmaskentryproduct) /\ (sto_an_earlier_resultmaskentryproduct) = 0) \/ exists ge_signed_half_earlier_resultmaskentryproductleft. (((dc_left_earlier_resultmaskentry) = 2 * ge_signed_half_earlier_resultmaskentryproductleft + 1 /\ (sto_ap_earlier_resultmaskentryproduct) = 0) /\ (sto_an_earlier_resultmaskentryproduct) = S ge_signed_half_earlier_resultmaskentryproductleft))) /\ ((((((dc_right_earlier_resultmaskentry) = 2 * (sto_bp_earlier_resultmaskentryproduct) /\ (sto_bn_earlier_resultmaskentryproduct) = 0) \/ exists ge_signed_half_earlier_resultmaskentryproductright. (((dc_right_earlier_resultmaskentry) = 2 * ge_signed_half_earlier_resultmaskentryproductright + 1 /\ (sto_bp_earlier_resultmaskentryproduct) = 0) /\ (sto_bn_earlier_resultmaskentryproduct) = S ge_signed_half_earlier_resultmaskentryproductright))) /\ ((((((dc_value_earlier_resultmask) = 2 * (sto_cp_earlier_resultmaskentryproduct) /\ (sto_cn_earlier_resultmaskentryproduct) = 0) \/ exists ge_signed_half_earlier_resultmaskentryproductoutput. (((dc_value_earlier_resultmask) = 2 * ge_signed_half_earlier_resultmaskentryproductoutput + 1 /\ (sto_cp_earlier_resultmaskentryproduct) = 0) /\ (sto_cn_earlier_resultmaskentryproduct) = S ge_signed_half_earlier_resultmaskentryproductoutput))) /\ ((sto_ap_earlier_resultmaskentryproduct * sto_bp_earlier_resultmaskentryproduct + sto_an_earlier_resultmaskentryproduct * sto_bn_earlier_resultmaskentryproduct) + sto_cn_earlier_resultmaskentryproduct = (sto_ap_earlier_resultmaskentryproduct * sto_bn_earlier_resultmaskentryproduct + sto_an_earlier_resultmaskentryproduct * sto_bp_earlier_resultmaskentryproduct) + sto_cp_earlier_resultmaskentryproduct))))))))))))))) \/ ((((dc_index_earlier_resultmask)=0 \/ ~(exists pvs_factor_earlier_resultmaskentrynondivisor. (m) = (dc_index_earlier_resultmask) * pvs_factor_earlier_resultmaskentrynondivisor)) /\ ((dc_value_earlier_resultmask)=0))))))) /\ (exists dst_positive_code_earlier_resultfold dst_positive_scale_earlier_resultfold dst_negative_code_earlier_resultfold dst_negative_scale_earlier_resultfold dst_positive_sum_earlier_resultfold dst_negative_sum_earlier_resultfold. (((dc_mask_earlier_result) = (((((dst_positive_code_earlier_resultfold) + (dst_positive_scale_earlier_resultfold)) * S ((dst_positive_code_earlier_resultfold) + (dst_positive_scale_earlier_resultfold)) + ((dst_positive_scale_earlier_resultfold) + (dst_positive_scale_earlier_resultfold))) + (((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) * S ((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) + ((dst_negative_scale_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)))) * S ((((dst_positive_code_earlier_resultfold) + (dst_positive_scale_earlier_resultfold)) * S ((dst_positive_code_earlier_resultfold) + (dst_positive_scale_earlier_resultfold)) + ((dst_positive_scale_earlier_resultfold) + (dst_positive_scale_earlier_resultfold))) + (((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) * S ((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) + ((dst_negative_scale_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)))) + ((((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) * S ((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) + ((dst_negative_scale_earlier_resultfold) + (dst_negative_scale_earlier_resultfold))) + (((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) * S ((dst_negative_code_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)) + ((dst_negative_scale_earlier_resultfold) + (dst_negative_scale_earlier_resultfold)))))) /\ (((exists fs_u_dst_earlier_resultfoldpositive fs_v_dst_earlier_resultfoldpositive. ((((exists fs_h_dst_earlier_resultfoldpositive_body_start. fs_h_dst_earlier_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_earlier_resultfoldpositive)) /\ exists fs_q_dst_earlier_resultfoldpositive_body_start. fs_u_dst_earlier_resultfoldpositive = fs_q_dst_earlier_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_earlier_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_earlier_resultfoldpositive_body_terminal. fs_h_dst_earlier_resultfoldpositive_body_terminal + S (dst_positive_sum_earlier_resultfold) = S ((S (S (m))) * fs_v_dst_earlier_resultfoldpositive)) /\ exists fs_q_dst_earlier_resultfoldpositive_body_terminal. fs_u_dst_earlier_resultfoldpositive = fs_q_dst_earlier_resultfoldpositive_body_terminal * S ((S (S (m))) * fs_v_dst_earlier_resultfoldpositive) + (dst_positive_sum_earlier_resultfold))) /\ forall fs_i_dst_earlier_resultfoldpositive_body_steps. (exists fs_lt_dst_earlier_resultfoldpositive_body_steps_bound. fs_lt_dst_earlier_resultfoldpositive_body_steps_bound + S fs_i_dst_earlier_resultfoldpositive_body_steps = S (m)) -> exists fs_a_dst_earlier_resultfoldpositive_body_steps fs_r_dst_earlier_resultfoldpositive_body_steps fs_s_dst_earlier_resultfoldpositive_body_steps. ((((exists fs_h_dst_earlier_resultfoldpositive_body_steps_summand. fs_h_dst_earlier_resultfoldpositive_body_steps_summand + S (fs_a_dst_earlier_resultfoldpositive_body_steps) = S ((S (fs_i_dst_earlier_resultfoldpositive_body_steps)) * dst_positive_scale_earlier_resultfold)) /\ exists fs_q_dst_earlier_resultfoldpositive_body_steps_summand. dst_positive_code_earlier_resultfold = fs_q_dst_earlier_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_earlier_resultfoldpositive_body_steps)) * dst_positive_scale_earlier_resultfold) + (fs_a_dst_earlier_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_earlier_resultfoldpositive_body_steps_partial. fs_h_dst_earlier_resultfoldpositive_body_steps_partial + S (fs_r_dst_earlier_resultfoldpositive_body_steps) = S ((S (fs_i_dst_earlier_resultfoldpositive_body_steps)) * fs_v_dst_earlier_resultfoldpositive)) /\ exists fs_q_dst_earlier_resultfoldpositive_body_steps_partial. fs_u_dst_earlier_resultfoldpositive = fs_q_dst_earlier_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_earlier_resultfoldpositive_body_steps)) * fs_v_dst_earlier_resultfoldpositive) + (fs_r_dst_earlier_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_earlier_resultfoldpositive_body_steps_successor. fs_h_dst_earlier_resultfoldpositive_body_steps_successor + S (fs_s_dst_earlier_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_earlier_resultfoldpositive_body_steps)) * fs_v_dst_earlier_resultfoldpositive)) /\ exists fs_q_dst_earlier_resultfoldpositive_body_steps_successor. fs_u_dst_earlier_resultfoldpositive = fs_q_dst_earlier_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_earlier_resultfoldpositive_body_steps)) * fs_v_dst_earlier_resultfoldpositive) + (fs_s_dst_earlier_resultfoldpositive_body_steps))) /\ fs_s_dst_earlier_resultfoldpositive_body_steps = fs_r_dst_earlier_resultfoldpositive_body_steps + fs_a_dst_earlier_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_earlier_resultfoldnegative fs_v_dst_earlier_resultfoldnegative. ((((exists fs_h_dst_earlier_resultfoldnegative_body_start. fs_h_dst_earlier_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_earlier_resultfoldnegative)) /\ exists fs_q_dst_earlier_resultfoldnegative_body_start. fs_u_dst_earlier_resultfoldnegative = fs_q_dst_earlier_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_earlier_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_earlier_resultfoldnegative_body_terminal. fs_h_dst_earlier_resultfoldnegative_body_terminal + S (dst_negative_sum_earlier_resultfold) = S ((S (S (m))) * fs_v_dst_earlier_resultfoldnegative)) /\ exists fs_q_dst_earlier_resultfoldnegative_body_terminal. fs_u_dst_earlier_resultfoldnegative = fs_q_dst_earlier_resultfoldnegative_body_terminal * S ((S (S (m))) * fs_v_dst_earlier_resultfoldnegative) + (dst_negative_sum_earlier_resultfold))) /\ forall fs_i_dst_earlier_resultfoldnegative_body_steps. (exists fs_lt_dst_earlier_resultfoldnegative_body_steps_bound. fs_lt_dst_earlier_resultfoldnegative_body_steps_bound + S fs_i_dst_earlier_resultfoldnegative_body_steps = S (m)) -> exists fs_a_dst_earlier_resultfoldnegative_body_steps fs_r_dst_earlier_resultfoldnegative_body_steps fs_s_dst_earlier_resultfoldnegative_body_steps. ((((exists fs_h_dst_earlier_resultfoldnegative_body_steps_summand. fs_h_dst_earlier_resultfoldnegative_body_steps_summand + S (fs_a_dst_earlier_resultfoldnegative_body_steps) = S ((S (fs_i_dst_earlier_resultfoldnegative_body_steps)) * dst_negative_scale_earlier_resultfold)) /\ exists fs_q_dst_earlier_resultfoldnegative_body_steps_summand. dst_negative_code_earlier_resultfold = fs_q_dst_earlier_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_earlier_resultfoldnegative_body_steps)) * dst_negative_scale_earlier_resultfold) + (fs_a_dst_earlier_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_earlier_resultfoldnegative_body_steps_partial. fs_h_dst_earlier_resultfoldnegative_body_steps_partial + S (fs_r_dst_earlier_resultfoldnegative_body_steps) = S ((S (fs_i_dst_earlier_resultfoldnegative_body_steps)) * fs_v_dst_earlier_resultfoldnegative)) /\ exists fs_q_dst_earlier_resultfoldnegative_body_steps_partial. fs_u_dst_earlier_resultfoldnegative = fs_q_dst_earlier_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_earlier_resultfoldnegative_body_steps)) * fs_v_dst_earlier_resultfoldnegative) + (fs_r_dst_earlier_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_earlier_resultfoldnegative_body_steps_successor. fs_h_dst_earlier_resultfoldnegative_body_steps_successor + S (fs_s_dst_earlier_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_earlier_resultfoldnegative_body_steps)) * fs_v_dst_earlier_resultfoldnegative)) /\ exists fs_q_dst_earlier_resultfoldnegative_body_steps_successor. fs_u_dst_earlier_resultfoldnegative = fs_q_dst_earlier_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_earlier_resultfoldnegative_body_steps)) * fs_v_dst_earlier_resultfoldnegative) + (fs_s_dst_earlier_resultfoldnegative_body_steps))) /\ fs_s_dst_earlier_resultfoldnegative_body_steps = fs_r_dst_earlier_resultfoldnegative_body_steps + fs_a_dst_earlier_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_earlier_resultfoldresult ge_balance_negative_earlier_resultfoldresult. (((((z) = 2 * (ge_balance_positive_earlier_resultfoldresult) /\ (ge_balance_negative_earlier_resultfoldresult) = 0) \/ exists ge_signed_half_earlier_resultfoldresultdecode. (((z) = 2 * ge_signed_half_earlier_resultfoldresultdecode + 1 /\ (ge_balance_positive_earlier_resultfoldresult) = 0) /\ (ge_balance_negative_earlier_resultfoldresult) = S ge_signed_half_earlier_resultfoldresultdecode))) /\ ((dst_positive_sum_earlier_resultfold) + ge_balance_negative_earlier_resultfoldresult = (dst_negative_sum_earlier_resultfold) + ge_balance_positive_earlier_resultfoldresult)))))))))))))