mobius_divisor_sum_cancellation

Exact expanded first-order arithmetic statement

forall N M n z. (((exists dst_positive_code_cancel_iff_tabletable dst_positive_scale_cancel_iff_tabletable dst_negative_code_cancel_iff_tabletable dst_negative_scale_cancel_iff_tabletable. (((M) = (((((dst_positive_code_cancel_iff_tabletable) + (dst_positive_scale_cancel_iff_tabletable)) * S ((dst_positive_code_cancel_iff_tabletable) + (dst_positive_scale_cancel_iff_tabletable)) + ((dst_positive_scale_cancel_iff_tabletable) + (dst_positive_scale_cancel_iff_tabletable))) + (((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) * S ((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) + ((dst_negative_scale_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)))) * S ((((dst_positive_code_cancel_iff_tabletable) + (dst_positive_scale_cancel_iff_tabletable)) * S ((dst_positive_code_cancel_iff_tabletable) + (dst_positive_scale_cancel_iff_tabletable)) + ((dst_positive_scale_cancel_iff_tabletable) + (dst_positive_scale_cancel_iff_tabletable))) + (((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) * S ((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) + ((dst_negative_scale_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)))) + ((((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) * S ((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) + ((dst_negative_scale_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable))) + (((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) * S ((dst_negative_code_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)) + ((dst_negative_scale_cancel_iff_tabletable) + (dst_negative_scale_cancel_iff_tabletable)))))) /\ (forall dst_index_cancel_iff_tabletable. (exists pvs_le_gap_cancel_iff_tabletabledomain. pvs_le_gap_cancel_iff_tabletabledomain + (dst_index_cancel_iff_tabletable) = (N)) -> exists dst_positive_cancel_iff_tabletable dst_negative_cancel_iff_tabletable dst_value_cancel_iff_tabletable. ((((exists ff_h_pvs_cancel_iff_tabletableentrypositive. ff_h_pvs_cancel_iff_tabletableentrypositive + S (dst_positive_cancel_iff_tabletable) = S ((S (dst_index_cancel_iff_tabletable)) * dst_positive_scale_cancel_iff_tabletable)) /\ exists ff_q_pvs_cancel_iff_tabletableentrypositive. dst_positive_code_cancel_iff_tabletable = ff_q_pvs_cancel_iff_tabletableentrypositive * S ((S (dst_index_cancel_iff_tabletable)) * dst_positive_scale_cancel_iff_tabletable) + (dst_positive_cancel_iff_tabletable))) /\ (((((exists ff_h_pvs_cancel_iff_tabletableentrynegative. ff_h_pvs_cancel_iff_tabletableentrynegative + S (dst_negative_cancel_iff_tabletable) = S ((S (dst_index_cancel_iff_tabletable)) * dst_negative_scale_cancel_iff_tabletable)) /\ exists ff_q_pvs_cancel_iff_tabletableentrynegative. dst_negative_code_cancel_iff_tabletable = ff_q_pvs_cancel_iff_tabletableentrynegative * S ((S (dst_index_cancel_iff_tabletable)) * dst_negative_scale_cancel_iff_tabletable) + (dst_negative_cancel_iff_tabletable))) /\ (exists ge_balance_positive_cancel_iff_tabletableentryvalue ge_balance_negative_cancel_iff_tabletableentryvalue. (((((dst_value_cancel_iff_tabletable) = 2 * (ge_balance_positive_cancel_iff_tabletableentryvalue) /\ (ge_balance_negative_cancel_iff_tabletableentryvalue) = 0) \/ exists ge_signed_half_cancel_iff_tabletableentryvaluedecode. (((dst_value_cancel_iff_tabletable) = 2 * ge_signed_half_cancel_iff_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_tabletableentryvalue) = 0) /\ (ge_balance_negative_cancel_iff_tabletableentryvalue) = S ge_signed_half_cancel_iff_tabletableentryvaluedecode))) /\ ((dst_positive_cancel_iff_tabletable) + ge_balance_negative_cancel_iff_tabletableentryvalue = (dst_negative_cancel_iff_tabletable) + ge_balance_positive_cancel_iff_tabletableentryvalue))))))))) /\ (((exists dst_positive_code_cancel_iff_tablezero dst_positive_scale_cancel_iff_tablezero dst_negative_code_cancel_iff_tablezero dst_negative_scale_cancel_iff_tablezero dst_positive_cancel_iff_tablezero dst_negative_cancel_iff_tablezero. (((M) = (((((dst_positive_code_cancel_iff_tablezero) + (dst_positive_scale_cancel_iff_tablezero)) * S ((dst_positive_code_cancel_iff_tablezero) + (dst_positive_scale_cancel_iff_tablezero)) + ((dst_positive_scale_cancel_iff_tablezero) + (dst_positive_scale_cancel_iff_tablezero))) + (((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) * S ((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) + ((dst_negative_scale_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)))) * S ((((dst_positive_code_cancel_iff_tablezero) + (dst_positive_scale_cancel_iff_tablezero)) * S ((dst_positive_code_cancel_iff_tablezero) + (dst_positive_scale_cancel_iff_tablezero)) + ((dst_positive_scale_cancel_iff_tablezero) + (dst_positive_scale_cancel_iff_tablezero))) + (((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) * S ((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) + ((dst_negative_scale_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)))) + ((((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) * S ((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) + ((dst_negative_scale_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero))) + (((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) * S ((dst_negative_code_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)) + ((dst_negative_scale_cancel_iff_tablezero) + (dst_negative_scale_cancel_iff_tablezero)))))) /\ (((((exists ff_h_pvs_cancel_iff_tablezeropositive. ff_h_pvs_cancel_iff_tablezeropositive + S (dst_positive_cancel_iff_tablezero) = S ((S (0)) * dst_positive_scale_cancel_iff_tablezero)) /\ exists ff_q_pvs_cancel_iff_tablezeropositive. dst_positive_code_cancel_iff_tablezero = ff_q_pvs_cancel_iff_tablezeropositive * S ((S (0)) * dst_positive_scale_cancel_iff_tablezero) + (dst_positive_cancel_iff_tablezero))) /\ (((((exists ff_h_pvs_cancel_iff_tablezeronegative. ff_h_pvs_cancel_iff_tablezeronegative + S (dst_negative_cancel_iff_tablezero) = S ((S (0)) * dst_negative_scale_cancel_iff_tablezero)) /\ exists ff_q_pvs_cancel_iff_tablezeronegative. dst_negative_code_cancel_iff_tablezero = ff_q_pvs_cancel_iff_tablezeronegative * S ((S (0)) * dst_negative_scale_cancel_iff_tablezero) + (dst_negative_cancel_iff_tablezero))) /\ (exists ge_balance_positive_cancel_iff_tablezerovalue ge_balance_negative_cancel_iff_tablezerovalue. (((((0) = 2 * (ge_balance_positive_cancel_iff_tablezerovalue) /\ (ge_balance_negative_cancel_iff_tablezerovalue) = 0) \/ exists ge_signed_half_cancel_iff_tablezerovaluedecode. (((0) = 2 * ge_signed_half_cancel_iff_tablezerovaluedecode + 1 /\ (ge_balance_positive_cancel_iff_tablezerovalue) = 0) /\ (ge_balance_negative_cancel_iff_tablezerovalue) = S ge_signed_half_cancel_iff_tablezerovaluedecode))) /\ ((dst_positive_cancel_iff_tablezero) + ge_balance_negative_cancel_iff_tablezerovalue = (dst_negative_cancel_iff_tablezero) + ge_balance_positive_cancel_iff_tablezerovalue))))))))) /\ (forall mt_index_cancel_iff_table mt_value_cancel_iff_table. ~(mt_index_cancel_iff_table=0) -> (exists pvs_le_gap_cancel_iff_tabledomain. pvs_le_gap_cancel_iff_tabledomain + (mt_index_cancel_iff_table) = (N)) -> (exists dst_positive_code_cancel_iff_tableentry dst_positive_scale_cancel_iff_tableentry dst_negative_code_cancel_iff_tableentry dst_negative_scale_cancel_iff_tableentry dst_positive_cancel_iff_tableentry dst_negative_cancel_iff_tableentry. (((M) = (((((dst_positive_code_cancel_iff_tableentry) + (dst_positive_scale_cancel_iff_tableentry)) * S ((dst_positive_code_cancel_iff_tableentry) + (dst_positive_scale_cancel_iff_tableentry)) + ((dst_positive_scale_cancel_iff_tableentry) + (dst_positive_scale_cancel_iff_tableentry))) + (((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) * S ((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) + ((dst_negative_scale_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)))) * S ((((dst_positive_code_cancel_iff_tableentry) + (dst_positive_scale_cancel_iff_tableentry)) * S ((dst_positive_code_cancel_iff_tableentry) + (dst_positive_scale_cancel_iff_tableentry)) + ((dst_positive_scale_cancel_iff_tableentry) + (dst_positive_scale_cancel_iff_tableentry))) + (((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) * S ((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) + ((dst_negative_scale_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)))) + ((((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) * S ((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) + ((dst_negative_scale_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry))) + (((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) * S ((dst_negative_code_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)) + ((dst_negative_scale_cancel_iff_tableentry) + (dst_negative_scale_cancel_iff_tableentry)))))) /\ (((((exists ff_h_pvs_cancel_iff_tableentrypositive. ff_h_pvs_cancel_iff_tableentrypositive + S (dst_positive_cancel_iff_tableentry) = S ((S (mt_index_cancel_iff_table)) * dst_positive_scale_cancel_iff_tableentry)) /\ exists ff_q_pvs_cancel_iff_tableentrypositive. dst_positive_code_cancel_iff_tableentry = ff_q_pvs_cancel_iff_tableentrypositive * S ((S (mt_index_cancel_iff_table)) * dst_positive_scale_cancel_iff_tableentry) + (dst_positive_cancel_iff_tableentry))) /\ (((((exists ff_h_pvs_cancel_iff_tableentrynegative. ff_h_pvs_cancel_iff_tableentrynegative + S (dst_negative_cancel_iff_tableentry) = S ((S (mt_index_cancel_iff_table)) * dst_negative_scale_cancel_iff_tableentry)) /\ exists ff_q_pvs_cancel_iff_tableentrynegative. dst_negative_code_cancel_iff_tableentry = ff_q_pvs_cancel_iff_tableentrynegative * S ((S (mt_index_cancel_iff_table)) * dst_negative_scale_cancel_iff_tableentry) + (dst_negative_cancel_iff_tableentry))) /\ (exists ge_balance_positive_cancel_iff_tableentryvalue ge_balance_negative_cancel_iff_tableentryvalue. (((((mt_value_cancel_iff_table) = 2 * (ge_balance_positive_cancel_iff_tableentryvalue) /\ (ge_balance_negative_cancel_iff_tableentryvalue) = 0) \/ exists ge_signed_half_cancel_iff_tableentryvaluedecode. (((mt_value_cancel_iff_table) = 2 * ge_signed_half_cancel_iff_tableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_tableentryvalue) = 0) /\ (ge_balance_negative_cancel_iff_tableentryvalue) = S ge_signed_half_cancel_iff_tableentryvaluedecode))) /\ ((dst_positive_cancel_iff_tableentry) + ge_balance_negative_cancel_iff_tableentryvalue = (dst_negative_cancel_iff_tableentry) + ge_balance_positive_cancel_iff_tableentryvalue))))))))) -> (((~((mt_index_cancel_iff_table) = 0)) /\ ((((exists mv_square_prime_cancel_iff_tablevaluesquare. ((~((mv_square_prime_cancel_iff_tablevaluesquare) = 1) /\ forall pvs_left_cancel_iff_tablevaluesquareprime pvs_right_cancel_iff_tablevaluesquareprime. (mv_square_prime_cancel_iff_tablevaluesquare) = pvs_left_cancel_iff_tablevaluesquareprime * pvs_right_cancel_iff_tablevaluesquareprime -> pvs_left_cancel_iff_tablevaluesquareprime = 1 \/ pvs_right_cancel_iff_tablevaluesquareprime = 1) /\ (exists pvs_factor_cancel_iff_tablevaluesquaredivisor. (mt_index_cancel_iff_table) = (mv_square_prime_cancel_iff_tablevaluesquare * mv_square_prime_cancel_iff_tablevaluesquare) * pvs_factor_cancel_iff_tablevaluesquaredivisor))) /\ ((mt_value_cancel_iff_table) = 0))) \/ (((((~((mt_index_cancel_iff_table) = 0)) /\ (forall sfd_prime_cancel_iff_tablevaluesquarefree. (~((sfd_prime_cancel_iff_tablevaluesquarefree) = 1) /\ forall pvs_left_cancel_iff_tablevaluesquarefreedomain pvs_right_cancel_iff_tablevaluesquarefreedomain. (sfd_prime_cancel_iff_tablevaluesquarefree) = pvs_left_cancel_iff_tablevaluesquarefreedomain * pvs_right_cancel_iff_tablevaluesquarefreedomain -> pvs_left_cancel_iff_tablevaluesquarefreedomain = 1 \/ pvs_right_cancel_iff_tablevaluesquarefreedomain = 1) -> (exists pvs_le_gap_cancel_iff_tablevaluesquarefreebound. pvs_le_gap_cancel_iff_tablevaluesquarefreebound + (sfd_prime_cancel_iff_tablevaluesquarefree) = (mt_index_cancel_iff_table)) -> ~(exists pvs_factor_cancel_iff_tablevaluesquarefreesquare. (mt_index_cancel_iff_table) = (sfd_prime_cancel_iff_tablevaluesquarefree * sfd_prime_cancel_iff_tablevaluesquarefree) * pvs_factor_cancel_iff_tablevaluesquarefreesquare)))) /\ (exists mv_factor_code_cancel_iff_tablevaluefactors mv_factor_scale_cancel_iff_tablevaluefactors mv_factor_count_cancel_iff_tablevaluefactors. (((~(mt_index_cancel_iff_table = 0) /\ ((exists ff_u_fsat_cancel_iff_tablevaluefactorsfactorization_product ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_start. ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_start. ff_u_fsat_cancel_iff_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_terminal. ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_terminal + S (mt_index_cancel_iff_table) = S ((S (mv_factor_count_cancel_iff_tablevaluefactors)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_terminal. ff_u_fsat_cancel_iff_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_cancel_iff_tablevaluefactors)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product) + (mt_index_cancel_iff_table))) /\ forall ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product. (exists ff_lt_fsat_cancel_iff_tablevaluefactorsfactorization_product_bound. ff_lt_fsat_cancel_iff_tablevaluefactorsfactorization_product_bound + S ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product = mv_factor_count_cancel_iff_tablevaluefactors) -> exists ff_p_fsat_cancel_iff_tablevaluefactorsfactorization_product ff_r_fsat_cancel_iff_tablevaluefactorsfactorization_product ff_s_fsat_cancel_iff_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_factor. ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_factor + S (ff_p_fsat_cancel_iff_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product)) * mv_factor_scale_cancel_iff_tablevaluefactors)) /\ exists ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_factor. mv_factor_code_cancel_iff_tablevaluefactors = ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product)) * mv_factor_scale_cancel_iff_tablevaluefactors) + (ff_p_fsat_cancel_iff_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_partial. ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_partial + S (ff_r_fsat_cancel_iff_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_partial. ff_u_fsat_cancel_iff_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product) + (ff_r_fsat_cancel_iff_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_successor. ff_h_fsat_cancel_iff_tablevaluefactorsfactorization_product_successor + S (ff_s_fsat_cancel_iff_tablevaluefactorsfactorization_product) = S ((S (S ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_successor. ff_u_fsat_cancel_iff_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_iff_tablevaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_cancel_iff_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_iff_tablevaluefactorsfactorization_product) + (ff_s_fsat_cancel_iff_tablevaluefactorsfactorization_product))) /\ ff_s_fsat_cancel_iff_tablevaluefactorsfactorization_product = ff_r_fsat_cancel_iff_tablevaluefactorsfactorization_product * ff_p_fsat_cancel_iff_tablevaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_cancel_iff_tablevaluefactorsfactorization_primes. (exists ftsf_gap_fsat_cancel_iff_tablevaluefactorsfactorization_primes_bound. ftsf_gap_fsat_cancel_iff_tablevaluefactorsfactorization_primes_bound + S ftsf_index_fsat_cancel_iff_tablevaluefactorsfactorization_primes = (mv_factor_count_cancel_iff_tablevaluefactors)) -> exists ftsf_factor_fsat_cancel_iff_tablevaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_cancel_iff_tablevaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_cancel_iff_tablevaluefactorsfactorization_primes)) * mv_factor_scale_cancel_iff_tablevaluefactors)) /\ exists ff_q_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_entry. mv_factor_code_cancel_iff_tablevaluefactors = ff_q_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_cancel_iff_tablevaluefactorsfactorization_primes)) * mv_factor_scale_cancel_iff_tablevaluefactors) + (ftsf_factor_fsat_cancel_iff_tablevaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_cancel_iff_tablevaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_prime. ftsf_factor_fsat_cancel_iff_tablevaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_cancel_iff_tablevaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_cancel_iff_tablevaluefactorsparityeven. (mv_factor_count_cancel_iff_tablevaluefactors) = 2 * mv_even_half_cancel_iff_tablevaluefactorsparityeven) /\ ((mt_value_cancel_iff_table) = 2))) \/ (((exists mv_odd_half_cancel_iff_tablevaluefactorsparityodd. (mv_factor_count_cancel_iff_tablevaluefactors) = 2 * mv_odd_half_cancel_iff_tablevaluefactorsparityodd + 1) /\ ((mt_value_cancel_iff_table) = 1)))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_cancel_iff_bound. pvs_le_gap_cancel_iff_bound + (n) = (N)) -> ((((((~((n)=0)) /\ (exists dm_mask_table_cancel_iff_resultforward. ((((exists dst_positive_code_cancel_iff_resultforwardmasktable dst_positive_scale_cancel_iff_resultforwardmasktable dst_negative_code_cancel_iff_resultforwardmasktable dst_negative_scale_cancel_iff_resultforwardmasktable. (((dm_mask_table_cancel_iff_resultforward) = (((((dst_positive_code_cancel_iff_resultforwardmasktable) + (dst_positive_scale_cancel_iff_resultforwardmasktable)) * S ((dst_positive_code_cancel_iff_resultforwardmasktable) + (dst_positive_scale_cancel_iff_resultforwardmasktable)) + ((dst_positive_scale_cancel_iff_resultforwardmasktable) + (dst_positive_scale_cancel_iff_resultforwardmasktable))) + (((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) * S ((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) + ((dst_negative_scale_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)))) * S ((((dst_positive_code_cancel_iff_resultforwardmasktable) + (dst_positive_scale_cancel_iff_resultforwardmasktable)) * S ((dst_positive_code_cancel_iff_resultforwardmasktable) + (dst_positive_scale_cancel_iff_resultforwardmasktable)) + ((dst_positive_scale_cancel_iff_resultforwardmasktable) + (dst_positive_scale_cancel_iff_resultforwardmasktable))) + (((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) * S ((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) + ((dst_negative_scale_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)))) + ((((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) * S ((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) + ((dst_negative_scale_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable))) + (((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) * S ((dst_negative_code_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)) + ((dst_negative_scale_cancel_iff_resultforwardmasktable) + (dst_negative_scale_cancel_iff_resultforwardmasktable)))))) /\ (forall dst_index_cancel_iff_resultforwardmasktable. (exists pvs_le_gap_cancel_iff_resultforwardmasktabledomain. pvs_le_gap_cancel_iff_resultforwardmasktabledomain + (dst_index_cancel_iff_resultforwardmasktable) = (n)) -> exists dst_positive_cancel_iff_resultforwardmasktable dst_negative_cancel_iff_resultforwardmasktable dst_value_cancel_iff_resultforwardmasktable. ((((exists ff_h_pvs_cancel_iff_resultforwardmasktableentrypositive. ff_h_pvs_cancel_iff_resultforwardmasktableentrypositive + S (dst_positive_cancel_iff_resultforwardmasktable) = S ((S (dst_index_cancel_iff_resultforwardmasktable)) * dst_positive_scale_cancel_iff_resultforwardmasktable)) /\ exists ff_q_pvs_cancel_iff_resultforwardmasktableentrypositive. dst_positive_code_cancel_iff_resultforwardmasktable = ff_q_pvs_cancel_iff_resultforwardmasktableentrypositive * S ((S (dst_index_cancel_iff_resultforwardmasktable)) * dst_positive_scale_cancel_iff_resultforwardmasktable) + (dst_positive_cancel_iff_resultforwardmasktable))) /\ (((((exists ff_h_pvs_cancel_iff_resultforwardmasktableentrynegative. ff_h_pvs_cancel_iff_resultforwardmasktableentrynegative + S (dst_negative_cancel_iff_resultforwardmasktable) = S ((S (dst_index_cancel_iff_resultforwardmasktable)) * dst_negative_scale_cancel_iff_resultforwardmasktable)) /\ exists ff_q_pvs_cancel_iff_resultforwardmasktableentrynegative. dst_negative_code_cancel_iff_resultforwardmasktable = ff_q_pvs_cancel_iff_resultforwardmasktableentrynegative * S ((S (dst_index_cancel_iff_resultforwardmasktable)) * dst_negative_scale_cancel_iff_resultforwardmasktable) + (dst_negative_cancel_iff_resultforwardmasktable))) /\ (exists ge_balance_positive_cancel_iff_resultforwardmasktableentryvalue ge_balance_negative_cancel_iff_resultforwardmasktableentryvalue. (((((dst_value_cancel_iff_resultforwardmasktable) = 2 * (ge_balance_positive_cancel_iff_resultforwardmasktableentryvalue) /\ (ge_balance_negative_cancel_iff_resultforwardmasktableentryvalue) = 0) \/ exists ge_signed_half_cancel_iff_resultforwardmasktableentryvaluedecode. (((dst_value_cancel_iff_resultforwardmasktable) = 2 * ge_signed_half_cancel_iff_resultforwardmasktableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_resultforwardmasktableentryvalue) = 0) /\ (ge_balance_negative_cancel_iff_resultforwardmasktableentryvalue) = S ge_signed_half_cancel_iff_resultforwardmasktableentryvaluedecode))) /\ ((dst_positive_cancel_iff_resultforwardmasktable) + ge_balance_negative_cancel_iff_resultforwardmasktableentryvalue = (dst_negative_cancel_iff_resultforwardmasktable) + ge_balance_positive_cancel_iff_resultforwardmasktableentryvalue))))))))) /\ (forall dm_index_cancel_iff_resultforwardmask dm_value_cancel_iff_resultforwardmask. (exists pvs_le_gap_cancel_iff_resultforwardmaskdomain. pvs_le_gap_cancel_iff_resultforwardmaskdomain + (dm_index_cancel_iff_resultforwardmask) = (n)) -> (exists dst_positive_code_cancel_iff_resultforwardmasklookup dst_positive_scale_cancel_iff_resultforwardmasklookup dst_negative_code_cancel_iff_resultforwardmasklookup dst_negative_scale_cancel_iff_resultforwardmasklookup dst_positive_cancel_iff_resultforwardmasklookup dst_negative_cancel_iff_resultforwardmasklookup. (((dm_mask_table_cancel_iff_resultforward) = (((((dst_positive_code_cancel_iff_resultforwardmasklookup) + (dst_positive_scale_cancel_iff_resultforwardmasklookup)) * S ((dst_positive_code_cancel_iff_resultforwardmasklookup) + (dst_positive_scale_cancel_iff_resultforwardmasklookup)) + ((dst_positive_scale_cancel_iff_resultforwardmasklookup) + (dst_positive_scale_cancel_iff_resultforwardmasklookup))) + (((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) * S ((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) + ((dst_negative_scale_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)))) * S ((((dst_positive_code_cancel_iff_resultforwardmasklookup) + (dst_positive_scale_cancel_iff_resultforwardmasklookup)) * S ((dst_positive_code_cancel_iff_resultforwardmasklookup) + (dst_positive_scale_cancel_iff_resultforwardmasklookup)) + ((dst_positive_scale_cancel_iff_resultforwardmasklookup) + (dst_positive_scale_cancel_iff_resultforwardmasklookup))) + (((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) * S ((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) + ((dst_negative_scale_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)))) + ((((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) * S ((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) + ((dst_negative_scale_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup))) + (((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) * S ((dst_negative_code_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)) + ((dst_negative_scale_cancel_iff_resultforwardmasklookup) + (dst_negative_scale_cancel_iff_resultforwardmasklookup)))))) /\ (((((exists ff_h_pvs_cancel_iff_resultforwardmasklookuppositive. ff_h_pvs_cancel_iff_resultforwardmasklookuppositive + S (dst_positive_cancel_iff_resultforwardmasklookup) = S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_positive_scale_cancel_iff_resultforwardmasklookup)) /\ exists ff_q_pvs_cancel_iff_resultforwardmasklookuppositive. dst_positive_code_cancel_iff_resultforwardmasklookup = ff_q_pvs_cancel_iff_resultforwardmasklookuppositive * S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_positive_scale_cancel_iff_resultforwardmasklookup) + (dst_positive_cancel_iff_resultforwardmasklookup))) /\ (((((exists ff_h_pvs_cancel_iff_resultforwardmasklookupnegative. ff_h_pvs_cancel_iff_resultforwardmasklookupnegative + S (dst_negative_cancel_iff_resultforwardmasklookup) = S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_negative_scale_cancel_iff_resultforwardmasklookup)) /\ exists ff_q_pvs_cancel_iff_resultforwardmasklookupnegative. dst_negative_code_cancel_iff_resultforwardmasklookup = ff_q_pvs_cancel_iff_resultforwardmasklookupnegative * S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_negative_scale_cancel_iff_resultforwardmasklookup) + (dst_negative_cancel_iff_resultforwardmasklookup))) /\ (exists ge_balance_positive_cancel_iff_resultforwardmasklookupvalue ge_balance_negative_cancel_iff_resultforwardmasklookupvalue. (((((dm_value_cancel_iff_resultforwardmask) = 2 * (ge_balance_positive_cancel_iff_resultforwardmasklookupvalue) /\ (ge_balance_negative_cancel_iff_resultforwardmasklookupvalue) = 0) \/ exists ge_signed_half_cancel_iff_resultforwardmasklookupvaluedecode. (((dm_value_cancel_iff_resultforwardmask) = 2 * ge_signed_half_cancel_iff_resultforwardmasklookupvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_resultforwardmasklookupvalue) = 0) /\ (ge_balance_negative_cancel_iff_resultforwardmasklookupvalue) = S ge_signed_half_cancel_iff_resultforwardmasklookupvaluedecode))) /\ ((dst_positive_cancel_iff_resultforwardmasklookup) + ge_balance_negative_cancel_iff_resultforwardmasklookupvalue = (dst_negative_cancel_iff_resultforwardmasklookup) + ge_balance_positive_cancel_iff_resultforwardmasklookupvalue))))))))) -> ((((~((dm_index_cancel_iff_resultforwardmask)=0)) /\ (exists dm_quotient_cancel_iff_resultforwardmaskentry. (((n)=(dm_index_cancel_iff_resultforwardmask)*dm_quotient_cancel_iff_resultforwardmaskentry) /\ (exists dst_positive_code_cancel_iff_resultforwardmaskentryinput dst_positive_scale_cancel_iff_resultforwardmaskentryinput dst_negative_code_cancel_iff_resultforwardmaskentryinput dst_negative_scale_cancel_iff_resultforwardmaskentryinput dst_positive_cancel_iff_resultforwardmaskentryinput dst_negative_cancel_iff_resultforwardmaskentryinput. (((M) = (((((dst_positive_code_cancel_iff_resultforwardmaskentryinput) + (dst_positive_scale_cancel_iff_resultforwardmaskentryinput)) * S ((dst_positive_code_cancel_iff_resultforwardmaskentryinput) + (dst_positive_scale_cancel_iff_resultforwardmaskentryinput)) + ((dst_positive_scale_cancel_iff_resultforwardmaskentryinput) + (dst_positive_scale_cancel_iff_resultforwardmaskentryinput))) + (((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) * S ((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) + ((dst_negative_scale_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)))) * S ((((dst_positive_code_cancel_iff_resultforwardmaskentryinput) + (dst_positive_scale_cancel_iff_resultforwardmaskentryinput)) * S ((dst_positive_code_cancel_iff_resultforwardmaskentryinput) + (dst_positive_scale_cancel_iff_resultforwardmaskentryinput)) + ((dst_positive_scale_cancel_iff_resultforwardmaskentryinput) + (dst_positive_scale_cancel_iff_resultforwardmaskentryinput))) + (((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) * S ((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) + ((dst_negative_scale_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)))) + ((((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) * S ((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) + ((dst_negative_scale_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput))) + (((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) * S ((dst_negative_code_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) + ((dst_negative_scale_cancel_iff_resultforwardmaskentryinput) + (dst_negative_scale_cancel_iff_resultforwardmaskentryinput)))))) /\ (((((exists ff_h_pvs_cancel_iff_resultforwardmaskentryinputpositive. ff_h_pvs_cancel_iff_resultforwardmaskentryinputpositive + S (dst_positive_cancel_iff_resultforwardmaskentryinput) = S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_positive_scale_cancel_iff_resultforwardmaskentryinput)) /\ exists ff_q_pvs_cancel_iff_resultforwardmaskentryinputpositive. dst_positive_code_cancel_iff_resultforwardmaskentryinput = ff_q_pvs_cancel_iff_resultforwardmaskentryinputpositive * S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_positive_scale_cancel_iff_resultforwardmaskentryinput) + (dst_positive_cancel_iff_resultforwardmaskentryinput))) /\ (((((exists ff_h_pvs_cancel_iff_resultforwardmaskentryinputnegative. ff_h_pvs_cancel_iff_resultforwardmaskentryinputnegative + S (dst_negative_cancel_iff_resultforwardmaskentryinput) = S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_negative_scale_cancel_iff_resultforwardmaskentryinput)) /\ exists ff_q_pvs_cancel_iff_resultforwardmaskentryinputnegative. dst_negative_code_cancel_iff_resultforwardmaskentryinput = ff_q_pvs_cancel_iff_resultforwardmaskentryinputnegative * S ((S (dm_index_cancel_iff_resultforwardmask)) * dst_negative_scale_cancel_iff_resultforwardmaskentryinput) + (dst_negative_cancel_iff_resultforwardmaskentryinput))) /\ (exists ge_balance_positive_cancel_iff_resultforwardmaskentryinputvalue ge_balance_negative_cancel_iff_resultforwardmaskentryinputvalue. (((((dm_value_cancel_iff_resultforwardmask) = 2 * (ge_balance_positive_cancel_iff_resultforwardmaskentryinputvalue) /\ (ge_balance_negative_cancel_iff_resultforwardmaskentryinputvalue) = 0) \/ exists ge_signed_half_cancel_iff_resultforwardmaskentryinputvaluedecode. (((dm_value_cancel_iff_resultforwardmask) = 2 * ge_signed_half_cancel_iff_resultforwardmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_resultforwardmaskentryinputvalue) = 0) /\ (ge_balance_negative_cancel_iff_resultforwardmaskentryinputvalue) = S ge_signed_half_cancel_iff_resultforwardmaskentryinputvaluedecode))) /\ ((dst_positive_cancel_iff_resultforwardmaskentryinput) + ge_balance_negative_cancel_iff_resultforwardmaskentryinputvalue = (dst_negative_cancel_iff_resultforwardmaskentryinput) + ge_balance_positive_cancel_iff_resultforwardmaskentryinputvalue))))))))))))) \/ ((((dm_index_cancel_iff_resultforwardmask)=0 \/ ~(exists pvs_factor_cancel_iff_resultforwardmaskentrynondivisor. (n) = (dm_index_cancel_iff_resultforwardmask) * pvs_factor_cancel_iff_resultforwardmaskentrynondivisor)) /\ ((dm_value_cancel_iff_resultforwardmask)=0))))))) /\ (exists dst_positive_code_cancel_iff_resultforwardfold dst_positive_scale_cancel_iff_resultforwardfold dst_negative_code_cancel_iff_resultforwardfold dst_negative_scale_cancel_iff_resultforwardfold dst_positive_sum_cancel_iff_resultforwardfold dst_negative_sum_cancel_iff_resultforwardfold. (((dm_mask_table_cancel_iff_resultforward) = (((((dst_positive_code_cancel_iff_resultforwardfold) + (dst_positive_scale_cancel_iff_resultforwardfold)) * S ((dst_positive_code_cancel_iff_resultforwardfold) + (dst_positive_scale_cancel_iff_resultforwardfold)) + ((dst_positive_scale_cancel_iff_resultforwardfold) + (dst_positive_scale_cancel_iff_resultforwardfold))) + (((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) * S ((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) + ((dst_negative_scale_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)))) * S ((((dst_positive_code_cancel_iff_resultforwardfold) + (dst_positive_scale_cancel_iff_resultforwardfold)) * S ((dst_positive_code_cancel_iff_resultforwardfold) + (dst_positive_scale_cancel_iff_resultforwardfold)) + ((dst_positive_scale_cancel_iff_resultforwardfold) + (dst_positive_scale_cancel_iff_resultforwardfold))) + (((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) * S ((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) + ((dst_negative_scale_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)))) + ((((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) * S ((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) + ((dst_negative_scale_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold))) + (((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) * S ((dst_negative_code_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)) + ((dst_negative_scale_cancel_iff_resultforwardfold) + (dst_negative_scale_cancel_iff_resultforwardfold)))))) /\ (((exists fs_u_dst_cancel_iff_resultforwardfoldpositive fs_v_dst_cancel_iff_resultforwardfoldpositive. ((((exists fs_h_dst_cancel_iff_resultforwardfoldpositive_body_start. fs_h_dst_cancel_iff_resultforwardfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_iff_resultforwardfoldpositive)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldpositive_body_start. fs_u_dst_cancel_iff_resultforwardfoldpositive = fs_q_dst_cancel_iff_resultforwardfoldpositive_body_start * S ((S (0)) * fs_v_dst_cancel_iff_resultforwardfoldpositive) + (0))) /\ ((((exists fs_h_dst_cancel_iff_resultforwardfoldpositive_body_terminal. fs_h_dst_cancel_iff_resultforwardfoldpositive_body_terminal + S (dst_positive_sum_cancel_iff_resultforwardfold) = S ((S (S (n))) * fs_v_dst_cancel_iff_resultforwardfoldpositive)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldpositive_body_terminal. fs_u_dst_cancel_iff_resultforwardfoldpositive = fs_q_dst_cancel_iff_resultforwardfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_cancel_iff_resultforwardfoldpositive) + (dst_positive_sum_cancel_iff_resultforwardfold))) /\ forall fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps. (exists fs_lt_dst_cancel_iff_resultforwardfoldpositive_body_steps_bound. fs_lt_dst_cancel_iff_resultforwardfoldpositive_body_steps_bound + S fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps = S (n)) -> exists fs_a_dst_cancel_iff_resultforwardfoldpositive_body_steps fs_r_dst_cancel_iff_resultforwardfoldpositive_body_steps fs_s_dst_cancel_iff_resultforwardfoldpositive_body_steps. ((((exists fs_h_dst_cancel_iff_resultforwardfoldpositive_body_steps_summand. fs_h_dst_cancel_iff_resultforwardfoldpositive_body_steps_summand + S (fs_a_dst_cancel_iff_resultforwardfoldpositive_body_steps) = S ((S (fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps)) * dst_positive_scale_cancel_iff_resultforwardfold)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldpositive_body_steps_summand. dst_positive_code_cancel_iff_resultforwardfold = fs_q_dst_cancel_iff_resultforwardfoldpositive_body_steps_summand * S ((S (fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps)) * dst_positive_scale_cancel_iff_resultforwardfold) + (fs_a_dst_cancel_iff_resultforwardfoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultforwardfoldpositive_body_steps_partial. fs_h_dst_cancel_iff_resultforwardfoldpositive_body_steps_partial + S (fs_r_dst_cancel_iff_resultforwardfoldpositive_body_steps) = S ((S (fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldpositive)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldpositive_body_steps_partial. fs_u_dst_cancel_iff_resultforwardfoldpositive = fs_q_dst_cancel_iff_resultforwardfoldpositive_body_steps_partial * S ((S (fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldpositive) + (fs_r_dst_cancel_iff_resultforwardfoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultforwardfoldpositive_body_steps_successor. fs_h_dst_cancel_iff_resultforwardfoldpositive_body_steps_successor + S (fs_s_dst_cancel_iff_resultforwardfoldpositive_body_steps) = S ((S (S fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldpositive)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldpositive_body_steps_successor. fs_u_dst_cancel_iff_resultforwardfoldpositive = fs_q_dst_cancel_iff_resultforwardfoldpositive_body_steps_successor * S ((S (S fs_i_dst_cancel_iff_resultforwardfoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldpositive) + (fs_s_dst_cancel_iff_resultforwardfoldpositive_body_steps))) /\ fs_s_dst_cancel_iff_resultforwardfoldpositive_body_steps = fs_r_dst_cancel_iff_resultforwardfoldpositive_body_steps + fs_a_dst_cancel_iff_resultforwardfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_cancel_iff_resultforwardfoldnegative fs_v_dst_cancel_iff_resultforwardfoldnegative. ((((exists fs_h_dst_cancel_iff_resultforwardfoldnegative_body_start. fs_h_dst_cancel_iff_resultforwardfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_iff_resultforwardfoldnegative)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldnegative_body_start. fs_u_dst_cancel_iff_resultforwardfoldnegative = fs_q_dst_cancel_iff_resultforwardfoldnegative_body_start * S ((S (0)) * fs_v_dst_cancel_iff_resultforwardfoldnegative) + (0))) /\ ((((exists fs_h_dst_cancel_iff_resultforwardfoldnegative_body_terminal. fs_h_dst_cancel_iff_resultforwardfoldnegative_body_terminal + S (dst_negative_sum_cancel_iff_resultforwardfold) = S ((S (S (n))) * fs_v_dst_cancel_iff_resultforwardfoldnegative)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldnegative_body_terminal. fs_u_dst_cancel_iff_resultforwardfoldnegative = fs_q_dst_cancel_iff_resultforwardfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_cancel_iff_resultforwardfoldnegative) + (dst_negative_sum_cancel_iff_resultforwardfold))) /\ forall fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps. (exists fs_lt_dst_cancel_iff_resultforwardfoldnegative_body_steps_bound. fs_lt_dst_cancel_iff_resultforwardfoldnegative_body_steps_bound + S fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps = S (n)) -> exists fs_a_dst_cancel_iff_resultforwardfoldnegative_body_steps fs_r_dst_cancel_iff_resultforwardfoldnegative_body_steps fs_s_dst_cancel_iff_resultforwardfoldnegative_body_steps. ((((exists fs_h_dst_cancel_iff_resultforwardfoldnegative_body_steps_summand. fs_h_dst_cancel_iff_resultforwardfoldnegative_body_steps_summand + S (fs_a_dst_cancel_iff_resultforwardfoldnegative_body_steps) = S ((S (fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps)) * dst_negative_scale_cancel_iff_resultforwardfold)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldnegative_body_steps_summand. dst_negative_code_cancel_iff_resultforwardfold = fs_q_dst_cancel_iff_resultforwardfoldnegative_body_steps_summand * S ((S (fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps)) * dst_negative_scale_cancel_iff_resultforwardfold) + (fs_a_dst_cancel_iff_resultforwardfoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultforwardfoldnegative_body_steps_partial. fs_h_dst_cancel_iff_resultforwardfoldnegative_body_steps_partial + S (fs_r_dst_cancel_iff_resultforwardfoldnegative_body_steps) = S ((S (fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldnegative)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldnegative_body_steps_partial. fs_u_dst_cancel_iff_resultforwardfoldnegative = fs_q_dst_cancel_iff_resultforwardfoldnegative_body_steps_partial * S ((S (fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldnegative) + (fs_r_dst_cancel_iff_resultforwardfoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultforwardfoldnegative_body_steps_successor. fs_h_dst_cancel_iff_resultforwardfoldnegative_body_steps_successor + S (fs_s_dst_cancel_iff_resultforwardfoldnegative_body_steps) = S ((S (S fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldnegative)) /\ exists fs_q_dst_cancel_iff_resultforwardfoldnegative_body_steps_successor. fs_u_dst_cancel_iff_resultforwardfoldnegative = fs_q_dst_cancel_iff_resultforwardfoldnegative_body_steps_successor * S ((S (S fs_i_dst_cancel_iff_resultforwardfoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultforwardfoldnegative) + (fs_s_dst_cancel_iff_resultforwardfoldnegative_body_steps))) /\ fs_s_dst_cancel_iff_resultforwardfoldnegative_body_steps = fs_r_dst_cancel_iff_resultforwardfoldnegative_body_steps + fs_a_dst_cancel_iff_resultforwardfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_cancel_iff_resultforwardfoldresult ge_balance_negative_cancel_iff_resultforwardfoldresult. (((((z) = 2 * (ge_balance_positive_cancel_iff_resultforwardfoldresult) /\ (ge_balance_negative_cancel_iff_resultforwardfoldresult) = 0) \/ exists ge_signed_half_cancel_iff_resultforwardfoldresultdecode. (((z) = 2 * ge_signed_half_cancel_iff_resultforwardfoldresultdecode + 1 /\ (ge_balance_positive_cancel_iff_resultforwardfoldresult) = 0) /\ (ge_balance_negative_cancel_iff_resultforwardfoldresult) = S ge_signed_half_cancel_iff_resultforwardfoldresultdecode))) /\ ((dst_positive_sum_cancel_iff_resultforwardfold) + ge_balance_negative_cancel_iff_resultforwardfoldresult = (dst_negative_sum_cancel_iff_resultforwardfold) + ge_balance_positive_cancel_iff_resultforwardfoldresult))))))))))))) -> (((n)=1 /\ (z)=2) \/ (~((n)=1) /\ (z)=0))) /\ ((((n)=1 /\ (z)=2) \/ (~((n)=1) /\ (z)=0)) -> (((~((n)=0)) /\ (exists dm_mask_table_cancel_iff_resultreverse. ((((exists dst_positive_code_cancel_iff_resultreversemasktable dst_positive_scale_cancel_iff_resultreversemasktable dst_negative_code_cancel_iff_resultreversemasktable dst_negative_scale_cancel_iff_resultreversemasktable. (((dm_mask_table_cancel_iff_resultreverse) = (((((dst_positive_code_cancel_iff_resultreversemasktable) + (dst_positive_scale_cancel_iff_resultreversemasktable)) * S ((dst_positive_code_cancel_iff_resultreversemasktable) + (dst_positive_scale_cancel_iff_resultreversemasktable)) + ((dst_positive_scale_cancel_iff_resultreversemasktable) + (dst_positive_scale_cancel_iff_resultreversemasktable))) + (((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) * S ((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) + ((dst_negative_scale_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)))) * S ((((dst_positive_code_cancel_iff_resultreversemasktable) + (dst_positive_scale_cancel_iff_resultreversemasktable)) * S ((dst_positive_code_cancel_iff_resultreversemasktable) + (dst_positive_scale_cancel_iff_resultreversemasktable)) + ((dst_positive_scale_cancel_iff_resultreversemasktable) + (dst_positive_scale_cancel_iff_resultreversemasktable))) + (((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) * S ((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) + ((dst_negative_scale_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)))) + ((((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) * S ((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) + ((dst_negative_scale_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable))) + (((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) * S ((dst_negative_code_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)) + ((dst_negative_scale_cancel_iff_resultreversemasktable) + (dst_negative_scale_cancel_iff_resultreversemasktable)))))) /\ (forall dst_index_cancel_iff_resultreversemasktable. (exists pvs_le_gap_cancel_iff_resultreversemasktabledomain. pvs_le_gap_cancel_iff_resultreversemasktabledomain + (dst_index_cancel_iff_resultreversemasktable) = (n)) -> exists dst_positive_cancel_iff_resultreversemasktable dst_negative_cancel_iff_resultreversemasktable dst_value_cancel_iff_resultreversemasktable. ((((exists ff_h_pvs_cancel_iff_resultreversemasktableentrypositive. ff_h_pvs_cancel_iff_resultreversemasktableentrypositive + S (dst_positive_cancel_iff_resultreversemasktable) = S ((S (dst_index_cancel_iff_resultreversemasktable)) * dst_positive_scale_cancel_iff_resultreversemasktable)) /\ exists ff_q_pvs_cancel_iff_resultreversemasktableentrypositive. dst_positive_code_cancel_iff_resultreversemasktable = ff_q_pvs_cancel_iff_resultreversemasktableentrypositive * S ((S (dst_index_cancel_iff_resultreversemasktable)) * dst_positive_scale_cancel_iff_resultreversemasktable) + (dst_positive_cancel_iff_resultreversemasktable))) /\ (((((exists ff_h_pvs_cancel_iff_resultreversemasktableentrynegative. ff_h_pvs_cancel_iff_resultreversemasktableentrynegative + S (dst_negative_cancel_iff_resultreversemasktable) = S ((S (dst_index_cancel_iff_resultreversemasktable)) * dst_negative_scale_cancel_iff_resultreversemasktable)) /\ exists ff_q_pvs_cancel_iff_resultreversemasktableentrynegative. dst_negative_code_cancel_iff_resultreversemasktable = ff_q_pvs_cancel_iff_resultreversemasktableentrynegative * S ((S (dst_index_cancel_iff_resultreversemasktable)) * dst_negative_scale_cancel_iff_resultreversemasktable) + (dst_negative_cancel_iff_resultreversemasktable))) /\ (exists ge_balance_positive_cancel_iff_resultreversemasktableentryvalue ge_balance_negative_cancel_iff_resultreversemasktableentryvalue. (((((dst_value_cancel_iff_resultreversemasktable) = 2 * (ge_balance_positive_cancel_iff_resultreversemasktableentryvalue) /\ (ge_balance_negative_cancel_iff_resultreversemasktableentryvalue) = 0) \/ exists ge_signed_half_cancel_iff_resultreversemasktableentryvaluedecode. (((dst_value_cancel_iff_resultreversemasktable) = 2 * ge_signed_half_cancel_iff_resultreversemasktableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_resultreversemasktableentryvalue) = 0) /\ (ge_balance_negative_cancel_iff_resultreversemasktableentryvalue) = S ge_signed_half_cancel_iff_resultreversemasktableentryvaluedecode))) /\ ((dst_positive_cancel_iff_resultreversemasktable) + ge_balance_negative_cancel_iff_resultreversemasktableentryvalue = (dst_negative_cancel_iff_resultreversemasktable) + ge_balance_positive_cancel_iff_resultreversemasktableentryvalue))))))))) /\ (forall dm_index_cancel_iff_resultreversemask dm_value_cancel_iff_resultreversemask. (exists pvs_le_gap_cancel_iff_resultreversemaskdomain. pvs_le_gap_cancel_iff_resultreversemaskdomain + (dm_index_cancel_iff_resultreversemask) = (n)) -> (exists dst_positive_code_cancel_iff_resultreversemasklookup dst_positive_scale_cancel_iff_resultreversemasklookup dst_negative_code_cancel_iff_resultreversemasklookup dst_negative_scale_cancel_iff_resultreversemasklookup dst_positive_cancel_iff_resultreversemasklookup dst_negative_cancel_iff_resultreversemasklookup. (((dm_mask_table_cancel_iff_resultreverse) = (((((dst_positive_code_cancel_iff_resultreversemasklookup) + (dst_positive_scale_cancel_iff_resultreversemasklookup)) * S ((dst_positive_code_cancel_iff_resultreversemasklookup) + (dst_positive_scale_cancel_iff_resultreversemasklookup)) + ((dst_positive_scale_cancel_iff_resultreversemasklookup) + (dst_positive_scale_cancel_iff_resultreversemasklookup))) + (((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) * S ((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) + ((dst_negative_scale_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)))) * S ((((dst_positive_code_cancel_iff_resultreversemasklookup) + (dst_positive_scale_cancel_iff_resultreversemasklookup)) * S ((dst_positive_code_cancel_iff_resultreversemasklookup) + (dst_positive_scale_cancel_iff_resultreversemasklookup)) + ((dst_positive_scale_cancel_iff_resultreversemasklookup) + (dst_positive_scale_cancel_iff_resultreversemasklookup))) + (((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) * S ((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) + ((dst_negative_scale_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)))) + ((((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) * S ((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) + ((dst_negative_scale_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup))) + (((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) * S ((dst_negative_code_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)) + ((dst_negative_scale_cancel_iff_resultreversemasklookup) + (dst_negative_scale_cancel_iff_resultreversemasklookup)))))) /\ (((((exists ff_h_pvs_cancel_iff_resultreversemasklookuppositive. ff_h_pvs_cancel_iff_resultreversemasklookuppositive + S (dst_positive_cancel_iff_resultreversemasklookup) = S ((S (dm_index_cancel_iff_resultreversemask)) * dst_positive_scale_cancel_iff_resultreversemasklookup)) /\ exists ff_q_pvs_cancel_iff_resultreversemasklookuppositive. dst_positive_code_cancel_iff_resultreversemasklookup = ff_q_pvs_cancel_iff_resultreversemasklookuppositive * S ((S (dm_index_cancel_iff_resultreversemask)) * dst_positive_scale_cancel_iff_resultreversemasklookup) + (dst_positive_cancel_iff_resultreversemasklookup))) /\ (((((exists ff_h_pvs_cancel_iff_resultreversemasklookupnegative. ff_h_pvs_cancel_iff_resultreversemasklookupnegative + S (dst_negative_cancel_iff_resultreversemasklookup) = S ((S (dm_index_cancel_iff_resultreversemask)) * dst_negative_scale_cancel_iff_resultreversemasklookup)) /\ exists ff_q_pvs_cancel_iff_resultreversemasklookupnegative. dst_negative_code_cancel_iff_resultreversemasklookup = ff_q_pvs_cancel_iff_resultreversemasklookupnegative * S ((S (dm_index_cancel_iff_resultreversemask)) * dst_negative_scale_cancel_iff_resultreversemasklookup) + (dst_negative_cancel_iff_resultreversemasklookup))) /\ (exists ge_balance_positive_cancel_iff_resultreversemasklookupvalue ge_balance_negative_cancel_iff_resultreversemasklookupvalue. (((((dm_value_cancel_iff_resultreversemask) = 2 * (ge_balance_positive_cancel_iff_resultreversemasklookupvalue) /\ (ge_balance_negative_cancel_iff_resultreversemasklookupvalue) = 0) \/ exists ge_signed_half_cancel_iff_resultreversemasklookupvaluedecode. (((dm_value_cancel_iff_resultreversemask) = 2 * ge_signed_half_cancel_iff_resultreversemasklookupvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_resultreversemasklookupvalue) = 0) /\ (ge_balance_negative_cancel_iff_resultreversemasklookupvalue) = S ge_signed_half_cancel_iff_resultreversemasklookupvaluedecode))) /\ ((dst_positive_cancel_iff_resultreversemasklookup) + ge_balance_negative_cancel_iff_resultreversemasklookupvalue = (dst_negative_cancel_iff_resultreversemasklookup) + ge_balance_positive_cancel_iff_resultreversemasklookupvalue))))))))) -> ((((~((dm_index_cancel_iff_resultreversemask)=0)) /\ (exists dm_quotient_cancel_iff_resultreversemaskentry. (((n)=(dm_index_cancel_iff_resultreversemask)*dm_quotient_cancel_iff_resultreversemaskentry) /\ (exists dst_positive_code_cancel_iff_resultreversemaskentryinput dst_positive_scale_cancel_iff_resultreversemaskentryinput dst_negative_code_cancel_iff_resultreversemaskentryinput dst_negative_scale_cancel_iff_resultreversemaskentryinput dst_positive_cancel_iff_resultreversemaskentryinput dst_negative_cancel_iff_resultreversemaskentryinput. (((M) = (((((dst_positive_code_cancel_iff_resultreversemaskentryinput) + (dst_positive_scale_cancel_iff_resultreversemaskentryinput)) * S ((dst_positive_code_cancel_iff_resultreversemaskentryinput) + (dst_positive_scale_cancel_iff_resultreversemaskentryinput)) + ((dst_positive_scale_cancel_iff_resultreversemaskentryinput) + (dst_positive_scale_cancel_iff_resultreversemaskentryinput))) + (((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) * S ((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) + ((dst_negative_scale_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)))) * S ((((dst_positive_code_cancel_iff_resultreversemaskentryinput) + (dst_positive_scale_cancel_iff_resultreversemaskentryinput)) * S ((dst_positive_code_cancel_iff_resultreversemaskentryinput) + (dst_positive_scale_cancel_iff_resultreversemaskentryinput)) + ((dst_positive_scale_cancel_iff_resultreversemaskentryinput) + (dst_positive_scale_cancel_iff_resultreversemaskentryinput))) + (((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) * S ((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) + ((dst_negative_scale_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)))) + ((((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) * S ((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) + ((dst_negative_scale_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput))) + (((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) * S ((dst_negative_code_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)) + ((dst_negative_scale_cancel_iff_resultreversemaskentryinput) + (dst_negative_scale_cancel_iff_resultreversemaskentryinput)))))) /\ (((((exists ff_h_pvs_cancel_iff_resultreversemaskentryinputpositive. ff_h_pvs_cancel_iff_resultreversemaskentryinputpositive + S (dst_positive_cancel_iff_resultreversemaskentryinput) = S ((S (dm_index_cancel_iff_resultreversemask)) * dst_positive_scale_cancel_iff_resultreversemaskentryinput)) /\ exists ff_q_pvs_cancel_iff_resultreversemaskentryinputpositive. dst_positive_code_cancel_iff_resultreversemaskentryinput = ff_q_pvs_cancel_iff_resultreversemaskentryinputpositive * S ((S (dm_index_cancel_iff_resultreversemask)) * dst_positive_scale_cancel_iff_resultreversemaskentryinput) + (dst_positive_cancel_iff_resultreversemaskentryinput))) /\ (((((exists ff_h_pvs_cancel_iff_resultreversemaskentryinputnegative. ff_h_pvs_cancel_iff_resultreversemaskentryinputnegative + S (dst_negative_cancel_iff_resultreversemaskentryinput) = S ((S (dm_index_cancel_iff_resultreversemask)) * dst_negative_scale_cancel_iff_resultreversemaskentryinput)) /\ exists ff_q_pvs_cancel_iff_resultreversemaskentryinputnegative. dst_negative_code_cancel_iff_resultreversemaskentryinput = ff_q_pvs_cancel_iff_resultreversemaskentryinputnegative * S ((S (dm_index_cancel_iff_resultreversemask)) * dst_negative_scale_cancel_iff_resultreversemaskentryinput) + (dst_negative_cancel_iff_resultreversemaskentryinput))) /\ (exists ge_balance_positive_cancel_iff_resultreversemaskentryinputvalue ge_balance_negative_cancel_iff_resultreversemaskentryinputvalue. (((((dm_value_cancel_iff_resultreversemask) = 2 * (ge_balance_positive_cancel_iff_resultreversemaskentryinputvalue) /\ (ge_balance_negative_cancel_iff_resultreversemaskentryinputvalue) = 0) \/ exists ge_signed_half_cancel_iff_resultreversemaskentryinputvaluedecode. (((dm_value_cancel_iff_resultreversemask) = 2 * ge_signed_half_cancel_iff_resultreversemaskentryinputvaluedecode + 1 /\ (ge_balance_positive_cancel_iff_resultreversemaskentryinputvalue) = 0) /\ (ge_balance_negative_cancel_iff_resultreversemaskentryinputvalue) = S ge_signed_half_cancel_iff_resultreversemaskentryinputvaluedecode))) /\ ((dst_positive_cancel_iff_resultreversemaskentryinput) + ge_balance_negative_cancel_iff_resultreversemaskentryinputvalue = (dst_negative_cancel_iff_resultreversemaskentryinput) + ge_balance_positive_cancel_iff_resultreversemaskentryinputvalue))))))))))))) \/ ((((dm_index_cancel_iff_resultreversemask)=0 \/ ~(exists pvs_factor_cancel_iff_resultreversemaskentrynondivisor. (n) = (dm_index_cancel_iff_resultreversemask) * pvs_factor_cancel_iff_resultreversemaskentrynondivisor)) /\ ((dm_value_cancel_iff_resultreversemask)=0))))))) /\ (exists dst_positive_code_cancel_iff_resultreversefold dst_positive_scale_cancel_iff_resultreversefold dst_negative_code_cancel_iff_resultreversefold dst_negative_scale_cancel_iff_resultreversefold dst_positive_sum_cancel_iff_resultreversefold dst_negative_sum_cancel_iff_resultreversefold. (((dm_mask_table_cancel_iff_resultreverse) = (((((dst_positive_code_cancel_iff_resultreversefold) + (dst_positive_scale_cancel_iff_resultreversefold)) * S ((dst_positive_code_cancel_iff_resultreversefold) + (dst_positive_scale_cancel_iff_resultreversefold)) + ((dst_positive_scale_cancel_iff_resultreversefold) + (dst_positive_scale_cancel_iff_resultreversefold))) + (((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) * S ((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) + ((dst_negative_scale_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)))) * S ((((dst_positive_code_cancel_iff_resultreversefold) + (dst_positive_scale_cancel_iff_resultreversefold)) * S ((dst_positive_code_cancel_iff_resultreversefold) + (dst_positive_scale_cancel_iff_resultreversefold)) + ((dst_positive_scale_cancel_iff_resultreversefold) + (dst_positive_scale_cancel_iff_resultreversefold))) + (((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) * S ((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) + ((dst_negative_scale_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)))) + ((((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) * S ((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) + ((dst_negative_scale_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold))) + (((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) * S ((dst_negative_code_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)) + ((dst_negative_scale_cancel_iff_resultreversefold) + (dst_negative_scale_cancel_iff_resultreversefold)))))) /\ (((exists fs_u_dst_cancel_iff_resultreversefoldpositive fs_v_dst_cancel_iff_resultreversefoldpositive. ((((exists fs_h_dst_cancel_iff_resultreversefoldpositive_body_start. fs_h_dst_cancel_iff_resultreversefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_iff_resultreversefoldpositive)) /\ exists fs_q_dst_cancel_iff_resultreversefoldpositive_body_start. fs_u_dst_cancel_iff_resultreversefoldpositive = fs_q_dst_cancel_iff_resultreversefoldpositive_body_start * S ((S (0)) * fs_v_dst_cancel_iff_resultreversefoldpositive) + (0))) /\ ((((exists fs_h_dst_cancel_iff_resultreversefoldpositive_body_terminal. fs_h_dst_cancel_iff_resultreversefoldpositive_body_terminal + S (dst_positive_sum_cancel_iff_resultreversefold) = S ((S (S (n))) * fs_v_dst_cancel_iff_resultreversefoldpositive)) /\ exists fs_q_dst_cancel_iff_resultreversefoldpositive_body_terminal. fs_u_dst_cancel_iff_resultreversefoldpositive = fs_q_dst_cancel_iff_resultreversefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_cancel_iff_resultreversefoldpositive) + (dst_positive_sum_cancel_iff_resultreversefold))) /\ forall fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps. (exists fs_lt_dst_cancel_iff_resultreversefoldpositive_body_steps_bound. fs_lt_dst_cancel_iff_resultreversefoldpositive_body_steps_bound + S fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps = S (n)) -> exists fs_a_dst_cancel_iff_resultreversefoldpositive_body_steps fs_r_dst_cancel_iff_resultreversefoldpositive_body_steps fs_s_dst_cancel_iff_resultreversefoldpositive_body_steps. ((((exists fs_h_dst_cancel_iff_resultreversefoldpositive_body_steps_summand. fs_h_dst_cancel_iff_resultreversefoldpositive_body_steps_summand + S (fs_a_dst_cancel_iff_resultreversefoldpositive_body_steps) = S ((S (fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps)) * dst_positive_scale_cancel_iff_resultreversefold)) /\ exists fs_q_dst_cancel_iff_resultreversefoldpositive_body_steps_summand. dst_positive_code_cancel_iff_resultreversefold = fs_q_dst_cancel_iff_resultreversefoldpositive_body_steps_summand * S ((S (fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps)) * dst_positive_scale_cancel_iff_resultreversefold) + (fs_a_dst_cancel_iff_resultreversefoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultreversefoldpositive_body_steps_partial. fs_h_dst_cancel_iff_resultreversefoldpositive_body_steps_partial + S (fs_r_dst_cancel_iff_resultreversefoldpositive_body_steps) = S ((S (fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldpositive)) /\ exists fs_q_dst_cancel_iff_resultreversefoldpositive_body_steps_partial. fs_u_dst_cancel_iff_resultreversefoldpositive = fs_q_dst_cancel_iff_resultreversefoldpositive_body_steps_partial * S ((S (fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldpositive) + (fs_r_dst_cancel_iff_resultreversefoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultreversefoldpositive_body_steps_successor. fs_h_dst_cancel_iff_resultreversefoldpositive_body_steps_successor + S (fs_s_dst_cancel_iff_resultreversefoldpositive_body_steps) = S ((S (S fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldpositive)) /\ exists fs_q_dst_cancel_iff_resultreversefoldpositive_body_steps_successor. fs_u_dst_cancel_iff_resultreversefoldpositive = fs_q_dst_cancel_iff_resultreversefoldpositive_body_steps_successor * S ((S (S fs_i_dst_cancel_iff_resultreversefoldpositive_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldpositive) + (fs_s_dst_cancel_iff_resultreversefoldpositive_body_steps))) /\ fs_s_dst_cancel_iff_resultreversefoldpositive_body_steps = fs_r_dst_cancel_iff_resultreversefoldpositive_body_steps + fs_a_dst_cancel_iff_resultreversefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_cancel_iff_resultreversefoldnegative fs_v_dst_cancel_iff_resultreversefoldnegative. ((((exists fs_h_dst_cancel_iff_resultreversefoldnegative_body_start. fs_h_dst_cancel_iff_resultreversefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_iff_resultreversefoldnegative)) /\ exists fs_q_dst_cancel_iff_resultreversefoldnegative_body_start. fs_u_dst_cancel_iff_resultreversefoldnegative = fs_q_dst_cancel_iff_resultreversefoldnegative_body_start * S ((S (0)) * fs_v_dst_cancel_iff_resultreversefoldnegative) + (0))) /\ ((((exists fs_h_dst_cancel_iff_resultreversefoldnegative_body_terminal. fs_h_dst_cancel_iff_resultreversefoldnegative_body_terminal + S (dst_negative_sum_cancel_iff_resultreversefold) = S ((S (S (n))) * fs_v_dst_cancel_iff_resultreversefoldnegative)) /\ exists fs_q_dst_cancel_iff_resultreversefoldnegative_body_terminal. fs_u_dst_cancel_iff_resultreversefoldnegative = fs_q_dst_cancel_iff_resultreversefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_cancel_iff_resultreversefoldnegative) + (dst_negative_sum_cancel_iff_resultreversefold))) /\ forall fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps. (exists fs_lt_dst_cancel_iff_resultreversefoldnegative_body_steps_bound. fs_lt_dst_cancel_iff_resultreversefoldnegative_body_steps_bound + S fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps = S (n)) -> exists fs_a_dst_cancel_iff_resultreversefoldnegative_body_steps fs_r_dst_cancel_iff_resultreversefoldnegative_body_steps fs_s_dst_cancel_iff_resultreversefoldnegative_body_steps. ((((exists fs_h_dst_cancel_iff_resultreversefoldnegative_body_steps_summand. fs_h_dst_cancel_iff_resultreversefoldnegative_body_steps_summand + S (fs_a_dst_cancel_iff_resultreversefoldnegative_body_steps) = S ((S (fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps)) * dst_negative_scale_cancel_iff_resultreversefold)) /\ exists fs_q_dst_cancel_iff_resultreversefoldnegative_body_steps_summand. dst_negative_code_cancel_iff_resultreversefold = fs_q_dst_cancel_iff_resultreversefoldnegative_body_steps_summand * S ((S (fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps)) * dst_negative_scale_cancel_iff_resultreversefold) + (fs_a_dst_cancel_iff_resultreversefoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultreversefoldnegative_body_steps_partial. fs_h_dst_cancel_iff_resultreversefoldnegative_body_steps_partial + S (fs_r_dst_cancel_iff_resultreversefoldnegative_body_steps) = S ((S (fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldnegative)) /\ exists fs_q_dst_cancel_iff_resultreversefoldnegative_body_steps_partial. fs_u_dst_cancel_iff_resultreversefoldnegative = fs_q_dst_cancel_iff_resultreversefoldnegative_body_steps_partial * S ((S (fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldnegative) + (fs_r_dst_cancel_iff_resultreversefoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_iff_resultreversefoldnegative_body_steps_successor. fs_h_dst_cancel_iff_resultreversefoldnegative_body_steps_successor + S (fs_s_dst_cancel_iff_resultreversefoldnegative_body_steps) = S ((S (S fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldnegative)) /\ exists fs_q_dst_cancel_iff_resultreversefoldnegative_body_steps_successor. fs_u_dst_cancel_iff_resultreversefoldnegative = fs_q_dst_cancel_iff_resultreversefoldnegative_body_steps_successor * S ((S (S fs_i_dst_cancel_iff_resultreversefoldnegative_body_steps)) * fs_v_dst_cancel_iff_resultreversefoldnegative) + (fs_s_dst_cancel_iff_resultreversefoldnegative_body_steps))) /\ fs_s_dst_cancel_iff_resultreversefoldnegative_body_steps = fs_r_dst_cancel_iff_resultreversefoldnegative_body_steps + fs_a_dst_cancel_iff_resultreversefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_cancel_iff_resultreversefoldresult ge_balance_negative_cancel_iff_resultreversefoldresult. (((((z) = 2 * (ge_balance_positive_cancel_iff_resultreversefoldresult) /\ (ge_balance_negative_cancel_iff_resultreversefoldresult) = 0) \/ exists ge_signed_half_cancel_iff_resultreversefoldresultdecode. (((z) = 2 * ge_signed_half_cancel_iff_resultreversefoldresultdecode + 1 /\ (ge_balance_positive_cancel_iff_resultreversefoldresult) = 0) /\ (ge_balance_negative_cancel_iff_resultreversefoldresult) = S ge_signed_half_cancel_iff_resultreversefoldresultdecode))) /\ ((dst_positive_sum_cancel_iff_resultreversefold) + ge_balance_negative_cancel_iff_resultreversefoldresult = (dst_negative_sum_cancel_iff_resultreversefold) + ge_balance_positive_cancel_iff_resultreversefoldresult))))))))))))))))