MobiusTable(N,M)

((exists dst_positive_code_lowertiertable dst_positive_scale_lowertiertable dst_negative_code_lowertiertable dst_negative_scale_lowertiertable. ((((M)) = (((((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) * S ((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) + ((dst_positive_scale_lowertiertable) + (dst_positive_scale_lowertiertable))) + (((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable)))) * S ((((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) * S ((dst_positive_code_lowertiertable) + (dst_positive_scale_lowertiertable)) + ((dst_positive_scale_lowertiertable) + (dst_positive_scale_lowertiertable))) + (((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable)))) + ((((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable))) + (((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) * S ((dst_negative_code_lowertiertable) + (dst_negative_scale_lowertiertable)) + ((dst_negative_scale_lowertiertable) + (dst_negative_scale_lowertiertable)))))) /\ (forall dst_index_lowertiertable. (exists pvs_le_gap_lowertiertabledomain. pvs_le_gap_lowertiertabledomain + (dst_index_lowertiertable) = ((N))) -> exists dst_positive_lowertiertable dst_negative_lowertiertable dst_value_lowertiertable. ((((exists ff_h_pvs_lowertiertableentrypositive. ff_h_pvs_lowertiertableentrypositive + S (dst_positive_lowertiertable) = S ((S (dst_index_lowertiertable)) * dst_positive_scale_lowertiertable)) /\ exists ff_q_pvs_lowertiertableentrypositive. dst_positive_code_lowertiertable = ff_q_pvs_lowertiertableentrypositive * S ((S (dst_index_lowertiertable)) * dst_positive_scale_lowertiertable) + (dst_positive_lowertiertable))) /\ (((((exists ff_h_pvs_lowertiertableentrynegative. ff_h_pvs_lowertiertableentrynegative + S (dst_negative_lowertiertable) = S ((S (dst_index_lowertiertable)) * dst_negative_scale_lowertiertable)) /\ exists ff_q_pvs_lowertiertableentrynegative. dst_negative_code_lowertiertable = ff_q_pvs_lowertiertableentrynegative * S ((S (dst_index_lowertiertable)) * dst_negative_scale_lowertiertable) + (dst_negative_lowertiertable))) /\ (exists ge_balance_positive_lowertiertableentryvalue ge_balance_negative_lowertiertableentryvalue. (((((dst_value_lowertiertable) = 2 * (ge_balance_positive_lowertiertableentryvalue) /\ (ge_balance_negative_lowertiertableentryvalue) = 0) \/ exists ge_signed_half_lowertiertableentryvaluedecode. (((dst_value_lowertiertable) = 2 * ge_signed_half_lowertiertableentryvaluedecode + 1 /\ (ge_balance_positive_lowertiertableentryvalue) = 0) /\ (ge_balance_negative_lowertiertableentryvalue) = S ge_signed_half_lowertiertableentryvaluedecode))) /\ ((dst_positive_lowertiertable) + ge_balance_negative_lowertiertableentryvalue = (dst_negative_lowertiertable) + ge_balance_positive_lowertiertableentryvalue))))))))) /\ (((exists dst_positive_code_lowertierzero dst_positive_scale_lowertierzero dst_negative_code_lowertierzero dst_negative_scale_lowertierzero dst_positive_lowertierzero dst_negative_lowertierzero. ((((M)) = (((((dst_positive_code_lowertierzero) + (dst_positive_scale_lowertierzero)) * S ((dst_positive_code_lowertierzero) + (dst_positive_scale_lowertierzero)) + ((dst_positive_scale_lowertierzero) + (dst_positive_scale_lowertierzero))) + (((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) * S ((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) + ((dst_negative_scale_lowertierzero) + (dst_negative_scale_lowertierzero)))) * S ((((dst_positive_code_lowertierzero) + (dst_positive_scale_lowertierzero)) * S ((dst_positive_code_lowertierzero) + (dst_positive_scale_lowertierzero)) + ((dst_positive_scale_lowertierzero) + (dst_positive_scale_lowertierzero))) + (((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) * S ((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) + ((dst_negative_scale_lowertierzero) + (dst_negative_scale_lowertierzero)))) + ((((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) * S ((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) + ((dst_negative_scale_lowertierzero) + (dst_negative_scale_lowertierzero))) + (((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) * S ((dst_negative_code_lowertierzero) + (dst_negative_scale_lowertierzero)) + ((dst_negative_scale_lowertierzero) + (dst_negative_scale_lowertierzero)))))) /\ (((((exists ff_h_pvs_lowertierzeropositive. ff_h_pvs_lowertierzeropositive + S (dst_positive_lowertierzero) = S ((S (0)) * dst_positive_scale_lowertierzero)) /\ exists ff_q_pvs_lowertierzeropositive. dst_positive_code_lowertierzero = ff_q_pvs_lowertierzeropositive * S ((S (0)) * dst_positive_scale_lowertierzero) + (dst_positive_lowertierzero))) /\ (((((exists ff_h_pvs_lowertierzeronegative. ff_h_pvs_lowertierzeronegative + S (dst_negative_lowertierzero) = S ((S (0)) * dst_negative_scale_lowertierzero)) /\ exists ff_q_pvs_lowertierzeronegative. dst_negative_code_lowertierzero = ff_q_pvs_lowertierzeronegative * S ((S (0)) * dst_negative_scale_lowertierzero) + (dst_negative_lowertierzero))) /\ (exists ge_balance_positive_lowertierzerovalue ge_balance_negative_lowertierzerovalue. (((((0) = 2 * (ge_balance_positive_lowertierzerovalue) /\ (ge_balance_negative_lowertierzerovalue) = 0) \/ exists ge_signed_half_lowertierzerovaluedecode. (((0) = 2 * ge_signed_half_lowertierzerovaluedecode + 1 /\ (ge_balance_positive_lowertierzerovalue) = 0) /\ (ge_balance_negative_lowertierzerovalue) = S ge_signed_half_lowertierzerovaluedecode))) /\ ((dst_positive_lowertierzero) + ge_balance_negative_lowertierzerovalue = (dst_negative_lowertierzero) + ge_balance_positive_lowertierzerovalue))))))))) /\ (forall mt_index_lowertier mt_value_lowertier. ~(mt_index_lowertier=0) -> (exists pvs_le_gap_lowertierdomain. pvs_le_gap_lowertierdomain + (mt_index_lowertier) = ((N))) -> (exists dst_positive_code_lowertierentry dst_positive_scale_lowertierentry dst_negative_code_lowertierentry dst_negative_scale_lowertierentry dst_positive_lowertierentry dst_negative_lowertierentry. ((((M)) = (((((dst_positive_code_lowertierentry) + (dst_positive_scale_lowertierentry)) * S ((dst_positive_code_lowertierentry) + (dst_positive_scale_lowertierentry)) + ((dst_positive_scale_lowertierentry) + (dst_positive_scale_lowertierentry))) + (((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) * S ((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) + ((dst_negative_scale_lowertierentry) + (dst_negative_scale_lowertierentry)))) * S ((((dst_positive_code_lowertierentry) + (dst_positive_scale_lowertierentry)) * S ((dst_positive_code_lowertierentry) + (dst_positive_scale_lowertierentry)) + ((dst_positive_scale_lowertierentry) + (dst_positive_scale_lowertierentry))) + (((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) * S ((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) + ((dst_negative_scale_lowertierentry) + (dst_negative_scale_lowertierentry)))) + ((((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) * S ((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) + ((dst_negative_scale_lowertierentry) + (dst_negative_scale_lowertierentry))) + (((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) * S ((dst_negative_code_lowertierentry) + (dst_negative_scale_lowertierentry)) + ((dst_negative_scale_lowertierentry) + (dst_negative_scale_lowertierentry)))))) /\ (((((exists ff_h_pvs_lowertierentrypositive. ff_h_pvs_lowertierentrypositive + S (dst_positive_lowertierentry) = S ((S (mt_index_lowertier)) * dst_positive_scale_lowertierentry)) /\ exists ff_q_pvs_lowertierentrypositive. dst_positive_code_lowertierentry = ff_q_pvs_lowertierentrypositive * S ((S (mt_index_lowertier)) * dst_positive_scale_lowertierentry) + (dst_positive_lowertierentry))) /\ (((((exists ff_h_pvs_lowertierentrynegative. ff_h_pvs_lowertierentrynegative + S (dst_negative_lowertierentry) = S ((S (mt_index_lowertier)) * dst_negative_scale_lowertierentry)) /\ exists ff_q_pvs_lowertierentrynegative. dst_negative_code_lowertierentry = ff_q_pvs_lowertierentrynegative * S ((S (mt_index_lowertier)) * dst_negative_scale_lowertierentry) + (dst_negative_lowertierentry))) /\ (exists ge_balance_positive_lowertierentryvalue ge_balance_negative_lowertierentryvalue. (((((mt_value_lowertier) = 2 * (ge_balance_positive_lowertierentryvalue) /\ (ge_balance_negative_lowertierentryvalue) = 0) \/ exists ge_signed_half_lowertierentryvaluedecode. (((mt_value_lowertier) = 2 * ge_signed_half_lowertierentryvaluedecode + 1 /\ (ge_balance_positive_lowertierentryvalue) = 0) /\ (ge_balance_negative_lowertierentryvalue) = S ge_signed_half_lowertierentryvaluedecode))) /\ ((dst_positive_lowertierentry) + ge_balance_negative_lowertierentryvalue = (dst_negative_lowertierentry) + ge_balance_positive_lowertierentryvalue))))))))) -> (((~((mt_index_lowertier) = 0)) /\ ((((exists mv_square_prime_lowertiervaluesquare. ((~((mv_square_prime_lowertiervaluesquare) = 1) /\ forall pvs_left_lowertiervaluesquareprime pvs_right_lowertiervaluesquareprime. (mv_square_prime_lowertiervaluesquare) = pvs_left_lowertiervaluesquareprime * pvs_right_lowertiervaluesquareprime -> pvs_left_lowertiervaluesquareprime = 1 \/ pvs_right_lowertiervaluesquareprime = 1) /\ (exists pvs_factor_lowertiervaluesquaredivisor. (mt_index_lowertier) = (mv_square_prime_lowertiervaluesquare * mv_square_prime_lowertiervaluesquare) * pvs_factor_lowertiervaluesquaredivisor))) /\ ((mt_value_lowertier) = 0))) \/ (((((~((mt_index_lowertier) = 0)) /\ (forall sfd_prime_lowertiervaluesquarefree. (~((sfd_prime_lowertiervaluesquarefree) = 1) /\ forall pvs_left_lowertiervaluesquarefreedomain pvs_right_lowertiervaluesquarefreedomain. (sfd_prime_lowertiervaluesquarefree) = pvs_left_lowertiervaluesquarefreedomain * pvs_right_lowertiervaluesquarefreedomain -> pvs_left_lowertiervaluesquarefreedomain = 1 \/ pvs_right_lowertiervaluesquarefreedomain = 1) -> (exists pvs_le_gap_lowertiervaluesquarefreebound. pvs_le_gap_lowertiervaluesquarefreebound + (sfd_prime_lowertiervaluesquarefree) = (mt_index_lowertier)) -> ~(exists pvs_factor_lowertiervaluesquarefreesquare. (mt_index_lowertier) = (sfd_prime_lowertiervaluesquarefree * sfd_prime_lowertiervaluesquarefree) * pvs_factor_lowertiervaluesquarefreesquare)))) /\ (exists mv_factor_code_lowertiervaluefactors mv_factor_scale_lowertiervaluefactors mv_factor_count_lowertiervaluefactors. (((~(mt_index_lowertier = 0) /\ ((exists ff_u_fsat_lowertiervaluefactorsfactorization_product ff_v_fsat_lowertiervaluefactorsfactorization_product. ((((exists ff_h_fsat_lowertiervaluefactorsfactorization_product_start. ff_h_fsat_lowertiervaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_lowertiervaluefactorsfactorization_product)) /\ exists ff_q_fsat_lowertiervaluefactorsfactorization_product_start. ff_u_fsat_lowertiervaluefactorsfactorization_product = ff_q_fsat_lowertiervaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_lowertiervaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_lowertiervaluefactorsfactorization_product_terminal. ff_h_fsat_lowertiervaluefactorsfactorization_product_terminal + S (mt_index_lowertier) = S ((S (mv_factor_count_lowertiervaluefactors)) * ff_v_fsat_lowertiervaluefactorsfactorization_product)) /\ exists ff_q_fsat_lowertiervaluefactorsfactorization_product_terminal. ff_u_fsat_lowertiervaluefactorsfactorization_product = ff_q_fsat_lowertiervaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_lowertiervaluefactors)) * ff_v_fsat_lowertiervaluefactorsfactorization_product) + (mt_index_lowertier))) /\ forall ff_i_fsat_lowertiervaluefactorsfactorization_product. (exists ff_lt_fsat_lowertiervaluefactorsfactorization_product_bound. ff_lt_fsat_lowertiervaluefactorsfactorization_product_bound + S ff_i_fsat_lowertiervaluefactorsfactorization_product = mv_factor_count_lowertiervaluefactors) -> exists ff_p_fsat_lowertiervaluefactorsfactorization_product ff_r_fsat_lowertiervaluefactorsfactorization_product ff_s_fsat_lowertiervaluefactorsfactorization_product. ((((exists ff_h_fsat_lowertiervaluefactorsfactorization_product_factor. ff_h_fsat_lowertiervaluefactorsfactorization_product_factor + S (ff_p_fsat_lowertiervaluefactorsfactorization_product) = S ((S (ff_i_fsat_lowertiervaluefactorsfactorization_product)) * mv_factor_scale_lowertiervaluefactors)) /\ exists ff_q_fsat_lowertiervaluefactorsfactorization_product_factor. mv_factor_code_lowertiervaluefactors = ff_q_fsat_lowertiervaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_lowertiervaluefactorsfactorization_product)) * mv_factor_scale_lowertiervaluefactors) + (ff_p_fsat_lowertiervaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_lowertiervaluefactorsfactorization_product_partial. ff_h_fsat_lowertiervaluefactorsfactorization_product_partial + S (ff_r_fsat_lowertiervaluefactorsfactorization_product) = S ((S (ff_i_fsat_lowertiervaluefactorsfactorization_product)) * ff_v_fsat_lowertiervaluefactorsfactorization_product)) /\ exists ff_q_fsat_lowertiervaluefactorsfactorization_product_partial. ff_u_fsat_lowertiervaluefactorsfactorization_product = ff_q_fsat_lowertiervaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_lowertiervaluefactorsfactorization_product)) * ff_v_fsat_lowertiervaluefactorsfactorization_product) + (ff_r_fsat_lowertiervaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_lowertiervaluefactorsfactorization_product_successor. ff_h_fsat_lowertiervaluefactorsfactorization_product_successor + S (ff_s_fsat_lowertiervaluefactorsfactorization_product) = S ((S (S ff_i_fsat_lowertiervaluefactorsfactorization_product)) * ff_v_fsat_lowertiervaluefactorsfactorization_product)) /\ exists ff_q_fsat_lowertiervaluefactorsfactorization_product_successor. ff_u_fsat_lowertiervaluefactorsfactorization_product = ff_q_fsat_lowertiervaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_lowertiervaluefactorsfactorization_product)) * ff_v_fsat_lowertiervaluefactorsfactorization_product) + (ff_s_fsat_lowertiervaluefactorsfactorization_product))) /\ ff_s_fsat_lowertiervaluefactorsfactorization_product = ff_r_fsat_lowertiervaluefactorsfactorization_product * ff_p_fsat_lowertiervaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_lowertiervaluefactorsfactorization_primes. (exists ftsf_gap_fsat_lowertiervaluefactorsfactorization_primes_bound. ftsf_gap_fsat_lowertiervaluefactorsfactorization_primes_bound + S ftsf_index_fsat_lowertiervaluefactorsfactorization_primes = (mv_factor_count_lowertiervaluefactors)) -> exists ftsf_factor_fsat_lowertiervaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_lowertiervaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_lowertiervaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_lowertiervaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_lowertiervaluefactorsfactorization_primes)) * mv_factor_scale_lowertiervaluefactors)) /\ exists ff_q_ftsf_fsat_lowertiervaluefactorsfactorization_primes_entry. mv_factor_code_lowertiervaluefactors = ff_q_ftsf_fsat_lowertiervaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_lowertiervaluefactorsfactorization_primes)) * mv_factor_scale_lowertiervaluefactors) + (ftsf_factor_fsat_lowertiervaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_lowertiervaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_lowertiervaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_lowertiervaluefactorsfactorization_primes_prime. ftsf_factor_fsat_lowertiervaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_lowertiervaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_lowertiervaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_lowertiervaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_lowertiervaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_lowertiervaluefactorsparityeven. (mv_factor_count_lowertiervaluefactors) = 2 * mv_even_half_lowertiervaluefactorsparityeven) /\ ((mt_value_lowertier) = 2))) \/ (((exists mv_odd_half_lowertiervaluefactorsparityodd. (mv_factor_count_lowertiervaluefactors) = 2 * mv_odd_half_lowertiervaluefactorsparityodd + 1) /\ ((mt_value_lowertier) = 1)))))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.