mobius_squarefree_evaluation

Exact expanded first-order arithmetic statement

forall n b c l z. (((~((n) = 0)) /\ (forall sfd_prime_evaluation_sf. (~((sfd_prime_evaluation_sf) = 1) /\ forall pvs_left_evaluation_sfdomain pvs_right_evaluation_sfdomain. (sfd_prime_evaluation_sf) = pvs_left_evaluation_sfdomain * pvs_right_evaluation_sfdomain -> pvs_left_evaluation_sfdomain = 1 \/ pvs_right_evaluation_sfdomain = 1) -> (exists pvs_le_gap_evaluation_sfbound. pvs_le_gap_evaluation_sfbound + (sfd_prime_evaluation_sf) = (n)) -> ~(exists pvs_factor_evaluation_sfsquare. (n) = (sfd_prime_evaluation_sf * sfd_prime_evaluation_sf) * pvs_factor_evaluation_sfsquare)))) -> ((~(n = 0) /\ ((exists ff_u_fsat_mv_evaluation_factors_product ff_v_fsat_mv_evaluation_factors_product. ((((exists ff_h_fsat_mv_evaluation_factors_product_start. ff_h_fsat_mv_evaluation_factors_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_start. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_start * S ((S (0)) * ff_v_fsat_mv_evaluation_factors_product) + (1))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_terminal. ff_h_fsat_mv_evaluation_factors_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_terminal. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_terminal * S ((S (l)) * ff_v_fsat_mv_evaluation_factors_product) + (n))) /\ forall ff_i_fsat_mv_evaluation_factors_product. (exists ff_lt_fsat_mv_evaluation_factors_product_bound. ff_lt_fsat_mv_evaluation_factors_product_bound + S ff_i_fsat_mv_evaluation_factors_product = l) -> exists ff_p_fsat_mv_evaluation_factors_product ff_r_fsat_mv_evaluation_factors_product ff_s_fsat_mv_evaluation_factors_product. ((((exists ff_h_fsat_mv_evaluation_factors_product_factor. ff_h_fsat_mv_evaluation_factors_product_factor + S (ff_p_fsat_mv_evaluation_factors_product) = S ((S (ff_i_fsat_mv_evaluation_factors_product)) * c)) /\ exists ff_q_fsat_mv_evaluation_factors_product_factor. b = ff_q_fsat_mv_evaluation_factors_product_factor * S ((S (ff_i_fsat_mv_evaluation_factors_product)) * c) + (ff_p_fsat_mv_evaluation_factors_product))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_partial. ff_h_fsat_mv_evaluation_factors_product_partial + S (ff_r_fsat_mv_evaluation_factors_product) = S ((S (ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_partial. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_partial * S ((S (ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product) + (ff_r_fsat_mv_evaluation_factors_product))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_successor. ff_h_fsat_mv_evaluation_factors_product_successor + S (ff_s_fsat_mv_evaluation_factors_product) = S ((S (S ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_successor. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_successor * S ((S (S ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product) + (ff_s_fsat_mv_evaluation_factors_product))) /\ ff_s_fsat_mv_evaluation_factors_product = ff_r_fsat_mv_evaluation_factors_product * ff_p_fsat_mv_evaluation_factors_product)))))) /\ (forall ftsf_index_fsat_mv_evaluation_factors_primes. (exists ftsf_gap_fsat_mv_evaluation_factors_primes_bound. ftsf_gap_fsat_mv_evaluation_factors_primes_bound + S ftsf_index_fsat_mv_evaluation_factors_primes = (l)) -> exists ftsf_factor_fsat_mv_evaluation_factors_primes. ((((exists ff_h_ftsf_fsat_mv_evaluation_factors_primes_entry. ff_h_ftsf_fsat_mv_evaluation_factors_primes_entry + S (ftsf_factor_fsat_mv_evaluation_factors_primes) = S ((S (ftsf_index_fsat_mv_evaluation_factors_primes)) * c)) /\ exists ff_q_ftsf_fsat_mv_evaluation_factors_primes_entry. b = ff_q_ftsf_fsat_mv_evaluation_factors_primes_entry * S ((S (ftsf_index_fsat_mv_evaluation_factors_primes)) * c) + (ftsf_factor_fsat_mv_evaluation_factors_primes))) /\ ((~(ftsf_factor_fsat_mv_evaluation_factors_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime. ftsf_factor_fsat_mv_evaluation_factors_primes = frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime * frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime -> frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime = 1))))))) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_evaluation_valuesquare. ((~((mv_square_prime_evaluation_valuesquare) = 1) /\ forall pvs_left_evaluation_valuesquareprime pvs_right_evaluation_valuesquareprime. (mv_square_prime_evaluation_valuesquare) = pvs_left_evaluation_valuesquareprime * pvs_right_evaluation_valuesquareprime -> pvs_left_evaluation_valuesquareprime = 1 \/ pvs_right_evaluation_valuesquareprime = 1) /\ (exists pvs_factor_evaluation_valuesquaredivisor. (n) = (mv_square_prime_evaluation_valuesquare * mv_square_prime_evaluation_valuesquare) * pvs_factor_evaluation_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_evaluation_valuesquarefree. (~((sfd_prime_evaluation_valuesquarefree) = 1) /\ forall pvs_left_evaluation_valuesquarefreedomain pvs_right_evaluation_valuesquarefreedomain. (sfd_prime_evaluation_valuesquarefree) = pvs_left_evaluation_valuesquarefreedomain * pvs_right_evaluation_valuesquarefreedomain -> pvs_left_evaluation_valuesquarefreedomain = 1 \/ pvs_right_evaluation_valuesquarefreedomain = 1) -> (exists pvs_le_gap_evaluation_valuesquarefreebound. pvs_le_gap_evaluation_valuesquarefreebound + (sfd_prime_evaluation_valuesquarefree) = (n)) -> ~(exists pvs_factor_evaluation_valuesquarefreesquare. (n) = (sfd_prime_evaluation_valuesquarefree * sfd_prime_evaluation_valuesquarefree) * pvs_factor_evaluation_valuesquarefreesquare)))) /\ (exists mv_factor_code_evaluation_valuefactors mv_factor_scale_evaluation_valuefactors mv_factor_count_evaluation_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_evaluation_valuefactorsfactorization_product ff_v_fsat_evaluation_valuefactorsfactorization_product. ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_start. ff_h_fsat_evaluation_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_start. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_terminal. ff_h_fsat_evaluation_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_evaluation_valuefactors)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_terminal. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_evaluation_valuefactors)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_evaluation_valuefactorsfactorization_product. (exists ff_lt_fsat_evaluation_valuefactorsfactorization_product_bound. ff_lt_fsat_evaluation_valuefactorsfactorization_product_bound + S ff_i_fsat_evaluation_valuefactorsfactorization_product = mv_factor_count_evaluation_valuefactors) -> exists ff_p_fsat_evaluation_valuefactorsfactorization_product ff_r_fsat_evaluation_valuefactorsfactorization_product ff_s_fsat_evaluation_valuefactorsfactorization_product. ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_factor. ff_h_fsat_evaluation_valuefactorsfactorization_product_factor + S (ff_p_fsat_evaluation_valuefactorsfactorization_product) = S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * mv_factor_scale_evaluation_valuefactors)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_factor. mv_factor_code_evaluation_valuefactors = ff_q_fsat_evaluation_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * mv_factor_scale_evaluation_valuefactors) + (ff_p_fsat_evaluation_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_partial. ff_h_fsat_evaluation_valuefactorsfactorization_product_partial + S (ff_r_fsat_evaluation_valuefactorsfactorization_product) = S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_partial. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (ff_r_fsat_evaluation_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_successor. ff_h_fsat_evaluation_valuefactorsfactorization_product_successor + S (ff_s_fsat_evaluation_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_successor. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (ff_s_fsat_evaluation_valuefactorsfactorization_product))) /\ ff_s_fsat_evaluation_valuefactorsfactorization_product = ff_r_fsat_evaluation_valuefactorsfactorization_product * ff_p_fsat_evaluation_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_evaluation_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_evaluation_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_evaluation_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_evaluation_valuefactorsfactorization_primes = (mv_factor_count_evaluation_valuefactors)) -> exists ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_evaluation_valuefactorsfactorization_primes)) * mv_factor_scale_evaluation_valuefactors)) /\ exists ff_q_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry. mv_factor_code_evaluation_valuefactors = ff_q_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_evaluation_valuefactorsfactorization_primes)) * mv_factor_scale_evaluation_valuefactors) + (ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_evaluation_valuefactorsparityeven. (mv_factor_count_evaluation_valuefactors) = 2 * mv_even_half_evaluation_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_evaluation_valuefactorsparityodd. (mv_factor_count_evaluation_valuefactors) = 2 * mv_odd_half_evaluation_valuefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> ((((exists mv_even_half_evaluation_resulteven. (l) = 2 * mv_even_half_evaluation_resulteven) /\ ((z) = 2))) \/ (((exists mv_odd_half_evaluation_resultodd. (l) = 2 * mv_odd_half_evaluation_resultodd + 1) /\ ((z) = 1))))