mobius_prime_factor_toggle_negates

Exact expanded first-order arithmetic statement

forall p d e a b. (~((p) = 1) /\ forall pvs_left_value_prime pvs_right_value_prime. (p) = pvs_left_value_prime * pvs_right_value_prime -> pvs_left_value_prime = 1 \/ pvs_right_value_prime = 1) -> ((((~(exists pvs_factor_value_togglefresh_input. (d) = (p) * pvs_factor_value_togglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_value_togglefresh_output. (e) = (p) * pvs_factor_value_togglefresh_output)))) \/ (((exists pvs_factor_value_togglesquare. (d) = ((p)*(p)) * pvs_factor_value_togglesquare) /\ ((e)=(d)))))) -> (((~((d) = 0)) /\ ((((exists mv_square_prime_value_sourcesquare. ((~((mv_square_prime_value_sourcesquare) = 1) /\ forall pvs_left_value_sourcesquareprime pvs_right_value_sourcesquareprime. (mv_square_prime_value_sourcesquare) = pvs_left_value_sourcesquareprime * pvs_right_value_sourcesquareprime -> pvs_left_value_sourcesquareprime = 1 \/ pvs_right_value_sourcesquareprime = 1) /\ (exists pvs_factor_value_sourcesquaredivisor. (d) = (mv_square_prime_value_sourcesquare * mv_square_prime_value_sourcesquare) * pvs_factor_value_sourcesquaredivisor))) /\ ((a) = 0))) \/ (((((~((d) = 0)) /\ (forall sfd_prime_value_sourcesquarefree. (~((sfd_prime_value_sourcesquarefree) = 1) /\ forall pvs_left_value_sourcesquarefreedomain pvs_right_value_sourcesquarefreedomain. (sfd_prime_value_sourcesquarefree) = pvs_left_value_sourcesquarefreedomain * pvs_right_value_sourcesquarefreedomain -> pvs_left_value_sourcesquarefreedomain = 1 \/ pvs_right_value_sourcesquarefreedomain = 1) -> (exists pvs_le_gap_value_sourcesquarefreebound. pvs_le_gap_value_sourcesquarefreebound + (sfd_prime_value_sourcesquarefree) = (d)) -> ~(exists pvs_factor_value_sourcesquarefreesquare. (d) = (sfd_prime_value_sourcesquarefree * sfd_prime_value_sourcesquarefree) * pvs_factor_value_sourcesquarefreesquare)))) /\ (exists mv_factor_code_value_sourcefactors mv_factor_scale_value_sourcefactors mv_factor_count_value_sourcefactors. (((~(d = 0) /\ ((exists ff_u_fsat_value_sourcefactorsfactorization_product ff_v_fsat_value_sourcefactorsfactorization_product. ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_start. ff_h_fsat_value_sourcefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_start. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_terminal. ff_h_fsat_value_sourcefactorsfactorization_product_terminal + S (d) = S ((S (mv_factor_count_value_sourcefactors)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_terminal. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_terminal * S ((S (mv_factor_count_value_sourcefactors)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (d))) /\ forall ff_i_fsat_value_sourcefactorsfactorization_product. (exists ff_lt_fsat_value_sourcefactorsfactorization_product_bound. ff_lt_fsat_value_sourcefactorsfactorization_product_bound + S ff_i_fsat_value_sourcefactorsfactorization_product = mv_factor_count_value_sourcefactors) -> exists ff_p_fsat_value_sourcefactorsfactorization_product ff_r_fsat_value_sourcefactorsfactorization_product ff_s_fsat_value_sourcefactorsfactorization_product. ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_factor. ff_h_fsat_value_sourcefactorsfactorization_product_factor + S (ff_p_fsat_value_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * mv_factor_scale_value_sourcefactors)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_factor. mv_factor_code_value_sourcefactors = ff_q_fsat_value_sourcefactorsfactorization_product_factor * S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * mv_factor_scale_value_sourcefactors) + (ff_p_fsat_value_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_partial. ff_h_fsat_value_sourcefactorsfactorization_product_partial + S (ff_r_fsat_value_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_partial. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_partial * S ((S (ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (ff_r_fsat_value_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_sourcefactorsfactorization_product_successor. ff_h_fsat_value_sourcefactorsfactorization_product_successor + S (ff_s_fsat_value_sourcefactorsfactorization_product) = S ((S (S ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_value_sourcefactorsfactorization_product_successor. ff_u_fsat_value_sourcefactorsfactorization_product = ff_q_fsat_value_sourcefactorsfactorization_product_successor * S ((S (S ff_i_fsat_value_sourcefactorsfactorization_product)) * ff_v_fsat_value_sourcefactorsfactorization_product) + (ff_s_fsat_value_sourcefactorsfactorization_product))) /\ ff_s_fsat_value_sourcefactorsfactorization_product = ff_r_fsat_value_sourcefactorsfactorization_product * ff_p_fsat_value_sourcefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_value_sourcefactorsfactorization_primes. (exists ftsf_gap_fsat_value_sourcefactorsfactorization_primes_bound. ftsf_gap_fsat_value_sourcefactorsfactorization_primes_bound + S ftsf_index_fsat_value_sourcefactorsfactorization_primes = (mv_factor_count_value_sourcefactors)) -> exists ftsf_factor_fsat_value_sourcefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_value_sourcefactorsfactorization_primes_entry. ff_h_ftsf_fsat_value_sourcefactorsfactorization_primes_entry + S (ftsf_factor_fsat_value_sourcefactorsfactorization_primes) = S ((S (ftsf_index_fsat_value_sourcefactorsfactorization_primes)) * mv_factor_scale_value_sourcefactors)) /\ exists ff_q_ftsf_fsat_value_sourcefactorsfactorization_primes_entry. mv_factor_code_value_sourcefactors = ff_q_ftsf_fsat_value_sourcefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_value_sourcefactorsfactorization_primes)) * mv_factor_scale_value_sourcefactors) + (ftsf_factor_fsat_value_sourcefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_value_sourcefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_value_sourcefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_value_sourcefactorsfactorization_primes_prime. ftsf_factor_fsat_value_sourcefactorsfactorization_primes = frm_prime_left_ftsf_fsat_value_sourcefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_value_sourcefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_value_sourcefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_value_sourcefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_value_sourcefactorsparityeven. (mv_factor_count_value_sourcefactors) = 2 * mv_even_half_value_sourcefactorsparityeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_value_sourcefactorsparityodd. (mv_factor_count_value_sourcefactors) = 2 * mv_odd_half_value_sourcefactorsparityodd + 1) /\ ((a) = 1))))))))))) -> (((~((e) = 0)) /\ ((((exists mv_square_prime_value_targetsquare. ((~((mv_square_prime_value_targetsquare) = 1) /\ forall pvs_left_value_targetsquareprime pvs_right_value_targetsquareprime. (mv_square_prime_value_targetsquare) = pvs_left_value_targetsquareprime * pvs_right_value_targetsquareprime -> pvs_left_value_targetsquareprime = 1 \/ pvs_right_value_targetsquareprime = 1) /\ (exists pvs_factor_value_targetsquaredivisor. (e) = (mv_square_prime_value_targetsquare * mv_square_prime_value_targetsquare) * pvs_factor_value_targetsquaredivisor))) /\ ((b) = 0))) \/ (((((~((e) = 0)) /\ (forall sfd_prime_value_targetsquarefree. (~((sfd_prime_value_targetsquarefree) = 1) /\ forall pvs_left_value_targetsquarefreedomain pvs_right_value_targetsquarefreedomain. (sfd_prime_value_targetsquarefree) = pvs_left_value_targetsquarefreedomain * pvs_right_value_targetsquarefreedomain -> pvs_left_value_targetsquarefreedomain = 1 \/ pvs_right_value_targetsquarefreedomain = 1) -> (exists pvs_le_gap_value_targetsquarefreebound. pvs_le_gap_value_targetsquarefreebound + (sfd_prime_value_targetsquarefree) = (e)) -> ~(exists pvs_factor_value_targetsquarefreesquare. (e) = (sfd_prime_value_targetsquarefree * sfd_prime_value_targetsquarefree) * pvs_factor_value_targetsquarefreesquare)))) /\ (exists mv_factor_code_value_targetfactors mv_factor_scale_value_targetfactors mv_factor_count_value_targetfactors. (((~(e = 0) /\ ((exists ff_u_fsat_value_targetfactorsfactorization_product ff_v_fsat_value_targetfactorsfactorization_product. ((((exists ff_h_fsat_value_targetfactorsfactorization_product_start. ff_h_fsat_value_targetfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_start. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_value_targetfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_value_targetfactorsfactorization_product_terminal. ff_h_fsat_value_targetfactorsfactorization_product_terminal + S (e) = S ((S (mv_factor_count_value_targetfactors)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_terminal. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_terminal * S ((S (mv_factor_count_value_targetfactors)) * ff_v_fsat_value_targetfactorsfactorization_product) + (e))) /\ forall ff_i_fsat_value_targetfactorsfactorization_product. (exists ff_lt_fsat_value_targetfactorsfactorization_product_bound. ff_lt_fsat_value_targetfactorsfactorization_product_bound + S ff_i_fsat_value_targetfactorsfactorization_product = mv_factor_count_value_targetfactors) -> exists ff_p_fsat_value_targetfactorsfactorization_product ff_r_fsat_value_targetfactorsfactorization_product ff_s_fsat_value_targetfactorsfactorization_product. ((((exists ff_h_fsat_value_targetfactorsfactorization_product_factor. ff_h_fsat_value_targetfactorsfactorization_product_factor + S (ff_p_fsat_value_targetfactorsfactorization_product) = S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * mv_factor_scale_value_targetfactors)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_factor. mv_factor_code_value_targetfactors = ff_q_fsat_value_targetfactorsfactorization_product_factor * S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * mv_factor_scale_value_targetfactors) + (ff_p_fsat_value_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_targetfactorsfactorization_product_partial. ff_h_fsat_value_targetfactorsfactorization_product_partial + S (ff_r_fsat_value_targetfactorsfactorization_product) = S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_partial. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_partial * S ((S (ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product) + (ff_r_fsat_value_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_targetfactorsfactorization_product_successor. ff_h_fsat_value_targetfactorsfactorization_product_successor + S (ff_s_fsat_value_targetfactorsfactorization_product) = S ((S (S ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product)) /\ exists ff_q_fsat_value_targetfactorsfactorization_product_successor. ff_u_fsat_value_targetfactorsfactorization_product = ff_q_fsat_value_targetfactorsfactorization_product_successor * S ((S (S ff_i_fsat_value_targetfactorsfactorization_product)) * ff_v_fsat_value_targetfactorsfactorization_product) + (ff_s_fsat_value_targetfactorsfactorization_product))) /\ ff_s_fsat_value_targetfactorsfactorization_product = ff_r_fsat_value_targetfactorsfactorization_product * ff_p_fsat_value_targetfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_value_targetfactorsfactorization_primes. (exists ftsf_gap_fsat_value_targetfactorsfactorization_primes_bound. ftsf_gap_fsat_value_targetfactorsfactorization_primes_bound + S ftsf_index_fsat_value_targetfactorsfactorization_primes = (mv_factor_count_value_targetfactors)) -> exists ftsf_factor_fsat_value_targetfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_value_targetfactorsfactorization_primes_entry. ff_h_ftsf_fsat_value_targetfactorsfactorization_primes_entry + S (ftsf_factor_fsat_value_targetfactorsfactorization_primes) = S ((S (ftsf_index_fsat_value_targetfactorsfactorization_primes)) * mv_factor_scale_value_targetfactors)) /\ exists ff_q_ftsf_fsat_value_targetfactorsfactorization_primes_entry. mv_factor_code_value_targetfactors = ff_q_ftsf_fsat_value_targetfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_value_targetfactorsfactorization_primes)) * mv_factor_scale_value_targetfactors) + (ftsf_factor_fsat_value_targetfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_value_targetfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_value_targetfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_value_targetfactorsfactorization_primes_prime. ftsf_factor_fsat_value_targetfactorsfactorization_primes = frm_prime_left_ftsf_fsat_value_targetfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_value_targetfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_value_targetfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_value_targetfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_value_targetfactorsparityeven. (mv_factor_count_value_targetfactors) = 2 * mv_even_half_value_targetfactorsparityeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_value_targetfactorsparityodd. (mv_factor_count_value_targetfactors) = 2 * mv_odd_half_value_targetfactorsparityodd + 1) /\ ((b) = 1))))))))))) -> (exists mps_positive_value_negation mps_negative_value_negation. (((((a) = 2 * (mps_positive_value_negation) /\ (mps_negative_value_negation) = 0) \/ exists ge_signed_half_value_negationsource. (((a) = 2 * ge_signed_half_value_negationsource + 1 /\ (mps_positive_value_negation) = 0) /\ (mps_negative_value_negation) = S ge_signed_half_value_negationsource))) /\ ((((b) = 2 * (mps_negative_value_negation) /\ (mps_positive_value_negation) = 0) \/ exists ge_signed_half_value_negationtarget. (((b) = 2 * ge_signed_half_value_negationtarget + 1 /\ (mps_negative_value_negation) = 0) /\ (mps_positive_value_negation) = S ge_signed_half_value_negationtarget)))))