dirichlet_convolution_positive_source_extensional

forall F G H K n a b. (forall dm_index_sum_source_left dm_first_value_sum_source_left dm_second_value_sum_source_left. ~(dm_index_sum_source_left=0) -> (exists pvs_le_gap_sum_source_leftdomain. pvs_le_gap_sum_source_leftdomain + (dm_index_sum_source_left) = (n)) -> (exists dst_positive_code_sum_source_leftfirst dst_positive_scale_sum_source_leftfirst dst_negative_code_sum_source_leftfirst dst_negative_scale_sum_source_leftfirst dst_positive_sum_source_leftfirst dst_negative_sum_source_leftfirst. (((F) = (((((dst_positive_code_sum_source_leftfirst) + (dst_positive_scale_sum_source_leftfirst)) * S ((dst_positive_code_sum_source_leftfirst) + (dst_positive_scale_sum_source_leftfirst)) + ((dst_positive_scale_sum_source_leftfirst) + (dst_positive_scale_sum_source_leftfirst))) + (((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) * S ((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) + ((dst_negative_scale_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)))) * S ((((dst_positive_code_sum_source_leftfirst) + (dst_positive_scale_sum_source_leftfirst)) * S ((dst_positive_code_sum_source_leftfirst) + (dst_positive_scale_sum_source_leftfirst)) + ((dst_positive_scale_sum_source_leftfirst) + (dst_positive_scale_sum_source_leftfirst))) + (((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) * S ((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) + ((dst_negative_scale_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)))) + ((((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) * S ((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) + ((dst_negative_scale_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst))) + (((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) * S ((dst_negative_code_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)) + ((dst_negative_scale_sum_source_leftfirst) + (dst_negative_scale_sum_source_leftfirst)))))) /\ (((((exists ff_h_pvs_sum_source_leftfirstpositive. ff_h_pvs_sum_source_leftfirstpositive + S (dst_positive_sum_source_leftfirst) = S ((S (dm_index_sum_source_left)) * dst_positive_scale_sum_source_leftfirst)) /\ exists ff_q_pvs_sum_source_leftfirstpositive. dst_positive_code_sum_source_leftfirst = ff_q_pvs_sum_source_leftfirstpositive * S ((S (dm_index_sum_source_left)) * dst_positive_scale_sum_source_leftfirst) + (dst_positive_sum_source_leftfirst))) /\ (((((exists ff_h_pvs_sum_source_leftfirstnegative. ff_h_pvs_sum_source_leftfirstnegative + S (dst_negative_sum_source_leftfirst) = S ((S (dm_index_sum_source_left)) * dst_negative_scale_sum_source_leftfirst)) /\ exists ff_q_pvs_sum_source_leftfirstnegative. dst_negative_code_sum_source_leftfirst = ff_q_pvs_sum_source_leftfirstnegative * S ((S (dm_index_sum_source_left)) * dst_negative_scale_sum_source_leftfirst) + (dst_negative_sum_source_leftfirst))) /\ (exists ge_balance_positive_sum_source_leftfirstvalue ge_balance_negative_sum_source_leftfirstvalue. (((((dm_first_value_sum_source_left) = 2 * (ge_balance_positive_sum_source_leftfirstvalue) /\ (ge_balance_negative_sum_source_leftfirstvalue) = 0) \/ exists ge_signed_half_sum_source_leftfirstvaluedecode. (((dm_first_value_sum_source_left) = 2 * ge_signed_half_sum_source_leftfirstvaluedecode + 1 /\ (ge_balance_positive_sum_source_leftfirstvalue) = 0) /\ (ge_balance_negative_sum_source_leftfirstvalue) = S ge_signed_half_sum_source_leftfirstvaluedecode))) /\ ((dst_positive_sum_source_leftfirst) + ge_balance_negative_sum_source_leftfirstvalue = (dst_negative_sum_source_leftfirst) + ge_balance_positive_sum_source_leftfirstvalue))))))))) -> (exists dst_positive_code_sum_source_leftsecond dst_positive_scale_sum_source_leftsecond dst_negative_code_sum_source_leftsecond dst_negative_scale_sum_source_leftsecond dst_positive_sum_source_leftsecond dst_negative_sum_source_leftsecond. (((H) = (((((dst_positive_code_sum_source_leftsecond) + (dst_positive_scale_sum_source_leftsecond)) * S ((dst_positive_code_sum_source_leftsecond) + (dst_positive_scale_sum_source_leftsecond)) + ((dst_positive_scale_sum_source_leftsecond) + (dst_positive_scale_sum_source_leftsecond))) + (((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) * S ((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) + ((dst_negative_scale_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)))) * S ((((dst_positive_code_sum_source_leftsecond) + (dst_positive_scale_sum_source_leftsecond)) * S ((dst_positive_code_sum_source_leftsecond) + (dst_positive_scale_sum_source_leftsecond)) + ((dst_positive_scale_sum_source_leftsecond) + (dst_positive_scale_sum_source_leftsecond))) + (((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) * S ((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) + ((dst_negative_scale_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)))) + ((((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) * S ((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) + ((dst_negative_scale_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond))) + (((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) * S ((dst_negative_code_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)) + ((dst_negative_scale_sum_source_leftsecond) + (dst_negative_scale_sum_source_leftsecond)))))) /\ (((((exists ff_h_pvs_sum_source_leftsecondpositive. ff_h_pvs_sum_source_leftsecondpositive + S (dst_positive_sum_source_leftsecond) = S ((S (dm_index_sum_source_left)) * dst_positive_scale_sum_source_leftsecond)) /\ exists ff_q_pvs_sum_source_leftsecondpositive. dst_positive_code_sum_source_leftsecond = ff_q_pvs_sum_source_leftsecondpositive * S ((S (dm_index_sum_source_left)) * dst_positive_scale_sum_source_leftsecond) + (dst_positive_sum_source_leftsecond))) /\ (((((exists ff_h_pvs_sum_source_leftsecondnegative. ff_h_pvs_sum_source_leftsecondnegative + S (dst_negative_sum_source_leftsecond) = S ((S (dm_index_sum_source_left)) * dst_negative_scale_sum_source_leftsecond)) /\ exists ff_q_pvs_sum_source_leftsecondnegative. dst_negative_code_sum_source_leftsecond = ff_q_pvs_sum_source_leftsecondnegative * S ((S (dm_index_sum_source_left)) * dst_negative_scale_sum_source_leftsecond) + (dst_negative_sum_source_leftsecond))) /\ (exists ge_balance_positive_sum_source_leftsecondvalue ge_balance_negative_sum_source_leftsecondvalue. (((((dm_second_value_sum_source_left) = 2 * (ge_balance_positive_sum_source_leftsecondvalue) /\ (ge_balance_negative_sum_source_leftsecondvalue) = 0) \/ exists ge_signed_half_sum_source_leftsecondvaluedecode. (((dm_second_value_sum_source_left) = 2 * ge_signed_half_sum_source_leftsecondvaluedecode + 1 /\ (ge_balance_positive_sum_source_leftsecondvalue) = 0) /\ (ge_balance_negative_sum_source_leftsecondvalue) = S ge_signed_half_sum_source_leftsecondvaluedecode))) /\ ((dst_positive_sum_source_leftsecond) + ge_balance_negative_sum_source_leftsecondvalue = (dst_negative_sum_source_leftsecond) + ge_balance_positive_sum_source_leftsecondvalue))))))))) -> dm_first_value_sum_source_left=dm_second_value_sum_source_left) -> (forall dm_index_sum_source_right dm_first_value_sum_source_right dm_second_value_sum_source_right. ~(dm_index_sum_source_right=0) -> (exists pvs_le_gap_sum_source_rightdomain. pvs_le_gap_sum_source_rightdomain + (dm_index_sum_source_right) = (n)) -> (exists dst_positive_code_sum_source_rightfirst dst_positive_scale_sum_source_rightfirst dst_negative_code_sum_source_rightfirst dst_negative_scale_sum_source_rightfirst dst_positive_sum_source_rightfirst dst_negative_sum_source_rightfirst. (((G) = (((((dst_positive_code_sum_source_rightfirst) + (dst_positive_scale_sum_source_rightfirst)) * S ((dst_positive_code_sum_source_rightfirst) + (dst_positive_scale_sum_source_rightfirst)) + ((dst_positive_scale_sum_source_rightfirst) + (dst_positive_scale_sum_source_rightfirst))) + (((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) * S ((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) + ((dst_negative_scale_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)))) * S ((((dst_positive_code_sum_source_rightfirst) + (dst_positive_scale_sum_source_rightfirst)) * S ((dst_positive_code_sum_source_rightfirst) + (dst_positive_scale_sum_source_rightfirst)) + ((dst_positive_scale_sum_source_rightfirst) + (dst_positive_scale_sum_source_rightfirst))) + (((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) * S ((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) + ((dst_negative_scale_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)))) + ((((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) * S ((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) + ((dst_negative_scale_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst))) + (((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) * S ((dst_negative_code_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)) + ((dst_negative_scale_sum_source_rightfirst) + (dst_negative_scale_sum_source_rightfirst)))))) /\ (((((exists ff_h_pvs_sum_source_rightfirstpositive. ff_h_pvs_sum_source_rightfirstpositive + S (dst_positive_sum_source_rightfirst) = S ((S (dm_index_sum_source_right)) * dst_positive_scale_sum_source_rightfirst)) /\ exists ff_q_pvs_sum_source_rightfirstpositive. dst_positive_code_sum_source_rightfirst = ff_q_pvs_sum_source_rightfirstpositive * S ((S (dm_index_sum_source_right)) * dst_positive_scale_sum_source_rightfirst) + (dst_positive_sum_source_rightfirst))) /\ (((((exists ff_h_pvs_sum_source_rightfirstnegative. ff_h_pvs_sum_source_rightfirstnegative + S (dst_negative_sum_source_rightfirst) = S ((S (dm_index_sum_source_right)) * dst_negative_scale_sum_source_rightfirst)) /\ exists ff_q_pvs_sum_source_rightfirstnegative. dst_negative_code_sum_source_rightfirst = ff_q_pvs_sum_source_rightfirstnegative * S ((S (dm_index_sum_source_right)) * dst_negative_scale_sum_source_rightfirst) + (dst_negative_sum_source_rightfirst))) /\ (exists ge_balance_positive_sum_source_rightfirstvalue ge_balance_negative_sum_source_rightfirstvalue. (((((dm_first_value_sum_source_right) = 2 * (ge_balance_positive_sum_source_rightfirstvalue) /\ (ge_balance_negative_sum_source_rightfirstvalue) = 0) \/ exists ge_signed_half_sum_source_rightfirstvaluedecode. (((dm_first_value_sum_source_right) = 2 * ge_signed_half_sum_source_rightfirstvaluedecode + 1 /\ (ge_balance_positive_sum_source_rightfirstvalue) = 0) /\ (ge_balance_negative_sum_source_rightfirstvalue) = S ge_signed_half_sum_source_rightfirstvaluedecode))) /\ ((dst_positive_sum_source_rightfirst) + ge_balance_negative_sum_source_rightfirstvalue = (dst_negative_sum_source_rightfirst) + ge_balance_positive_sum_source_rightfirstvalue))))))))) -> (exists dst_positive_code_sum_source_rightsecond dst_positive_scale_sum_source_rightsecond dst_negative_code_sum_source_rightsecond dst_negative_scale_sum_source_rightsecond dst_positive_sum_source_rightsecond dst_negative_sum_source_rightsecond. (((K) = (((((dst_positive_code_sum_source_rightsecond) + (dst_positive_scale_sum_source_rightsecond)) * S ((dst_positive_code_sum_source_rightsecond) + (dst_positive_scale_sum_source_rightsecond)) + ((dst_positive_scale_sum_source_rightsecond) + (dst_positive_scale_sum_source_rightsecond))) + (((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) * S ((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) + ((dst_negative_scale_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)))) * S ((((dst_positive_code_sum_source_rightsecond) + (dst_positive_scale_sum_source_rightsecond)) * S ((dst_positive_code_sum_source_rightsecond) + (dst_positive_scale_sum_source_rightsecond)) + ((dst_positive_scale_sum_source_rightsecond) + (dst_positive_scale_sum_source_rightsecond))) + (((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) * S ((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) + ((dst_negative_scale_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)))) + ((((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) * S ((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) + ((dst_negative_scale_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond))) + (((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) * S ((dst_negative_code_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)) + ((dst_negative_scale_sum_source_rightsecond) + (dst_negative_scale_sum_source_rightsecond)))))) /\ (((((exists ff_h_pvs_sum_source_rightsecondpositive. ff_h_pvs_sum_source_rightsecondpositive + S (dst_positive_sum_source_rightsecond) = S ((S (dm_index_sum_source_right)) * dst_positive_scale_sum_source_rightsecond)) /\ exists ff_q_pvs_sum_source_rightsecondpositive. dst_positive_code_sum_source_rightsecond = ff_q_pvs_sum_source_rightsecondpositive * S ((S (dm_index_sum_source_right)) * dst_positive_scale_sum_source_rightsecond) + (dst_positive_sum_source_rightsecond))) /\ (((((exists ff_h_pvs_sum_source_rightsecondnegative. ff_h_pvs_sum_source_rightsecondnegative + S (dst_negative_sum_source_rightsecond) = S ((S (dm_index_sum_source_right)) * dst_negative_scale_sum_source_rightsecond)) /\ exists ff_q_pvs_sum_source_rightsecondnegative. dst_negative_code_sum_source_rightsecond = ff_q_pvs_sum_source_rightsecondnegative * S ((S (dm_index_sum_source_right)) * dst_negative_scale_sum_source_rightsecond) + (dst_negative_sum_source_rightsecond))) /\ (exists ge_balance_positive_sum_source_rightsecondvalue ge_balance_negative_sum_source_rightsecondvalue. (((((dm_second_value_sum_source_right) = 2 * (ge_balance_positive_sum_source_rightsecondvalue) /\ (ge_balance_negative_sum_source_rightsecondvalue) = 0) \/ exists ge_signed_half_sum_source_rightsecondvaluedecode. (((dm_second_value_sum_source_right) = 2 * ge_signed_half_sum_source_rightsecondvaluedecode + 1 /\ (ge_balance_positive_sum_source_rightsecondvalue) = 0) /\ (ge_balance_negative_sum_source_rightsecondvalue) = S ge_signed_half_sum_source_rightsecondvaluedecode))) /\ ((dst_positive_sum_source_rightsecond) + ge_balance_negative_sum_source_rightsecondvalue = (dst_negative_sum_source_rightsecond) + ge_balance_positive_sum_source_rightsecondvalue))))))))) -> dm_first_value_sum_source_right=dm_second_value_sum_source_right) -> (((~((n)=0)) /\ (exists dc_mask_sum_source_first. ((((exists dst_positive_code_sum_source_firstmasktable dst_positive_scale_sum_source_firstmasktable dst_negative_code_sum_source_firstmasktable dst_negative_scale_sum_source_firstmasktable. (((dc_mask_sum_source_first) = (((((dst_positive_code_sum_source_firstmasktable) + (dst_positive_scale_sum_source_firstmasktable)) * S ((dst_positive_code_sum_source_firstmasktable) + (dst_positive_scale_sum_source_firstmasktable)) + ((dst_positive_scale_sum_source_firstmasktable) + (dst_positive_scale_sum_source_firstmasktable))) + (((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) * S ((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) + ((dst_negative_scale_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)))) * S ((((dst_positive_code_sum_source_firstmasktable) + (dst_positive_scale_sum_source_firstmasktable)) * S ((dst_positive_code_sum_source_firstmasktable) + (dst_positive_scale_sum_source_firstmasktable)) + ((dst_positive_scale_sum_source_firstmasktable) + (dst_positive_scale_sum_source_firstmasktable))) + (((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) * S ((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) + ((dst_negative_scale_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)))) + ((((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) * S ((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) + ((dst_negative_scale_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable))) + (((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) * S ((dst_negative_code_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)) + ((dst_negative_scale_sum_source_firstmasktable) + (dst_negative_scale_sum_source_firstmasktable)))))) /\ (forall dst_index_sum_source_firstmasktable. (exists pvs_le_gap_sum_source_firstmasktabledomain. pvs_le_gap_sum_source_firstmasktabledomain + (dst_index_sum_source_firstmasktable) = (n)) -> exists dst_positive_sum_source_firstmasktable dst_negative_sum_source_firstmasktable dst_value_sum_source_firstmasktable. ((((exists ff_h_pvs_sum_source_firstmasktableentrypositive. ff_h_pvs_sum_source_firstmasktableentrypositive + S (dst_positive_sum_source_firstmasktable) = S ((S (dst_index_sum_source_firstmasktable)) * dst_positive_scale_sum_source_firstmasktable)) /\ exists ff_q_pvs_sum_source_firstmasktableentrypositive. dst_positive_code_sum_source_firstmasktable = ff_q_pvs_sum_source_firstmasktableentrypositive * S ((S (dst_index_sum_source_firstmasktable)) * dst_positive_scale_sum_source_firstmasktable) + (dst_positive_sum_source_firstmasktable))) /\ (((((exists ff_h_pvs_sum_source_firstmasktableentrynegative. ff_h_pvs_sum_source_firstmasktableentrynegative + S (dst_negative_sum_source_firstmasktable) = S ((S (dst_index_sum_source_firstmasktable)) * dst_negative_scale_sum_source_firstmasktable)) /\ exists ff_q_pvs_sum_source_firstmasktableentrynegative. dst_negative_code_sum_source_firstmasktable = ff_q_pvs_sum_source_firstmasktableentrynegative * S ((S (dst_index_sum_source_firstmasktable)) * dst_negative_scale_sum_source_firstmasktable) + (dst_negative_sum_source_firstmasktable))) /\ (exists ge_balance_positive_sum_source_firstmasktableentryvalue ge_balance_negative_sum_source_firstmasktableentryvalue. (((((dst_value_sum_source_firstmasktable) = 2 * (ge_balance_positive_sum_source_firstmasktableentryvalue) /\ (ge_balance_negative_sum_source_firstmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_source_firstmasktableentryvaluedecode. (((dst_value_sum_source_firstmasktable) = 2 * ge_signed_half_sum_source_firstmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_source_firstmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_source_firstmasktableentryvalue) = S ge_signed_half_sum_source_firstmasktableentryvaluedecode))) /\ ((dst_positive_sum_source_firstmasktable) + ge_balance_negative_sum_source_firstmasktableentryvalue = (dst_negative_sum_source_firstmasktable) + ge_balance_positive_sum_source_firstmasktableentryvalue))))))))) /\ (forall dc_index_sum_source_firstmask dc_value_sum_source_firstmask. (exists pvs_le_gap_sum_source_firstmaskdomain. pvs_le_gap_sum_source_firstmaskdomain + (dc_index_sum_source_firstmask) = (n)) -> (exists dst_positive_code_sum_source_firstmasklookup dst_positive_scale_sum_source_firstmasklookup dst_negative_code_sum_source_firstmasklookup dst_negative_scale_sum_source_firstmasklookup dst_positive_sum_source_firstmasklookup dst_negative_sum_source_firstmasklookup. (((dc_mask_sum_source_first) = (((((dst_positive_code_sum_source_firstmasklookup) + (dst_positive_scale_sum_source_firstmasklookup)) * S ((dst_positive_code_sum_source_firstmasklookup) + (dst_positive_scale_sum_source_firstmasklookup)) + ((dst_positive_scale_sum_source_firstmasklookup) + (dst_positive_scale_sum_source_firstmasklookup))) + (((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) * S ((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) + ((dst_negative_scale_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)))) * S ((((dst_positive_code_sum_source_firstmasklookup) + (dst_positive_scale_sum_source_firstmasklookup)) * S ((dst_positive_code_sum_source_firstmasklookup) + (dst_positive_scale_sum_source_firstmasklookup)) + ((dst_positive_scale_sum_source_firstmasklookup) + (dst_positive_scale_sum_source_firstmasklookup))) + (((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) * S ((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) + ((dst_negative_scale_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)))) + ((((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) * S ((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) + ((dst_negative_scale_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup))) + (((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) * S ((dst_negative_code_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)) + ((dst_negative_scale_sum_source_firstmasklookup) + (dst_negative_scale_sum_source_firstmasklookup)))))) /\ (((((exists ff_h_pvs_sum_source_firstmasklookuppositive. ff_h_pvs_sum_source_firstmasklookuppositive + S (dst_positive_sum_source_firstmasklookup) = S ((S (dc_index_sum_source_firstmask)) * dst_positive_scale_sum_source_firstmasklookup)) /\ exists ff_q_pvs_sum_source_firstmasklookuppositive. dst_positive_code_sum_source_firstmasklookup = ff_q_pvs_sum_source_firstmasklookuppositive * S ((S (dc_index_sum_source_firstmask)) * dst_positive_scale_sum_source_firstmasklookup) + (dst_positive_sum_source_firstmasklookup))) /\ (((((exists ff_h_pvs_sum_source_firstmasklookupnegative. ff_h_pvs_sum_source_firstmasklookupnegative + S (dst_negative_sum_source_firstmasklookup) = S ((S (dc_index_sum_source_firstmask)) * dst_negative_scale_sum_source_firstmasklookup)) /\ exists ff_q_pvs_sum_source_firstmasklookupnegative. dst_negative_code_sum_source_firstmasklookup = ff_q_pvs_sum_source_firstmasklookupnegative * S ((S (dc_index_sum_source_firstmask)) * dst_negative_scale_sum_source_firstmasklookup) + (dst_negative_sum_source_firstmasklookup))) /\ (exists ge_balance_positive_sum_source_firstmasklookupvalue ge_balance_negative_sum_source_firstmasklookupvalue. (((((dc_value_sum_source_firstmask) = 2 * (ge_balance_positive_sum_source_firstmasklookupvalue) /\ (ge_balance_negative_sum_source_firstmasklookupvalue) = 0) \/ exists ge_signed_half_sum_source_firstmasklookupvaluedecode. (((dc_value_sum_source_firstmask) = 2 * ge_signed_half_sum_source_firstmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_source_firstmasklookupvalue) = 0) /\ (ge_balance_negative_sum_source_firstmasklookupvalue) = S ge_signed_half_sum_source_firstmasklookupvaluedecode))) /\ ((dst_positive_sum_source_firstmasklookup) + ge_balance_negative_sum_source_firstmasklookupvalue = (dst_negative_sum_source_firstmasklookup) + ge_balance_positive_sum_source_firstmasklookupvalue))))))))) -> ((((~((dc_index_sum_source_firstmask)=0)) /\ (exists dc_quotient_sum_source_firstmaskentry dc_left_sum_source_firstmaskentry dc_right_sum_source_firstmaskentry. (((n)=(dc_index_sum_source_firstmask)*dc_quotient_sum_source_firstmaskentry) /\ (((exists dst_positive_code_sum_source_firstmaskentryleft dst_positive_scale_sum_source_firstmaskentryleft dst_negative_code_sum_source_firstmaskentryleft dst_negative_scale_sum_source_firstmaskentryleft dst_positive_sum_source_firstmaskentryleft dst_negative_sum_source_firstmaskentryleft. (((F) = (((((dst_positive_code_sum_source_firstmaskentryleft) + (dst_positive_scale_sum_source_firstmaskentryleft)) * S ((dst_positive_code_sum_source_firstmaskentryleft) + (dst_positive_scale_sum_source_firstmaskentryleft)) + ((dst_positive_scale_sum_source_firstmaskentryleft) + (dst_positive_scale_sum_source_firstmaskentryleft))) + (((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) * S ((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) + ((dst_negative_scale_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)))) * S ((((dst_positive_code_sum_source_firstmaskentryleft) + (dst_positive_scale_sum_source_firstmaskentryleft)) * S ((dst_positive_code_sum_source_firstmaskentryleft) + (dst_positive_scale_sum_source_firstmaskentryleft)) + ((dst_positive_scale_sum_source_firstmaskentryleft) + (dst_positive_scale_sum_source_firstmaskentryleft))) + (((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) * S ((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) + ((dst_negative_scale_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)))) + ((((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) * S ((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) + ((dst_negative_scale_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft))) + (((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) * S ((dst_negative_code_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)) + ((dst_negative_scale_sum_source_firstmaskentryleft) + (dst_negative_scale_sum_source_firstmaskentryleft)))))) /\ (((((exists ff_h_pvs_sum_source_firstmaskentryleftpositive. ff_h_pvs_sum_source_firstmaskentryleftpositive + S (dst_positive_sum_source_firstmaskentryleft) = S ((S (dc_index_sum_source_firstmask)) * dst_positive_scale_sum_source_firstmaskentryleft)) /\ exists ff_q_pvs_sum_source_firstmaskentryleftpositive. dst_positive_code_sum_source_firstmaskentryleft = ff_q_pvs_sum_source_firstmaskentryleftpositive * S ((S (dc_index_sum_source_firstmask)) * dst_positive_scale_sum_source_firstmaskentryleft) + (dst_positive_sum_source_firstmaskentryleft))) /\ (((((exists ff_h_pvs_sum_source_firstmaskentryleftnegative. ff_h_pvs_sum_source_firstmaskentryleftnegative + S (dst_negative_sum_source_firstmaskentryleft) = S ((S (dc_index_sum_source_firstmask)) * dst_negative_scale_sum_source_firstmaskentryleft)) /\ exists ff_q_pvs_sum_source_firstmaskentryleftnegative. dst_negative_code_sum_source_firstmaskentryleft = ff_q_pvs_sum_source_firstmaskentryleftnegative * S ((S (dc_index_sum_source_firstmask)) * dst_negative_scale_sum_source_firstmaskentryleft) + (dst_negative_sum_source_firstmaskentryleft))) /\ (exists ge_balance_positive_sum_source_firstmaskentryleftvalue ge_balance_negative_sum_source_firstmaskentryleftvalue. (((((dc_left_sum_source_firstmaskentry) = 2 * (ge_balance_positive_sum_source_firstmaskentryleftvalue) /\ (ge_balance_negative_sum_source_firstmaskentryleftvalue) = 0) \/ exists ge_signed_half_sum_source_firstmaskentryleftvaluedecode. (((dc_left_sum_source_firstmaskentry) = 2 * ge_signed_half_sum_source_firstmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_source_firstmaskentryleftvalue) = 0) /\ (ge_balance_negative_sum_source_firstmaskentryleftvalue) = S ge_signed_half_sum_source_firstmaskentryleftvaluedecode))) /\ ((dst_positive_sum_source_firstmaskentryleft) + ge_balance_negative_sum_source_firstmaskentryleftvalue = (dst_negative_sum_source_firstmaskentryleft) + ge_balance_positive_sum_source_firstmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_source_firstmaskentryright dst_positive_scale_sum_source_firstmaskentryright dst_negative_code_sum_source_firstmaskentryright dst_negative_scale_sum_source_firstmaskentryright dst_positive_sum_source_firstmaskentryright dst_negative_sum_source_firstmaskentryright. (((G) = (((((dst_positive_code_sum_source_firstmaskentryright) + (dst_positive_scale_sum_source_firstmaskentryright)) * S ((dst_positive_code_sum_source_firstmaskentryright) + (dst_positive_scale_sum_source_firstmaskentryright)) + ((dst_positive_scale_sum_source_firstmaskentryright) + (dst_positive_scale_sum_source_firstmaskentryright))) + (((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) * S ((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) + ((dst_negative_scale_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)))) * S ((((dst_positive_code_sum_source_firstmaskentryright) + (dst_positive_scale_sum_source_firstmaskentryright)) * S ((dst_positive_code_sum_source_firstmaskentryright) + (dst_positive_scale_sum_source_firstmaskentryright)) + ((dst_positive_scale_sum_source_firstmaskentryright) + (dst_positive_scale_sum_source_firstmaskentryright))) + (((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) * S ((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) + ((dst_negative_scale_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)))) + ((((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) * S ((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) + ((dst_negative_scale_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright))) + (((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) * S ((dst_negative_code_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)) + ((dst_negative_scale_sum_source_firstmaskentryright) + (dst_negative_scale_sum_source_firstmaskentryright)))))) /\ (((((exists ff_h_pvs_sum_source_firstmaskentryrightpositive. ff_h_pvs_sum_source_firstmaskentryrightpositive + S (dst_positive_sum_source_firstmaskentryright) = S ((S (dc_quotient_sum_source_firstmaskentry)) * dst_positive_scale_sum_source_firstmaskentryright)) /\ exists ff_q_pvs_sum_source_firstmaskentryrightpositive. dst_positive_code_sum_source_firstmaskentryright = ff_q_pvs_sum_source_firstmaskentryrightpositive * S ((S (dc_quotient_sum_source_firstmaskentry)) * dst_positive_scale_sum_source_firstmaskentryright) + (dst_positive_sum_source_firstmaskentryright))) /\ (((((exists ff_h_pvs_sum_source_firstmaskentryrightnegative. ff_h_pvs_sum_source_firstmaskentryrightnegative + S (dst_negative_sum_source_firstmaskentryright) = S ((S (dc_quotient_sum_source_firstmaskentry)) * dst_negative_scale_sum_source_firstmaskentryright)) /\ exists ff_q_pvs_sum_source_firstmaskentryrightnegative. dst_negative_code_sum_source_firstmaskentryright = ff_q_pvs_sum_source_firstmaskentryrightnegative * S ((S (dc_quotient_sum_source_firstmaskentry)) * dst_negative_scale_sum_source_firstmaskentryright) + (dst_negative_sum_source_firstmaskentryright))) /\ (exists ge_balance_positive_sum_source_firstmaskentryrightvalue ge_balance_negative_sum_source_firstmaskentryrightvalue. (((((dc_right_sum_source_firstmaskentry) = 2 * (ge_balance_positive_sum_source_firstmaskentryrightvalue) /\ (ge_balance_negative_sum_source_firstmaskentryrightvalue) = 0) \/ exists ge_signed_half_sum_source_firstmaskentryrightvaluedecode. (((dc_right_sum_source_firstmaskentry) = 2 * ge_signed_half_sum_source_firstmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_source_firstmaskentryrightvalue) = 0) /\ (ge_balance_negative_sum_source_firstmaskentryrightvalue) = S ge_signed_half_sum_source_firstmaskentryrightvaluedecode))) /\ ((dst_positive_sum_source_firstmaskentryright) + ge_balance_negative_sum_source_firstmaskentryrightvalue = (dst_negative_sum_source_firstmaskentryright) + ge_balance_positive_sum_source_firstmaskentryrightvalue))))))))) /\ (exists sto_ap_sum_source_firstmaskentryproduct sto_an_sum_source_firstmaskentryproduct sto_bp_sum_source_firstmaskentryproduct sto_bn_sum_source_firstmaskentryproduct sto_cp_sum_source_firstmaskentryproduct sto_cn_sum_source_firstmaskentryproduct. (((((dc_left_sum_source_firstmaskentry) = 2 * (sto_ap_sum_source_firstmaskentryproduct) /\ (sto_an_sum_source_firstmaskentryproduct) = 0) \/ exists ge_signed_half_sum_source_firstmaskentryproductleft. (((dc_left_sum_source_firstmaskentry) = 2 * ge_signed_half_sum_source_firstmaskentryproductleft + 1 /\ (sto_ap_sum_source_firstmaskentryproduct) = 0) /\ (sto_an_sum_source_firstmaskentryproduct) = S ge_signed_half_sum_source_firstmaskentryproductleft))) /\ ((((((dc_right_sum_source_firstmaskentry) = 2 * (sto_bp_sum_source_firstmaskentryproduct) /\ (sto_bn_sum_source_firstmaskentryproduct) = 0) \/ exists ge_signed_half_sum_source_firstmaskentryproductright. (((dc_right_sum_source_firstmaskentry) = 2 * ge_signed_half_sum_source_firstmaskentryproductright + 1 /\ (sto_bp_sum_source_firstmaskentryproduct) = 0) /\ (sto_bn_sum_source_firstmaskentryproduct) = S ge_signed_half_sum_source_firstmaskentryproductright))) /\ ((((((dc_value_sum_source_firstmask) = 2 * (sto_cp_sum_source_firstmaskentryproduct) /\ (sto_cn_sum_source_firstmaskentryproduct) = 0) \/ exists ge_signed_half_sum_source_firstmaskentryproductoutput. (((dc_value_sum_source_firstmask) = 2 * ge_signed_half_sum_source_firstmaskentryproductoutput + 1 /\ (sto_cp_sum_source_firstmaskentryproduct) = 0) /\ (sto_cn_sum_source_firstmaskentryproduct) = S ge_signed_half_sum_source_firstmaskentryproductoutput))) /\ ((sto_ap_sum_source_firstmaskentryproduct * sto_bp_sum_source_firstmaskentryproduct + sto_an_sum_source_firstmaskentryproduct * sto_bn_sum_source_firstmaskentryproduct) + sto_cn_sum_source_firstmaskentryproduct = (sto_ap_sum_source_firstmaskentryproduct * sto_bn_sum_source_firstmaskentryproduct + sto_an_sum_source_firstmaskentryproduct * sto_bp_sum_source_firstmaskentryproduct) + sto_cp_sum_source_firstmaskentryproduct))))))))))))))) \/ ((((dc_index_sum_source_firstmask)=0 \/ ~(exists pvs_factor_sum_source_firstmaskentrynondivisor. (n) = (dc_index_sum_source_firstmask) * pvs_factor_sum_source_firstmaskentrynondivisor)) /\ ((dc_value_sum_source_firstmask)=0))))))) /\ (exists dst_positive_code_sum_source_firstfold dst_positive_scale_sum_source_firstfold dst_negative_code_sum_source_firstfold dst_negative_scale_sum_source_firstfold dst_positive_sum_sum_source_firstfold dst_negative_sum_sum_source_firstfold. (((dc_mask_sum_source_first) = (((((dst_positive_code_sum_source_firstfold) + (dst_positive_scale_sum_source_firstfold)) * S ((dst_positive_code_sum_source_firstfold) + (dst_positive_scale_sum_source_firstfold)) + ((dst_positive_scale_sum_source_firstfold) + (dst_positive_scale_sum_source_firstfold))) + (((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) * S ((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) + ((dst_negative_scale_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)))) * S ((((dst_positive_code_sum_source_firstfold) + (dst_positive_scale_sum_source_firstfold)) * S ((dst_positive_code_sum_source_firstfold) + (dst_positive_scale_sum_source_firstfold)) + ((dst_positive_scale_sum_source_firstfold) + (dst_positive_scale_sum_source_firstfold))) + (((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) * S ((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) + ((dst_negative_scale_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)))) + ((((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) * S ((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) + ((dst_negative_scale_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold))) + (((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) * S ((dst_negative_code_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)) + ((dst_negative_scale_sum_source_firstfold) + (dst_negative_scale_sum_source_firstfold)))))) /\ (((exists fs_u_dst_sum_source_firstfoldpositive fs_v_dst_sum_source_firstfoldpositive. ((((exists fs_h_dst_sum_source_firstfoldpositive_body_start. fs_h_dst_sum_source_firstfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_source_firstfoldpositive)) /\ exists fs_q_dst_sum_source_firstfoldpositive_body_start. fs_u_dst_sum_source_firstfoldpositive = fs_q_dst_sum_source_firstfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_source_firstfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_source_firstfoldpositive_body_terminal. fs_h_dst_sum_source_firstfoldpositive_body_terminal + S (dst_positive_sum_sum_source_firstfold) = S ((S (S (n))) * fs_v_dst_sum_source_firstfoldpositive)) /\ exists fs_q_dst_sum_source_firstfoldpositive_body_terminal. fs_u_dst_sum_source_firstfoldpositive = fs_q_dst_sum_source_firstfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_source_firstfoldpositive) + (dst_positive_sum_sum_source_firstfold))) /\ forall fs_i_dst_sum_source_firstfoldpositive_body_steps. (exists fs_lt_dst_sum_source_firstfoldpositive_body_steps_bound. fs_lt_dst_sum_source_firstfoldpositive_body_steps_bound + S fs_i_dst_sum_source_firstfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_source_firstfoldpositive_body_steps fs_r_dst_sum_source_firstfoldpositive_body_steps fs_s_dst_sum_source_firstfoldpositive_body_steps. ((((exists fs_h_dst_sum_source_firstfoldpositive_body_steps_summand. fs_h_dst_sum_source_firstfoldpositive_body_steps_summand + S (fs_a_dst_sum_source_firstfoldpositive_body_steps) = S ((S (fs_i_dst_sum_source_firstfoldpositive_body_steps)) * dst_positive_scale_sum_source_firstfold)) /\ exists fs_q_dst_sum_source_firstfoldpositive_body_steps_summand. dst_positive_code_sum_source_firstfold = fs_q_dst_sum_source_firstfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_source_firstfoldpositive_body_steps)) * dst_positive_scale_sum_source_firstfold) + (fs_a_dst_sum_source_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_source_firstfoldpositive_body_steps_partial. fs_h_dst_sum_source_firstfoldpositive_body_steps_partial + S (fs_r_dst_sum_source_firstfoldpositive_body_steps) = S ((S (fs_i_dst_sum_source_firstfoldpositive_body_steps)) * fs_v_dst_sum_source_firstfoldpositive)) /\ exists fs_q_dst_sum_source_firstfoldpositive_body_steps_partial. fs_u_dst_sum_source_firstfoldpositive = fs_q_dst_sum_source_firstfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_source_firstfoldpositive_body_steps)) * fs_v_dst_sum_source_firstfoldpositive) + (fs_r_dst_sum_source_firstfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_source_firstfoldpositive_body_steps_successor. fs_h_dst_sum_source_firstfoldpositive_body_steps_successor + S (fs_s_dst_sum_source_firstfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_source_firstfoldpositive_body_steps)) * fs_v_dst_sum_source_firstfoldpositive)) /\ exists fs_q_dst_sum_source_firstfoldpositive_body_steps_successor. fs_u_dst_sum_source_firstfoldpositive = fs_q_dst_sum_source_firstfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_source_firstfoldpositive_body_steps)) * fs_v_dst_sum_source_firstfoldpositive) + (fs_s_dst_sum_source_firstfoldpositive_body_steps))) /\ fs_s_dst_sum_source_firstfoldpositive_body_steps = fs_r_dst_sum_source_firstfoldpositive_body_steps + fs_a_dst_sum_source_firstfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_source_firstfoldnegative fs_v_dst_sum_source_firstfoldnegative. ((((exists fs_h_dst_sum_source_firstfoldnegative_body_start. fs_h_dst_sum_source_firstfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_source_firstfoldnegative)) /\ exists fs_q_dst_sum_source_firstfoldnegative_body_start. fs_u_dst_sum_source_firstfoldnegative = fs_q_dst_sum_source_firstfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_source_firstfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_source_firstfoldnegative_body_terminal. fs_h_dst_sum_source_firstfoldnegative_body_terminal + S (dst_negative_sum_sum_source_firstfold) = S ((S (S (n))) * fs_v_dst_sum_source_firstfoldnegative)) /\ exists fs_q_dst_sum_source_firstfoldnegative_body_terminal. fs_u_dst_sum_source_firstfoldnegative = fs_q_dst_sum_source_firstfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_source_firstfoldnegative) + (dst_negative_sum_sum_source_firstfold))) /\ forall fs_i_dst_sum_source_firstfoldnegative_body_steps. (exists fs_lt_dst_sum_source_firstfoldnegative_body_steps_bound. fs_lt_dst_sum_source_firstfoldnegative_body_steps_bound + S fs_i_dst_sum_source_firstfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_source_firstfoldnegative_body_steps fs_r_dst_sum_source_firstfoldnegative_body_steps fs_s_dst_sum_source_firstfoldnegative_body_steps. ((((exists fs_h_dst_sum_source_firstfoldnegative_body_steps_summand. fs_h_dst_sum_source_firstfoldnegative_body_steps_summand + S (fs_a_dst_sum_source_firstfoldnegative_body_steps) = S ((S (fs_i_dst_sum_source_firstfoldnegative_body_steps)) * dst_negative_scale_sum_source_firstfold)) /\ exists fs_q_dst_sum_source_firstfoldnegative_body_steps_summand. dst_negative_code_sum_source_firstfold = fs_q_dst_sum_source_firstfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_source_firstfoldnegative_body_steps)) * dst_negative_scale_sum_source_firstfold) + (fs_a_dst_sum_source_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_source_firstfoldnegative_body_steps_partial. fs_h_dst_sum_source_firstfoldnegative_body_steps_partial + S (fs_r_dst_sum_source_firstfoldnegative_body_steps) = S ((S (fs_i_dst_sum_source_firstfoldnegative_body_steps)) * fs_v_dst_sum_source_firstfoldnegative)) /\ exists fs_q_dst_sum_source_firstfoldnegative_body_steps_partial. fs_u_dst_sum_source_firstfoldnegative = fs_q_dst_sum_source_firstfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_source_firstfoldnegative_body_steps)) * fs_v_dst_sum_source_firstfoldnegative) + (fs_r_dst_sum_source_firstfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_source_firstfoldnegative_body_steps_successor. fs_h_dst_sum_source_firstfoldnegative_body_steps_successor + S (fs_s_dst_sum_source_firstfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_source_firstfoldnegative_body_steps)) * fs_v_dst_sum_source_firstfoldnegative)) /\ exists fs_q_dst_sum_source_firstfoldnegative_body_steps_successor. fs_u_dst_sum_source_firstfoldnegative = fs_q_dst_sum_source_firstfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_source_firstfoldnegative_body_steps)) * fs_v_dst_sum_source_firstfoldnegative) + (fs_s_dst_sum_source_firstfoldnegative_body_steps))) /\ fs_s_dst_sum_source_firstfoldnegative_body_steps = fs_r_dst_sum_source_firstfoldnegative_body_steps + fs_a_dst_sum_source_firstfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_source_firstfoldresult ge_balance_negative_sum_source_firstfoldresult. (((((a) = 2 * (ge_balance_positive_sum_source_firstfoldresult) /\ (ge_balance_negative_sum_source_firstfoldresult) = 0) \/ exists ge_signed_half_sum_source_firstfoldresultdecode. (((a) = 2 * ge_signed_half_sum_source_firstfoldresultdecode + 1 /\ (ge_balance_positive_sum_source_firstfoldresult) = 0) /\ (ge_balance_negative_sum_source_firstfoldresult) = S ge_signed_half_sum_source_firstfoldresultdecode))) /\ ((dst_positive_sum_sum_source_firstfold) + ge_balance_negative_sum_source_firstfoldresult = (dst_negative_sum_sum_source_firstfold) + ge_balance_positive_sum_source_firstfoldresult))))))))))))) -> (((~((n)=0)) /\ (exists dc_mask_sum_source_second. ((((exists dst_positive_code_sum_source_secondmasktable dst_positive_scale_sum_source_secondmasktable dst_negative_code_sum_source_secondmasktable dst_negative_scale_sum_source_secondmasktable. (((dc_mask_sum_source_second) = (((((dst_positive_code_sum_source_secondmasktable) + (dst_positive_scale_sum_source_secondmasktable)) * S ((dst_positive_code_sum_source_secondmasktable) + (dst_positive_scale_sum_source_secondmasktable)) + ((dst_positive_scale_sum_source_secondmasktable) + (dst_positive_scale_sum_source_secondmasktable))) + (((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) * S ((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) + ((dst_negative_scale_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)))) * S ((((dst_positive_code_sum_source_secondmasktable) + (dst_positive_scale_sum_source_secondmasktable)) * S ((dst_positive_code_sum_source_secondmasktable) + (dst_positive_scale_sum_source_secondmasktable)) + ((dst_positive_scale_sum_source_secondmasktable) + (dst_positive_scale_sum_source_secondmasktable))) + (((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) * S ((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) + ((dst_negative_scale_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)))) + ((((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) * S ((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) + ((dst_negative_scale_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable))) + (((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) * S ((dst_negative_code_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)) + ((dst_negative_scale_sum_source_secondmasktable) + (dst_negative_scale_sum_source_secondmasktable)))))) /\ (forall dst_index_sum_source_secondmasktable. (exists pvs_le_gap_sum_source_secondmasktabledomain. pvs_le_gap_sum_source_secondmasktabledomain + (dst_index_sum_source_secondmasktable) = (n)) -> exists dst_positive_sum_source_secondmasktable dst_negative_sum_source_secondmasktable dst_value_sum_source_secondmasktable. ((((exists ff_h_pvs_sum_source_secondmasktableentrypositive. ff_h_pvs_sum_source_secondmasktableentrypositive + S (dst_positive_sum_source_secondmasktable) = S ((S (dst_index_sum_source_secondmasktable)) * dst_positive_scale_sum_source_secondmasktable)) /\ exists ff_q_pvs_sum_source_secondmasktableentrypositive. dst_positive_code_sum_source_secondmasktable = ff_q_pvs_sum_source_secondmasktableentrypositive * S ((S (dst_index_sum_source_secondmasktable)) * dst_positive_scale_sum_source_secondmasktable) + (dst_positive_sum_source_secondmasktable))) /\ (((((exists ff_h_pvs_sum_source_secondmasktableentrynegative. ff_h_pvs_sum_source_secondmasktableentrynegative + S (dst_negative_sum_source_secondmasktable) = S ((S (dst_index_sum_source_secondmasktable)) * dst_negative_scale_sum_source_secondmasktable)) /\ exists ff_q_pvs_sum_source_secondmasktableentrynegative. dst_negative_code_sum_source_secondmasktable = ff_q_pvs_sum_source_secondmasktableentrynegative * S ((S (dst_index_sum_source_secondmasktable)) * dst_negative_scale_sum_source_secondmasktable) + (dst_negative_sum_source_secondmasktable))) /\ (exists ge_balance_positive_sum_source_secondmasktableentryvalue ge_balance_negative_sum_source_secondmasktableentryvalue. (((((dst_value_sum_source_secondmasktable) = 2 * (ge_balance_positive_sum_source_secondmasktableentryvalue) /\ (ge_balance_negative_sum_source_secondmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_source_secondmasktableentryvaluedecode. (((dst_value_sum_source_secondmasktable) = 2 * ge_signed_half_sum_source_secondmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_source_secondmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_source_secondmasktableentryvalue) = S ge_signed_half_sum_source_secondmasktableentryvaluedecode))) /\ ((dst_positive_sum_source_secondmasktable) + ge_balance_negative_sum_source_secondmasktableentryvalue = (dst_negative_sum_source_secondmasktable) + ge_balance_positive_sum_source_secondmasktableentryvalue))))))))) /\ (forall dc_index_sum_source_secondmask dc_value_sum_source_secondmask. (exists pvs_le_gap_sum_source_secondmaskdomain. pvs_le_gap_sum_source_secondmaskdomain + (dc_index_sum_source_secondmask) = (n)) -> (exists dst_positive_code_sum_source_secondmasklookup dst_positive_scale_sum_source_secondmasklookup dst_negative_code_sum_source_secondmasklookup dst_negative_scale_sum_source_secondmasklookup dst_positive_sum_source_secondmasklookup dst_negative_sum_source_secondmasklookup. (((dc_mask_sum_source_second) = (((((dst_positive_code_sum_source_secondmasklookup) + (dst_positive_scale_sum_source_secondmasklookup)) * S ((dst_positive_code_sum_source_secondmasklookup) + (dst_positive_scale_sum_source_secondmasklookup)) + ((dst_positive_scale_sum_source_secondmasklookup) + (dst_positive_scale_sum_source_secondmasklookup))) + (((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) * S ((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) + ((dst_negative_scale_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)))) * S ((((dst_positive_code_sum_source_secondmasklookup) + (dst_positive_scale_sum_source_secondmasklookup)) * S ((dst_positive_code_sum_source_secondmasklookup) + (dst_positive_scale_sum_source_secondmasklookup)) + ((dst_positive_scale_sum_source_secondmasklookup) + (dst_positive_scale_sum_source_secondmasklookup))) + (((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) * S ((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) + ((dst_negative_scale_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)))) + ((((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) * S ((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) + ((dst_negative_scale_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup))) + (((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) * S ((dst_negative_code_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)) + ((dst_negative_scale_sum_source_secondmasklookup) + (dst_negative_scale_sum_source_secondmasklookup)))))) /\ (((((exists ff_h_pvs_sum_source_secondmasklookuppositive. ff_h_pvs_sum_source_secondmasklookuppositive + S (dst_positive_sum_source_secondmasklookup) = S ((S (dc_index_sum_source_secondmask)) * dst_positive_scale_sum_source_secondmasklookup)) /\ exists ff_q_pvs_sum_source_secondmasklookuppositive. dst_positive_code_sum_source_secondmasklookup = ff_q_pvs_sum_source_secondmasklookuppositive * S ((S (dc_index_sum_source_secondmask)) * dst_positive_scale_sum_source_secondmasklookup) + (dst_positive_sum_source_secondmasklookup))) /\ (((((exists ff_h_pvs_sum_source_secondmasklookupnegative. ff_h_pvs_sum_source_secondmasklookupnegative + S (dst_negative_sum_source_secondmasklookup) = S ((S (dc_index_sum_source_secondmask)) * dst_negative_scale_sum_source_secondmasklookup)) /\ exists ff_q_pvs_sum_source_secondmasklookupnegative. dst_negative_code_sum_source_secondmasklookup = ff_q_pvs_sum_source_secondmasklookupnegative * S ((S (dc_index_sum_source_secondmask)) * dst_negative_scale_sum_source_secondmasklookup) + (dst_negative_sum_source_secondmasklookup))) /\ (exists ge_balance_positive_sum_source_secondmasklookupvalue ge_balance_negative_sum_source_secondmasklookupvalue. (((((dc_value_sum_source_secondmask) = 2 * (ge_balance_positive_sum_source_secondmasklookupvalue) /\ (ge_balance_negative_sum_source_secondmasklookupvalue) = 0) \/ exists ge_signed_half_sum_source_secondmasklookupvaluedecode. (((dc_value_sum_source_secondmask) = 2 * ge_signed_half_sum_source_secondmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_source_secondmasklookupvalue) = 0) /\ (ge_balance_negative_sum_source_secondmasklookupvalue) = S ge_signed_half_sum_source_secondmasklookupvaluedecode))) /\ ((dst_positive_sum_source_secondmasklookup) + ge_balance_negative_sum_source_secondmasklookupvalue = (dst_negative_sum_source_secondmasklookup) + ge_balance_positive_sum_source_secondmasklookupvalue))))))))) -> ((((~((dc_index_sum_source_secondmask)=0)) /\ (exists dc_quotient_sum_source_secondmaskentry dc_left_sum_source_secondmaskentry dc_right_sum_source_secondmaskentry. (((n)=(dc_index_sum_source_secondmask)*dc_quotient_sum_source_secondmaskentry) /\ (((exists dst_positive_code_sum_source_secondmaskentryleft dst_positive_scale_sum_source_secondmaskentryleft dst_negative_code_sum_source_secondmaskentryleft dst_negative_scale_sum_source_secondmaskentryleft dst_positive_sum_source_secondmaskentryleft dst_negative_sum_source_secondmaskentryleft. (((H) = (((((dst_positive_code_sum_source_secondmaskentryleft) + (dst_positive_scale_sum_source_secondmaskentryleft)) * S ((dst_positive_code_sum_source_secondmaskentryleft) + (dst_positive_scale_sum_source_secondmaskentryleft)) + ((dst_positive_scale_sum_source_secondmaskentryleft) + (dst_positive_scale_sum_source_secondmaskentryleft))) + (((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) * S ((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) + ((dst_negative_scale_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)))) * S ((((dst_positive_code_sum_source_secondmaskentryleft) + (dst_positive_scale_sum_source_secondmaskentryleft)) * S ((dst_positive_code_sum_source_secondmaskentryleft) + (dst_positive_scale_sum_source_secondmaskentryleft)) + ((dst_positive_scale_sum_source_secondmaskentryleft) + (dst_positive_scale_sum_source_secondmaskentryleft))) + (((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) * S ((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) + ((dst_negative_scale_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)))) + ((((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) * S ((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) + ((dst_negative_scale_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft))) + (((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) * S ((dst_negative_code_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)) + ((dst_negative_scale_sum_source_secondmaskentryleft) + (dst_negative_scale_sum_source_secondmaskentryleft)))))) /\ (((((exists ff_h_pvs_sum_source_secondmaskentryleftpositive. ff_h_pvs_sum_source_secondmaskentryleftpositive + S (dst_positive_sum_source_secondmaskentryleft) = S ((S (dc_index_sum_source_secondmask)) * dst_positive_scale_sum_source_secondmaskentryleft)) /\ exists ff_q_pvs_sum_source_secondmaskentryleftpositive. dst_positive_code_sum_source_secondmaskentryleft = ff_q_pvs_sum_source_secondmaskentryleftpositive * S ((S (dc_index_sum_source_secondmask)) * dst_positive_scale_sum_source_secondmaskentryleft) + (dst_positive_sum_source_secondmaskentryleft))) /\ (((((exists ff_h_pvs_sum_source_secondmaskentryleftnegative. ff_h_pvs_sum_source_secondmaskentryleftnegative + S (dst_negative_sum_source_secondmaskentryleft) = S ((S (dc_index_sum_source_secondmask)) * dst_negative_scale_sum_source_secondmaskentryleft)) /\ exists ff_q_pvs_sum_source_secondmaskentryleftnegative. dst_negative_code_sum_source_secondmaskentryleft = ff_q_pvs_sum_source_secondmaskentryleftnegative * S ((S (dc_index_sum_source_secondmask)) * dst_negative_scale_sum_source_secondmaskentryleft) + (dst_negative_sum_source_secondmaskentryleft))) /\ (exists ge_balance_positive_sum_source_secondmaskentryleftvalue ge_balance_negative_sum_source_secondmaskentryleftvalue. (((((dc_left_sum_source_secondmaskentry) = 2 * (ge_balance_positive_sum_source_secondmaskentryleftvalue) /\ (ge_balance_negative_sum_source_secondmaskentryleftvalue) = 0) \/ exists ge_signed_half_sum_source_secondmaskentryleftvaluedecode. (((dc_left_sum_source_secondmaskentry) = 2 * ge_signed_half_sum_source_secondmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_sum_source_secondmaskentryleftvalue) = 0) /\ (ge_balance_negative_sum_source_secondmaskentryleftvalue) = S ge_signed_half_sum_source_secondmaskentryleftvaluedecode))) /\ ((dst_positive_sum_source_secondmaskentryleft) + ge_balance_negative_sum_source_secondmaskentryleftvalue = (dst_negative_sum_source_secondmaskentryleft) + ge_balance_positive_sum_source_secondmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_sum_source_secondmaskentryright dst_positive_scale_sum_source_secondmaskentryright dst_negative_code_sum_source_secondmaskentryright dst_negative_scale_sum_source_secondmaskentryright dst_positive_sum_source_secondmaskentryright dst_negative_sum_source_secondmaskentryright. (((K) = (((((dst_positive_code_sum_source_secondmaskentryright) + (dst_positive_scale_sum_source_secondmaskentryright)) * S ((dst_positive_code_sum_source_secondmaskentryright) + (dst_positive_scale_sum_source_secondmaskentryright)) + ((dst_positive_scale_sum_source_secondmaskentryright) + (dst_positive_scale_sum_source_secondmaskentryright))) + (((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) * S ((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) + ((dst_negative_scale_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)))) * S ((((dst_positive_code_sum_source_secondmaskentryright) + (dst_positive_scale_sum_source_secondmaskentryright)) * S ((dst_positive_code_sum_source_secondmaskentryright) + (dst_positive_scale_sum_source_secondmaskentryright)) + ((dst_positive_scale_sum_source_secondmaskentryright) + (dst_positive_scale_sum_source_secondmaskentryright))) + (((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) * S ((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) + ((dst_negative_scale_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)))) + ((((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) * S ((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) + ((dst_negative_scale_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright))) + (((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) * S ((dst_negative_code_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)) + ((dst_negative_scale_sum_source_secondmaskentryright) + (dst_negative_scale_sum_source_secondmaskentryright)))))) /\ (((((exists ff_h_pvs_sum_source_secondmaskentryrightpositive. ff_h_pvs_sum_source_secondmaskentryrightpositive + S (dst_positive_sum_source_secondmaskentryright) = S ((S (dc_quotient_sum_source_secondmaskentry)) * dst_positive_scale_sum_source_secondmaskentryright)) /\ exists ff_q_pvs_sum_source_secondmaskentryrightpositive. dst_positive_code_sum_source_secondmaskentryright = ff_q_pvs_sum_source_secondmaskentryrightpositive * S ((S (dc_quotient_sum_source_secondmaskentry)) * dst_positive_scale_sum_source_secondmaskentryright) + (dst_positive_sum_source_secondmaskentryright))) /\ (((((exists ff_h_pvs_sum_source_secondmaskentryrightnegative. ff_h_pvs_sum_source_secondmaskentryrightnegative + S (dst_negative_sum_source_secondmaskentryright) = S ((S (dc_quotient_sum_source_secondmaskentry)) * dst_negative_scale_sum_source_secondmaskentryright)) /\ exists ff_q_pvs_sum_source_secondmaskentryrightnegative. dst_negative_code_sum_source_secondmaskentryright = ff_q_pvs_sum_source_secondmaskentryrightnegative * S ((S (dc_quotient_sum_source_secondmaskentry)) * dst_negative_scale_sum_source_secondmaskentryright) + (dst_negative_sum_source_secondmaskentryright))) /\ (exists ge_balance_positive_sum_source_secondmaskentryrightvalue ge_balance_negative_sum_source_secondmaskentryrightvalue. (((((dc_right_sum_source_secondmaskentry) = 2 * (ge_balance_positive_sum_source_secondmaskentryrightvalue) /\ (ge_balance_negative_sum_source_secondmaskentryrightvalue) = 0) \/ exists ge_signed_half_sum_source_secondmaskentryrightvaluedecode. (((dc_right_sum_source_secondmaskentry) = 2 * ge_signed_half_sum_source_secondmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_sum_source_secondmaskentryrightvalue) = 0) /\ (ge_balance_negative_sum_source_secondmaskentryrightvalue) = S ge_signed_half_sum_source_secondmaskentryrightvaluedecode))) /\ ((dst_positive_sum_source_secondmaskentryright) + ge_balance_negative_sum_source_secondmaskentryrightvalue = (dst_negative_sum_source_secondmaskentryright) + ge_balance_positive_sum_source_secondmaskentryrightvalue))))))))) /\ (exists sto_ap_sum_source_secondmaskentryproduct sto_an_sum_source_secondmaskentryproduct sto_bp_sum_source_secondmaskentryproduct sto_bn_sum_source_secondmaskentryproduct sto_cp_sum_source_secondmaskentryproduct sto_cn_sum_source_secondmaskentryproduct. (((((dc_left_sum_source_secondmaskentry) = 2 * (sto_ap_sum_source_secondmaskentryproduct) /\ (sto_an_sum_source_secondmaskentryproduct) = 0) \/ exists ge_signed_half_sum_source_secondmaskentryproductleft. (((dc_left_sum_source_secondmaskentry) = 2 * ge_signed_half_sum_source_secondmaskentryproductleft + 1 /\ (sto_ap_sum_source_secondmaskentryproduct) = 0) /\ (sto_an_sum_source_secondmaskentryproduct) = S ge_signed_half_sum_source_secondmaskentryproductleft))) /\ ((((((dc_right_sum_source_secondmaskentry) = 2 * (sto_bp_sum_source_secondmaskentryproduct) /\ (sto_bn_sum_source_secondmaskentryproduct) = 0) \/ exists ge_signed_half_sum_source_secondmaskentryproductright. (((dc_right_sum_source_secondmaskentry) = 2 * ge_signed_half_sum_source_secondmaskentryproductright + 1 /\ (sto_bp_sum_source_secondmaskentryproduct) = 0) /\ (sto_bn_sum_source_secondmaskentryproduct) = S ge_signed_half_sum_source_secondmaskentryproductright))) /\ ((((((dc_value_sum_source_secondmask) = 2 * (sto_cp_sum_source_secondmaskentryproduct) /\ (sto_cn_sum_source_secondmaskentryproduct) = 0) \/ exists ge_signed_half_sum_source_secondmaskentryproductoutput. (((dc_value_sum_source_secondmask) = 2 * ge_signed_half_sum_source_secondmaskentryproductoutput + 1 /\ (sto_cp_sum_source_secondmaskentryproduct) = 0) /\ (sto_cn_sum_source_secondmaskentryproduct) = S ge_signed_half_sum_source_secondmaskentryproductoutput))) /\ ((sto_ap_sum_source_secondmaskentryproduct * sto_bp_sum_source_secondmaskentryproduct + sto_an_sum_source_secondmaskentryproduct * sto_bn_sum_source_secondmaskentryproduct) + sto_cn_sum_source_secondmaskentryproduct = (sto_ap_sum_source_secondmaskentryproduct * sto_bn_sum_source_secondmaskentryproduct + sto_an_sum_source_secondmaskentryproduct * sto_bp_sum_source_secondmaskentryproduct) + sto_cp_sum_source_secondmaskentryproduct))))))))))))))) \/ ((((dc_index_sum_source_secondmask)=0 \/ ~(exists pvs_factor_sum_source_secondmaskentrynondivisor. (n) = (dc_index_sum_source_secondmask) * pvs_factor_sum_source_secondmaskentrynondivisor)) /\ ((dc_value_sum_source_secondmask)=0))))))) /\ (exists dst_positive_code_sum_source_secondfold dst_positive_scale_sum_source_secondfold dst_negative_code_sum_source_secondfold dst_negative_scale_sum_source_secondfold dst_positive_sum_sum_source_secondfold dst_negative_sum_sum_source_secondfold. (((dc_mask_sum_source_second) = (((((dst_positive_code_sum_source_secondfold) + (dst_positive_scale_sum_source_secondfold)) * S ((dst_positive_code_sum_source_secondfold) + (dst_positive_scale_sum_source_secondfold)) + ((dst_positive_scale_sum_source_secondfold) + (dst_positive_scale_sum_source_secondfold))) + (((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) * S ((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) + ((dst_negative_scale_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)))) * S ((((dst_positive_code_sum_source_secondfold) + (dst_positive_scale_sum_source_secondfold)) * S ((dst_positive_code_sum_source_secondfold) + (dst_positive_scale_sum_source_secondfold)) + ((dst_positive_scale_sum_source_secondfold) + (dst_positive_scale_sum_source_secondfold))) + (((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) * S ((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) + ((dst_negative_scale_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)))) + ((((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) * S ((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) + ((dst_negative_scale_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold))) + (((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) * S ((dst_negative_code_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)) + ((dst_negative_scale_sum_source_secondfold) + (dst_negative_scale_sum_source_secondfold)))))) /\ (((exists fs_u_dst_sum_source_secondfoldpositive fs_v_dst_sum_source_secondfoldpositive. ((((exists fs_h_dst_sum_source_secondfoldpositive_body_start. fs_h_dst_sum_source_secondfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_source_secondfoldpositive)) /\ exists fs_q_dst_sum_source_secondfoldpositive_body_start. fs_u_dst_sum_source_secondfoldpositive = fs_q_dst_sum_source_secondfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_source_secondfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_source_secondfoldpositive_body_terminal. fs_h_dst_sum_source_secondfoldpositive_body_terminal + S (dst_positive_sum_sum_source_secondfold) = S ((S (S (n))) * fs_v_dst_sum_source_secondfoldpositive)) /\ exists fs_q_dst_sum_source_secondfoldpositive_body_terminal. fs_u_dst_sum_source_secondfoldpositive = fs_q_dst_sum_source_secondfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_source_secondfoldpositive) + (dst_positive_sum_sum_source_secondfold))) /\ forall fs_i_dst_sum_source_secondfoldpositive_body_steps. (exists fs_lt_dst_sum_source_secondfoldpositive_body_steps_bound. fs_lt_dst_sum_source_secondfoldpositive_body_steps_bound + S fs_i_dst_sum_source_secondfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_source_secondfoldpositive_body_steps fs_r_dst_sum_source_secondfoldpositive_body_steps fs_s_dst_sum_source_secondfoldpositive_body_steps. ((((exists fs_h_dst_sum_source_secondfoldpositive_body_steps_summand. fs_h_dst_sum_source_secondfoldpositive_body_steps_summand + S (fs_a_dst_sum_source_secondfoldpositive_body_steps) = S ((S (fs_i_dst_sum_source_secondfoldpositive_body_steps)) * dst_positive_scale_sum_source_secondfold)) /\ exists fs_q_dst_sum_source_secondfoldpositive_body_steps_summand. dst_positive_code_sum_source_secondfold = fs_q_dst_sum_source_secondfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_source_secondfoldpositive_body_steps)) * dst_positive_scale_sum_source_secondfold) + (fs_a_dst_sum_source_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_source_secondfoldpositive_body_steps_partial. fs_h_dst_sum_source_secondfoldpositive_body_steps_partial + S (fs_r_dst_sum_source_secondfoldpositive_body_steps) = S ((S (fs_i_dst_sum_source_secondfoldpositive_body_steps)) * fs_v_dst_sum_source_secondfoldpositive)) /\ exists fs_q_dst_sum_source_secondfoldpositive_body_steps_partial. fs_u_dst_sum_source_secondfoldpositive = fs_q_dst_sum_source_secondfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_source_secondfoldpositive_body_steps)) * fs_v_dst_sum_source_secondfoldpositive) + (fs_r_dst_sum_source_secondfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_source_secondfoldpositive_body_steps_successor. fs_h_dst_sum_source_secondfoldpositive_body_steps_successor + S (fs_s_dst_sum_source_secondfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_source_secondfoldpositive_body_steps)) * fs_v_dst_sum_source_secondfoldpositive)) /\ exists fs_q_dst_sum_source_secondfoldpositive_body_steps_successor. fs_u_dst_sum_source_secondfoldpositive = fs_q_dst_sum_source_secondfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_source_secondfoldpositive_body_steps)) * fs_v_dst_sum_source_secondfoldpositive) + (fs_s_dst_sum_source_secondfoldpositive_body_steps))) /\ fs_s_dst_sum_source_secondfoldpositive_body_steps = fs_r_dst_sum_source_secondfoldpositive_body_steps + fs_a_dst_sum_source_secondfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_source_secondfoldnegative fs_v_dst_sum_source_secondfoldnegative. ((((exists fs_h_dst_sum_source_secondfoldnegative_body_start. fs_h_dst_sum_source_secondfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_source_secondfoldnegative)) /\ exists fs_q_dst_sum_source_secondfoldnegative_body_start. fs_u_dst_sum_source_secondfoldnegative = fs_q_dst_sum_source_secondfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_source_secondfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_source_secondfoldnegative_body_terminal. fs_h_dst_sum_source_secondfoldnegative_body_terminal + S (dst_negative_sum_sum_source_secondfold) = S ((S (S (n))) * fs_v_dst_sum_source_secondfoldnegative)) /\ exists fs_q_dst_sum_source_secondfoldnegative_body_terminal. fs_u_dst_sum_source_secondfoldnegative = fs_q_dst_sum_source_secondfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_source_secondfoldnegative) + (dst_negative_sum_sum_source_secondfold))) /\ forall fs_i_dst_sum_source_secondfoldnegative_body_steps. (exists fs_lt_dst_sum_source_secondfoldnegative_body_steps_bound. fs_lt_dst_sum_source_secondfoldnegative_body_steps_bound + S fs_i_dst_sum_source_secondfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_source_secondfoldnegative_body_steps fs_r_dst_sum_source_secondfoldnegative_body_steps fs_s_dst_sum_source_secondfoldnegative_body_steps. ((((exists fs_h_dst_sum_source_secondfoldnegative_body_steps_summand. fs_h_dst_sum_source_secondfoldnegative_body_steps_summand + S (fs_a_dst_sum_source_secondfoldnegative_body_steps) = S ((S (fs_i_dst_sum_source_secondfoldnegative_body_steps)) * dst_negative_scale_sum_source_secondfold)) /\ exists fs_q_dst_sum_source_secondfoldnegative_body_steps_summand. dst_negative_code_sum_source_secondfold = fs_q_dst_sum_source_secondfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_source_secondfoldnegative_body_steps)) * dst_negative_scale_sum_source_secondfold) + (fs_a_dst_sum_source_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_source_secondfoldnegative_body_steps_partial. fs_h_dst_sum_source_secondfoldnegative_body_steps_partial + S (fs_r_dst_sum_source_secondfoldnegative_body_steps) = S ((S (fs_i_dst_sum_source_secondfoldnegative_body_steps)) * fs_v_dst_sum_source_secondfoldnegative)) /\ exists fs_q_dst_sum_source_secondfoldnegative_body_steps_partial. fs_u_dst_sum_source_secondfoldnegative = fs_q_dst_sum_source_secondfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_source_secondfoldnegative_body_steps)) * fs_v_dst_sum_source_secondfoldnegative) + (fs_r_dst_sum_source_secondfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_source_secondfoldnegative_body_steps_successor. fs_h_dst_sum_source_secondfoldnegative_body_steps_successor + S (fs_s_dst_sum_source_secondfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_source_secondfoldnegative_body_steps)) * fs_v_dst_sum_source_secondfoldnegative)) /\ exists fs_q_dst_sum_source_secondfoldnegative_body_steps_successor. fs_u_dst_sum_source_secondfoldnegative = fs_q_dst_sum_source_secondfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_source_secondfoldnegative_body_steps)) * fs_v_dst_sum_source_secondfoldnegative) + (fs_s_dst_sum_source_secondfoldnegative_body_steps))) /\ fs_s_dst_sum_source_secondfoldnegative_body_steps = fs_r_dst_sum_source_secondfoldnegative_body_steps + fs_a_dst_sum_source_secondfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_source_secondfoldresult ge_balance_negative_sum_source_secondfoldresult. (((((b) = 2 * (ge_balance_positive_sum_source_secondfoldresult) /\ (ge_balance_negative_sum_source_secondfoldresult) = 0) \/ exists ge_signed_half_sum_source_secondfoldresultdecode. (((b) = 2 * ge_signed_half_sum_source_secondfoldresultdecode + 1 /\ (ge_balance_positive_sum_source_secondfoldresult) = 0) /\ (ge_balance_negative_sum_source_secondfoldresult) = S ge_signed_half_sum_source_secondfoldresultdecode))) /\ ((dst_positive_sum_sum_source_secondfold) + ge_balance_negative_sum_source_secondfoldresult = (dst_negative_sum_sum_source_secondfold) + ge_balance_positive_sum_source_secondfoldresult))))))))))))) -> a=b