dirichlet_constant_one_table_positive_unique

forall N F G. (((exists dst_positive_code_constant_oneunique_firsttable dst_positive_scale_constant_oneunique_firsttable dst_negative_code_constant_oneunique_firsttable dst_negative_scale_constant_oneunique_firsttable. (((F) = (((((dst_positive_code_constant_oneunique_firsttable) + (dst_positive_scale_constant_oneunique_firsttable)) * S ((dst_positive_code_constant_oneunique_firsttable) + (dst_positive_scale_constant_oneunique_firsttable)) + ((dst_positive_scale_constant_oneunique_firsttable) + (dst_positive_scale_constant_oneunique_firsttable))) + (((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) * S ((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) + ((dst_negative_scale_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)))) * S ((((dst_positive_code_constant_oneunique_firsttable) + (dst_positive_scale_constant_oneunique_firsttable)) * S ((dst_positive_code_constant_oneunique_firsttable) + (dst_positive_scale_constant_oneunique_firsttable)) + ((dst_positive_scale_constant_oneunique_firsttable) + (dst_positive_scale_constant_oneunique_firsttable))) + (((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) * S ((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) + ((dst_negative_scale_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)))) + ((((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) * S ((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) + ((dst_negative_scale_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable))) + (((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) * S ((dst_negative_code_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)) + ((dst_negative_scale_constant_oneunique_firsttable) + (dst_negative_scale_constant_oneunique_firsttable)))))) /\ (forall dst_index_constant_oneunique_firsttable. (exists pvs_le_gap_constant_oneunique_firsttabledomain. pvs_le_gap_constant_oneunique_firsttabledomain + (dst_index_constant_oneunique_firsttable) = (N)) -> exists dst_positive_constant_oneunique_firsttable dst_negative_constant_oneunique_firsttable dst_value_constant_oneunique_firsttable. ((((exists ff_h_pvs_constant_oneunique_firsttableentrypositive. ff_h_pvs_constant_oneunique_firsttableentrypositive + S (dst_positive_constant_oneunique_firsttable) = S ((S (dst_index_constant_oneunique_firsttable)) * dst_positive_scale_constant_oneunique_firsttable)) /\ exists ff_q_pvs_constant_oneunique_firsttableentrypositive. dst_positive_code_constant_oneunique_firsttable = ff_q_pvs_constant_oneunique_firsttableentrypositive * S ((S (dst_index_constant_oneunique_firsttable)) * dst_positive_scale_constant_oneunique_firsttable) + (dst_positive_constant_oneunique_firsttable))) /\ (((((exists ff_h_pvs_constant_oneunique_firsttableentrynegative. ff_h_pvs_constant_oneunique_firsttableentrynegative + S (dst_negative_constant_oneunique_firsttable) = S ((S (dst_index_constant_oneunique_firsttable)) * dst_negative_scale_constant_oneunique_firsttable)) /\ exists ff_q_pvs_constant_oneunique_firsttableentrynegative. dst_negative_code_constant_oneunique_firsttable = ff_q_pvs_constant_oneunique_firsttableentrynegative * S ((S (dst_index_constant_oneunique_firsttable)) * dst_negative_scale_constant_oneunique_firsttable) + (dst_negative_constant_oneunique_firsttable))) /\ (exists ge_balance_positive_constant_oneunique_firsttableentryvalue ge_balance_negative_constant_oneunique_firsttableentryvalue. (((((dst_value_constant_oneunique_firsttable) = 2 * (ge_balance_positive_constant_oneunique_firsttableentryvalue) /\ (ge_balance_negative_constant_oneunique_firsttableentryvalue) = 0) \/ exists ge_signed_half_constant_oneunique_firsttableentryvaluedecode. (((dst_value_constant_oneunique_firsttable) = 2 * ge_signed_half_constant_oneunique_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_constant_oneunique_firsttableentryvalue) = 0) /\ (ge_balance_negative_constant_oneunique_firsttableentryvalue) = S ge_signed_half_constant_oneunique_firsttableentryvaluedecode))) /\ ((dst_positive_constant_oneunique_firsttable) + ge_balance_negative_constant_oneunique_firsttableentryvalue = (dst_negative_constant_oneunique_firsttable) + ge_balance_positive_constant_oneunique_firsttableentryvalue))))))))) /\ (forall du_index_constant_oneunique_first du_value_constant_oneunique_first. ~(du_index_constant_oneunique_first=0) -> (exists pvs_le_gap_constant_oneunique_firstbound. pvs_le_gap_constant_oneunique_firstbound + (du_index_constant_oneunique_first) = (N)) -> (exists dst_positive_code_constant_oneunique_firstentry dst_positive_scale_constant_oneunique_firstentry dst_negative_code_constant_oneunique_firstentry dst_negative_scale_constant_oneunique_firstentry dst_positive_constant_oneunique_firstentry dst_negative_constant_oneunique_firstentry. (((F) = (((((dst_positive_code_constant_oneunique_firstentry) + (dst_positive_scale_constant_oneunique_firstentry)) * S ((dst_positive_code_constant_oneunique_firstentry) + (dst_positive_scale_constant_oneunique_firstentry)) + ((dst_positive_scale_constant_oneunique_firstentry) + (dst_positive_scale_constant_oneunique_firstentry))) + (((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) * S ((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) + ((dst_negative_scale_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)))) * S ((((dst_positive_code_constant_oneunique_firstentry) + (dst_positive_scale_constant_oneunique_firstentry)) * S ((dst_positive_code_constant_oneunique_firstentry) + (dst_positive_scale_constant_oneunique_firstentry)) + ((dst_positive_scale_constant_oneunique_firstentry) + (dst_positive_scale_constant_oneunique_firstentry))) + (((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) * S ((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) + ((dst_negative_scale_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)))) + ((((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) * S ((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) + ((dst_negative_scale_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry))) + (((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) * S ((dst_negative_code_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)) + ((dst_negative_scale_constant_oneunique_firstentry) + (dst_negative_scale_constant_oneunique_firstentry)))))) /\ (((((exists ff_h_pvs_constant_oneunique_firstentrypositive. ff_h_pvs_constant_oneunique_firstentrypositive + S (dst_positive_constant_oneunique_firstentry) = S ((S (du_index_constant_oneunique_first)) * dst_positive_scale_constant_oneunique_firstentry)) /\ exists ff_q_pvs_constant_oneunique_firstentrypositive. dst_positive_code_constant_oneunique_firstentry = ff_q_pvs_constant_oneunique_firstentrypositive * S ((S (du_index_constant_oneunique_first)) * dst_positive_scale_constant_oneunique_firstentry) + (dst_positive_constant_oneunique_firstentry))) /\ (((((exists ff_h_pvs_constant_oneunique_firstentrynegative. ff_h_pvs_constant_oneunique_firstentrynegative + S (dst_negative_constant_oneunique_firstentry) = S ((S (du_index_constant_oneunique_first)) * dst_negative_scale_constant_oneunique_firstentry)) /\ exists ff_q_pvs_constant_oneunique_firstentrynegative. dst_negative_code_constant_oneunique_firstentry = ff_q_pvs_constant_oneunique_firstentrynegative * S ((S (du_index_constant_oneunique_first)) * dst_negative_scale_constant_oneunique_firstentry) + (dst_negative_constant_oneunique_firstentry))) /\ (exists ge_balance_positive_constant_oneunique_firstentryvalue ge_balance_negative_constant_oneunique_firstentryvalue. (((((du_value_constant_oneunique_first) = 2 * (ge_balance_positive_constant_oneunique_firstentryvalue) /\ (ge_balance_negative_constant_oneunique_firstentryvalue) = 0) \/ exists ge_signed_half_constant_oneunique_firstentryvaluedecode. (((du_value_constant_oneunique_first) = 2 * ge_signed_half_constant_oneunique_firstentryvaluedecode + 1 /\ (ge_balance_positive_constant_oneunique_firstentryvalue) = 0) /\ (ge_balance_negative_constant_oneunique_firstentryvalue) = S ge_signed_half_constant_oneunique_firstentryvaluedecode))) /\ ((dst_positive_constant_oneunique_firstentry) + ge_balance_negative_constant_oneunique_firstentryvalue = (dst_negative_constant_oneunique_firstentry) + ge_balance_positive_constant_oneunique_firstentryvalue))))))))) -> du_value_constant_oneunique_first=2))) -> (((exists dst_positive_code_constant_oneunique_secondtable dst_positive_scale_constant_oneunique_secondtable dst_negative_code_constant_oneunique_secondtable dst_negative_scale_constant_oneunique_secondtable. (((G) = (((((dst_positive_code_constant_oneunique_secondtable) + (dst_positive_scale_constant_oneunique_secondtable)) * S ((dst_positive_code_constant_oneunique_secondtable) + (dst_positive_scale_constant_oneunique_secondtable)) + ((dst_positive_scale_constant_oneunique_secondtable) + (dst_positive_scale_constant_oneunique_secondtable))) + (((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) * S ((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) + ((dst_negative_scale_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)))) * S ((((dst_positive_code_constant_oneunique_secondtable) + (dst_positive_scale_constant_oneunique_secondtable)) * S ((dst_positive_code_constant_oneunique_secondtable) + (dst_positive_scale_constant_oneunique_secondtable)) + ((dst_positive_scale_constant_oneunique_secondtable) + (dst_positive_scale_constant_oneunique_secondtable))) + (((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) * S ((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) + ((dst_negative_scale_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)))) + ((((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) * S ((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) + ((dst_negative_scale_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable))) + (((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) * S ((dst_negative_code_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)) + ((dst_negative_scale_constant_oneunique_secondtable) + (dst_negative_scale_constant_oneunique_secondtable)))))) /\ (forall dst_index_constant_oneunique_secondtable. (exists pvs_le_gap_constant_oneunique_secondtabledomain. pvs_le_gap_constant_oneunique_secondtabledomain + (dst_index_constant_oneunique_secondtable) = (N)) -> exists dst_positive_constant_oneunique_secondtable dst_negative_constant_oneunique_secondtable dst_value_constant_oneunique_secondtable. ((((exists ff_h_pvs_constant_oneunique_secondtableentrypositive. ff_h_pvs_constant_oneunique_secondtableentrypositive + S (dst_positive_constant_oneunique_secondtable) = S ((S (dst_index_constant_oneunique_secondtable)) * dst_positive_scale_constant_oneunique_secondtable)) /\ exists ff_q_pvs_constant_oneunique_secondtableentrypositive. dst_positive_code_constant_oneunique_secondtable = ff_q_pvs_constant_oneunique_secondtableentrypositive * S ((S (dst_index_constant_oneunique_secondtable)) * dst_positive_scale_constant_oneunique_secondtable) + (dst_positive_constant_oneunique_secondtable))) /\ (((((exists ff_h_pvs_constant_oneunique_secondtableentrynegative. ff_h_pvs_constant_oneunique_secondtableentrynegative + S (dst_negative_constant_oneunique_secondtable) = S ((S (dst_index_constant_oneunique_secondtable)) * dst_negative_scale_constant_oneunique_secondtable)) /\ exists ff_q_pvs_constant_oneunique_secondtableentrynegative. dst_negative_code_constant_oneunique_secondtable = ff_q_pvs_constant_oneunique_secondtableentrynegative * S ((S (dst_index_constant_oneunique_secondtable)) * dst_negative_scale_constant_oneunique_secondtable) + (dst_negative_constant_oneunique_secondtable))) /\ (exists ge_balance_positive_constant_oneunique_secondtableentryvalue ge_balance_negative_constant_oneunique_secondtableentryvalue. (((((dst_value_constant_oneunique_secondtable) = 2 * (ge_balance_positive_constant_oneunique_secondtableentryvalue) /\ (ge_balance_negative_constant_oneunique_secondtableentryvalue) = 0) \/ exists ge_signed_half_constant_oneunique_secondtableentryvaluedecode. (((dst_value_constant_oneunique_secondtable) = 2 * ge_signed_half_constant_oneunique_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_constant_oneunique_secondtableentryvalue) = 0) /\ (ge_balance_negative_constant_oneunique_secondtableentryvalue) = S ge_signed_half_constant_oneunique_secondtableentryvaluedecode))) /\ ((dst_positive_constant_oneunique_secondtable) + ge_balance_negative_constant_oneunique_secondtableentryvalue = (dst_negative_constant_oneunique_secondtable) + ge_balance_positive_constant_oneunique_secondtableentryvalue))))))))) /\ (forall du_index_constant_oneunique_second du_value_constant_oneunique_second. ~(du_index_constant_oneunique_second=0) -> (exists pvs_le_gap_constant_oneunique_secondbound. pvs_le_gap_constant_oneunique_secondbound + (du_index_constant_oneunique_second) = (N)) -> (exists dst_positive_code_constant_oneunique_secondentry dst_positive_scale_constant_oneunique_secondentry dst_negative_code_constant_oneunique_secondentry dst_negative_scale_constant_oneunique_secondentry dst_positive_constant_oneunique_secondentry dst_negative_constant_oneunique_secondentry. (((G) = (((((dst_positive_code_constant_oneunique_secondentry) + (dst_positive_scale_constant_oneunique_secondentry)) * S ((dst_positive_code_constant_oneunique_secondentry) + (dst_positive_scale_constant_oneunique_secondentry)) + ((dst_positive_scale_constant_oneunique_secondentry) + (dst_positive_scale_constant_oneunique_secondentry))) + (((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) * S ((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) + ((dst_negative_scale_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)))) * S ((((dst_positive_code_constant_oneunique_secondentry) + (dst_positive_scale_constant_oneunique_secondentry)) * S ((dst_positive_code_constant_oneunique_secondentry) + (dst_positive_scale_constant_oneunique_secondentry)) + ((dst_positive_scale_constant_oneunique_secondentry) + (dst_positive_scale_constant_oneunique_secondentry))) + (((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) * S ((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) + ((dst_negative_scale_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)))) + ((((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) * S ((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) + ((dst_negative_scale_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry))) + (((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) * S ((dst_negative_code_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)) + ((dst_negative_scale_constant_oneunique_secondentry) + (dst_negative_scale_constant_oneunique_secondentry)))))) /\ (((((exists ff_h_pvs_constant_oneunique_secondentrypositive. ff_h_pvs_constant_oneunique_secondentrypositive + S (dst_positive_constant_oneunique_secondentry) = S ((S (du_index_constant_oneunique_second)) * dst_positive_scale_constant_oneunique_secondentry)) /\ exists ff_q_pvs_constant_oneunique_secondentrypositive. dst_positive_code_constant_oneunique_secondentry = ff_q_pvs_constant_oneunique_secondentrypositive * S ((S (du_index_constant_oneunique_second)) * dst_positive_scale_constant_oneunique_secondentry) + (dst_positive_constant_oneunique_secondentry))) /\ (((((exists ff_h_pvs_constant_oneunique_secondentrynegative. ff_h_pvs_constant_oneunique_secondentrynegative + S (dst_negative_constant_oneunique_secondentry) = S ((S (du_index_constant_oneunique_second)) * dst_negative_scale_constant_oneunique_secondentry)) /\ exists ff_q_pvs_constant_oneunique_secondentrynegative. dst_negative_code_constant_oneunique_secondentry = ff_q_pvs_constant_oneunique_secondentrynegative * S ((S (du_index_constant_oneunique_second)) * dst_negative_scale_constant_oneunique_secondentry) + (dst_negative_constant_oneunique_secondentry))) /\ (exists ge_balance_positive_constant_oneunique_secondentryvalue ge_balance_negative_constant_oneunique_secondentryvalue. (((((du_value_constant_oneunique_second) = 2 * (ge_balance_positive_constant_oneunique_secondentryvalue) /\ (ge_balance_negative_constant_oneunique_secondentryvalue) = 0) \/ exists ge_signed_half_constant_oneunique_secondentryvaluedecode. (((du_value_constant_oneunique_second) = 2 * ge_signed_half_constant_oneunique_secondentryvaluedecode + 1 /\ (ge_balance_positive_constant_oneunique_secondentryvalue) = 0) /\ (ge_balance_negative_constant_oneunique_secondentryvalue) = S ge_signed_half_constant_oneunique_secondentryvaluedecode))) /\ ((dst_positive_constant_oneunique_secondentry) + ge_balance_negative_constant_oneunique_secondentryvalue = (dst_negative_constant_oneunique_secondentry) + ge_balance_positive_constant_oneunique_secondentryvalue))))))))) -> du_value_constant_oneunique_second=2))) -> (forall dm_index_constant_oneunique_result dm_first_value_constant_oneunique_result dm_second_value_constant_oneunique_result. ~(dm_index_constant_oneunique_result=0) -> (exists pvs_le_gap_constant_oneunique_resultdomain. pvs_le_gap_constant_oneunique_resultdomain + (dm_index_constant_oneunique_result) = (N)) -> (exists dst_positive_code_constant_oneunique_resultfirst dst_positive_scale_constant_oneunique_resultfirst dst_negative_code_constant_oneunique_resultfirst dst_negative_scale_constant_oneunique_resultfirst dst_positive_constant_oneunique_resultfirst dst_negative_constant_oneunique_resultfirst. (((F) = (((((dst_positive_code_constant_oneunique_resultfirst) + (dst_positive_scale_constant_oneunique_resultfirst)) * S ((dst_positive_code_constant_oneunique_resultfirst) + (dst_positive_scale_constant_oneunique_resultfirst)) + ((dst_positive_scale_constant_oneunique_resultfirst) + (dst_positive_scale_constant_oneunique_resultfirst))) + (((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) * S ((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) + ((dst_negative_scale_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)))) * S ((((dst_positive_code_constant_oneunique_resultfirst) + (dst_positive_scale_constant_oneunique_resultfirst)) * S ((dst_positive_code_constant_oneunique_resultfirst) + (dst_positive_scale_constant_oneunique_resultfirst)) + ((dst_positive_scale_constant_oneunique_resultfirst) + (dst_positive_scale_constant_oneunique_resultfirst))) + (((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) * S ((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) + ((dst_negative_scale_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)))) + ((((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) * S ((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) + ((dst_negative_scale_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst))) + (((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) * S ((dst_negative_code_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)) + ((dst_negative_scale_constant_oneunique_resultfirst) + (dst_negative_scale_constant_oneunique_resultfirst)))))) /\ (((((exists ff_h_pvs_constant_oneunique_resultfirstpositive. ff_h_pvs_constant_oneunique_resultfirstpositive + S (dst_positive_constant_oneunique_resultfirst) = S ((S (dm_index_constant_oneunique_result)) * dst_positive_scale_constant_oneunique_resultfirst)) /\ exists ff_q_pvs_constant_oneunique_resultfirstpositive. dst_positive_code_constant_oneunique_resultfirst = ff_q_pvs_constant_oneunique_resultfirstpositive * S ((S (dm_index_constant_oneunique_result)) * dst_positive_scale_constant_oneunique_resultfirst) + (dst_positive_constant_oneunique_resultfirst))) /\ (((((exists ff_h_pvs_constant_oneunique_resultfirstnegative. ff_h_pvs_constant_oneunique_resultfirstnegative + S (dst_negative_constant_oneunique_resultfirst) = S ((S (dm_index_constant_oneunique_result)) * dst_negative_scale_constant_oneunique_resultfirst)) /\ exists ff_q_pvs_constant_oneunique_resultfirstnegative. dst_negative_code_constant_oneunique_resultfirst = ff_q_pvs_constant_oneunique_resultfirstnegative * S ((S (dm_index_constant_oneunique_result)) * dst_negative_scale_constant_oneunique_resultfirst) + (dst_negative_constant_oneunique_resultfirst))) /\ (exists ge_balance_positive_constant_oneunique_resultfirstvalue ge_balance_negative_constant_oneunique_resultfirstvalue. (((((dm_first_value_constant_oneunique_result) = 2 * (ge_balance_positive_constant_oneunique_resultfirstvalue) /\ (ge_balance_negative_constant_oneunique_resultfirstvalue) = 0) \/ exists ge_signed_half_constant_oneunique_resultfirstvaluedecode. (((dm_first_value_constant_oneunique_result) = 2 * ge_signed_half_constant_oneunique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_constant_oneunique_resultfirstvalue) = 0) /\ (ge_balance_negative_constant_oneunique_resultfirstvalue) = S ge_signed_half_constant_oneunique_resultfirstvaluedecode))) /\ ((dst_positive_constant_oneunique_resultfirst) + ge_balance_negative_constant_oneunique_resultfirstvalue = (dst_negative_constant_oneunique_resultfirst) + ge_balance_positive_constant_oneunique_resultfirstvalue))))))))) -> (exists dst_positive_code_constant_oneunique_resultsecond dst_positive_scale_constant_oneunique_resultsecond dst_negative_code_constant_oneunique_resultsecond dst_negative_scale_constant_oneunique_resultsecond dst_positive_constant_oneunique_resultsecond dst_negative_constant_oneunique_resultsecond. (((G) = (((((dst_positive_code_constant_oneunique_resultsecond) + (dst_positive_scale_constant_oneunique_resultsecond)) * S ((dst_positive_code_constant_oneunique_resultsecond) + (dst_positive_scale_constant_oneunique_resultsecond)) + ((dst_positive_scale_constant_oneunique_resultsecond) + (dst_positive_scale_constant_oneunique_resultsecond))) + (((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) * S ((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) + ((dst_negative_scale_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)))) * S ((((dst_positive_code_constant_oneunique_resultsecond) + (dst_positive_scale_constant_oneunique_resultsecond)) * S ((dst_positive_code_constant_oneunique_resultsecond) + (dst_positive_scale_constant_oneunique_resultsecond)) + ((dst_positive_scale_constant_oneunique_resultsecond) + (dst_positive_scale_constant_oneunique_resultsecond))) + (((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) * S ((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) + ((dst_negative_scale_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)))) + ((((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) * S ((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) + ((dst_negative_scale_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond))) + (((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) * S ((dst_negative_code_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)) + ((dst_negative_scale_constant_oneunique_resultsecond) + (dst_negative_scale_constant_oneunique_resultsecond)))))) /\ (((((exists ff_h_pvs_constant_oneunique_resultsecondpositive. ff_h_pvs_constant_oneunique_resultsecondpositive + S (dst_positive_constant_oneunique_resultsecond) = S ((S (dm_index_constant_oneunique_result)) * dst_positive_scale_constant_oneunique_resultsecond)) /\ exists ff_q_pvs_constant_oneunique_resultsecondpositive. dst_positive_code_constant_oneunique_resultsecond = ff_q_pvs_constant_oneunique_resultsecondpositive * S ((S (dm_index_constant_oneunique_result)) * dst_positive_scale_constant_oneunique_resultsecond) + (dst_positive_constant_oneunique_resultsecond))) /\ (((((exists ff_h_pvs_constant_oneunique_resultsecondnegative. ff_h_pvs_constant_oneunique_resultsecondnegative + S (dst_negative_constant_oneunique_resultsecond) = S ((S (dm_index_constant_oneunique_result)) * dst_negative_scale_constant_oneunique_resultsecond)) /\ exists ff_q_pvs_constant_oneunique_resultsecondnegative. dst_negative_code_constant_oneunique_resultsecond = ff_q_pvs_constant_oneunique_resultsecondnegative * S ((S (dm_index_constant_oneunique_result)) * dst_negative_scale_constant_oneunique_resultsecond) + (dst_negative_constant_oneunique_resultsecond))) /\ (exists ge_balance_positive_constant_oneunique_resultsecondvalue ge_balance_negative_constant_oneunique_resultsecondvalue. (((((dm_second_value_constant_oneunique_result) = 2 * (ge_balance_positive_constant_oneunique_resultsecondvalue) /\ (ge_balance_negative_constant_oneunique_resultsecondvalue) = 0) \/ exists ge_signed_half_constant_oneunique_resultsecondvaluedecode. (((dm_second_value_constant_oneunique_result) = 2 * ge_signed_half_constant_oneunique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_constant_oneunique_resultsecondvalue) = 0) /\ (ge_balance_negative_constant_oneunique_resultsecondvalue) = S ge_signed_half_constant_oneunique_resultsecondvaluedecode))) /\ ((dst_positive_constant_oneunique_resultsecond) + ge_balance_negative_constant_oneunique_resultsecondvalue = (dst_negative_constant_oneunique_resultsecond) + ge_balance_positive_constant_oneunique_resultsecondvalue))))))))) -> dm_first_value_constant_oneunique_result=dm_second_value_constant_oneunique_result)