MobiusPositiveValues(N,F)

forall mdc_positive_index_lowercontinuation mdc_positive_value_lowercontinuation. ~(mdc_positive_index_lowercontinuation=0) -> (exists pvs_le_gap_lowercontinuationbound. pvs_le_gap_lowercontinuationbound + (mdc_positive_index_lowercontinuation) = ((N))) -> (exists dst_positive_code_lowercontinuationentry dst_positive_scale_lowercontinuationentry dst_negative_code_lowercontinuationentry dst_negative_scale_lowercontinuationentry dst_positive_lowercontinuationentry dst_negative_lowercontinuationentry. ((((F)) = (((((dst_positive_code_lowercontinuationentry) + (dst_positive_scale_lowercontinuationentry)) * S ((dst_positive_code_lowercontinuationentry) + (dst_positive_scale_lowercontinuationentry)) + ((dst_positive_scale_lowercontinuationentry) + (dst_positive_scale_lowercontinuationentry))) + (((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) * S ((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) + ((dst_negative_scale_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)))) * S ((((dst_positive_code_lowercontinuationentry) + (dst_positive_scale_lowercontinuationentry)) * S ((dst_positive_code_lowercontinuationentry) + (dst_positive_scale_lowercontinuationentry)) + ((dst_positive_scale_lowercontinuationentry) + (dst_positive_scale_lowercontinuationentry))) + (((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) * S ((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) + ((dst_negative_scale_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)))) + ((((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) * S ((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) + ((dst_negative_scale_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry))) + (((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) * S ((dst_negative_code_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)) + ((dst_negative_scale_lowercontinuationentry) + (dst_negative_scale_lowercontinuationentry)))))) /\ (((((exists ff_h_pvs_lowercontinuationentrypositive. ff_h_pvs_lowercontinuationentrypositive + S (dst_positive_lowercontinuationentry) = S ((S (mdc_positive_index_lowercontinuation)) * dst_positive_scale_lowercontinuationentry)) /\ exists ff_q_pvs_lowercontinuationentrypositive. dst_positive_code_lowercontinuationentry = ff_q_pvs_lowercontinuationentrypositive * S ((S (mdc_positive_index_lowercontinuation)) * dst_positive_scale_lowercontinuationentry) + (dst_positive_lowercontinuationentry))) /\ (((((exists ff_h_pvs_lowercontinuationentrynegative. ff_h_pvs_lowercontinuationentrynegative + S (dst_negative_lowercontinuationentry) = S ((S (mdc_positive_index_lowercontinuation)) * dst_negative_scale_lowercontinuationentry)) /\ exists ff_q_pvs_lowercontinuationentrynegative. dst_negative_code_lowercontinuationentry = ff_q_pvs_lowercontinuationentrynegative * S ((S (mdc_positive_index_lowercontinuation)) * dst_negative_scale_lowercontinuationentry) + (dst_negative_lowercontinuationentry))) /\ (exists ge_balance_positive_lowercontinuationentryvalue ge_balance_negative_lowercontinuationentryvalue. (((((mdc_positive_value_lowercontinuation) = 2 * (ge_balance_positive_lowercontinuationentryvalue) /\ (ge_balance_negative_lowercontinuationentryvalue) = 0) \/ exists ge_signed_half_lowercontinuationentryvaluedecode. (((mdc_positive_value_lowercontinuation) = 2 * ge_signed_half_lowercontinuationentryvaluedecode + 1 /\ (ge_balance_positive_lowercontinuationentryvalue) = 0) /\ (ge_balance_negative_lowercontinuationentryvalue) = S ge_signed_half_lowercontinuationentryvaluedecode))) /\ ((dst_positive_lowercontinuationentry) + ge_balance_negative_lowercontinuationentryvalue = (dst_negative_lowercontinuationentry) + ge_balance_positive_lowercontinuationentryvalue))))))))) -> (((~((mdc_positive_index_lowercontinuation) = 0)) /\ ((((exists mv_square_prime_lowercontinuationmobiussquare. ((~((mv_square_prime_lowercontinuationmobiussquare) = 1) /\ forall pvs_left_lowercontinuationmobiussquareprime pvs_right_lowercontinuationmobiussquareprime. (mv_square_prime_lowercontinuationmobiussquare) = pvs_left_lowercontinuationmobiussquareprime * pvs_right_lowercontinuationmobiussquareprime -> pvs_left_lowercontinuationmobiussquareprime = 1 \/ pvs_right_lowercontinuationmobiussquareprime = 1) /\ (exists pvs_factor_lowercontinuationmobiussquaredivisor. (mdc_positive_index_lowercontinuation) = (mv_square_prime_lowercontinuationmobiussquare * mv_square_prime_lowercontinuationmobiussquare) * pvs_factor_lowercontinuationmobiussquaredivisor))) /\ ((mdc_positive_value_lowercontinuation) = 0))) \/ (((((~((mdc_positive_index_lowercontinuation) = 0)) /\ (forall sfd_prime_lowercontinuationmobiussquarefree. (~((sfd_prime_lowercontinuationmobiussquarefree) = 1) /\ forall pvs_left_lowercontinuationmobiussquarefreedomain pvs_right_lowercontinuationmobiussquarefreedomain. (sfd_prime_lowercontinuationmobiussquarefree) = pvs_left_lowercontinuationmobiussquarefreedomain * pvs_right_lowercontinuationmobiussquarefreedomain -> pvs_left_lowercontinuationmobiussquarefreedomain = 1 \/ pvs_right_lowercontinuationmobiussquarefreedomain = 1) -> (exists pvs_le_gap_lowercontinuationmobiussquarefreebound. pvs_le_gap_lowercontinuationmobiussquarefreebound + (sfd_prime_lowercontinuationmobiussquarefree) = (mdc_positive_index_lowercontinuation)) -> ~(exists pvs_factor_lowercontinuationmobiussquarefreesquare. (mdc_positive_index_lowercontinuation) = (sfd_prime_lowercontinuationmobiussquarefree * sfd_prime_lowercontinuationmobiussquarefree) * pvs_factor_lowercontinuationmobiussquarefreesquare)))) /\ (exists mv_factor_code_lowercontinuationmobiusfactors mv_factor_scale_lowercontinuationmobiusfactors mv_factor_count_lowercontinuationmobiusfactors. (((~(mdc_positive_index_lowercontinuation = 0) /\ ((exists ff_u_fsat_lowercontinuationmobiusfactorsfactorization_product ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product. ((((exists ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_start. ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_start. ff_u_fsat_lowercontinuationmobiusfactorsfactorization_product = ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_terminal. ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_terminal + S (mdc_positive_index_lowercontinuation) = S ((S (mv_factor_count_lowercontinuationmobiusfactors)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_terminal. ff_u_fsat_lowercontinuationmobiusfactorsfactorization_product = ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_terminal * S ((S (mv_factor_count_lowercontinuationmobiusfactors)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product) + (mdc_positive_index_lowercontinuation))) /\ forall ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product. (exists ff_lt_fsat_lowercontinuationmobiusfactorsfactorization_product_bound. ff_lt_fsat_lowercontinuationmobiusfactorsfactorization_product_bound + S ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product = mv_factor_count_lowercontinuationmobiusfactors) -> exists ff_p_fsat_lowercontinuationmobiusfactorsfactorization_product ff_r_fsat_lowercontinuationmobiusfactorsfactorization_product ff_s_fsat_lowercontinuationmobiusfactorsfactorization_product. ((((exists ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_factor. ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_factor + S (ff_p_fsat_lowercontinuationmobiusfactorsfactorization_product) = S ((S (ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product)) * mv_factor_scale_lowercontinuationmobiusfactors)) /\ exists ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_factor. mv_factor_code_lowercontinuationmobiusfactors = ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_factor * S ((S (ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product)) * mv_factor_scale_lowercontinuationmobiusfactors) + (ff_p_fsat_lowercontinuationmobiusfactorsfactorization_product))) /\ ((((exists ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_partial. ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_partial + S (ff_r_fsat_lowercontinuationmobiusfactorsfactorization_product) = S ((S (ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_partial. ff_u_fsat_lowercontinuationmobiusfactorsfactorization_product = ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_partial * S ((S (ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product) + (ff_r_fsat_lowercontinuationmobiusfactorsfactorization_product))) /\ ((((exists ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_successor. ff_h_fsat_lowercontinuationmobiusfactorsfactorization_product_successor + S (ff_s_fsat_lowercontinuationmobiusfactorsfactorization_product) = S ((S (S ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_successor. ff_u_fsat_lowercontinuationmobiusfactorsfactorization_product = ff_q_fsat_lowercontinuationmobiusfactorsfactorization_product_successor * S ((S (S ff_i_fsat_lowercontinuationmobiusfactorsfactorization_product)) * ff_v_fsat_lowercontinuationmobiusfactorsfactorization_product) + (ff_s_fsat_lowercontinuationmobiusfactorsfactorization_product))) /\ ff_s_fsat_lowercontinuationmobiusfactorsfactorization_product = ff_r_fsat_lowercontinuationmobiusfactorsfactorization_product * ff_p_fsat_lowercontinuationmobiusfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_lowercontinuationmobiusfactorsfactorization_primes. (exists ftsf_gap_fsat_lowercontinuationmobiusfactorsfactorization_primes_bound. ftsf_gap_fsat_lowercontinuationmobiusfactorsfactorization_primes_bound + S ftsf_index_fsat_lowercontinuationmobiusfactorsfactorization_primes = (mv_factor_count_lowercontinuationmobiusfactors)) -> exists ftsf_factor_fsat_lowercontinuationmobiusfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_entry. ff_h_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_entry + S (ftsf_factor_fsat_lowercontinuationmobiusfactorsfactorization_primes) = S ((S (ftsf_index_fsat_lowercontinuationmobiusfactorsfactorization_primes)) * mv_factor_scale_lowercontinuationmobiusfactors)) /\ exists ff_q_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_entry. mv_factor_code_lowercontinuationmobiusfactors = ff_q_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_lowercontinuationmobiusfactorsfactorization_primes)) * mv_factor_scale_lowercontinuationmobiusfactors) + (ftsf_factor_fsat_lowercontinuationmobiusfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_lowercontinuationmobiusfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_prime. ftsf_factor_fsat_lowercontinuationmobiusfactorsfactorization_primes = frm_prime_left_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_lowercontinuationmobiusfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_lowercontinuationmobiusfactorsparityeven. (mv_factor_count_lowercontinuationmobiusfactors) = 2 * mv_even_half_lowercontinuationmobiusfactorsparityeven) /\ ((mdc_positive_value_lowercontinuation) = 2))) \/ (((exists mv_odd_half_lowercontinuationmobiusfactorsparityodd. (mv_factor_count_lowercontinuationmobiusfactors) = 2 * mv_odd_half_lowercontinuationmobiusfactorsparityodd + 1) /\ ((mdc_positive_value_lowercontinuation) = 1)))))))))))

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