mobius_table_extensional

Exact expanded first-order arithmetic statement

forall N F G. (((exists dst_positive_code_unique_firsttable dst_positive_scale_unique_firsttable dst_negative_code_unique_firsttable dst_negative_scale_unique_firsttable. (((F) = (((((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) * S ((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) + ((dst_positive_scale_unique_firsttable) + (dst_positive_scale_unique_firsttable))) + (((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable)))) * S ((((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) * S ((dst_positive_code_unique_firsttable) + (dst_positive_scale_unique_firsttable)) + ((dst_positive_scale_unique_firsttable) + (dst_positive_scale_unique_firsttable))) + (((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable)))) + ((((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable))) + (((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) * S ((dst_negative_code_unique_firsttable) + (dst_negative_scale_unique_firsttable)) + ((dst_negative_scale_unique_firsttable) + (dst_negative_scale_unique_firsttable)))))) /\ (forall dst_index_unique_firsttable. (exists pvs_le_gap_unique_firsttabledomain. pvs_le_gap_unique_firsttabledomain + (dst_index_unique_firsttable) = (N)) -> exists dst_positive_unique_firsttable dst_negative_unique_firsttable dst_value_unique_firsttable. ((((exists ff_h_pvs_unique_firsttableentrypositive. ff_h_pvs_unique_firsttableentrypositive + S (dst_positive_unique_firsttable) = S ((S (dst_index_unique_firsttable)) * dst_positive_scale_unique_firsttable)) /\ exists ff_q_pvs_unique_firsttableentrypositive. dst_positive_code_unique_firsttable = ff_q_pvs_unique_firsttableentrypositive * S ((S (dst_index_unique_firsttable)) * dst_positive_scale_unique_firsttable) + (dst_positive_unique_firsttable))) /\ (((((exists ff_h_pvs_unique_firsttableentrynegative. ff_h_pvs_unique_firsttableentrynegative + S (dst_negative_unique_firsttable) = S ((S (dst_index_unique_firsttable)) * dst_negative_scale_unique_firsttable)) /\ exists ff_q_pvs_unique_firsttableentrynegative. dst_negative_code_unique_firsttable = ff_q_pvs_unique_firsttableentrynegative * S ((S (dst_index_unique_firsttable)) * dst_negative_scale_unique_firsttable) + (dst_negative_unique_firsttable))) /\ (exists ge_balance_positive_unique_firsttableentryvalue ge_balance_negative_unique_firsttableentryvalue. (((((dst_value_unique_firsttable) = 2 * (ge_balance_positive_unique_firsttableentryvalue) /\ (ge_balance_negative_unique_firsttableentryvalue) = 0) \/ exists ge_signed_half_unique_firsttableentryvaluedecode. (((dst_value_unique_firsttable) = 2 * ge_signed_half_unique_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_unique_firsttableentryvalue) = 0) /\ (ge_balance_negative_unique_firsttableentryvalue) = S ge_signed_half_unique_firsttableentryvaluedecode))) /\ ((dst_positive_unique_firsttable) + ge_balance_negative_unique_firsttableentryvalue = (dst_negative_unique_firsttable) + ge_balance_positive_unique_firsttableentryvalue))))))))) /\ (((exists dst_positive_code_unique_firstzero dst_positive_scale_unique_firstzero dst_negative_code_unique_firstzero dst_negative_scale_unique_firstzero dst_positive_unique_firstzero dst_negative_unique_firstzero. (((F) = (((((dst_positive_code_unique_firstzero) + (dst_positive_scale_unique_firstzero)) * S ((dst_positive_code_unique_firstzero) + (dst_positive_scale_unique_firstzero)) + ((dst_positive_scale_unique_firstzero) + (dst_positive_scale_unique_firstzero))) + (((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) * S ((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) + ((dst_negative_scale_unique_firstzero) + (dst_negative_scale_unique_firstzero)))) * S ((((dst_positive_code_unique_firstzero) + (dst_positive_scale_unique_firstzero)) * S ((dst_positive_code_unique_firstzero) + (dst_positive_scale_unique_firstzero)) + ((dst_positive_scale_unique_firstzero) + (dst_positive_scale_unique_firstzero))) + (((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) * S ((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) + ((dst_negative_scale_unique_firstzero) + (dst_negative_scale_unique_firstzero)))) + ((((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) * S ((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) + ((dst_negative_scale_unique_firstzero) + (dst_negative_scale_unique_firstzero))) + (((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) * S ((dst_negative_code_unique_firstzero) + (dst_negative_scale_unique_firstzero)) + ((dst_negative_scale_unique_firstzero) + (dst_negative_scale_unique_firstzero)))))) /\ (((((exists ff_h_pvs_unique_firstzeropositive. ff_h_pvs_unique_firstzeropositive + S (dst_positive_unique_firstzero) = S ((S (0)) * dst_positive_scale_unique_firstzero)) /\ exists ff_q_pvs_unique_firstzeropositive. dst_positive_code_unique_firstzero = ff_q_pvs_unique_firstzeropositive * S ((S (0)) * dst_positive_scale_unique_firstzero) + (dst_positive_unique_firstzero))) /\ (((((exists ff_h_pvs_unique_firstzeronegative. ff_h_pvs_unique_firstzeronegative + S (dst_negative_unique_firstzero) = S ((S (0)) * dst_negative_scale_unique_firstzero)) /\ exists ff_q_pvs_unique_firstzeronegative. dst_negative_code_unique_firstzero = ff_q_pvs_unique_firstzeronegative * S ((S (0)) * dst_negative_scale_unique_firstzero) + (dst_negative_unique_firstzero))) /\ (exists ge_balance_positive_unique_firstzerovalue ge_balance_negative_unique_firstzerovalue. (((((0) = 2 * (ge_balance_positive_unique_firstzerovalue) /\ (ge_balance_negative_unique_firstzerovalue) = 0) \/ exists ge_signed_half_unique_firstzerovaluedecode. (((0) = 2 * ge_signed_half_unique_firstzerovaluedecode + 1 /\ (ge_balance_positive_unique_firstzerovalue) = 0) /\ (ge_balance_negative_unique_firstzerovalue) = S ge_signed_half_unique_firstzerovaluedecode))) /\ ((dst_positive_unique_firstzero) + ge_balance_negative_unique_firstzerovalue = (dst_negative_unique_firstzero) + ge_balance_positive_unique_firstzerovalue))))))))) /\ (forall mt_index_unique_first mt_value_unique_first. ~(mt_index_unique_first=0) -> (exists pvs_le_gap_unique_firstdomain. pvs_le_gap_unique_firstdomain + (mt_index_unique_first) = (N)) -> (exists dst_positive_code_unique_firstentry dst_positive_scale_unique_firstentry dst_negative_code_unique_firstentry dst_negative_scale_unique_firstentry dst_positive_unique_firstentry dst_negative_unique_firstentry. (((F) = (((((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) * S ((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) + ((dst_positive_scale_unique_firstentry) + (dst_positive_scale_unique_firstentry))) + (((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry)))) * S ((((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) * S ((dst_positive_code_unique_firstentry) + (dst_positive_scale_unique_firstentry)) + ((dst_positive_scale_unique_firstentry) + (dst_positive_scale_unique_firstentry))) + (((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry)))) + ((((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry))) + (((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) * S ((dst_negative_code_unique_firstentry) + (dst_negative_scale_unique_firstentry)) + ((dst_negative_scale_unique_firstentry) + (dst_negative_scale_unique_firstentry)))))) /\ (((((exists ff_h_pvs_unique_firstentrypositive. ff_h_pvs_unique_firstentrypositive + S (dst_positive_unique_firstentry) = S ((S (mt_index_unique_first)) * dst_positive_scale_unique_firstentry)) /\ exists ff_q_pvs_unique_firstentrypositive. dst_positive_code_unique_firstentry = ff_q_pvs_unique_firstentrypositive * S ((S (mt_index_unique_first)) * dst_positive_scale_unique_firstentry) + (dst_positive_unique_firstentry))) /\ (((((exists ff_h_pvs_unique_firstentrynegative. ff_h_pvs_unique_firstentrynegative + S (dst_negative_unique_firstentry) = S ((S (mt_index_unique_first)) * dst_negative_scale_unique_firstentry)) /\ exists ff_q_pvs_unique_firstentrynegative. dst_negative_code_unique_firstentry = ff_q_pvs_unique_firstentrynegative * S ((S (mt_index_unique_first)) * dst_negative_scale_unique_firstentry) + (dst_negative_unique_firstentry))) /\ (exists ge_balance_positive_unique_firstentryvalue ge_balance_negative_unique_firstentryvalue. (((((mt_value_unique_first) = 2 * (ge_balance_positive_unique_firstentryvalue) /\ (ge_balance_negative_unique_firstentryvalue) = 0) \/ exists ge_signed_half_unique_firstentryvaluedecode. (((mt_value_unique_first) = 2 * ge_signed_half_unique_firstentryvaluedecode + 1 /\ (ge_balance_positive_unique_firstentryvalue) = 0) /\ (ge_balance_negative_unique_firstentryvalue) = S ge_signed_half_unique_firstentryvaluedecode))) /\ ((dst_positive_unique_firstentry) + ge_balance_negative_unique_firstentryvalue = (dst_negative_unique_firstentry) + ge_balance_positive_unique_firstentryvalue))))))))) -> (((~((mt_index_unique_first) = 0)) /\ ((((exists mv_square_prime_unique_firstvaluesquare. ((~((mv_square_prime_unique_firstvaluesquare) = 1) /\ forall pvs_left_unique_firstvaluesquareprime pvs_right_unique_firstvaluesquareprime. (mv_square_prime_unique_firstvaluesquare) = pvs_left_unique_firstvaluesquareprime * pvs_right_unique_firstvaluesquareprime -> pvs_left_unique_firstvaluesquareprime = 1 \/ pvs_right_unique_firstvaluesquareprime = 1) /\ (exists pvs_factor_unique_firstvaluesquaredivisor. (mt_index_unique_first) = (mv_square_prime_unique_firstvaluesquare * mv_square_prime_unique_firstvaluesquare) * pvs_factor_unique_firstvaluesquaredivisor))) /\ ((mt_value_unique_first) = 0))) \/ (((((~((mt_index_unique_first) = 0)) /\ (forall sfd_prime_unique_firstvaluesquarefree. (~((sfd_prime_unique_firstvaluesquarefree) = 1) /\ forall pvs_left_unique_firstvaluesquarefreedomain pvs_right_unique_firstvaluesquarefreedomain. (sfd_prime_unique_firstvaluesquarefree) = pvs_left_unique_firstvaluesquarefreedomain * pvs_right_unique_firstvaluesquarefreedomain -> pvs_left_unique_firstvaluesquarefreedomain = 1 \/ pvs_right_unique_firstvaluesquarefreedomain = 1) -> (exists pvs_le_gap_unique_firstvaluesquarefreebound. pvs_le_gap_unique_firstvaluesquarefreebound + (sfd_prime_unique_firstvaluesquarefree) = (mt_index_unique_first)) -> ~(exists pvs_factor_unique_firstvaluesquarefreesquare. (mt_index_unique_first) = (sfd_prime_unique_firstvaluesquarefree * sfd_prime_unique_firstvaluesquarefree) * pvs_factor_unique_firstvaluesquarefreesquare)))) /\ (exists mv_factor_code_unique_firstvaluefactors mv_factor_scale_unique_firstvaluefactors mv_factor_count_unique_firstvaluefactors. (((~(mt_index_unique_first = 0) /\ ((exists ff_u_fsat_unique_firstvaluefactorsfactorization_product ff_v_fsat_unique_firstvaluefactorsfactorization_product. ((((exists ff_h_fsat_unique_firstvaluefactorsfactorization_product_start. ff_h_fsat_unique_firstvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_firstvaluefactorsfactorization_product_start. ff_u_fsat_unique_firstvaluefactorsfactorization_product = ff_q_fsat_unique_firstvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_unique_firstvaluefactorsfactorization_product_terminal. ff_h_fsat_unique_firstvaluefactorsfactorization_product_terminal + S (mt_index_unique_first) = S ((S (mv_factor_count_unique_firstvaluefactors)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_firstvaluefactorsfactorization_product_terminal. ff_u_fsat_unique_firstvaluefactorsfactorization_product = ff_q_fsat_unique_firstvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_unique_firstvaluefactors)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product) + (mt_index_unique_first))) /\ forall ff_i_fsat_unique_firstvaluefactorsfactorization_product. (exists ff_lt_fsat_unique_firstvaluefactorsfactorization_product_bound. ff_lt_fsat_unique_firstvaluefactorsfactorization_product_bound + S ff_i_fsat_unique_firstvaluefactorsfactorization_product = mv_factor_count_unique_firstvaluefactors) -> exists ff_p_fsat_unique_firstvaluefactorsfactorization_product ff_r_fsat_unique_firstvaluefactorsfactorization_product ff_s_fsat_unique_firstvaluefactorsfactorization_product. ((((exists ff_h_fsat_unique_firstvaluefactorsfactorization_product_factor. ff_h_fsat_unique_firstvaluefactorsfactorization_product_factor + S (ff_p_fsat_unique_firstvaluefactorsfactorization_product) = S ((S (ff_i_fsat_unique_firstvaluefactorsfactorization_product)) * mv_factor_scale_unique_firstvaluefactors)) /\ exists ff_q_fsat_unique_firstvaluefactorsfactorization_product_factor. mv_factor_code_unique_firstvaluefactors = ff_q_fsat_unique_firstvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_unique_firstvaluefactorsfactorization_product)) * mv_factor_scale_unique_firstvaluefactors) + (ff_p_fsat_unique_firstvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_firstvaluefactorsfactorization_product_partial. ff_h_fsat_unique_firstvaluefactorsfactorization_product_partial + S (ff_r_fsat_unique_firstvaluefactorsfactorization_product) = S ((S (ff_i_fsat_unique_firstvaluefactorsfactorization_product)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_firstvaluefactorsfactorization_product_partial. ff_u_fsat_unique_firstvaluefactorsfactorization_product = ff_q_fsat_unique_firstvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_unique_firstvaluefactorsfactorization_product)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product) + (ff_r_fsat_unique_firstvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_firstvaluefactorsfactorization_product_successor. ff_h_fsat_unique_firstvaluefactorsfactorization_product_successor + S (ff_s_fsat_unique_firstvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_unique_firstvaluefactorsfactorization_product)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_firstvaluefactorsfactorization_product_successor. ff_u_fsat_unique_firstvaluefactorsfactorization_product = ff_q_fsat_unique_firstvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_unique_firstvaluefactorsfactorization_product)) * ff_v_fsat_unique_firstvaluefactorsfactorization_product) + (ff_s_fsat_unique_firstvaluefactorsfactorization_product))) /\ ff_s_fsat_unique_firstvaluefactorsfactorization_product = ff_r_fsat_unique_firstvaluefactorsfactorization_product * ff_p_fsat_unique_firstvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_unique_firstvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_unique_firstvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_unique_firstvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_unique_firstvaluefactorsfactorization_primes = (mv_factor_count_unique_firstvaluefactors)) -> exists ftsf_factor_fsat_unique_firstvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_unique_firstvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_unique_firstvaluefactorsfactorization_primes)) * mv_factor_scale_unique_firstvaluefactors)) /\ exists ff_q_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_entry. mv_factor_code_unique_firstvaluefactors = ff_q_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_unique_firstvaluefactorsfactorization_primes)) * mv_factor_scale_unique_firstvaluefactors) + (ftsf_factor_fsat_unique_firstvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_unique_firstvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_unique_firstvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_unique_firstvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_unique_firstvaluefactorsparityeven. (mv_factor_count_unique_firstvaluefactors) = 2 * mv_even_half_unique_firstvaluefactorsparityeven) /\ ((mt_value_unique_first) = 2))) \/ (((exists mv_odd_half_unique_firstvaluefactorsparityodd. (mv_factor_count_unique_firstvaluefactors) = 2 * mv_odd_half_unique_firstvaluefactorsparityodd + 1) /\ ((mt_value_unique_first) = 1)))))))))))))))) -> (((exists dst_positive_code_unique_secondtable dst_positive_scale_unique_secondtable dst_negative_code_unique_secondtable dst_negative_scale_unique_secondtable. (((G) = (((((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) * S ((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) + ((dst_positive_scale_unique_secondtable) + (dst_positive_scale_unique_secondtable))) + (((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable)))) * S ((((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) * S ((dst_positive_code_unique_secondtable) + (dst_positive_scale_unique_secondtable)) + ((dst_positive_scale_unique_secondtable) + (dst_positive_scale_unique_secondtable))) + (((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable)))) + ((((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable))) + (((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) * S ((dst_negative_code_unique_secondtable) + (dst_negative_scale_unique_secondtable)) + ((dst_negative_scale_unique_secondtable) + (dst_negative_scale_unique_secondtable)))))) /\ (forall dst_index_unique_secondtable. (exists pvs_le_gap_unique_secondtabledomain. pvs_le_gap_unique_secondtabledomain + (dst_index_unique_secondtable) = (N)) -> exists dst_positive_unique_secondtable dst_negative_unique_secondtable dst_value_unique_secondtable. ((((exists ff_h_pvs_unique_secondtableentrypositive. ff_h_pvs_unique_secondtableentrypositive + S (dst_positive_unique_secondtable) = S ((S (dst_index_unique_secondtable)) * dst_positive_scale_unique_secondtable)) /\ exists ff_q_pvs_unique_secondtableentrypositive. dst_positive_code_unique_secondtable = ff_q_pvs_unique_secondtableentrypositive * S ((S (dst_index_unique_secondtable)) * dst_positive_scale_unique_secondtable) + (dst_positive_unique_secondtable))) /\ (((((exists ff_h_pvs_unique_secondtableentrynegative. ff_h_pvs_unique_secondtableentrynegative + S (dst_negative_unique_secondtable) = S ((S (dst_index_unique_secondtable)) * dst_negative_scale_unique_secondtable)) /\ exists ff_q_pvs_unique_secondtableentrynegative. dst_negative_code_unique_secondtable = ff_q_pvs_unique_secondtableentrynegative * S ((S (dst_index_unique_secondtable)) * dst_negative_scale_unique_secondtable) + (dst_negative_unique_secondtable))) /\ (exists ge_balance_positive_unique_secondtableentryvalue ge_balance_negative_unique_secondtableentryvalue. (((((dst_value_unique_secondtable) = 2 * (ge_balance_positive_unique_secondtableentryvalue) /\ (ge_balance_negative_unique_secondtableentryvalue) = 0) \/ exists ge_signed_half_unique_secondtableentryvaluedecode. (((dst_value_unique_secondtable) = 2 * ge_signed_half_unique_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondtableentryvalue) = 0) /\ (ge_balance_negative_unique_secondtableentryvalue) = S ge_signed_half_unique_secondtableentryvaluedecode))) /\ ((dst_positive_unique_secondtable) + ge_balance_negative_unique_secondtableentryvalue = (dst_negative_unique_secondtable) + ge_balance_positive_unique_secondtableentryvalue))))))))) /\ (((exists dst_positive_code_unique_secondzero dst_positive_scale_unique_secondzero dst_negative_code_unique_secondzero dst_negative_scale_unique_secondzero dst_positive_unique_secondzero dst_negative_unique_secondzero. (((G) = (((((dst_positive_code_unique_secondzero) + (dst_positive_scale_unique_secondzero)) * S ((dst_positive_code_unique_secondzero) + (dst_positive_scale_unique_secondzero)) + ((dst_positive_scale_unique_secondzero) + (dst_positive_scale_unique_secondzero))) + (((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) * S ((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) + ((dst_negative_scale_unique_secondzero) + (dst_negative_scale_unique_secondzero)))) * S ((((dst_positive_code_unique_secondzero) + (dst_positive_scale_unique_secondzero)) * S ((dst_positive_code_unique_secondzero) + (dst_positive_scale_unique_secondzero)) + ((dst_positive_scale_unique_secondzero) + (dst_positive_scale_unique_secondzero))) + (((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) * S ((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) + ((dst_negative_scale_unique_secondzero) + (dst_negative_scale_unique_secondzero)))) + ((((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) * S ((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) + ((dst_negative_scale_unique_secondzero) + (dst_negative_scale_unique_secondzero))) + (((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) * S ((dst_negative_code_unique_secondzero) + (dst_negative_scale_unique_secondzero)) + ((dst_negative_scale_unique_secondzero) + (dst_negative_scale_unique_secondzero)))))) /\ (((((exists ff_h_pvs_unique_secondzeropositive. ff_h_pvs_unique_secondzeropositive + S (dst_positive_unique_secondzero) = S ((S (0)) * dst_positive_scale_unique_secondzero)) /\ exists ff_q_pvs_unique_secondzeropositive. dst_positive_code_unique_secondzero = ff_q_pvs_unique_secondzeropositive * S ((S (0)) * dst_positive_scale_unique_secondzero) + (dst_positive_unique_secondzero))) /\ (((((exists ff_h_pvs_unique_secondzeronegative. ff_h_pvs_unique_secondzeronegative + S (dst_negative_unique_secondzero) = S ((S (0)) * dst_negative_scale_unique_secondzero)) /\ exists ff_q_pvs_unique_secondzeronegative. dst_negative_code_unique_secondzero = ff_q_pvs_unique_secondzeronegative * S ((S (0)) * dst_negative_scale_unique_secondzero) + (dst_negative_unique_secondzero))) /\ (exists ge_balance_positive_unique_secondzerovalue ge_balance_negative_unique_secondzerovalue. (((((0) = 2 * (ge_balance_positive_unique_secondzerovalue) /\ (ge_balance_negative_unique_secondzerovalue) = 0) \/ exists ge_signed_half_unique_secondzerovaluedecode. (((0) = 2 * ge_signed_half_unique_secondzerovaluedecode + 1 /\ (ge_balance_positive_unique_secondzerovalue) = 0) /\ (ge_balance_negative_unique_secondzerovalue) = S ge_signed_half_unique_secondzerovaluedecode))) /\ ((dst_positive_unique_secondzero) + ge_balance_negative_unique_secondzerovalue = (dst_negative_unique_secondzero) + ge_balance_positive_unique_secondzerovalue))))))))) /\ (forall mt_index_unique_second mt_value_unique_second. ~(mt_index_unique_second=0) -> (exists pvs_le_gap_unique_seconddomain. pvs_le_gap_unique_seconddomain + (mt_index_unique_second) = (N)) -> (exists dst_positive_code_unique_secondentry dst_positive_scale_unique_secondentry dst_negative_code_unique_secondentry dst_negative_scale_unique_secondentry dst_positive_unique_secondentry dst_negative_unique_secondentry. (((G) = (((((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) * S ((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) + ((dst_positive_scale_unique_secondentry) + (dst_positive_scale_unique_secondentry))) + (((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry)))) * S ((((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) * S ((dst_positive_code_unique_secondentry) + (dst_positive_scale_unique_secondentry)) + ((dst_positive_scale_unique_secondentry) + (dst_positive_scale_unique_secondentry))) + (((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry)))) + ((((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry))) + (((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) * S ((dst_negative_code_unique_secondentry) + (dst_negative_scale_unique_secondentry)) + ((dst_negative_scale_unique_secondentry) + (dst_negative_scale_unique_secondentry)))))) /\ (((((exists ff_h_pvs_unique_secondentrypositive. ff_h_pvs_unique_secondentrypositive + S (dst_positive_unique_secondentry) = S ((S (mt_index_unique_second)) * dst_positive_scale_unique_secondentry)) /\ exists ff_q_pvs_unique_secondentrypositive. dst_positive_code_unique_secondentry = ff_q_pvs_unique_secondentrypositive * S ((S (mt_index_unique_second)) * dst_positive_scale_unique_secondentry) + (dst_positive_unique_secondentry))) /\ (((((exists ff_h_pvs_unique_secondentrynegative. ff_h_pvs_unique_secondentrynegative + S (dst_negative_unique_secondentry) = S ((S (mt_index_unique_second)) * dst_negative_scale_unique_secondentry)) /\ exists ff_q_pvs_unique_secondentrynegative. dst_negative_code_unique_secondentry = ff_q_pvs_unique_secondentrynegative * S ((S (mt_index_unique_second)) * dst_negative_scale_unique_secondentry) + (dst_negative_unique_secondentry))) /\ (exists ge_balance_positive_unique_secondentryvalue ge_balance_negative_unique_secondentryvalue. (((((mt_value_unique_second) = 2 * (ge_balance_positive_unique_secondentryvalue) /\ (ge_balance_negative_unique_secondentryvalue) = 0) \/ exists ge_signed_half_unique_secondentryvaluedecode. (((mt_value_unique_second) = 2 * ge_signed_half_unique_secondentryvaluedecode + 1 /\ (ge_balance_positive_unique_secondentryvalue) = 0) /\ (ge_balance_negative_unique_secondentryvalue) = S ge_signed_half_unique_secondentryvaluedecode))) /\ ((dst_positive_unique_secondentry) + ge_balance_negative_unique_secondentryvalue = (dst_negative_unique_secondentry) + ge_balance_positive_unique_secondentryvalue))))))))) -> (((~((mt_index_unique_second) = 0)) /\ ((((exists mv_square_prime_unique_secondvaluesquare. ((~((mv_square_prime_unique_secondvaluesquare) = 1) /\ forall pvs_left_unique_secondvaluesquareprime pvs_right_unique_secondvaluesquareprime. (mv_square_prime_unique_secondvaluesquare) = pvs_left_unique_secondvaluesquareprime * pvs_right_unique_secondvaluesquareprime -> pvs_left_unique_secondvaluesquareprime = 1 \/ pvs_right_unique_secondvaluesquareprime = 1) /\ (exists pvs_factor_unique_secondvaluesquaredivisor. (mt_index_unique_second) = (mv_square_prime_unique_secondvaluesquare * mv_square_prime_unique_secondvaluesquare) * pvs_factor_unique_secondvaluesquaredivisor))) /\ ((mt_value_unique_second) = 0))) \/ (((((~((mt_index_unique_second) = 0)) /\ (forall sfd_prime_unique_secondvaluesquarefree. (~((sfd_prime_unique_secondvaluesquarefree) = 1) /\ forall pvs_left_unique_secondvaluesquarefreedomain pvs_right_unique_secondvaluesquarefreedomain. (sfd_prime_unique_secondvaluesquarefree) = pvs_left_unique_secondvaluesquarefreedomain * pvs_right_unique_secondvaluesquarefreedomain -> pvs_left_unique_secondvaluesquarefreedomain = 1 \/ pvs_right_unique_secondvaluesquarefreedomain = 1) -> (exists pvs_le_gap_unique_secondvaluesquarefreebound. pvs_le_gap_unique_secondvaluesquarefreebound + (sfd_prime_unique_secondvaluesquarefree) = (mt_index_unique_second)) -> ~(exists pvs_factor_unique_secondvaluesquarefreesquare. (mt_index_unique_second) = (sfd_prime_unique_secondvaluesquarefree * sfd_prime_unique_secondvaluesquarefree) * pvs_factor_unique_secondvaluesquarefreesquare)))) /\ (exists mv_factor_code_unique_secondvaluefactors mv_factor_scale_unique_secondvaluefactors mv_factor_count_unique_secondvaluefactors. (((~(mt_index_unique_second = 0) /\ ((exists ff_u_fsat_unique_secondvaluefactorsfactorization_product ff_v_fsat_unique_secondvaluefactorsfactorization_product. ((((exists ff_h_fsat_unique_secondvaluefactorsfactorization_product_start. ff_h_fsat_unique_secondvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_secondvaluefactorsfactorization_product_start. ff_u_fsat_unique_secondvaluefactorsfactorization_product = ff_q_fsat_unique_secondvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_unique_secondvaluefactorsfactorization_product_terminal. ff_h_fsat_unique_secondvaluefactorsfactorization_product_terminal + S (mt_index_unique_second) = S ((S (mv_factor_count_unique_secondvaluefactors)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_secondvaluefactorsfactorization_product_terminal. ff_u_fsat_unique_secondvaluefactorsfactorization_product = ff_q_fsat_unique_secondvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_unique_secondvaluefactors)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product) + (mt_index_unique_second))) /\ forall ff_i_fsat_unique_secondvaluefactorsfactorization_product. (exists ff_lt_fsat_unique_secondvaluefactorsfactorization_product_bound. ff_lt_fsat_unique_secondvaluefactorsfactorization_product_bound + S ff_i_fsat_unique_secondvaluefactorsfactorization_product = mv_factor_count_unique_secondvaluefactors) -> exists ff_p_fsat_unique_secondvaluefactorsfactorization_product ff_r_fsat_unique_secondvaluefactorsfactorization_product ff_s_fsat_unique_secondvaluefactorsfactorization_product. ((((exists ff_h_fsat_unique_secondvaluefactorsfactorization_product_factor. ff_h_fsat_unique_secondvaluefactorsfactorization_product_factor + S (ff_p_fsat_unique_secondvaluefactorsfactorization_product) = S ((S (ff_i_fsat_unique_secondvaluefactorsfactorization_product)) * mv_factor_scale_unique_secondvaluefactors)) /\ exists ff_q_fsat_unique_secondvaluefactorsfactorization_product_factor. mv_factor_code_unique_secondvaluefactors = ff_q_fsat_unique_secondvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_unique_secondvaluefactorsfactorization_product)) * mv_factor_scale_unique_secondvaluefactors) + (ff_p_fsat_unique_secondvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_secondvaluefactorsfactorization_product_partial. ff_h_fsat_unique_secondvaluefactorsfactorization_product_partial + S (ff_r_fsat_unique_secondvaluefactorsfactorization_product) = S ((S (ff_i_fsat_unique_secondvaluefactorsfactorization_product)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_secondvaluefactorsfactorization_product_partial. ff_u_fsat_unique_secondvaluefactorsfactorization_product = ff_q_fsat_unique_secondvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_unique_secondvaluefactorsfactorization_product)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product) + (ff_r_fsat_unique_secondvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_secondvaluefactorsfactorization_product_successor. ff_h_fsat_unique_secondvaluefactorsfactorization_product_successor + S (ff_s_fsat_unique_secondvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_unique_secondvaluefactorsfactorization_product)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product)) /\ exists ff_q_fsat_unique_secondvaluefactorsfactorization_product_successor. ff_u_fsat_unique_secondvaluefactorsfactorization_product = ff_q_fsat_unique_secondvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_unique_secondvaluefactorsfactorization_product)) * ff_v_fsat_unique_secondvaluefactorsfactorization_product) + (ff_s_fsat_unique_secondvaluefactorsfactorization_product))) /\ ff_s_fsat_unique_secondvaluefactorsfactorization_product = ff_r_fsat_unique_secondvaluefactorsfactorization_product * ff_p_fsat_unique_secondvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_unique_secondvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_unique_secondvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_unique_secondvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_unique_secondvaluefactorsfactorization_primes = (mv_factor_count_unique_secondvaluefactors)) -> exists ftsf_factor_fsat_unique_secondvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_unique_secondvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_unique_secondvaluefactorsfactorization_primes)) * mv_factor_scale_unique_secondvaluefactors)) /\ exists ff_q_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_entry. mv_factor_code_unique_secondvaluefactors = ff_q_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_unique_secondvaluefactorsfactorization_primes)) * mv_factor_scale_unique_secondvaluefactors) + (ftsf_factor_fsat_unique_secondvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_unique_secondvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_unique_secondvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_unique_secondvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_unique_secondvaluefactorsparityeven. (mv_factor_count_unique_secondvaluefactors) = 2 * mv_even_half_unique_secondvaluefactorsparityeven) /\ ((mt_value_unique_second) = 2))) \/ (((exists mv_odd_half_unique_secondvaluefactorsparityodd. (mv_factor_count_unique_secondvaluefactors) = 2 * mv_odd_half_unique_secondvaluefactorsparityodd + 1) /\ ((mt_value_unique_second) = 1)))))))))))))))) -> (forall dst_index_unique_values dst_first_unique_values dst_second_unique_values. (exists pvs_gap_unique_valuesbound. pvs_gap_unique_valuesbound + S (dst_index_unique_values) = (S N)) -> (exists dst_positive_code_unique_valuesfirst dst_positive_scale_unique_valuesfirst dst_negative_code_unique_valuesfirst dst_negative_scale_unique_valuesfirst dst_positive_unique_valuesfirst dst_negative_unique_valuesfirst. (((F) = (((((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) * S ((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) + ((dst_positive_scale_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst))) + (((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)))) * S ((((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) * S ((dst_positive_code_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst)) + ((dst_positive_scale_unique_valuesfirst) + (dst_positive_scale_unique_valuesfirst))) + (((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)))) + ((((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst))) + (((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) * S ((dst_negative_code_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)) + ((dst_negative_scale_unique_valuesfirst) + (dst_negative_scale_unique_valuesfirst)))))) /\ (((((exists ff_h_pvs_unique_valuesfirstpositive. ff_h_pvs_unique_valuesfirstpositive + S (dst_positive_unique_valuesfirst) = S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuesfirst)) /\ exists ff_q_pvs_unique_valuesfirstpositive. dst_positive_code_unique_valuesfirst = ff_q_pvs_unique_valuesfirstpositive * S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuesfirst) + (dst_positive_unique_valuesfirst))) /\ (((((exists ff_h_pvs_unique_valuesfirstnegative. ff_h_pvs_unique_valuesfirstnegative + S (dst_negative_unique_valuesfirst) = S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuesfirst)) /\ exists ff_q_pvs_unique_valuesfirstnegative. dst_negative_code_unique_valuesfirst = ff_q_pvs_unique_valuesfirstnegative * S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuesfirst) + (dst_negative_unique_valuesfirst))) /\ (exists ge_balance_positive_unique_valuesfirstvalue ge_balance_negative_unique_valuesfirstvalue. (((((dst_first_unique_values) = 2 * (ge_balance_positive_unique_valuesfirstvalue) /\ (ge_balance_negative_unique_valuesfirstvalue) = 0) \/ exists ge_signed_half_unique_valuesfirstvaluedecode. (((dst_first_unique_values) = 2 * ge_signed_half_unique_valuesfirstvaluedecode + 1 /\ (ge_balance_positive_unique_valuesfirstvalue) = 0) /\ (ge_balance_negative_unique_valuesfirstvalue) = S ge_signed_half_unique_valuesfirstvaluedecode))) /\ ((dst_positive_unique_valuesfirst) + ge_balance_negative_unique_valuesfirstvalue = (dst_negative_unique_valuesfirst) + ge_balance_positive_unique_valuesfirstvalue))))))))) -> (exists dst_positive_code_unique_valuessecond dst_positive_scale_unique_valuessecond dst_negative_code_unique_valuessecond dst_negative_scale_unique_valuessecond dst_positive_unique_valuessecond dst_negative_unique_valuessecond. (((G) = (((((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) * S ((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) + ((dst_positive_scale_unique_valuessecond) + (dst_positive_scale_unique_valuessecond))) + (((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)))) * S ((((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) * S ((dst_positive_code_unique_valuessecond) + (dst_positive_scale_unique_valuessecond)) + ((dst_positive_scale_unique_valuessecond) + (dst_positive_scale_unique_valuessecond))) + (((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)))) + ((((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond))) + (((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) * S ((dst_negative_code_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)) + ((dst_negative_scale_unique_valuessecond) + (dst_negative_scale_unique_valuessecond)))))) /\ (((((exists ff_h_pvs_unique_valuessecondpositive. ff_h_pvs_unique_valuessecondpositive + S (dst_positive_unique_valuessecond) = S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuessecond)) /\ exists ff_q_pvs_unique_valuessecondpositive. dst_positive_code_unique_valuessecond = ff_q_pvs_unique_valuessecondpositive * S ((S (dst_index_unique_values)) * dst_positive_scale_unique_valuessecond) + (dst_positive_unique_valuessecond))) /\ (((((exists ff_h_pvs_unique_valuessecondnegative. ff_h_pvs_unique_valuessecondnegative + S (dst_negative_unique_valuessecond) = S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuessecond)) /\ exists ff_q_pvs_unique_valuessecondnegative. dst_negative_code_unique_valuessecond = ff_q_pvs_unique_valuessecondnegative * S ((S (dst_index_unique_values)) * dst_negative_scale_unique_valuessecond) + (dst_negative_unique_valuessecond))) /\ (exists ge_balance_positive_unique_valuessecondvalue ge_balance_negative_unique_valuessecondvalue. (((((dst_second_unique_values) = 2 * (ge_balance_positive_unique_valuessecondvalue) /\ (ge_balance_negative_unique_valuessecondvalue) = 0) \/ exists ge_signed_half_unique_valuessecondvaluedecode. (((dst_second_unique_values) = 2 * ge_signed_half_unique_valuessecondvaluedecode + 1 /\ (ge_balance_positive_unique_valuessecondvalue) = 0) /\ (ge_balance_negative_unique_valuessecondvalue) = S ge_signed_half_unique_valuessecondvaluedecode))) /\ ((dst_positive_unique_valuessecond) + ge_balance_negative_unique_valuessecondvalue = (dst_negative_unique_valuessecond) + ge_balance_positive_unique_valuessecondvalue))))))))) -> dst_first_unique_values = dst_second_unique_values)