mobius_table_lookup

Exact expanded first-order arithmetic statement

forall N M i. (((exists dst_positive_code_lookup_sourcetable dst_positive_scale_lookup_sourcetable dst_negative_code_lookup_sourcetable dst_negative_scale_lookup_sourcetable. (((M) = (((((dst_positive_code_lookup_sourcetable) + (dst_positive_scale_lookup_sourcetable)) * S ((dst_positive_code_lookup_sourcetable) + (dst_positive_scale_lookup_sourcetable)) + ((dst_positive_scale_lookup_sourcetable) + (dst_positive_scale_lookup_sourcetable))) + (((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) * S ((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) + ((dst_negative_scale_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)))) * S ((((dst_positive_code_lookup_sourcetable) + (dst_positive_scale_lookup_sourcetable)) * S ((dst_positive_code_lookup_sourcetable) + (dst_positive_scale_lookup_sourcetable)) + ((dst_positive_scale_lookup_sourcetable) + (dst_positive_scale_lookup_sourcetable))) + (((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) * S ((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) + ((dst_negative_scale_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)))) + ((((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) * S ((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) + ((dst_negative_scale_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable))) + (((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) * S ((dst_negative_code_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)) + ((dst_negative_scale_lookup_sourcetable) + (dst_negative_scale_lookup_sourcetable)))))) /\ (forall dst_index_lookup_sourcetable. (exists pvs_le_gap_lookup_sourcetabledomain. pvs_le_gap_lookup_sourcetabledomain + (dst_index_lookup_sourcetable) = (N)) -> exists dst_positive_lookup_sourcetable dst_negative_lookup_sourcetable dst_value_lookup_sourcetable. ((((exists ff_h_pvs_lookup_sourcetableentrypositive. ff_h_pvs_lookup_sourcetableentrypositive + S (dst_positive_lookup_sourcetable) = S ((S (dst_index_lookup_sourcetable)) * dst_positive_scale_lookup_sourcetable)) /\ exists ff_q_pvs_lookup_sourcetableentrypositive. dst_positive_code_lookup_sourcetable = ff_q_pvs_lookup_sourcetableentrypositive * S ((S (dst_index_lookup_sourcetable)) * dst_positive_scale_lookup_sourcetable) + (dst_positive_lookup_sourcetable))) /\ (((((exists ff_h_pvs_lookup_sourcetableentrynegative. ff_h_pvs_lookup_sourcetableentrynegative + S (dst_negative_lookup_sourcetable) = S ((S (dst_index_lookup_sourcetable)) * dst_negative_scale_lookup_sourcetable)) /\ exists ff_q_pvs_lookup_sourcetableentrynegative. dst_negative_code_lookup_sourcetable = ff_q_pvs_lookup_sourcetableentrynegative * S ((S (dst_index_lookup_sourcetable)) * dst_negative_scale_lookup_sourcetable) + (dst_negative_lookup_sourcetable))) /\ (exists ge_balance_positive_lookup_sourcetableentryvalue ge_balance_negative_lookup_sourcetableentryvalue. (((((dst_value_lookup_sourcetable) = 2 * (ge_balance_positive_lookup_sourcetableentryvalue) /\ (ge_balance_negative_lookup_sourcetableentryvalue) = 0) \/ exists ge_signed_half_lookup_sourcetableentryvaluedecode. (((dst_value_lookup_sourcetable) = 2 * ge_signed_half_lookup_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_lookup_sourcetableentryvalue) = 0) /\ (ge_balance_negative_lookup_sourcetableentryvalue) = S ge_signed_half_lookup_sourcetableentryvaluedecode))) /\ ((dst_positive_lookup_sourcetable) + ge_balance_negative_lookup_sourcetableentryvalue = (dst_negative_lookup_sourcetable) + ge_balance_positive_lookup_sourcetableentryvalue))))))))) /\ (((exists dst_positive_code_lookup_sourcezero dst_positive_scale_lookup_sourcezero dst_negative_code_lookup_sourcezero dst_negative_scale_lookup_sourcezero dst_positive_lookup_sourcezero dst_negative_lookup_sourcezero. (((M) = (((((dst_positive_code_lookup_sourcezero) + (dst_positive_scale_lookup_sourcezero)) * S ((dst_positive_code_lookup_sourcezero) + (dst_positive_scale_lookup_sourcezero)) + ((dst_positive_scale_lookup_sourcezero) + (dst_positive_scale_lookup_sourcezero))) + (((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) * S ((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) + ((dst_negative_scale_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)))) * S ((((dst_positive_code_lookup_sourcezero) + (dst_positive_scale_lookup_sourcezero)) * S ((dst_positive_code_lookup_sourcezero) + (dst_positive_scale_lookup_sourcezero)) + ((dst_positive_scale_lookup_sourcezero) + (dst_positive_scale_lookup_sourcezero))) + (((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) * S ((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) + ((dst_negative_scale_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)))) + ((((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) * S ((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) + ((dst_negative_scale_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero))) + (((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) * S ((dst_negative_code_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)) + ((dst_negative_scale_lookup_sourcezero) + (dst_negative_scale_lookup_sourcezero)))))) /\ (((((exists ff_h_pvs_lookup_sourcezeropositive. ff_h_pvs_lookup_sourcezeropositive + S (dst_positive_lookup_sourcezero) = S ((S (0)) * dst_positive_scale_lookup_sourcezero)) /\ exists ff_q_pvs_lookup_sourcezeropositive. dst_positive_code_lookup_sourcezero = ff_q_pvs_lookup_sourcezeropositive * S ((S (0)) * dst_positive_scale_lookup_sourcezero) + (dst_positive_lookup_sourcezero))) /\ (((((exists ff_h_pvs_lookup_sourcezeronegative. ff_h_pvs_lookup_sourcezeronegative + S (dst_negative_lookup_sourcezero) = S ((S (0)) * dst_negative_scale_lookup_sourcezero)) /\ exists ff_q_pvs_lookup_sourcezeronegative. dst_negative_code_lookup_sourcezero = ff_q_pvs_lookup_sourcezeronegative * S ((S (0)) * dst_negative_scale_lookup_sourcezero) + (dst_negative_lookup_sourcezero))) /\ (exists ge_balance_positive_lookup_sourcezerovalue ge_balance_negative_lookup_sourcezerovalue. (((((0) = 2 * (ge_balance_positive_lookup_sourcezerovalue) /\ (ge_balance_negative_lookup_sourcezerovalue) = 0) \/ exists ge_signed_half_lookup_sourcezerovaluedecode. (((0) = 2 * ge_signed_half_lookup_sourcezerovaluedecode + 1 /\ (ge_balance_positive_lookup_sourcezerovalue) = 0) /\ (ge_balance_negative_lookup_sourcezerovalue) = S ge_signed_half_lookup_sourcezerovaluedecode))) /\ ((dst_positive_lookup_sourcezero) + ge_balance_negative_lookup_sourcezerovalue = (dst_negative_lookup_sourcezero) + ge_balance_positive_lookup_sourcezerovalue))))))))) /\ (forall mt_index_lookup_source mt_value_lookup_source. ~(mt_index_lookup_source=0) -> (exists pvs_le_gap_lookup_sourcedomain. pvs_le_gap_lookup_sourcedomain + (mt_index_lookup_source) = (N)) -> (exists dst_positive_code_lookup_sourceentry dst_positive_scale_lookup_sourceentry dst_negative_code_lookup_sourceentry dst_negative_scale_lookup_sourceentry dst_positive_lookup_sourceentry dst_negative_lookup_sourceentry. (((M) = (((((dst_positive_code_lookup_sourceentry) + (dst_positive_scale_lookup_sourceentry)) * S ((dst_positive_code_lookup_sourceentry) + (dst_positive_scale_lookup_sourceentry)) + ((dst_positive_scale_lookup_sourceentry) + (dst_positive_scale_lookup_sourceentry))) + (((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) * S ((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) + ((dst_negative_scale_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)))) * S ((((dst_positive_code_lookup_sourceentry) + (dst_positive_scale_lookup_sourceentry)) * S ((dst_positive_code_lookup_sourceentry) + (dst_positive_scale_lookup_sourceentry)) + ((dst_positive_scale_lookup_sourceentry) + (dst_positive_scale_lookup_sourceentry))) + (((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) * S ((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) + ((dst_negative_scale_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)))) + ((((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) * S ((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) + ((dst_negative_scale_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry))) + (((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) * S ((dst_negative_code_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)) + ((dst_negative_scale_lookup_sourceentry) + (dst_negative_scale_lookup_sourceentry)))))) /\ (((((exists ff_h_pvs_lookup_sourceentrypositive. ff_h_pvs_lookup_sourceentrypositive + S (dst_positive_lookup_sourceentry) = S ((S (mt_index_lookup_source)) * dst_positive_scale_lookup_sourceentry)) /\ exists ff_q_pvs_lookup_sourceentrypositive. dst_positive_code_lookup_sourceentry = ff_q_pvs_lookup_sourceentrypositive * S ((S (mt_index_lookup_source)) * dst_positive_scale_lookup_sourceentry) + (dst_positive_lookup_sourceentry))) /\ (((((exists ff_h_pvs_lookup_sourceentrynegative. ff_h_pvs_lookup_sourceentrynegative + S (dst_negative_lookup_sourceentry) = S ((S (mt_index_lookup_source)) * dst_negative_scale_lookup_sourceentry)) /\ exists ff_q_pvs_lookup_sourceentrynegative. dst_negative_code_lookup_sourceentry = ff_q_pvs_lookup_sourceentrynegative * S ((S (mt_index_lookup_source)) * dst_negative_scale_lookup_sourceentry) + (dst_negative_lookup_sourceentry))) /\ (exists ge_balance_positive_lookup_sourceentryvalue ge_balance_negative_lookup_sourceentryvalue. (((((mt_value_lookup_source) = 2 * (ge_balance_positive_lookup_sourceentryvalue) /\ (ge_balance_negative_lookup_sourceentryvalue) = 0) \/ exists ge_signed_half_lookup_sourceentryvaluedecode. (((mt_value_lookup_source) = 2 * ge_signed_half_lookup_sourceentryvaluedecode + 1 /\ (ge_balance_positive_lookup_sourceentryvalue) = 0) /\ (ge_balance_negative_lookup_sourceentryvalue) = S ge_signed_half_lookup_sourceentryvaluedecode))) /\ ((dst_positive_lookup_sourceentry) + ge_balance_negative_lookup_sourceentryvalue = (dst_negative_lookup_sourceentry) + ge_balance_positive_lookup_sourceentryvalue))))))))) -> (((~((mt_index_lookup_source) = 0)) /\ ((((exists mv_square_prime_lookup_sourcevaluesquare. ((~((mv_square_prime_lookup_sourcevaluesquare) = 1) /\ forall pvs_left_lookup_sourcevaluesquareprime pvs_right_lookup_sourcevaluesquareprime. (mv_square_prime_lookup_sourcevaluesquare) = pvs_left_lookup_sourcevaluesquareprime * pvs_right_lookup_sourcevaluesquareprime -> pvs_left_lookup_sourcevaluesquareprime = 1 \/ pvs_right_lookup_sourcevaluesquareprime = 1) /\ (exists pvs_factor_lookup_sourcevaluesquaredivisor. (mt_index_lookup_source) = (mv_square_prime_lookup_sourcevaluesquare * mv_square_prime_lookup_sourcevaluesquare) * pvs_factor_lookup_sourcevaluesquaredivisor))) /\ ((mt_value_lookup_source) = 0))) \/ (((((~((mt_index_lookup_source) = 0)) /\ (forall sfd_prime_lookup_sourcevaluesquarefree. (~((sfd_prime_lookup_sourcevaluesquarefree) = 1) /\ forall pvs_left_lookup_sourcevaluesquarefreedomain pvs_right_lookup_sourcevaluesquarefreedomain. (sfd_prime_lookup_sourcevaluesquarefree) = pvs_left_lookup_sourcevaluesquarefreedomain * pvs_right_lookup_sourcevaluesquarefreedomain -> pvs_left_lookup_sourcevaluesquarefreedomain = 1 \/ pvs_right_lookup_sourcevaluesquarefreedomain = 1) -> (exists pvs_le_gap_lookup_sourcevaluesquarefreebound. pvs_le_gap_lookup_sourcevaluesquarefreebound + (sfd_prime_lookup_sourcevaluesquarefree) = (mt_index_lookup_source)) -> ~(exists pvs_factor_lookup_sourcevaluesquarefreesquare. (mt_index_lookup_source) = (sfd_prime_lookup_sourcevaluesquarefree * sfd_prime_lookup_sourcevaluesquarefree) * pvs_factor_lookup_sourcevaluesquarefreesquare)))) /\ (exists mv_factor_code_lookup_sourcevaluefactors mv_factor_scale_lookup_sourcevaluefactors mv_factor_count_lookup_sourcevaluefactors. (((~(mt_index_lookup_source = 0) /\ ((exists ff_u_fsat_lookup_sourcevaluefactorsfactorization_product ff_v_fsat_lookup_sourcevaluefactorsfactorization_product. ((((exists ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_start. ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_start. ff_u_fsat_lookup_sourcevaluefactorsfactorization_product = ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_terminal. ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_terminal + S (mt_index_lookup_source) = S ((S (mv_factor_count_lookup_sourcevaluefactors)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_terminal. ff_u_fsat_lookup_sourcevaluefactorsfactorization_product = ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_lookup_sourcevaluefactors)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product) + (mt_index_lookup_source))) /\ forall ff_i_fsat_lookup_sourcevaluefactorsfactorization_product. (exists ff_lt_fsat_lookup_sourcevaluefactorsfactorization_product_bound. ff_lt_fsat_lookup_sourcevaluefactorsfactorization_product_bound + S ff_i_fsat_lookup_sourcevaluefactorsfactorization_product = mv_factor_count_lookup_sourcevaluefactors) -> exists ff_p_fsat_lookup_sourcevaluefactorsfactorization_product ff_r_fsat_lookup_sourcevaluefactorsfactorization_product ff_s_fsat_lookup_sourcevaluefactorsfactorization_product. ((((exists ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_factor. ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_factor + S (ff_p_fsat_lookup_sourcevaluefactorsfactorization_product) = S ((S (ff_i_fsat_lookup_sourcevaluefactorsfactorization_product)) * mv_factor_scale_lookup_sourcevaluefactors)) /\ exists ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_factor. mv_factor_code_lookup_sourcevaluefactors = ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_lookup_sourcevaluefactorsfactorization_product)) * mv_factor_scale_lookup_sourcevaluefactors) + (ff_p_fsat_lookup_sourcevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_partial. ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_partial + S (ff_r_fsat_lookup_sourcevaluefactorsfactorization_product) = S ((S (ff_i_fsat_lookup_sourcevaluefactorsfactorization_product)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_partial. ff_u_fsat_lookup_sourcevaluefactorsfactorization_product = ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_lookup_sourcevaluefactorsfactorization_product)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product) + (ff_r_fsat_lookup_sourcevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_successor. ff_h_fsat_lookup_sourcevaluefactorsfactorization_product_successor + S (ff_s_fsat_lookup_sourcevaluefactorsfactorization_product) = S ((S (S ff_i_fsat_lookup_sourcevaluefactorsfactorization_product)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_successor. ff_u_fsat_lookup_sourcevaluefactorsfactorization_product = ff_q_fsat_lookup_sourcevaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_lookup_sourcevaluefactorsfactorization_product)) * ff_v_fsat_lookup_sourcevaluefactorsfactorization_product) + (ff_s_fsat_lookup_sourcevaluefactorsfactorization_product))) /\ ff_s_fsat_lookup_sourcevaluefactorsfactorization_product = ff_r_fsat_lookup_sourcevaluefactorsfactorization_product * ff_p_fsat_lookup_sourcevaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_lookup_sourcevaluefactorsfactorization_primes. (exists ftsf_gap_fsat_lookup_sourcevaluefactorsfactorization_primes_bound. ftsf_gap_fsat_lookup_sourcevaluefactorsfactorization_primes_bound + S ftsf_index_fsat_lookup_sourcevaluefactorsfactorization_primes = (mv_factor_count_lookup_sourcevaluefactors)) -> exists ftsf_factor_fsat_lookup_sourcevaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_lookup_sourcevaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_lookup_sourcevaluefactorsfactorization_primes)) * mv_factor_scale_lookup_sourcevaluefactors)) /\ exists ff_q_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_entry. mv_factor_code_lookup_sourcevaluefactors = ff_q_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_lookup_sourcevaluefactorsfactorization_primes)) * mv_factor_scale_lookup_sourcevaluefactors) + (ftsf_factor_fsat_lookup_sourcevaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_lookup_sourcevaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_prime. ftsf_factor_fsat_lookup_sourcevaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_lookup_sourcevaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_lookup_sourcevaluefactorsparityeven. (mv_factor_count_lookup_sourcevaluefactors) = 2 * mv_even_half_lookup_sourcevaluefactorsparityeven) /\ ((mt_value_lookup_source) = 2))) \/ (((exists mv_odd_half_lookup_sourcevaluefactorsparityodd. (mv_factor_count_lookup_sourcevaluefactors) = 2 * mv_odd_half_lookup_sourcevaluefactorsparityodd + 1) /\ ((mt_value_lookup_source) = 1)))))))))))))))) -> ~(i=0) -> (exists pvs_le_gap_lookup_bound. pvs_le_gap_lookup_bound + (i) = (N)) -> exists z. (exists dst_positive_code_lookup_entry dst_positive_scale_lookup_entry dst_negative_code_lookup_entry dst_negative_scale_lookup_entry dst_positive_lookup_entry dst_negative_lookup_entry. (((M) = (((((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) * S ((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) + ((dst_positive_scale_lookup_entry) + (dst_positive_scale_lookup_entry))) + (((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry)))) * S ((((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) * S ((dst_positive_code_lookup_entry) + (dst_positive_scale_lookup_entry)) + ((dst_positive_scale_lookup_entry) + (dst_positive_scale_lookup_entry))) + (((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry)))) + ((((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry))) + (((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) * S ((dst_negative_code_lookup_entry) + (dst_negative_scale_lookup_entry)) + ((dst_negative_scale_lookup_entry) + (dst_negative_scale_lookup_entry)))))) /\ (((((exists ff_h_pvs_lookup_entrypositive. ff_h_pvs_lookup_entrypositive + S (dst_positive_lookup_entry) = S ((S (i)) * dst_positive_scale_lookup_entry)) /\ exists ff_q_pvs_lookup_entrypositive. dst_positive_code_lookup_entry = ff_q_pvs_lookup_entrypositive * S ((S (i)) * dst_positive_scale_lookup_entry) + (dst_positive_lookup_entry))) /\ (((((exists ff_h_pvs_lookup_entrynegative. ff_h_pvs_lookup_entrynegative + S (dst_negative_lookup_entry) = S ((S (i)) * dst_negative_scale_lookup_entry)) /\ exists ff_q_pvs_lookup_entrynegative. dst_negative_code_lookup_entry = ff_q_pvs_lookup_entrynegative * S ((S (i)) * dst_negative_scale_lookup_entry) + (dst_negative_lookup_entry))) /\ (exists ge_balance_positive_lookup_entryvalue ge_balance_negative_lookup_entryvalue. (((((z) = 2 * (ge_balance_positive_lookup_entryvalue) /\ (ge_balance_negative_lookup_entryvalue) = 0) \/ exists ge_signed_half_lookup_entryvaluedecode. (((z) = 2 * ge_signed_half_lookup_entryvaluedecode + 1 /\ (ge_balance_positive_lookup_entryvalue) = 0) /\ (ge_balance_negative_lookup_entryvalue) = S ge_signed_half_lookup_entryvaluedecode))) /\ ((dst_positive_lookup_entry) + ge_balance_negative_lookup_entryvalue = (dst_negative_lookup_entry) + ge_balance_positive_lookup_entryvalue))))))))) /\ (((~((i) = 0)) /\ ((((exists mv_square_prime_lookup_valuesquare. ((~((mv_square_prime_lookup_valuesquare) = 1) /\ forall pvs_left_lookup_valuesquareprime pvs_right_lookup_valuesquareprime. (mv_square_prime_lookup_valuesquare) = pvs_left_lookup_valuesquareprime * pvs_right_lookup_valuesquareprime -> pvs_left_lookup_valuesquareprime = 1 \/ pvs_right_lookup_valuesquareprime = 1) /\ (exists pvs_factor_lookup_valuesquaredivisor. (i) = (mv_square_prime_lookup_valuesquare * mv_square_prime_lookup_valuesquare) * pvs_factor_lookup_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((i) = 0)) /\ (forall sfd_prime_lookup_valuesquarefree. (~((sfd_prime_lookup_valuesquarefree) = 1) /\ forall pvs_left_lookup_valuesquarefreedomain pvs_right_lookup_valuesquarefreedomain. (sfd_prime_lookup_valuesquarefree) = pvs_left_lookup_valuesquarefreedomain * pvs_right_lookup_valuesquarefreedomain -> pvs_left_lookup_valuesquarefreedomain = 1 \/ pvs_right_lookup_valuesquarefreedomain = 1) -> (exists pvs_le_gap_lookup_valuesquarefreebound. pvs_le_gap_lookup_valuesquarefreebound + (sfd_prime_lookup_valuesquarefree) = (i)) -> ~(exists pvs_factor_lookup_valuesquarefreesquare. (i) = (sfd_prime_lookup_valuesquarefree * sfd_prime_lookup_valuesquarefree) * pvs_factor_lookup_valuesquarefreesquare)))) /\ (exists mv_factor_code_lookup_valuefactors mv_factor_scale_lookup_valuefactors mv_factor_count_lookup_valuefactors. (((~(i = 0) /\ ((exists ff_u_fsat_lookup_valuefactorsfactorization_product ff_v_fsat_lookup_valuefactorsfactorization_product. ((((exists ff_h_fsat_lookup_valuefactorsfactorization_product_start. ff_h_fsat_lookup_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_lookup_valuefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_valuefactorsfactorization_product_start. ff_u_fsat_lookup_valuefactorsfactorization_product = ff_q_fsat_lookup_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_lookup_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_lookup_valuefactorsfactorization_product_terminal. ff_h_fsat_lookup_valuefactorsfactorization_product_terminal + S (i) = S ((S (mv_factor_count_lookup_valuefactors)) * ff_v_fsat_lookup_valuefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_valuefactorsfactorization_product_terminal. ff_u_fsat_lookup_valuefactorsfactorization_product = ff_q_fsat_lookup_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_lookup_valuefactors)) * ff_v_fsat_lookup_valuefactorsfactorization_product) + (i))) /\ forall ff_i_fsat_lookup_valuefactorsfactorization_product. (exists ff_lt_fsat_lookup_valuefactorsfactorization_product_bound. ff_lt_fsat_lookup_valuefactorsfactorization_product_bound + S ff_i_fsat_lookup_valuefactorsfactorization_product = mv_factor_count_lookup_valuefactors) -> exists ff_p_fsat_lookup_valuefactorsfactorization_product ff_r_fsat_lookup_valuefactorsfactorization_product ff_s_fsat_lookup_valuefactorsfactorization_product. ((((exists ff_h_fsat_lookup_valuefactorsfactorization_product_factor. ff_h_fsat_lookup_valuefactorsfactorization_product_factor + S (ff_p_fsat_lookup_valuefactorsfactorization_product) = S ((S (ff_i_fsat_lookup_valuefactorsfactorization_product)) * mv_factor_scale_lookup_valuefactors)) /\ exists ff_q_fsat_lookup_valuefactorsfactorization_product_factor. mv_factor_code_lookup_valuefactors = ff_q_fsat_lookup_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_lookup_valuefactorsfactorization_product)) * mv_factor_scale_lookup_valuefactors) + (ff_p_fsat_lookup_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_lookup_valuefactorsfactorization_product_partial. ff_h_fsat_lookup_valuefactorsfactorization_product_partial + S (ff_r_fsat_lookup_valuefactorsfactorization_product) = S ((S (ff_i_fsat_lookup_valuefactorsfactorization_product)) * ff_v_fsat_lookup_valuefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_valuefactorsfactorization_product_partial. ff_u_fsat_lookup_valuefactorsfactorization_product = ff_q_fsat_lookup_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_lookup_valuefactorsfactorization_product)) * ff_v_fsat_lookup_valuefactorsfactorization_product) + (ff_r_fsat_lookup_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_lookup_valuefactorsfactorization_product_successor. ff_h_fsat_lookup_valuefactorsfactorization_product_successor + S (ff_s_fsat_lookup_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_lookup_valuefactorsfactorization_product)) * ff_v_fsat_lookup_valuefactorsfactorization_product)) /\ exists ff_q_fsat_lookup_valuefactorsfactorization_product_successor. ff_u_fsat_lookup_valuefactorsfactorization_product = ff_q_fsat_lookup_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_lookup_valuefactorsfactorization_product)) * ff_v_fsat_lookup_valuefactorsfactorization_product) + (ff_s_fsat_lookup_valuefactorsfactorization_product))) /\ ff_s_fsat_lookup_valuefactorsfactorization_product = ff_r_fsat_lookup_valuefactorsfactorization_product * ff_p_fsat_lookup_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_lookup_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_lookup_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_lookup_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_lookup_valuefactorsfactorization_primes = (mv_factor_count_lookup_valuefactors)) -> exists ftsf_factor_fsat_lookup_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_lookup_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_lookup_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_lookup_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_lookup_valuefactorsfactorization_primes)) * mv_factor_scale_lookup_valuefactors)) /\ exists ff_q_ftsf_fsat_lookup_valuefactorsfactorization_primes_entry. mv_factor_code_lookup_valuefactors = ff_q_ftsf_fsat_lookup_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_lookup_valuefactorsfactorization_primes)) * mv_factor_scale_lookup_valuefactors) + (ftsf_factor_fsat_lookup_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_lookup_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_lookup_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_lookup_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_lookup_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_lookup_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_lookup_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_lookup_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_lookup_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_lookup_valuefactorsparityeven. (mv_factor_count_lookup_valuefactors) = 2 * mv_even_half_lookup_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_lookup_valuefactorsparityodd. (mv_factor_count_lookup_valuefactors) = 2 * mv_odd_half_lookup_valuefactorsparityodd + 1) /\ ((z) = 1)))))))))))