dirichlet_kronecker_delta_table_positive_unique

Exact expanded first-order arithmetic statement

forall N F G. (((exists dst_positive_code_kronecker_deltaunique_firsttable dst_positive_scale_kronecker_deltaunique_firsttable dst_negative_code_kronecker_deltaunique_firsttable dst_negative_scale_kronecker_deltaunique_firsttable. (((F) = (((((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) * S ((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) + ((dst_positive_scale_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable))) + (((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)))) * S ((((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) * S ((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) + ((dst_positive_scale_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable))) + (((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)))) + ((((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable))) + (((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)))))) /\ (forall dst_index_kronecker_deltaunique_firsttable. (exists pvs_le_gap_kronecker_deltaunique_firsttabledomain. pvs_le_gap_kronecker_deltaunique_firsttabledomain + (dst_index_kronecker_deltaunique_firsttable) = (N)) -> exists dst_positive_kronecker_deltaunique_firsttable dst_negative_kronecker_deltaunique_firsttable dst_value_kronecker_deltaunique_firsttable. ((((exists ff_h_pvs_kronecker_deltaunique_firsttableentrypositive. ff_h_pvs_kronecker_deltaunique_firsttableentrypositive + S (dst_positive_kronecker_deltaunique_firsttable) = S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_positive_scale_kronecker_deltaunique_firsttable)) /\ exists ff_q_pvs_kronecker_deltaunique_firsttableentrypositive. dst_positive_code_kronecker_deltaunique_firsttable = ff_q_pvs_kronecker_deltaunique_firsttableentrypositive * S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_positive_scale_kronecker_deltaunique_firsttable) + (dst_positive_kronecker_deltaunique_firsttable))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_firsttableentrynegative. ff_h_pvs_kronecker_deltaunique_firsttableentrynegative + S (dst_negative_kronecker_deltaunique_firsttable) = S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_negative_scale_kronecker_deltaunique_firsttable)) /\ exists ff_q_pvs_kronecker_deltaunique_firsttableentrynegative. dst_negative_code_kronecker_deltaunique_firsttable = ff_q_pvs_kronecker_deltaunique_firsttableentrynegative * S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_kronecker_deltaunique_firsttable))) /\ (exists ge_balance_positive_kronecker_deltaunique_firsttableentryvalue ge_balance_negative_kronecker_deltaunique_firsttableentryvalue. (((((dst_value_kronecker_deltaunique_firsttable) = 2 * (ge_balance_positive_kronecker_deltaunique_firsttableentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_firsttableentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_firsttableentryvaluedecode. (((dst_value_kronecker_deltaunique_firsttable) = 2 * ge_signed_half_kronecker_deltaunique_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_firsttableentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_firsttableentryvalue) = S ge_signed_half_kronecker_deltaunique_firsttableentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_firsttable) + ge_balance_negative_kronecker_deltaunique_firsttableentryvalue = (dst_negative_kronecker_deltaunique_firsttable) + ge_balance_positive_kronecker_deltaunique_firsttableentryvalue))))))))) /\ (forall du_index_kronecker_deltaunique_first du_value_kronecker_deltaunique_first. ~(du_index_kronecker_deltaunique_first=0) -> (exists pvs_le_gap_kronecker_deltaunique_firstbound. pvs_le_gap_kronecker_deltaunique_firstbound + (du_index_kronecker_deltaunique_first) = (N)) -> (exists dst_positive_code_kronecker_deltaunique_firstentry dst_positive_scale_kronecker_deltaunique_firstentry dst_negative_code_kronecker_deltaunique_firstentry dst_negative_scale_kronecker_deltaunique_firstentry dst_positive_kronecker_deltaunique_firstentry dst_negative_kronecker_deltaunique_firstentry. (((F) = (((((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) * S ((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) + ((dst_positive_scale_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry))) + (((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)))) * S ((((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) * S ((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) + ((dst_positive_scale_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry))) + (((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)))) + ((((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry))) + (((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_firstentrypositive. ff_h_pvs_kronecker_deltaunique_firstentrypositive + S (dst_positive_kronecker_deltaunique_firstentry) = S ((S (du_index_kronecker_deltaunique_first)) * dst_positive_scale_kronecker_deltaunique_firstentry)) /\ exists ff_q_pvs_kronecker_deltaunique_firstentrypositive. dst_positive_code_kronecker_deltaunique_firstentry = ff_q_pvs_kronecker_deltaunique_firstentrypositive * S ((S (du_index_kronecker_deltaunique_first)) * dst_positive_scale_kronecker_deltaunique_firstentry) + (dst_positive_kronecker_deltaunique_firstentry))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_firstentrynegative. ff_h_pvs_kronecker_deltaunique_firstentrynegative + S (dst_negative_kronecker_deltaunique_firstentry) = S ((S (du_index_kronecker_deltaunique_first)) * dst_negative_scale_kronecker_deltaunique_firstentry)) /\ exists ff_q_pvs_kronecker_deltaunique_firstentrynegative. dst_negative_code_kronecker_deltaunique_firstentry = ff_q_pvs_kronecker_deltaunique_firstentrynegative * S ((S (du_index_kronecker_deltaunique_first)) * dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_kronecker_deltaunique_firstentry))) /\ (exists ge_balance_positive_kronecker_deltaunique_firstentryvalue ge_balance_negative_kronecker_deltaunique_firstentryvalue. (((((du_value_kronecker_deltaunique_first) = 2 * (ge_balance_positive_kronecker_deltaunique_firstentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_firstentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_firstentryvaluedecode. (((du_value_kronecker_deltaunique_first) = 2 * ge_signed_half_kronecker_deltaunique_firstentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_firstentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_firstentryvalue) = S ge_signed_half_kronecker_deltaunique_firstentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_firstentry) + ge_balance_negative_kronecker_deltaunique_firstentryvalue = (dst_negative_kronecker_deltaunique_firstentry) + ge_balance_positive_kronecker_deltaunique_firstentryvalue))))))))) -> ((((du_index_kronecker_deltaunique_first)=1 -> (du_value_kronecker_deltaunique_first)=2) /\ (~((du_index_kronecker_deltaunique_first)=1) -> (du_value_kronecker_deltaunique_first)=0)))))) -> (((exists dst_positive_code_kronecker_deltaunique_secondtable dst_positive_scale_kronecker_deltaunique_secondtable dst_negative_code_kronecker_deltaunique_secondtable dst_negative_scale_kronecker_deltaunique_secondtable. (((G) = (((((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) * S ((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) + ((dst_positive_scale_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable))) + (((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)))) * S ((((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) * S ((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) + ((dst_positive_scale_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable))) + (((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)))) + ((((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable))) + (((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)))))) /\ (forall dst_index_kronecker_deltaunique_secondtable. (exists pvs_le_gap_kronecker_deltaunique_secondtabledomain. pvs_le_gap_kronecker_deltaunique_secondtabledomain + (dst_index_kronecker_deltaunique_secondtable) = (N)) -> exists dst_positive_kronecker_deltaunique_secondtable dst_negative_kronecker_deltaunique_secondtable dst_value_kronecker_deltaunique_secondtable. ((((exists ff_h_pvs_kronecker_deltaunique_secondtableentrypositive. ff_h_pvs_kronecker_deltaunique_secondtableentrypositive + S (dst_positive_kronecker_deltaunique_secondtable) = S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_positive_scale_kronecker_deltaunique_secondtable)) /\ exists ff_q_pvs_kronecker_deltaunique_secondtableentrypositive. dst_positive_code_kronecker_deltaunique_secondtable = ff_q_pvs_kronecker_deltaunique_secondtableentrypositive * S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_positive_scale_kronecker_deltaunique_secondtable) + (dst_positive_kronecker_deltaunique_secondtable))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_secondtableentrynegative. ff_h_pvs_kronecker_deltaunique_secondtableentrynegative + S (dst_negative_kronecker_deltaunique_secondtable) = S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_negative_scale_kronecker_deltaunique_secondtable)) /\ exists ff_q_pvs_kronecker_deltaunique_secondtableentrynegative. dst_negative_code_kronecker_deltaunique_secondtable = ff_q_pvs_kronecker_deltaunique_secondtableentrynegative * S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_kronecker_deltaunique_secondtable))) /\ (exists ge_balance_positive_kronecker_deltaunique_secondtableentryvalue ge_balance_negative_kronecker_deltaunique_secondtableentryvalue. (((((dst_value_kronecker_deltaunique_secondtable) = 2 * (ge_balance_positive_kronecker_deltaunique_secondtableentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_secondtableentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_secondtableentryvaluedecode. (((dst_value_kronecker_deltaunique_secondtable) = 2 * ge_signed_half_kronecker_deltaunique_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_secondtableentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_secondtableentryvalue) = S ge_signed_half_kronecker_deltaunique_secondtableentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_secondtable) + ge_balance_negative_kronecker_deltaunique_secondtableentryvalue = (dst_negative_kronecker_deltaunique_secondtable) + ge_balance_positive_kronecker_deltaunique_secondtableentryvalue))))))))) /\ (forall du_index_kronecker_deltaunique_second du_value_kronecker_deltaunique_second. ~(du_index_kronecker_deltaunique_second=0) -> (exists pvs_le_gap_kronecker_deltaunique_secondbound. pvs_le_gap_kronecker_deltaunique_secondbound + (du_index_kronecker_deltaunique_second) = (N)) -> (exists dst_positive_code_kronecker_deltaunique_secondentry dst_positive_scale_kronecker_deltaunique_secondentry dst_negative_code_kronecker_deltaunique_secondentry dst_negative_scale_kronecker_deltaunique_secondentry dst_positive_kronecker_deltaunique_secondentry dst_negative_kronecker_deltaunique_secondentry. (((G) = (((((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) * S ((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) + ((dst_positive_scale_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry))) + (((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)))) * S ((((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) * S ((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) + ((dst_positive_scale_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry))) + (((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)))) + ((((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry))) + (((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_secondentrypositive. ff_h_pvs_kronecker_deltaunique_secondentrypositive + S (dst_positive_kronecker_deltaunique_secondentry) = S ((S (du_index_kronecker_deltaunique_second)) * dst_positive_scale_kronecker_deltaunique_secondentry)) /\ exists ff_q_pvs_kronecker_deltaunique_secondentrypositive. dst_positive_code_kronecker_deltaunique_secondentry = ff_q_pvs_kronecker_deltaunique_secondentrypositive * S ((S (du_index_kronecker_deltaunique_second)) * dst_positive_scale_kronecker_deltaunique_secondentry) + (dst_positive_kronecker_deltaunique_secondentry))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_secondentrynegative. ff_h_pvs_kronecker_deltaunique_secondentrynegative + S (dst_negative_kronecker_deltaunique_secondentry) = S ((S (du_index_kronecker_deltaunique_second)) * dst_negative_scale_kronecker_deltaunique_secondentry)) /\ exists ff_q_pvs_kronecker_deltaunique_secondentrynegative. dst_negative_code_kronecker_deltaunique_secondentry = ff_q_pvs_kronecker_deltaunique_secondentrynegative * S ((S (du_index_kronecker_deltaunique_second)) * dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_kronecker_deltaunique_secondentry))) /\ (exists ge_balance_positive_kronecker_deltaunique_secondentryvalue ge_balance_negative_kronecker_deltaunique_secondentryvalue. (((((du_value_kronecker_deltaunique_second) = 2 * (ge_balance_positive_kronecker_deltaunique_secondentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_secondentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_secondentryvaluedecode. (((du_value_kronecker_deltaunique_second) = 2 * ge_signed_half_kronecker_deltaunique_secondentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_secondentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_secondentryvalue) = S ge_signed_half_kronecker_deltaunique_secondentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_secondentry) + ge_balance_negative_kronecker_deltaunique_secondentryvalue = (dst_negative_kronecker_deltaunique_secondentry) + ge_balance_positive_kronecker_deltaunique_secondentryvalue))))))))) -> ((((du_index_kronecker_deltaunique_second)=1 -> (du_value_kronecker_deltaunique_second)=2) /\ (~((du_index_kronecker_deltaunique_second)=1) -> (du_value_kronecker_deltaunique_second)=0)))))) -> (forall dm_index_kronecker_deltaunique_result dm_first_value_kronecker_deltaunique_result dm_second_value_kronecker_deltaunique_result. ~(dm_index_kronecker_deltaunique_result=0) -> (exists pvs_le_gap_kronecker_deltaunique_resultdomain. pvs_le_gap_kronecker_deltaunique_resultdomain + (dm_index_kronecker_deltaunique_result) = (N)) -> (exists dst_positive_code_kronecker_deltaunique_resultfirst dst_positive_scale_kronecker_deltaunique_resultfirst dst_negative_code_kronecker_deltaunique_resultfirst dst_negative_scale_kronecker_deltaunique_resultfirst dst_positive_kronecker_deltaunique_resultfirst dst_negative_kronecker_deltaunique_resultfirst. (((F) = (((((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) * S ((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) + ((dst_positive_scale_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst))) + (((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)))) * S ((((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) * S ((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) + ((dst_positive_scale_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst))) + (((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)))) + ((((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst))) + (((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultfirstpositive. ff_h_pvs_kronecker_deltaunique_resultfirstpositive + S (dst_positive_kronecker_deltaunique_resultfirst) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultfirst)) /\ exists ff_q_pvs_kronecker_deltaunique_resultfirstpositive. dst_positive_code_kronecker_deltaunique_resultfirst = ff_q_pvs_kronecker_deltaunique_resultfirstpositive * S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultfirst) + (dst_positive_kronecker_deltaunique_resultfirst))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultfirstnegative. ff_h_pvs_kronecker_deltaunique_resultfirstnegative + S (dst_negative_kronecker_deltaunique_resultfirst) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultfirst)) /\ exists ff_q_pvs_kronecker_deltaunique_resultfirstnegative. dst_negative_code_kronecker_deltaunique_resultfirst = ff_q_pvs_kronecker_deltaunique_resultfirstnegative * S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_kronecker_deltaunique_resultfirst))) /\ (exists ge_balance_positive_kronecker_deltaunique_resultfirstvalue ge_balance_negative_kronecker_deltaunique_resultfirstvalue. (((((dm_first_value_kronecker_deltaunique_result) = 2 * (ge_balance_positive_kronecker_deltaunique_resultfirstvalue) /\ (ge_balance_negative_kronecker_deltaunique_resultfirstvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_resultfirstvaluedecode. (((dm_first_value_kronecker_deltaunique_result) = 2 * ge_signed_half_kronecker_deltaunique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_resultfirstvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_resultfirstvalue) = S ge_signed_half_kronecker_deltaunique_resultfirstvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_resultfirst) + ge_balance_negative_kronecker_deltaunique_resultfirstvalue = (dst_negative_kronecker_deltaunique_resultfirst) + ge_balance_positive_kronecker_deltaunique_resultfirstvalue))))))))) -> (exists dst_positive_code_kronecker_deltaunique_resultsecond dst_positive_scale_kronecker_deltaunique_resultsecond dst_negative_code_kronecker_deltaunique_resultsecond dst_negative_scale_kronecker_deltaunique_resultsecond dst_positive_kronecker_deltaunique_resultsecond dst_negative_kronecker_deltaunique_resultsecond. (((G) = (((((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) * S ((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) + ((dst_positive_scale_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond))) + (((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)))) * S ((((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) * S ((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) + ((dst_positive_scale_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond))) + (((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)))) + ((((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond))) + (((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultsecondpositive. ff_h_pvs_kronecker_deltaunique_resultsecondpositive + S (dst_positive_kronecker_deltaunique_resultsecond) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultsecond)) /\ exists ff_q_pvs_kronecker_deltaunique_resultsecondpositive. dst_positive_code_kronecker_deltaunique_resultsecond = ff_q_pvs_kronecker_deltaunique_resultsecondpositive * S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultsecond) + (dst_positive_kronecker_deltaunique_resultsecond))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultsecondnegative. ff_h_pvs_kronecker_deltaunique_resultsecondnegative + S (dst_negative_kronecker_deltaunique_resultsecond) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultsecond)) /\ exists ff_q_pvs_kronecker_deltaunique_resultsecondnegative. dst_negative_code_kronecker_deltaunique_resultsecond = ff_q_pvs_kronecker_deltaunique_resultsecondnegative * S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_kronecker_deltaunique_resultsecond))) /\ (exists ge_balance_positive_kronecker_deltaunique_resultsecondvalue ge_balance_negative_kronecker_deltaunique_resultsecondvalue. (((((dm_second_value_kronecker_deltaunique_result) = 2 * (ge_balance_positive_kronecker_deltaunique_resultsecondvalue) /\ (ge_balance_negative_kronecker_deltaunique_resultsecondvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_resultsecondvaluedecode. (((dm_second_value_kronecker_deltaunique_result) = 2 * ge_signed_half_kronecker_deltaunique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_resultsecondvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_resultsecondvalue) = S ge_signed_half_kronecker_deltaunique_resultsecondvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_resultsecond) + ge_balance_negative_kronecker_deltaunique_resultsecondvalue = (dst_negative_kronecker_deltaunique_resultsecond) + ge_balance_positive_kronecker_deltaunique_resultsecondvalue))))))))) -> dm_first_value_kronecker_deltaunique_result=dm_second_value_kronecker_deltaunique_result)