mobius_table_entry_iff

Exact expanded first-order arithmetic statement

forall N M i z. (((exists dst_positive_code_iff_tabletable dst_positive_scale_iff_tabletable dst_negative_code_iff_tabletable dst_negative_scale_iff_tabletable. (((M) = (((((dst_positive_code_iff_tabletable) + (dst_positive_scale_iff_tabletable)) * S ((dst_positive_code_iff_tabletable) + (dst_positive_scale_iff_tabletable)) + ((dst_positive_scale_iff_tabletable) + (dst_positive_scale_iff_tabletable))) + (((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) * S ((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) + ((dst_negative_scale_iff_tabletable) + (dst_negative_scale_iff_tabletable)))) * S ((((dst_positive_code_iff_tabletable) + (dst_positive_scale_iff_tabletable)) * S ((dst_positive_code_iff_tabletable) + (dst_positive_scale_iff_tabletable)) + ((dst_positive_scale_iff_tabletable) + (dst_positive_scale_iff_tabletable))) + (((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) * S ((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) + ((dst_negative_scale_iff_tabletable) + (dst_negative_scale_iff_tabletable)))) + ((((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) * S ((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) + ((dst_negative_scale_iff_tabletable) + (dst_negative_scale_iff_tabletable))) + (((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) * S ((dst_negative_code_iff_tabletable) + (dst_negative_scale_iff_tabletable)) + ((dst_negative_scale_iff_tabletable) + (dst_negative_scale_iff_tabletable)))))) /\ (forall dst_index_iff_tabletable. (exists pvs_le_gap_iff_tabletabledomain. pvs_le_gap_iff_tabletabledomain + (dst_index_iff_tabletable) = (N)) -> exists dst_positive_iff_tabletable dst_negative_iff_tabletable dst_value_iff_tabletable. ((((exists ff_h_pvs_iff_tabletableentrypositive. ff_h_pvs_iff_tabletableentrypositive + S (dst_positive_iff_tabletable) = S ((S (dst_index_iff_tabletable)) * dst_positive_scale_iff_tabletable)) /\ exists ff_q_pvs_iff_tabletableentrypositive. dst_positive_code_iff_tabletable = ff_q_pvs_iff_tabletableentrypositive * S ((S (dst_index_iff_tabletable)) * dst_positive_scale_iff_tabletable) + (dst_positive_iff_tabletable))) /\ (((((exists ff_h_pvs_iff_tabletableentrynegative. ff_h_pvs_iff_tabletableentrynegative + S (dst_negative_iff_tabletable) = S ((S (dst_index_iff_tabletable)) * dst_negative_scale_iff_tabletable)) /\ exists ff_q_pvs_iff_tabletableentrynegative. dst_negative_code_iff_tabletable = ff_q_pvs_iff_tabletableentrynegative * S ((S (dst_index_iff_tabletable)) * dst_negative_scale_iff_tabletable) + (dst_negative_iff_tabletable))) /\ (exists ge_balance_positive_iff_tabletableentryvalue ge_balance_negative_iff_tabletableentryvalue. (((((dst_value_iff_tabletable) = 2 * (ge_balance_positive_iff_tabletableentryvalue) /\ (ge_balance_negative_iff_tabletableentryvalue) = 0) \/ exists ge_signed_half_iff_tabletableentryvaluedecode. (((dst_value_iff_tabletable) = 2 * ge_signed_half_iff_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_iff_tabletableentryvalue) = 0) /\ (ge_balance_negative_iff_tabletableentryvalue) = S ge_signed_half_iff_tabletableentryvaluedecode))) /\ ((dst_positive_iff_tabletable) + ge_balance_negative_iff_tabletableentryvalue = (dst_negative_iff_tabletable) + ge_balance_positive_iff_tabletableentryvalue))))))))) /\ (((exists dst_positive_code_iff_tablezero dst_positive_scale_iff_tablezero dst_negative_code_iff_tablezero dst_negative_scale_iff_tablezero dst_positive_iff_tablezero dst_negative_iff_tablezero. (((M) = (((((dst_positive_code_iff_tablezero) + (dst_positive_scale_iff_tablezero)) * S ((dst_positive_code_iff_tablezero) + (dst_positive_scale_iff_tablezero)) + ((dst_positive_scale_iff_tablezero) + (dst_positive_scale_iff_tablezero))) + (((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) * S ((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) + ((dst_negative_scale_iff_tablezero) + (dst_negative_scale_iff_tablezero)))) * S ((((dst_positive_code_iff_tablezero) + (dst_positive_scale_iff_tablezero)) * S ((dst_positive_code_iff_tablezero) + (dst_positive_scale_iff_tablezero)) + ((dst_positive_scale_iff_tablezero) + (dst_positive_scale_iff_tablezero))) + (((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) * S ((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) + ((dst_negative_scale_iff_tablezero) + (dst_negative_scale_iff_tablezero)))) + ((((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) * S ((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) + ((dst_negative_scale_iff_tablezero) + (dst_negative_scale_iff_tablezero))) + (((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) * S ((dst_negative_code_iff_tablezero) + (dst_negative_scale_iff_tablezero)) + ((dst_negative_scale_iff_tablezero) + (dst_negative_scale_iff_tablezero)))))) /\ (((((exists ff_h_pvs_iff_tablezeropositive. ff_h_pvs_iff_tablezeropositive + S (dst_positive_iff_tablezero) = S ((S (0)) * dst_positive_scale_iff_tablezero)) /\ exists ff_q_pvs_iff_tablezeropositive. dst_positive_code_iff_tablezero = ff_q_pvs_iff_tablezeropositive * S ((S (0)) * dst_positive_scale_iff_tablezero) + (dst_positive_iff_tablezero))) /\ (((((exists ff_h_pvs_iff_tablezeronegative. ff_h_pvs_iff_tablezeronegative + S (dst_negative_iff_tablezero) = S ((S (0)) * dst_negative_scale_iff_tablezero)) /\ exists ff_q_pvs_iff_tablezeronegative. dst_negative_code_iff_tablezero = ff_q_pvs_iff_tablezeronegative * S ((S (0)) * dst_negative_scale_iff_tablezero) + (dst_negative_iff_tablezero))) /\ (exists ge_balance_positive_iff_tablezerovalue ge_balance_negative_iff_tablezerovalue. (((((0) = 2 * (ge_balance_positive_iff_tablezerovalue) /\ (ge_balance_negative_iff_tablezerovalue) = 0) \/ exists ge_signed_half_iff_tablezerovaluedecode. (((0) = 2 * ge_signed_half_iff_tablezerovaluedecode + 1 /\ (ge_balance_positive_iff_tablezerovalue) = 0) /\ (ge_balance_negative_iff_tablezerovalue) = S ge_signed_half_iff_tablezerovaluedecode))) /\ ((dst_positive_iff_tablezero) + ge_balance_negative_iff_tablezerovalue = (dst_negative_iff_tablezero) + ge_balance_positive_iff_tablezerovalue))))))))) /\ (forall mt_index_iff_table mt_value_iff_table. ~(mt_index_iff_table=0) -> (exists pvs_le_gap_iff_tabledomain. pvs_le_gap_iff_tabledomain + (mt_index_iff_table) = (N)) -> (exists dst_positive_code_iff_tableentry dst_positive_scale_iff_tableentry dst_negative_code_iff_tableentry dst_negative_scale_iff_tableentry dst_positive_iff_tableentry dst_negative_iff_tableentry. (((M) = (((((dst_positive_code_iff_tableentry) + (dst_positive_scale_iff_tableentry)) * S ((dst_positive_code_iff_tableentry) + (dst_positive_scale_iff_tableentry)) + ((dst_positive_scale_iff_tableentry) + (dst_positive_scale_iff_tableentry))) + (((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) * S ((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) + ((dst_negative_scale_iff_tableentry) + (dst_negative_scale_iff_tableentry)))) * S ((((dst_positive_code_iff_tableentry) + (dst_positive_scale_iff_tableentry)) * S ((dst_positive_code_iff_tableentry) + (dst_positive_scale_iff_tableentry)) + ((dst_positive_scale_iff_tableentry) + (dst_positive_scale_iff_tableentry))) + (((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) * S ((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) + ((dst_negative_scale_iff_tableentry) + (dst_negative_scale_iff_tableentry)))) + ((((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) * S ((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) + ((dst_negative_scale_iff_tableentry) + (dst_negative_scale_iff_tableentry))) + (((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) * S ((dst_negative_code_iff_tableentry) + (dst_negative_scale_iff_tableentry)) + ((dst_negative_scale_iff_tableentry) + (dst_negative_scale_iff_tableentry)))))) /\ (((((exists ff_h_pvs_iff_tableentrypositive. ff_h_pvs_iff_tableentrypositive + S (dst_positive_iff_tableentry) = S ((S (mt_index_iff_table)) * dst_positive_scale_iff_tableentry)) /\ exists ff_q_pvs_iff_tableentrypositive. dst_positive_code_iff_tableentry = ff_q_pvs_iff_tableentrypositive * S ((S (mt_index_iff_table)) * dst_positive_scale_iff_tableentry) + (dst_positive_iff_tableentry))) /\ (((((exists ff_h_pvs_iff_tableentrynegative. ff_h_pvs_iff_tableentrynegative + S (dst_negative_iff_tableentry) = S ((S (mt_index_iff_table)) * dst_negative_scale_iff_tableentry)) /\ exists ff_q_pvs_iff_tableentrynegative. dst_negative_code_iff_tableentry = ff_q_pvs_iff_tableentrynegative * S ((S (mt_index_iff_table)) * dst_negative_scale_iff_tableentry) + (dst_negative_iff_tableentry))) /\ (exists ge_balance_positive_iff_tableentryvalue ge_balance_negative_iff_tableentryvalue. (((((mt_value_iff_table) = 2 * (ge_balance_positive_iff_tableentryvalue) /\ (ge_balance_negative_iff_tableentryvalue) = 0) \/ exists ge_signed_half_iff_tableentryvaluedecode. (((mt_value_iff_table) = 2 * ge_signed_half_iff_tableentryvaluedecode + 1 /\ (ge_balance_positive_iff_tableentryvalue) = 0) /\ (ge_balance_negative_iff_tableentryvalue) = S ge_signed_half_iff_tableentryvaluedecode))) /\ ((dst_positive_iff_tableentry) + ge_balance_negative_iff_tableentryvalue = (dst_negative_iff_tableentry) + ge_balance_positive_iff_tableentryvalue))))))))) -> (((~((mt_index_iff_table) = 0)) /\ ((((exists mv_square_prime_iff_tablevaluesquare. ((~((mv_square_prime_iff_tablevaluesquare) = 1) /\ forall pvs_left_iff_tablevaluesquareprime pvs_right_iff_tablevaluesquareprime. (mv_square_prime_iff_tablevaluesquare) = pvs_left_iff_tablevaluesquareprime * pvs_right_iff_tablevaluesquareprime -> pvs_left_iff_tablevaluesquareprime = 1 \/ pvs_right_iff_tablevaluesquareprime = 1) /\ (exists pvs_factor_iff_tablevaluesquaredivisor. (mt_index_iff_table) = (mv_square_prime_iff_tablevaluesquare * mv_square_prime_iff_tablevaluesquare) * pvs_factor_iff_tablevaluesquaredivisor))) /\ ((mt_value_iff_table) = 0))) \/ (((((~((mt_index_iff_table) = 0)) /\ (forall sfd_prime_iff_tablevaluesquarefree. (~((sfd_prime_iff_tablevaluesquarefree) = 1) /\ forall pvs_left_iff_tablevaluesquarefreedomain pvs_right_iff_tablevaluesquarefreedomain. (sfd_prime_iff_tablevaluesquarefree) = pvs_left_iff_tablevaluesquarefreedomain * pvs_right_iff_tablevaluesquarefreedomain -> pvs_left_iff_tablevaluesquarefreedomain = 1 \/ pvs_right_iff_tablevaluesquarefreedomain = 1) -> (exists pvs_le_gap_iff_tablevaluesquarefreebound. pvs_le_gap_iff_tablevaluesquarefreebound + (sfd_prime_iff_tablevaluesquarefree) = (mt_index_iff_table)) -> ~(exists pvs_factor_iff_tablevaluesquarefreesquare. (mt_index_iff_table) = (sfd_prime_iff_tablevaluesquarefree * sfd_prime_iff_tablevaluesquarefree) * pvs_factor_iff_tablevaluesquarefreesquare)))) /\ (exists mv_factor_code_iff_tablevaluefactors mv_factor_scale_iff_tablevaluefactors mv_factor_count_iff_tablevaluefactors. (((~(mt_index_iff_table = 0) /\ ((exists ff_u_fsat_iff_tablevaluefactorsfactorization_product ff_v_fsat_iff_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_iff_tablevaluefactorsfactorization_product_start. ff_h_fsat_iff_tablevaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_tablevaluefactorsfactorization_product_start. ff_u_fsat_iff_tablevaluefactorsfactorization_product = ff_q_fsat_iff_tablevaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_iff_tablevaluefactorsfactorization_product_terminal. ff_h_fsat_iff_tablevaluefactorsfactorization_product_terminal + S (mt_index_iff_table) = S ((S (mv_factor_count_iff_tablevaluefactors)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_tablevaluefactorsfactorization_product_terminal. ff_u_fsat_iff_tablevaluefactorsfactorization_product = ff_q_fsat_iff_tablevaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_iff_tablevaluefactors)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product) + (mt_index_iff_table))) /\ forall ff_i_fsat_iff_tablevaluefactorsfactorization_product. (exists ff_lt_fsat_iff_tablevaluefactorsfactorization_product_bound. ff_lt_fsat_iff_tablevaluefactorsfactorization_product_bound + S ff_i_fsat_iff_tablevaluefactorsfactorization_product = mv_factor_count_iff_tablevaluefactors) -> exists ff_p_fsat_iff_tablevaluefactorsfactorization_product ff_r_fsat_iff_tablevaluefactorsfactorization_product ff_s_fsat_iff_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_iff_tablevaluefactorsfactorization_product_factor. ff_h_fsat_iff_tablevaluefactorsfactorization_product_factor + S (ff_p_fsat_iff_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_iff_tablevaluefactorsfactorization_product)) * mv_factor_scale_iff_tablevaluefactors)) /\ exists ff_q_fsat_iff_tablevaluefactorsfactorization_product_factor. mv_factor_code_iff_tablevaluefactors = ff_q_fsat_iff_tablevaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_iff_tablevaluefactorsfactorization_product)) * mv_factor_scale_iff_tablevaluefactors) + (ff_p_fsat_iff_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_tablevaluefactorsfactorization_product_partial. ff_h_fsat_iff_tablevaluefactorsfactorization_product_partial + S (ff_r_fsat_iff_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_tablevaluefactorsfactorization_product_partial. ff_u_fsat_iff_tablevaluefactorsfactorization_product = ff_q_fsat_iff_tablevaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product) + (ff_r_fsat_iff_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_tablevaluefactorsfactorization_product_successor. ff_h_fsat_iff_tablevaluefactorsfactorization_product_successor + S (ff_s_fsat_iff_tablevaluefactorsfactorization_product) = S ((S (S ff_i_fsat_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_tablevaluefactorsfactorization_product_successor. ff_u_fsat_iff_tablevaluefactorsfactorization_product = ff_q_fsat_iff_tablevaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_iff_tablevaluefactorsfactorization_product) + (ff_s_fsat_iff_tablevaluefactorsfactorization_product))) /\ ff_s_fsat_iff_tablevaluefactorsfactorization_product = ff_r_fsat_iff_tablevaluefactorsfactorization_product * ff_p_fsat_iff_tablevaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_iff_tablevaluefactorsfactorization_primes. (exists ftsf_gap_fsat_iff_tablevaluefactorsfactorization_primes_bound. ftsf_gap_fsat_iff_tablevaluefactorsfactorization_primes_bound + S ftsf_index_fsat_iff_tablevaluefactorsfactorization_primes = (mv_factor_count_iff_tablevaluefactors)) -> exists ftsf_factor_fsat_iff_tablevaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_iff_tablevaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_iff_tablevaluefactorsfactorization_primes)) * mv_factor_scale_iff_tablevaluefactors)) /\ exists ff_q_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_entry. mv_factor_code_iff_tablevaluefactors = ff_q_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_iff_tablevaluefactorsfactorization_primes)) * mv_factor_scale_iff_tablevaluefactors) + (ftsf_factor_fsat_iff_tablevaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_iff_tablevaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_prime. ftsf_factor_fsat_iff_tablevaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_iff_tablevaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_iff_tablevaluefactorsparityeven. (mv_factor_count_iff_tablevaluefactors) = 2 * mv_even_half_iff_tablevaluefactorsparityeven) /\ ((mt_value_iff_table) = 2))) \/ (((exists mv_odd_half_iff_tablevaluefactorsparityodd. (mv_factor_count_iff_tablevaluefactors) = 2 * mv_odd_half_iff_tablevaluefactorsparityodd + 1) /\ ((mt_value_iff_table) = 1)))))))))))))))) -> ~(i=0) -> (exists pvs_le_gap_iff_bound. pvs_le_gap_iff_bound + (i) = (N)) -> ((exists dst_positive_code_iff_entry_forward dst_positive_scale_iff_entry_forward dst_negative_code_iff_entry_forward dst_negative_scale_iff_entry_forward dst_positive_iff_entry_forward dst_negative_iff_entry_forward. (((M) = (((((dst_positive_code_iff_entry_forward) + (dst_positive_scale_iff_entry_forward)) * S ((dst_positive_code_iff_entry_forward) + (dst_positive_scale_iff_entry_forward)) + ((dst_positive_scale_iff_entry_forward) + (dst_positive_scale_iff_entry_forward))) + (((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) * S ((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) + ((dst_negative_scale_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)))) * S ((((dst_positive_code_iff_entry_forward) + (dst_positive_scale_iff_entry_forward)) * S ((dst_positive_code_iff_entry_forward) + (dst_positive_scale_iff_entry_forward)) + ((dst_positive_scale_iff_entry_forward) + (dst_positive_scale_iff_entry_forward))) + (((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) * S ((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) + ((dst_negative_scale_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)))) + ((((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) * S ((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) + ((dst_negative_scale_iff_entry_forward) + (dst_negative_scale_iff_entry_forward))) + (((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) * S ((dst_negative_code_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)) + ((dst_negative_scale_iff_entry_forward) + (dst_negative_scale_iff_entry_forward)))))) /\ (((((exists ff_h_pvs_iff_entry_forwardpositive. ff_h_pvs_iff_entry_forwardpositive + S (dst_positive_iff_entry_forward) = S ((S (i)) * dst_positive_scale_iff_entry_forward)) /\ exists ff_q_pvs_iff_entry_forwardpositive. dst_positive_code_iff_entry_forward = ff_q_pvs_iff_entry_forwardpositive * S ((S (i)) * dst_positive_scale_iff_entry_forward) + (dst_positive_iff_entry_forward))) /\ (((((exists ff_h_pvs_iff_entry_forwardnegative. ff_h_pvs_iff_entry_forwardnegative + S (dst_negative_iff_entry_forward) = S ((S (i)) * dst_negative_scale_iff_entry_forward)) /\ exists ff_q_pvs_iff_entry_forwardnegative. dst_negative_code_iff_entry_forward = ff_q_pvs_iff_entry_forwardnegative * S ((S (i)) * dst_negative_scale_iff_entry_forward) + (dst_negative_iff_entry_forward))) /\ (exists ge_balance_positive_iff_entry_forwardvalue ge_balance_negative_iff_entry_forwardvalue. (((((z) = 2 * (ge_balance_positive_iff_entry_forwardvalue) /\ (ge_balance_negative_iff_entry_forwardvalue) = 0) \/ exists ge_signed_half_iff_entry_forwardvaluedecode. (((z) = 2 * ge_signed_half_iff_entry_forwardvaluedecode + 1 /\ (ge_balance_positive_iff_entry_forwardvalue) = 0) /\ (ge_balance_negative_iff_entry_forwardvalue) = S ge_signed_half_iff_entry_forwardvaluedecode))) /\ ((dst_positive_iff_entry_forward) + ge_balance_negative_iff_entry_forwardvalue = (dst_negative_iff_entry_forward) + ge_balance_positive_iff_entry_forwardvalue))))))))) -> (((~((i) = 0)) /\ ((((exists mv_square_prime_iff_value_forwardsquare. ((~((mv_square_prime_iff_value_forwardsquare) = 1) /\ forall pvs_left_iff_value_forwardsquareprime pvs_right_iff_value_forwardsquareprime. (mv_square_prime_iff_value_forwardsquare) = pvs_left_iff_value_forwardsquareprime * pvs_right_iff_value_forwardsquareprime -> pvs_left_iff_value_forwardsquareprime = 1 \/ pvs_right_iff_value_forwardsquareprime = 1) /\ (exists pvs_factor_iff_value_forwardsquaredivisor. (i) = (mv_square_prime_iff_value_forwardsquare * mv_square_prime_iff_value_forwardsquare) * pvs_factor_iff_value_forwardsquaredivisor))) /\ ((z) = 0))) \/ (((((~((i) = 0)) /\ (forall sfd_prime_iff_value_forwardsquarefree. (~((sfd_prime_iff_value_forwardsquarefree) = 1) /\ forall pvs_left_iff_value_forwardsquarefreedomain pvs_right_iff_value_forwardsquarefreedomain. (sfd_prime_iff_value_forwardsquarefree) = pvs_left_iff_value_forwardsquarefreedomain * pvs_right_iff_value_forwardsquarefreedomain -> pvs_left_iff_value_forwardsquarefreedomain = 1 \/ pvs_right_iff_value_forwardsquarefreedomain = 1) -> (exists pvs_le_gap_iff_value_forwardsquarefreebound. pvs_le_gap_iff_value_forwardsquarefreebound + (sfd_prime_iff_value_forwardsquarefree) = (i)) -> ~(exists pvs_factor_iff_value_forwardsquarefreesquare. (i) = (sfd_prime_iff_value_forwardsquarefree * sfd_prime_iff_value_forwardsquarefree) * pvs_factor_iff_value_forwardsquarefreesquare)))) /\ (exists mv_factor_code_iff_value_forwardfactors mv_factor_scale_iff_value_forwardfactors mv_factor_count_iff_value_forwardfactors. (((~(i = 0) /\ ((exists ff_u_fsat_iff_value_forwardfactorsfactorization_product ff_v_fsat_iff_value_forwardfactorsfactorization_product. ((((exists ff_h_fsat_iff_value_forwardfactorsfactorization_product_start. ff_h_fsat_iff_value_forwardfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_forwardfactorsfactorization_product_start. ff_u_fsat_iff_value_forwardfactorsfactorization_product = ff_q_fsat_iff_value_forwardfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_iff_value_forwardfactorsfactorization_product_terminal. ff_h_fsat_iff_value_forwardfactorsfactorization_product_terminal + S (i) = S ((S (mv_factor_count_iff_value_forwardfactors)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_forwardfactorsfactorization_product_terminal. ff_u_fsat_iff_value_forwardfactorsfactorization_product = ff_q_fsat_iff_value_forwardfactorsfactorization_product_terminal * S ((S (mv_factor_count_iff_value_forwardfactors)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product) + (i))) /\ forall ff_i_fsat_iff_value_forwardfactorsfactorization_product. (exists ff_lt_fsat_iff_value_forwardfactorsfactorization_product_bound. ff_lt_fsat_iff_value_forwardfactorsfactorization_product_bound + S ff_i_fsat_iff_value_forwardfactorsfactorization_product = mv_factor_count_iff_value_forwardfactors) -> exists ff_p_fsat_iff_value_forwardfactorsfactorization_product ff_r_fsat_iff_value_forwardfactorsfactorization_product ff_s_fsat_iff_value_forwardfactorsfactorization_product. ((((exists ff_h_fsat_iff_value_forwardfactorsfactorization_product_factor. ff_h_fsat_iff_value_forwardfactorsfactorization_product_factor + S (ff_p_fsat_iff_value_forwardfactorsfactorization_product) = S ((S (ff_i_fsat_iff_value_forwardfactorsfactorization_product)) * mv_factor_scale_iff_value_forwardfactors)) /\ exists ff_q_fsat_iff_value_forwardfactorsfactorization_product_factor. mv_factor_code_iff_value_forwardfactors = ff_q_fsat_iff_value_forwardfactorsfactorization_product_factor * S ((S (ff_i_fsat_iff_value_forwardfactorsfactorization_product)) * mv_factor_scale_iff_value_forwardfactors) + (ff_p_fsat_iff_value_forwardfactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_value_forwardfactorsfactorization_product_partial. ff_h_fsat_iff_value_forwardfactorsfactorization_product_partial + S (ff_r_fsat_iff_value_forwardfactorsfactorization_product) = S ((S (ff_i_fsat_iff_value_forwardfactorsfactorization_product)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_forwardfactorsfactorization_product_partial. ff_u_fsat_iff_value_forwardfactorsfactorization_product = ff_q_fsat_iff_value_forwardfactorsfactorization_product_partial * S ((S (ff_i_fsat_iff_value_forwardfactorsfactorization_product)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product) + (ff_r_fsat_iff_value_forwardfactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_value_forwardfactorsfactorization_product_successor. ff_h_fsat_iff_value_forwardfactorsfactorization_product_successor + S (ff_s_fsat_iff_value_forwardfactorsfactorization_product) = S ((S (S ff_i_fsat_iff_value_forwardfactorsfactorization_product)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_forwardfactorsfactorization_product_successor. ff_u_fsat_iff_value_forwardfactorsfactorization_product = ff_q_fsat_iff_value_forwardfactorsfactorization_product_successor * S ((S (S ff_i_fsat_iff_value_forwardfactorsfactorization_product)) * ff_v_fsat_iff_value_forwardfactorsfactorization_product) + (ff_s_fsat_iff_value_forwardfactorsfactorization_product))) /\ ff_s_fsat_iff_value_forwardfactorsfactorization_product = ff_r_fsat_iff_value_forwardfactorsfactorization_product * ff_p_fsat_iff_value_forwardfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_iff_value_forwardfactorsfactorization_primes. (exists ftsf_gap_fsat_iff_value_forwardfactorsfactorization_primes_bound. ftsf_gap_fsat_iff_value_forwardfactorsfactorization_primes_bound + S ftsf_index_fsat_iff_value_forwardfactorsfactorization_primes = (mv_factor_count_iff_value_forwardfactors)) -> exists ftsf_factor_fsat_iff_value_forwardfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_entry. ff_h_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_entry + S (ftsf_factor_fsat_iff_value_forwardfactorsfactorization_primes) = S ((S (ftsf_index_fsat_iff_value_forwardfactorsfactorization_primes)) * mv_factor_scale_iff_value_forwardfactors)) /\ exists ff_q_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_entry. mv_factor_code_iff_value_forwardfactors = ff_q_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_iff_value_forwardfactorsfactorization_primes)) * mv_factor_scale_iff_value_forwardfactors) + (ftsf_factor_fsat_iff_value_forwardfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_iff_value_forwardfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_prime. ftsf_factor_fsat_iff_value_forwardfactorsfactorization_primes = frm_prime_left_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_iff_value_forwardfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_iff_value_forwardfactorsparityeven. (mv_factor_count_iff_value_forwardfactors) = 2 * mv_even_half_iff_value_forwardfactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_iff_value_forwardfactorsparityodd. (mv_factor_count_iff_value_forwardfactors) = 2 * mv_odd_half_iff_value_forwardfactorsparityodd + 1) /\ ((z) = 1)))))))))))) /\ ((((~((i) = 0)) /\ ((((exists mv_square_prime_iff_value_reversesquare. ((~((mv_square_prime_iff_value_reversesquare) = 1) /\ forall pvs_left_iff_value_reversesquareprime pvs_right_iff_value_reversesquareprime. (mv_square_prime_iff_value_reversesquare) = pvs_left_iff_value_reversesquareprime * pvs_right_iff_value_reversesquareprime -> pvs_left_iff_value_reversesquareprime = 1 \/ pvs_right_iff_value_reversesquareprime = 1) /\ (exists pvs_factor_iff_value_reversesquaredivisor. (i) = (mv_square_prime_iff_value_reversesquare * mv_square_prime_iff_value_reversesquare) * pvs_factor_iff_value_reversesquaredivisor))) /\ ((z) = 0))) \/ (((((~((i) = 0)) /\ (forall sfd_prime_iff_value_reversesquarefree. (~((sfd_prime_iff_value_reversesquarefree) = 1) /\ forall pvs_left_iff_value_reversesquarefreedomain pvs_right_iff_value_reversesquarefreedomain. (sfd_prime_iff_value_reversesquarefree) = pvs_left_iff_value_reversesquarefreedomain * pvs_right_iff_value_reversesquarefreedomain -> pvs_left_iff_value_reversesquarefreedomain = 1 \/ pvs_right_iff_value_reversesquarefreedomain = 1) -> (exists pvs_le_gap_iff_value_reversesquarefreebound. pvs_le_gap_iff_value_reversesquarefreebound + (sfd_prime_iff_value_reversesquarefree) = (i)) -> ~(exists pvs_factor_iff_value_reversesquarefreesquare. (i) = (sfd_prime_iff_value_reversesquarefree * sfd_prime_iff_value_reversesquarefree) * pvs_factor_iff_value_reversesquarefreesquare)))) /\ (exists mv_factor_code_iff_value_reversefactors mv_factor_scale_iff_value_reversefactors mv_factor_count_iff_value_reversefactors. (((~(i = 0) /\ ((exists ff_u_fsat_iff_value_reversefactorsfactorization_product ff_v_fsat_iff_value_reversefactorsfactorization_product. ((((exists ff_h_fsat_iff_value_reversefactorsfactorization_product_start. ff_h_fsat_iff_value_reversefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_iff_value_reversefactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_reversefactorsfactorization_product_start. ff_u_fsat_iff_value_reversefactorsfactorization_product = ff_q_fsat_iff_value_reversefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_iff_value_reversefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_iff_value_reversefactorsfactorization_product_terminal. ff_h_fsat_iff_value_reversefactorsfactorization_product_terminal + S (i) = S ((S (mv_factor_count_iff_value_reversefactors)) * ff_v_fsat_iff_value_reversefactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_reversefactorsfactorization_product_terminal. ff_u_fsat_iff_value_reversefactorsfactorization_product = ff_q_fsat_iff_value_reversefactorsfactorization_product_terminal * S ((S (mv_factor_count_iff_value_reversefactors)) * ff_v_fsat_iff_value_reversefactorsfactorization_product) + (i))) /\ forall ff_i_fsat_iff_value_reversefactorsfactorization_product. (exists ff_lt_fsat_iff_value_reversefactorsfactorization_product_bound. ff_lt_fsat_iff_value_reversefactorsfactorization_product_bound + S ff_i_fsat_iff_value_reversefactorsfactorization_product = mv_factor_count_iff_value_reversefactors) -> exists ff_p_fsat_iff_value_reversefactorsfactorization_product ff_r_fsat_iff_value_reversefactorsfactorization_product ff_s_fsat_iff_value_reversefactorsfactorization_product. ((((exists ff_h_fsat_iff_value_reversefactorsfactorization_product_factor. ff_h_fsat_iff_value_reversefactorsfactorization_product_factor + S (ff_p_fsat_iff_value_reversefactorsfactorization_product) = S ((S (ff_i_fsat_iff_value_reversefactorsfactorization_product)) * mv_factor_scale_iff_value_reversefactors)) /\ exists ff_q_fsat_iff_value_reversefactorsfactorization_product_factor. mv_factor_code_iff_value_reversefactors = ff_q_fsat_iff_value_reversefactorsfactorization_product_factor * S ((S (ff_i_fsat_iff_value_reversefactorsfactorization_product)) * mv_factor_scale_iff_value_reversefactors) + (ff_p_fsat_iff_value_reversefactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_value_reversefactorsfactorization_product_partial. ff_h_fsat_iff_value_reversefactorsfactorization_product_partial + S (ff_r_fsat_iff_value_reversefactorsfactorization_product) = S ((S (ff_i_fsat_iff_value_reversefactorsfactorization_product)) * ff_v_fsat_iff_value_reversefactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_reversefactorsfactorization_product_partial. ff_u_fsat_iff_value_reversefactorsfactorization_product = ff_q_fsat_iff_value_reversefactorsfactorization_product_partial * S ((S (ff_i_fsat_iff_value_reversefactorsfactorization_product)) * ff_v_fsat_iff_value_reversefactorsfactorization_product) + (ff_r_fsat_iff_value_reversefactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_value_reversefactorsfactorization_product_successor. ff_h_fsat_iff_value_reversefactorsfactorization_product_successor + S (ff_s_fsat_iff_value_reversefactorsfactorization_product) = S ((S (S ff_i_fsat_iff_value_reversefactorsfactorization_product)) * ff_v_fsat_iff_value_reversefactorsfactorization_product)) /\ exists ff_q_fsat_iff_value_reversefactorsfactorization_product_successor. ff_u_fsat_iff_value_reversefactorsfactorization_product = ff_q_fsat_iff_value_reversefactorsfactorization_product_successor * S ((S (S ff_i_fsat_iff_value_reversefactorsfactorization_product)) * ff_v_fsat_iff_value_reversefactorsfactorization_product) + (ff_s_fsat_iff_value_reversefactorsfactorization_product))) /\ ff_s_fsat_iff_value_reversefactorsfactorization_product = ff_r_fsat_iff_value_reversefactorsfactorization_product * ff_p_fsat_iff_value_reversefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_iff_value_reversefactorsfactorization_primes. (exists ftsf_gap_fsat_iff_value_reversefactorsfactorization_primes_bound. ftsf_gap_fsat_iff_value_reversefactorsfactorization_primes_bound + S ftsf_index_fsat_iff_value_reversefactorsfactorization_primes = (mv_factor_count_iff_value_reversefactors)) -> exists ftsf_factor_fsat_iff_value_reversefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_iff_value_reversefactorsfactorization_primes_entry. ff_h_ftsf_fsat_iff_value_reversefactorsfactorization_primes_entry + S (ftsf_factor_fsat_iff_value_reversefactorsfactorization_primes) = S ((S (ftsf_index_fsat_iff_value_reversefactorsfactorization_primes)) * mv_factor_scale_iff_value_reversefactors)) /\ exists ff_q_ftsf_fsat_iff_value_reversefactorsfactorization_primes_entry. mv_factor_code_iff_value_reversefactors = ff_q_ftsf_fsat_iff_value_reversefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_iff_value_reversefactorsfactorization_primes)) * mv_factor_scale_iff_value_reversefactors) + (ftsf_factor_fsat_iff_value_reversefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_iff_value_reversefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_iff_value_reversefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_iff_value_reversefactorsfactorization_primes_prime. ftsf_factor_fsat_iff_value_reversefactorsfactorization_primes = frm_prime_left_ftsf_fsat_iff_value_reversefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_iff_value_reversefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_iff_value_reversefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_iff_value_reversefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_iff_value_reversefactorsparityeven. (mv_factor_count_iff_value_reversefactors) = 2 * mv_even_half_iff_value_reversefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_iff_value_reversefactorsparityodd. (mv_factor_count_iff_value_reversefactors) = 2 * mv_odd_half_iff_value_reversefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> (exists dst_positive_code_iff_entry_reverse dst_positive_scale_iff_entry_reverse dst_negative_code_iff_entry_reverse dst_negative_scale_iff_entry_reverse dst_positive_iff_entry_reverse dst_negative_iff_entry_reverse. (((M) = (((((dst_positive_code_iff_entry_reverse) + (dst_positive_scale_iff_entry_reverse)) * S ((dst_positive_code_iff_entry_reverse) + (dst_positive_scale_iff_entry_reverse)) + ((dst_positive_scale_iff_entry_reverse) + (dst_positive_scale_iff_entry_reverse))) + (((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) * S ((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) + ((dst_negative_scale_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)))) * S ((((dst_positive_code_iff_entry_reverse) + (dst_positive_scale_iff_entry_reverse)) * S ((dst_positive_code_iff_entry_reverse) + (dst_positive_scale_iff_entry_reverse)) + ((dst_positive_scale_iff_entry_reverse) + (dst_positive_scale_iff_entry_reverse))) + (((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) * S ((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) + ((dst_negative_scale_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)))) + ((((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) * S ((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) + ((dst_negative_scale_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse))) + (((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) * S ((dst_negative_code_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)) + ((dst_negative_scale_iff_entry_reverse) + (dst_negative_scale_iff_entry_reverse)))))) /\ (((((exists ff_h_pvs_iff_entry_reversepositive. ff_h_pvs_iff_entry_reversepositive + S (dst_positive_iff_entry_reverse) = S ((S (i)) * dst_positive_scale_iff_entry_reverse)) /\ exists ff_q_pvs_iff_entry_reversepositive. dst_positive_code_iff_entry_reverse = ff_q_pvs_iff_entry_reversepositive * S ((S (i)) * dst_positive_scale_iff_entry_reverse) + (dst_positive_iff_entry_reverse))) /\ (((((exists ff_h_pvs_iff_entry_reversenegative. ff_h_pvs_iff_entry_reversenegative + S (dst_negative_iff_entry_reverse) = S ((S (i)) * dst_negative_scale_iff_entry_reverse)) /\ exists ff_q_pvs_iff_entry_reversenegative. dst_negative_code_iff_entry_reverse = ff_q_pvs_iff_entry_reversenegative * S ((S (i)) * dst_negative_scale_iff_entry_reverse) + (dst_negative_iff_entry_reverse))) /\ (exists ge_balance_positive_iff_entry_reversevalue ge_balance_negative_iff_entry_reversevalue. (((((z) = 2 * (ge_balance_positive_iff_entry_reversevalue) /\ (ge_balance_negative_iff_entry_reversevalue) = 0) \/ exists ge_signed_half_iff_entry_reversevaluedecode. (((z) = 2 * ge_signed_half_iff_entry_reversevaluedecode + 1 /\ (ge_balance_positive_iff_entry_reversevalue) = 0) /\ (ge_balance_negative_iff_entry_reversevalue) = S ge_signed_half_iff_entry_reversevaluedecode))) /\ ((dst_positive_iff_entry_reverse) + ge_balance_negative_iff_entry_reversevalue = (dst_negative_iff_entry_reverse) + ge_balance_positive_iff_entry_reversevalue))))))))))