mobius_table_restrict

forall N K M. (((exists dst_positive_code_restrict_sourcetable dst_positive_scale_restrict_sourcetable dst_negative_code_restrict_sourcetable dst_negative_scale_restrict_sourcetable. (((M) = (((((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) * S ((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) + ((dst_positive_scale_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))) * S ((((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) * S ((dst_positive_code_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable)) + ((dst_positive_scale_restrict_sourcetable) + (dst_positive_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))) + ((((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable))) + (((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) * S ((dst_negative_code_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)) + ((dst_negative_scale_restrict_sourcetable) + (dst_negative_scale_restrict_sourcetable)))))) /\ (forall dst_index_restrict_sourcetable. (exists pvs_le_gap_restrict_sourcetabledomain. pvs_le_gap_restrict_sourcetabledomain + (dst_index_restrict_sourcetable) = (N)) -> exists dst_positive_restrict_sourcetable dst_negative_restrict_sourcetable dst_value_restrict_sourcetable. ((((exists ff_h_pvs_restrict_sourcetableentrypositive. ff_h_pvs_restrict_sourcetableentrypositive + S (dst_positive_restrict_sourcetable) = S ((S (dst_index_restrict_sourcetable)) * dst_positive_scale_restrict_sourcetable)) /\ exists ff_q_pvs_restrict_sourcetableentrypositive. dst_positive_code_restrict_sourcetable = ff_q_pvs_restrict_sourcetableentrypositive * S ((S (dst_index_restrict_sourcetable)) * dst_positive_scale_restrict_sourcetable) + (dst_positive_restrict_sourcetable))) /\ (((((exists ff_h_pvs_restrict_sourcetableentrynegative. ff_h_pvs_restrict_sourcetableentrynegative + S (dst_negative_restrict_sourcetable) = S ((S (dst_index_restrict_sourcetable)) * dst_negative_scale_restrict_sourcetable)) /\ exists ff_q_pvs_restrict_sourcetableentrynegative. dst_negative_code_restrict_sourcetable = ff_q_pvs_restrict_sourcetableentrynegative * S ((S (dst_index_restrict_sourcetable)) * dst_negative_scale_restrict_sourcetable) + (dst_negative_restrict_sourcetable))) /\ (exists ge_balance_positive_restrict_sourcetableentryvalue ge_balance_negative_restrict_sourcetableentryvalue. (((((dst_value_restrict_sourcetable) = 2 * (ge_balance_positive_restrict_sourcetableentryvalue) /\ (ge_balance_negative_restrict_sourcetableentryvalue) = 0) \/ exists ge_signed_half_restrict_sourcetableentryvaluedecode. (((dst_value_restrict_sourcetable) = 2 * ge_signed_half_restrict_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_sourcetableentryvalue) = 0) /\ (ge_balance_negative_restrict_sourcetableentryvalue) = S ge_signed_half_restrict_sourcetableentryvaluedecode))) /\ ((dst_positive_restrict_sourcetable) + ge_balance_negative_restrict_sourcetableentryvalue = (dst_negative_restrict_sourcetable) + ge_balance_positive_restrict_sourcetableentryvalue))))))))) /\ (((exists dst_positive_code_restrict_sourcezero dst_positive_scale_restrict_sourcezero dst_negative_code_restrict_sourcezero dst_negative_scale_restrict_sourcezero dst_positive_restrict_sourcezero dst_negative_restrict_sourcezero. (((M) = (((((dst_positive_code_restrict_sourcezero) + (dst_positive_scale_restrict_sourcezero)) * S ((dst_positive_code_restrict_sourcezero) + (dst_positive_scale_restrict_sourcezero)) + ((dst_positive_scale_restrict_sourcezero) + (dst_positive_scale_restrict_sourcezero))) + (((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) * S ((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) + ((dst_negative_scale_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)))) * S ((((dst_positive_code_restrict_sourcezero) + (dst_positive_scale_restrict_sourcezero)) * S ((dst_positive_code_restrict_sourcezero) + (dst_positive_scale_restrict_sourcezero)) + ((dst_positive_scale_restrict_sourcezero) + (dst_positive_scale_restrict_sourcezero))) + (((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) * S ((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) + ((dst_negative_scale_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)))) + ((((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) * S ((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) + ((dst_negative_scale_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero))) + (((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) * S ((dst_negative_code_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)) + ((dst_negative_scale_restrict_sourcezero) + (dst_negative_scale_restrict_sourcezero)))))) /\ (((((exists ff_h_pvs_restrict_sourcezeropositive. ff_h_pvs_restrict_sourcezeropositive + S (dst_positive_restrict_sourcezero) = S ((S (0)) * dst_positive_scale_restrict_sourcezero)) /\ exists ff_q_pvs_restrict_sourcezeropositive. dst_positive_code_restrict_sourcezero = ff_q_pvs_restrict_sourcezeropositive * S ((S (0)) * dst_positive_scale_restrict_sourcezero) + (dst_positive_restrict_sourcezero))) /\ (((((exists ff_h_pvs_restrict_sourcezeronegative. ff_h_pvs_restrict_sourcezeronegative + S (dst_negative_restrict_sourcezero) = S ((S (0)) * dst_negative_scale_restrict_sourcezero)) /\ exists ff_q_pvs_restrict_sourcezeronegative. dst_negative_code_restrict_sourcezero = ff_q_pvs_restrict_sourcezeronegative * S ((S (0)) * dst_negative_scale_restrict_sourcezero) + (dst_negative_restrict_sourcezero))) /\ (exists ge_balance_positive_restrict_sourcezerovalue ge_balance_negative_restrict_sourcezerovalue. (((((0) = 2 * (ge_balance_positive_restrict_sourcezerovalue) /\ (ge_balance_negative_restrict_sourcezerovalue) = 0) \/ exists ge_signed_half_restrict_sourcezerovaluedecode. (((0) = 2 * ge_signed_half_restrict_sourcezerovaluedecode + 1 /\ (ge_balance_positive_restrict_sourcezerovalue) = 0) /\ (ge_balance_negative_restrict_sourcezerovalue) = S ge_signed_half_restrict_sourcezerovaluedecode))) /\ ((dst_positive_restrict_sourcezero) + ge_balance_negative_restrict_sourcezerovalue = (dst_negative_restrict_sourcezero) + ge_balance_positive_restrict_sourcezerovalue))))))))) /\ (forall mt_index_restrict_source mt_value_restrict_source. ~(mt_index_restrict_source=0) -> (exists pvs_le_gap_restrict_sourcedomain. pvs_le_gap_restrict_sourcedomain + (mt_index_restrict_source) = (N)) -> (exists dst_positive_code_restrict_sourceentry dst_positive_scale_restrict_sourceentry dst_negative_code_restrict_sourceentry dst_negative_scale_restrict_sourceentry dst_positive_restrict_sourceentry dst_negative_restrict_sourceentry. (((M) = (((((dst_positive_code_restrict_sourceentry) + (dst_positive_scale_restrict_sourceentry)) * S ((dst_positive_code_restrict_sourceentry) + (dst_positive_scale_restrict_sourceentry)) + ((dst_positive_scale_restrict_sourceentry) + (dst_positive_scale_restrict_sourceentry))) + (((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) * S ((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) + ((dst_negative_scale_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)))) * S ((((dst_positive_code_restrict_sourceentry) + (dst_positive_scale_restrict_sourceentry)) * S ((dst_positive_code_restrict_sourceentry) + (dst_positive_scale_restrict_sourceentry)) + ((dst_positive_scale_restrict_sourceentry) + (dst_positive_scale_restrict_sourceentry))) + (((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) * S ((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) + ((dst_negative_scale_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)))) + ((((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) * S ((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) + ((dst_negative_scale_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry))) + (((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) * S ((dst_negative_code_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)) + ((dst_negative_scale_restrict_sourceentry) + (dst_negative_scale_restrict_sourceentry)))))) /\ (((((exists ff_h_pvs_restrict_sourceentrypositive. ff_h_pvs_restrict_sourceentrypositive + S (dst_positive_restrict_sourceentry) = S ((S (mt_index_restrict_source)) * dst_positive_scale_restrict_sourceentry)) /\ exists ff_q_pvs_restrict_sourceentrypositive. dst_positive_code_restrict_sourceentry = ff_q_pvs_restrict_sourceentrypositive * S ((S (mt_index_restrict_source)) * dst_positive_scale_restrict_sourceentry) + (dst_positive_restrict_sourceentry))) /\ (((((exists ff_h_pvs_restrict_sourceentrynegative. ff_h_pvs_restrict_sourceentrynegative + S (dst_negative_restrict_sourceentry) = S ((S (mt_index_restrict_source)) * dst_negative_scale_restrict_sourceentry)) /\ exists ff_q_pvs_restrict_sourceentrynegative. dst_negative_code_restrict_sourceentry = ff_q_pvs_restrict_sourceentrynegative * S ((S (mt_index_restrict_source)) * dst_negative_scale_restrict_sourceentry) + (dst_negative_restrict_sourceentry))) /\ (exists ge_balance_positive_restrict_sourceentryvalue ge_balance_negative_restrict_sourceentryvalue. (((((mt_value_restrict_source) = 2 * (ge_balance_positive_restrict_sourceentryvalue) /\ (ge_balance_negative_restrict_sourceentryvalue) = 0) \/ exists ge_signed_half_restrict_sourceentryvaluedecode. (((mt_value_restrict_source) = 2 * ge_signed_half_restrict_sourceentryvaluedecode + 1 /\ (ge_balance_positive_restrict_sourceentryvalue) = 0) /\ (ge_balance_negative_restrict_sourceentryvalue) = S ge_signed_half_restrict_sourceentryvaluedecode))) /\ ((dst_positive_restrict_sourceentry) + ge_balance_negative_restrict_sourceentryvalue = (dst_negative_restrict_sourceentry) + ge_balance_positive_restrict_sourceentryvalue))))))))) -> (((~((mt_index_restrict_source) = 0)) /\ ((((exists mv_square_prime_restrict_sourcevaluesquare. ((~((mv_square_prime_restrict_sourcevaluesquare) = 1) /\ forall pvs_left_restrict_sourcevaluesquareprime pvs_right_restrict_sourcevaluesquareprime. (mv_square_prime_restrict_sourcevaluesquare) = pvs_left_restrict_sourcevaluesquareprime * pvs_right_restrict_sourcevaluesquareprime -> pvs_left_restrict_sourcevaluesquareprime = 1 \/ pvs_right_restrict_sourcevaluesquareprime = 1) /\ (exists pvs_factor_restrict_sourcevaluesquaredivisor. (mt_index_restrict_source) = (mv_square_prime_restrict_sourcevaluesquare * mv_square_prime_restrict_sourcevaluesquare) * pvs_factor_restrict_sourcevaluesquaredivisor))) /\ ((mt_value_restrict_source) = 0))) \/ (((((~((mt_index_restrict_source) = 0)) /\ (forall sfd_prime_restrict_sourcevaluesquarefree. (~((sfd_prime_restrict_sourcevaluesquarefree) = 1) /\ forall pvs_left_restrict_sourcevaluesquarefreedomain pvs_right_restrict_sourcevaluesquarefreedomain. (sfd_prime_restrict_sourcevaluesquarefree) = pvs_left_restrict_sourcevaluesquarefreedomain * pvs_right_restrict_sourcevaluesquarefreedomain -> pvs_left_restrict_sourcevaluesquarefreedomain = 1 \/ pvs_right_restrict_sourcevaluesquarefreedomain = 1) -> (exists pvs_le_gap_restrict_sourcevaluesquarefreebound. pvs_le_gap_restrict_sourcevaluesquarefreebound + (sfd_prime_restrict_sourcevaluesquarefree) = (mt_index_restrict_source)) -> ~(exists pvs_factor_restrict_sourcevaluesquarefreesquare. (mt_index_restrict_source) = (sfd_prime_restrict_sourcevaluesquarefree * sfd_prime_restrict_sourcevaluesquarefree) * pvs_factor_restrict_sourcevaluesquarefreesquare)))) /\ (exists mv_factor_code_restrict_sourcevaluefactors mv_factor_scale_restrict_sourcevaluefactors mv_factor_count_restrict_sourcevaluefactors. (((~(mt_index_restrict_source = 0) /\ ((exists ff_u_fsat_restrict_sourcevaluefactorsfactorization_product ff_v_fsat_restrict_sourcevaluefactorsfactorization_product. ((((exists ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_start. ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_start. ff_u_fsat_restrict_sourcevaluefactorsfactorization_product = ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_terminal. ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_terminal + S (mt_index_restrict_source) = S ((S (mv_factor_count_restrict_sourcevaluefactors)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_terminal. ff_u_fsat_restrict_sourcevaluefactorsfactorization_product = ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_restrict_sourcevaluefactors)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product) + (mt_index_restrict_source))) /\ forall ff_i_fsat_restrict_sourcevaluefactorsfactorization_product. (exists ff_lt_fsat_restrict_sourcevaluefactorsfactorization_product_bound. ff_lt_fsat_restrict_sourcevaluefactorsfactorization_product_bound + S ff_i_fsat_restrict_sourcevaluefactorsfactorization_product = mv_factor_count_restrict_sourcevaluefactors) -> exists ff_p_fsat_restrict_sourcevaluefactorsfactorization_product ff_r_fsat_restrict_sourcevaluefactorsfactorization_product ff_s_fsat_restrict_sourcevaluefactorsfactorization_product. ((((exists ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_factor. ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_factor + S (ff_p_fsat_restrict_sourcevaluefactorsfactorization_product) = S ((S (ff_i_fsat_restrict_sourcevaluefactorsfactorization_product)) * mv_factor_scale_restrict_sourcevaluefactors)) /\ exists ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_factor. mv_factor_code_restrict_sourcevaluefactors = ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_restrict_sourcevaluefactorsfactorization_product)) * mv_factor_scale_restrict_sourcevaluefactors) + (ff_p_fsat_restrict_sourcevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_partial. ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_partial + S (ff_r_fsat_restrict_sourcevaluefactorsfactorization_product) = S ((S (ff_i_fsat_restrict_sourcevaluefactorsfactorization_product)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_partial. ff_u_fsat_restrict_sourcevaluefactorsfactorization_product = ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_restrict_sourcevaluefactorsfactorization_product)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product) + (ff_r_fsat_restrict_sourcevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_successor. ff_h_fsat_restrict_sourcevaluefactorsfactorization_product_successor + S (ff_s_fsat_restrict_sourcevaluefactorsfactorization_product) = S ((S (S ff_i_fsat_restrict_sourcevaluefactorsfactorization_product)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_successor. ff_u_fsat_restrict_sourcevaluefactorsfactorization_product = ff_q_fsat_restrict_sourcevaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_restrict_sourcevaluefactorsfactorization_product)) * ff_v_fsat_restrict_sourcevaluefactorsfactorization_product) + (ff_s_fsat_restrict_sourcevaluefactorsfactorization_product))) /\ ff_s_fsat_restrict_sourcevaluefactorsfactorization_product = ff_r_fsat_restrict_sourcevaluefactorsfactorization_product * ff_p_fsat_restrict_sourcevaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_restrict_sourcevaluefactorsfactorization_primes. (exists ftsf_gap_fsat_restrict_sourcevaluefactorsfactorization_primes_bound. ftsf_gap_fsat_restrict_sourcevaluefactorsfactorization_primes_bound + S ftsf_index_fsat_restrict_sourcevaluefactorsfactorization_primes = (mv_factor_count_restrict_sourcevaluefactors)) -> exists ftsf_factor_fsat_restrict_sourcevaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_restrict_sourcevaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_restrict_sourcevaluefactorsfactorization_primes)) * mv_factor_scale_restrict_sourcevaluefactors)) /\ exists ff_q_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_entry. mv_factor_code_restrict_sourcevaluefactors = ff_q_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_restrict_sourcevaluefactorsfactorization_primes)) * mv_factor_scale_restrict_sourcevaluefactors) + (ftsf_factor_fsat_restrict_sourcevaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_restrict_sourcevaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_prime. ftsf_factor_fsat_restrict_sourcevaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_restrict_sourcevaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_restrict_sourcevaluefactorsparityeven. (mv_factor_count_restrict_sourcevaluefactors) = 2 * mv_even_half_restrict_sourcevaluefactorsparityeven) /\ ((mt_value_restrict_source) = 2))) \/ (((exists mv_odd_half_restrict_sourcevaluefactorsparityodd. (mv_factor_count_restrict_sourcevaluefactors) = 2 * mv_odd_half_restrict_sourcevaluefactorsparityodd + 1) /\ ((mt_value_restrict_source) = 1)))))))))))))))) -> (exists pvs_le_gap_restrict_bound. pvs_le_gap_restrict_bound + (K) = (N)) -> (((exists dst_positive_code_restrict_targettable dst_positive_scale_restrict_targettable dst_negative_code_restrict_targettable dst_negative_scale_restrict_targettable. (((M) = (((((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) * S ((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) + ((dst_positive_scale_restrict_targettable) + (dst_positive_scale_restrict_targettable))) + (((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable)))) * S ((((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) * S ((dst_positive_code_restrict_targettable) + (dst_positive_scale_restrict_targettable)) + ((dst_positive_scale_restrict_targettable) + (dst_positive_scale_restrict_targettable))) + (((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable)))) + ((((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable))) + (((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) * S ((dst_negative_code_restrict_targettable) + (dst_negative_scale_restrict_targettable)) + ((dst_negative_scale_restrict_targettable) + (dst_negative_scale_restrict_targettable)))))) /\ (forall dst_index_restrict_targettable. (exists pvs_le_gap_restrict_targettabledomain. pvs_le_gap_restrict_targettabledomain + (dst_index_restrict_targettable) = (K)) -> exists dst_positive_restrict_targettable dst_negative_restrict_targettable dst_value_restrict_targettable. ((((exists ff_h_pvs_restrict_targettableentrypositive. ff_h_pvs_restrict_targettableentrypositive + S (dst_positive_restrict_targettable) = S ((S (dst_index_restrict_targettable)) * dst_positive_scale_restrict_targettable)) /\ exists ff_q_pvs_restrict_targettableentrypositive. dst_positive_code_restrict_targettable = ff_q_pvs_restrict_targettableentrypositive * S ((S (dst_index_restrict_targettable)) * dst_positive_scale_restrict_targettable) + (dst_positive_restrict_targettable))) /\ (((((exists ff_h_pvs_restrict_targettableentrynegative. ff_h_pvs_restrict_targettableentrynegative + S (dst_negative_restrict_targettable) = S ((S (dst_index_restrict_targettable)) * dst_negative_scale_restrict_targettable)) /\ exists ff_q_pvs_restrict_targettableentrynegative. dst_negative_code_restrict_targettable = ff_q_pvs_restrict_targettableentrynegative * S ((S (dst_index_restrict_targettable)) * dst_negative_scale_restrict_targettable) + (dst_negative_restrict_targettable))) /\ (exists ge_balance_positive_restrict_targettableentryvalue ge_balance_negative_restrict_targettableentryvalue. (((((dst_value_restrict_targettable) = 2 * (ge_balance_positive_restrict_targettableentryvalue) /\ (ge_balance_negative_restrict_targettableentryvalue) = 0) \/ exists ge_signed_half_restrict_targettableentryvaluedecode. (((dst_value_restrict_targettable) = 2 * ge_signed_half_restrict_targettableentryvaluedecode + 1 /\ (ge_balance_positive_restrict_targettableentryvalue) = 0) /\ (ge_balance_negative_restrict_targettableentryvalue) = S ge_signed_half_restrict_targettableentryvaluedecode))) /\ ((dst_positive_restrict_targettable) + ge_balance_negative_restrict_targettableentryvalue = (dst_negative_restrict_targettable) + ge_balance_positive_restrict_targettableentryvalue))))))))) /\ (((exists dst_positive_code_restrict_targetzero dst_positive_scale_restrict_targetzero dst_negative_code_restrict_targetzero dst_negative_scale_restrict_targetzero dst_positive_restrict_targetzero dst_negative_restrict_targetzero. (((M) = (((((dst_positive_code_restrict_targetzero) + (dst_positive_scale_restrict_targetzero)) * S ((dst_positive_code_restrict_targetzero) + (dst_positive_scale_restrict_targetzero)) + ((dst_positive_scale_restrict_targetzero) + (dst_positive_scale_restrict_targetzero))) + (((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) * S ((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) + ((dst_negative_scale_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)))) * S ((((dst_positive_code_restrict_targetzero) + (dst_positive_scale_restrict_targetzero)) * S ((dst_positive_code_restrict_targetzero) + (dst_positive_scale_restrict_targetzero)) + ((dst_positive_scale_restrict_targetzero) + (dst_positive_scale_restrict_targetzero))) + (((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) * S ((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) + ((dst_negative_scale_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)))) + ((((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) * S ((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) + ((dst_negative_scale_restrict_targetzero) + (dst_negative_scale_restrict_targetzero))) + (((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) * S ((dst_negative_code_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)) + ((dst_negative_scale_restrict_targetzero) + (dst_negative_scale_restrict_targetzero)))))) /\ (((((exists ff_h_pvs_restrict_targetzeropositive. ff_h_pvs_restrict_targetzeropositive + S (dst_positive_restrict_targetzero) = S ((S (0)) * dst_positive_scale_restrict_targetzero)) /\ exists ff_q_pvs_restrict_targetzeropositive. dst_positive_code_restrict_targetzero = ff_q_pvs_restrict_targetzeropositive * S ((S (0)) * dst_positive_scale_restrict_targetzero) + (dst_positive_restrict_targetzero))) /\ (((((exists ff_h_pvs_restrict_targetzeronegative. ff_h_pvs_restrict_targetzeronegative + S (dst_negative_restrict_targetzero) = S ((S (0)) * dst_negative_scale_restrict_targetzero)) /\ exists ff_q_pvs_restrict_targetzeronegative. dst_negative_code_restrict_targetzero = ff_q_pvs_restrict_targetzeronegative * S ((S (0)) * dst_negative_scale_restrict_targetzero) + (dst_negative_restrict_targetzero))) /\ (exists ge_balance_positive_restrict_targetzerovalue ge_balance_negative_restrict_targetzerovalue. (((((0) = 2 * (ge_balance_positive_restrict_targetzerovalue) /\ (ge_balance_negative_restrict_targetzerovalue) = 0) \/ exists ge_signed_half_restrict_targetzerovaluedecode. (((0) = 2 * ge_signed_half_restrict_targetzerovaluedecode + 1 /\ (ge_balance_positive_restrict_targetzerovalue) = 0) /\ (ge_balance_negative_restrict_targetzerovalue) = S ge_signed_half_restrict_targetzerovaluedecode))) /\ ((dst_positive_restrict_targetzero) + ge_balance_negative_restrict_targetzerovalue = (dst_negative_restrict_targetzero) + ge_balance_positive_restrict_targetzerovalue))))))))) /\ (forall mt_index_restrict_target mt_value_restrict_target. ~(mt_index_restrict_target=0) -> (exists pvs_le_gap_restrict_targetdomain. pvs_le_gap_restrict_targetdomain + (mt_index_restrict_target) = (K)) -> (exists dst_positive_code_restrict_targetentry dst_positive_scale_restrict_targetentry dst_negative_code_restrict_targetentry dst_negative_scale_restrict_targetentry dst_positive_restrict_targetentry dst_negative_restrict_targetentry. (((M) = (((((dst_positive_code_restrict_targetentry) + (dst_positive_scale_restrict_targetentry)) * S ((dst_positive_code_restrict_targetentry) + (dst_positive_scale_restrict_targetentry)) + ((dst_positive_scale_restrict_targetentry) + (dst_positive_scale_restrict_targetentry))) + (((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) * S ((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) + ((dst_negative_scale_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)))) * S ((((dst_positive_code_restrict_targetentry) + (dst_positive_scale_restrict_targetentry)) * S ((dst_positive_code_restrict_targetentry) + (dst_positive_scale_restrict_targetentry)) + ((dst_positive_scale_restrict_targetentry) + (dst_positive_scale_restrict_targetentry))) + (((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) * S ((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) + ((dst_negative_scale_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)))) + ((((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) * S ((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) + ((dst_negative_scale_restrict_targetentry) + (dst_negative_scale_restrict_targetentry))) + (((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) * S ((dst_negative_code_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)) + ((dst_negative_scale_restrict_targetentry) + (dst_negative_scale_restrict_targetentry)))))) /\ (((((exists ff_h_pvs_restrict_targetentrypositive. ff_h_pvs_restrict_targetentrypositive + S (dst_positive_restrict_targetentry) = S ((S (mt_index_restrict_target)) * dst_positive_scale_restrict_targetentry)) /\ exists ff_q_pvs_restrict_targetentrypositive. dst_positive_code_restrict_targetentry = ff_q_pvs_restrict_targetentrypositive * S ((S (mt_index_restrict_target)) * dst_positive_scale_restrict_targetentry) + (dst_positive_restrict_targetentry))) /\ (((((exists ff_h_pvs_restrict_targetentrynegative. ff_h_pvs_restrict_targetentrynegative + S (dst_negative_restrict_targetentry) = S ((S (mt_index_restrict_target)) * dst_negative_scale_restrict_targetentry)) /\ exists ff_q_pvs_restrict_targetentrynegative. dst_negative_code_restrict_targetentry = ff_q_pvs_restrict_targetentrynegative * S ((S (mt_index_restrict_target)) * dst_negative_scale_restrict_targetentry) + (dst_negative_restrict_targetentry))) /\ (exists ge_balance_positive_restrict_targetentryvalue ge_balance_negative_restrict_targetentryvalue. (((((mt_value_restrict_target) = 2 * (ge_balance_positive_restrict_targetentryvalue) /\ (ge_balance_negative_restrict_targetentryvalue) = 0) \/ exists ge_signed_half_restrict_targetentryvaluedecode. (((mt_value_restrict_target) = 2 * ge_signed_half_restrict_targetentryvaluedecode + 1 /\ (ge_balance_positive_restrict_targetentryvalue) = 0) /\ (ge_balance_negative_restrict_targetentryvalue) = S ge_signed_half_restrict_targetentryvaluedecode))) /\ ((dst_positive_restrict_targetentry) + ge_balance_negative_restrict_targetentryvalue = (dst_negative_restrict_targetentry) + ge_balance_positive_restrict_targetentryvalue))))))))) -> (((~((mt_index_restrict_target) = 0)) /\ ((((exists mv_square_prime_restrict_targetvaluesquare. ((~((mv_square_prime_restrict_targetvaluesquare) = 1) /\ forall pvs_left_restrict_targetvaluesquareprime pvs_right_restrict_targetvaluesquareprime. (mv_square_prime_restrict_targetvaluesquare) = pvs_left_restrict_targetvaluesquareprime * pvs_right_restrict_targetvaluesquareprime -> pvs_left_restrict_targetvaluesquareprime = 1 \/ pvs_right_restrict_targetvaluesquareprime = 1) /\ (exists pvs_factor_restrict_targetvaluesquaredivisor. (mt_index_restrict_target) = (mv_square_prime_restrict_targetvaluesquare * mv_square_prime_restrict_targetvaluesquare) * pvs_factor_restrict_targetvaluesquaredivisor))) /\ ((mt_value_restrict_target) = 0))) \/ (((((~((mt_index_restrict_target) = 0)) /\ (forall sfd_prime_restrict_targetvaluesquarefree. (~((sfd_prime_restrict_targetvaluesquarefree) = 1) /\ forall pvs_left_restrict_targetvaluesquarefreedomain pvs_right_restrict_targetvaluesquarefreedomain. (sfd_prime_restrict_targetvaluesquarefree) = pvs_left_restrict_targetvaluesquarefreedomain * pvs_right_restrict_targetvaluesquarefreedomain -> pvs_left_restrict_targetvaluesquarefreedomain = 1 \/ pvs_right_restrict_targetvaluesquarefreedomain = 1) -> (exists pvs_le_gap_restrict_targetvaluesquarefreebound. pvs_le_gap_restrict_targetvaluesquarefreebound + (sfd_prime_restrict_targetvaluesquarefree) = (mt_index_restrict_target)) -> ~(exists pvs_factor_restrict_targetvaluesquarefreesquare. (mt_index_restrict_target) = (sfd_prime_restrict_targetvaluesquarefree * sfd_prime_restrict_targetvaluesquarefree) * pvs_factor_restrict_targetvaluesquarefreesquare)))) /\ (exists mv_factor_code_restrict_targetvaluefactors mv_factor_scale_restrict_targetvaluefactors mv_factor_count_restrict_targetvaluefactors. (((~(mt_index_restrict_target = 0) /\ ((exists ff_u_fsat_restrict_targetvaluefactorsfactorization_product ff_v_fsat_restrict_targetvaluefactorsfactorization_product. ((((exists ff_h_fsat_restrict_targetvaluefactorsfactorization_product_start. ff_h_fsat_restrict_targetvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_targetvaluefactorsfactorization_product_start. ff_u_fsat_restrict_targetvaluefactorsfactorization_product = ff_q_fsat_restrict_targetvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_restrict_targetvaluefactorsfactorization_product_terminal. ff_h_fsat_restrict_targetvaluefactorsfactorization_product_terminal + S (mt_index_restrict_target) = S ((S (mv_factor_count_restrict_targetvaluefactors)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_targetvaluefactorsfactorization_product_terminal. ff_u_fsat_restrict_targetvaluefactorsfactorization_product = ff_q_fsat_restrict_targetvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_restrict_targetvaluefactors)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product) + (mt_index_restrict_target))) /\ forall ff_i_fsat_restrict_targetvaluefactorsfactorization_product. (exists ff_lt_fsat_restrict_targetvaluefactorsfactorization_product_bound. ff_lt_fsat_restrict_targetvaluefactorsfactorization_product_bound + S ff_i_fsat_restrict_targetvaluefactorsfactorization_product = mv_factor_count_restrict_targetvaluefactors) -> exists ff_p_fsat_restrict_targetvaluefactorsfactorization_product ff_r_fsat_restrict_targetvaluefactorsfactorization_product ff_s_fsat_restrict_targetvaluefactorsfactorization_product. ((((exists ff_h_fsat_restrict_targetvaluefactorsfactorization_product_factor. ff_h_fsat_restrict_targetvaluefactorsfactorization_product_factor + S (ff_p_fsat_restrict_targetvaluefactorsfactorization_product) = S ((S (ff_i_fsat_restrict_targetvaluefactorsfactorization_product)) * mv_factor_scale_restrict_targetvaluefactors)) /\ exists ff_q_fsat_restrict_targetvaluefactorsfactorization_product_factor. mv_factor_code_restrict_targetvaluefactors = ff_q_fsat_restrict_targetvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_restrict_targetvaluefactorsfactorization_product)) * mv_factor_scale_restrict_targetvaluefactors) + (ff_p_fsat_restrict_targetvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_restrict_targetvaluefactorsfactorization_product_partial. ff_h_fsat_restrict_targetvaluefactorsfactorization_product_partial + S (ff_r_fsat_restrict_targetvaluefactorsfactorization_product) = S ((S (ff_i_fsat_restrict_targetvaluefactorsfactorization_product)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_targetvaluefactorsfactorization_product_partial. ff_u_fsat_restrict_targetvaluefactorsfactorization_product = ff_q_fsat_restrict_targetvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_restrict_targetvaluefactorsfactorization_product)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product) + (ff_r_fsat_restrict_targetvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_restrict_targetvaluefactorsfactorization_product_successor. ff_h_fsat_restrict_targetvaluefactorsfactorization_product_successor + S (ff_s_fsat_restrict_targetvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_restrict_targetvaluefactorsfactorization_product)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product)) /\ exists ff_q_fsat_restrict_targetvaluefactorsfactorization_product_successor. ff_u_fsat_restrict_targetvaluefactorsfactorization_product = ff_q_fsat_restrict_targetvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_restrict_targetvaluefactorsfactorization_product)) * ff_v_fsat_restrict_targetvaluefactorsfactorization_product) + (ff_s_fsat_restrict_targetvaluefactorsfactorization_product))) /\ ff_s_fsat_restrict_targetvaluefactorsfactorization_product = ff_r_fsat_restrict_targetvaluefactorsfactorization_product * ff_p_fsat_restrict_targetvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_restrict_targetvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_restrict_targetvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_restrict_targetvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_restrict_targetvaluefactorsfactorization_primes = (mv_factor_count_restrict_targetvaluefactors)) -> exists ftsf_factor_fsat_restrict_targetvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_restrict_targetvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_restrict_targetvaluefactorsfactorization_primes)) * mv_factor_scale_restrict_targetvaluefactors)) /\ exists ff_q_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_entry. mv_factor_code_restrict_targetvaluefactors = ff_q_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_restrict_targetvaluefactorsfactorization_primes)) * mv_factor_scale_restrict_targetvaluefactors) + (ftsf_factor_fsat_restrict_targetvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_restrict_targetvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_restrict_targetvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_restrict_targetvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_restrict_targetvaluefactorsparityeven. (mv_factor_count_restrict_targetvaluefactors) = 2 * mv_even_half_restrict_targetvaluefactorsparityeven) /\ ((mt_value_restrict_target) = 2))) \/ (((exists mv_odd_half_restrict_targetvaluefactorsparityodd. (mv_factor_count_restrict_targetvaluefactors) = 2 * mv_odd_half_restrict_targetvaluefactorsparityodd + 1) /\ ((mt_value_restrict_target) = 1))))))))))))))))