mobius_divisor_sum_cancellation_exists

forall n. ~(n=0) -> exists M z. (((((exists dst_positive_code_cancel_exists_tabletable dst_positive_scale_cancel_exists_tabletable dst_negative_code_cancel_exists_tabletable dst_negative_scale_cancel_exists_tabletable. (((M) = (((((dst_positive_code_cancel_exists_tabletable) + (dst_positive_scale_cancel_exists_tabletable)) * S ((dst_positive_code_cancel_exists_tabletable) + (dst_positive_scale_cancel_exists_tabletable)) + ((dst_positive_scale_cancel_exists_tabletable) + (dst_positive_scale_cancel_exists_tabletable))) + (((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) * S ((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) + ((dst_negative_scale_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)))) * S ((((dst_positive_code_cancel_exists_tabletable) + (dst_positive_scale_cancel_exists_tabletable)) * S ((dst_positive_code_cancel_exists_tabletable) + (dst_positive_scale_cancel_exists_tabletable)) + ((dst_positive_scale_cancel_exists_tabletable) + (dst_positive_scale_cancel_exists_tabletable))) + (((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) * S ((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) + ((dst_negative_scale_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)))) + ((((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) * S ((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) + ((dst_negative_scale_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable))) + (((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) * S ((dst_negative_code_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)) + ((dst_negative_scale_cancel_exists_tabletable) + (dst_negative_scale_cancel_exists_tabletable)))))) /\ (forall dst_index_cancel_exists_tabletable. (exists pvs_le_gap_cancel_exists_tabletabledomain. pvs_le_gap_cancel_exists_tabletabledomain + (dst_index_cancel_exists_tabletable) = (n)) -> exists dst_positive_cancel_exists_tabletable dst_negative_cancel_exists_tabletable dst_value_cancel_exists_tabletable. ((((exists ff_h_pvs_cancel_exists_tabletableentrypositive. ff_h_pvs_cancel_exists_tabletableentrypositive + S (dst_positive_cancel_exists_tabletable) = S ((S (dst_index_cancel_exists_tabletable)) * dst_positive_scale_cancel_exists_tabletable)) /\ exists ff_q_pvs_cancel_exists_tabletableentrypositive. dst_positive_code_cancel_exists_tabletable = ff_q_pvs_cancel_exists_tabletableentrypositive * S ((S (dst_index_cancel_exists_tabletable)) * dst_positive_scale_cancel_exists_tabletable) + (dst_positive_cancel_exists_tabletable))) /\ (((((exists ff_h_pvs_cancel_exists_tabletableentrynegative. ff_h_pvs_cancel_exists_tabletableentrynegative + S (dst_negative_cancel_exists_tabletable) = S ((S (dst_index_cancel_exists_tabletable)) * dst_negative_scale_cancel_exists_tabletable)) /\ exists ff_q_pvs_cancel_exists_tabletableentrynegative. dst_negative_code_cancel_exists_tabletable = ff_q_pvs_cancel_exists_tabletableentrynegative * S ((S (dst_index_cancel_exists_tabletable)) * dst_negative_scale_cancel_exists_tabletable) + (dst_negative_cancel_exists_tabletable))) /\ (exists ge_balance_positive_cancel_exists_tabletableentryvalue ge_balance_negative_cancel_exists_tabletableentryvalue. (((((dst_value_cancel_exists_tabletable) = 2 * (ge_balance_positive_cancel_exists_tabletableentryvalue) /\ (ge_balance_negative_cancel_exists_tabletableentryvalue) = 0) \/ exists ge_signed_half_cancel_exists_tabletableentryvaluedecode. (((dst_value_cancel_exists_tabletable) = 2 * ge_signed_half_cancel_exists_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_exists_tabletableentryvalue) = 0) /\ (ge_balance_negative_cancel_exists_tabletableentryvalue) = S ge_signed_half_cancel_exists_tabletableentryvaluedecode))) /\ ((dst_positive_cancel_exists_tabletable) + ge_balance_negative_cancel_exists_tabletableentryvalue = (dst_negative_cancel_exists_tabletable) + ge_balance_positive_cancel_exists_tabletableentryvalue))))))))) /\ (((exists dst_positive_code_cancel_exists_tablezero dst_positive_scale_cancel_exists_tablezero dst_negative_code_cancel_exists_tablezero dst_negative_scale_cancel_exists_tablezero dst_positive_cancel_exists_tablezero dst_negative_cancel_exists_tablezero. (((M) = (((((dst_positive_code_cancel_exists_tablezero) + (dst_positive_scale_cancel_exists_tablezero)) * S ((dst_positive_code_cancel_exists_tablezero) + (dst_positive_scale_cancel_exists_tablezero)) + ((dst_positive_scale_cancel_exists_tablezero) + (dst_positive_scale_cancel_exists_tablezero))) + (((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) * S ((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) + ((dst_negative_scale_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)))) * S ((((dst_positive_code_cancel_exists_tablezero) + (dst_positive_scale_cancel_exists_tablezero)) * S ((dst_positive_code_cancel_exists_tablezero) + (dst_positive_scale_cancel_exists_tablezero)) + ((dst_positive_scale_cancel_exists_tablezero) + (dst_positive_scale_cancel_exists_tablezero))) + (((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) * S ((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) + ((dst_negative_scale_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)))) + ((((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) * S ((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) + ((dst_negative_scale_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero))) + (((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) * S ((dst_negative_code_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)) + ((dst_negative_scale_cancel_exists_tablezero) + (dst_negative_scale_cancel_exists_tablezero)))))) /\ (((((exists ff_h_pvs_cancel_exists_tablezeropositive. ff_h_pvs_cancel_exists_tablezeropositive + S (dst_positive_cancel_exists_tablezero) = S ((S (0)) * dst_positive_scale_cancel_exists_tablezero)) /\ exists ff_q_pvs_cancel_exists_tablezeropositive. dst_positive_code_cancel_exists_tablezero = ff_q_pvs_cancel_exists_tablezeropositive * S ((S (0)) * dst_positive_scale_cancel_exists_tablezero) + (dst_positive_cancel_exists_tablezero))) /\ (((((exists ff_h_pvs_cancel_exists_tablezeronegative. ff_h_pvs_cancel_exists_tablezeronegative + S (dst_negative_cancel_exists_tablezero) = S ((S (0)) * dst_negative_scale_cancel_exists_tablezero)) /\ exists ff_q_pvs_cancel_exists_tablezeronegative. dst_negative_code_cancel_exists_tablezero = ff_q_pvs_cancel_exists_tablezeronegative * S ((S (0)) * dst_negative_scale_cancel_exists_tablezero) + (dst_negative_cancel_exists_tablezero))) /\ (exists ge_balance_positive_cancel_exists_tablezerovalue ge_balance_negative_cancel_exists_tablezerovalue. (((((0) = 2 * (ge_balance_positive_cancel_exists_tablezerovalue) /\ (ge_balance_negative_cancel_exists_tablezerovalue) = 0) \/ exists ge_signed_half_cancel_exists_tablezerovaluedecode. (((0) = 2 * ge_signed_half_cancel_exists_tablezerovaluedecode + 1 /\ (ge_balance_positive_cancel_exists_tablezerovalue) = 0) /\ (ge_balance_negative_cancel_exists_tablezerovalue) = S ge_signed_half_cancel_exists_tablezerovaluedecode))) /\ ((dst_positive_cancel_exists_tablezero) + ge_balance_negative_cancel_exists_tablezerovalue = (dst_negative_cancel_exists_tablezero) + ge_balance_positive_cancel_exists_tablezerovalue))))))))) /\ (forall mt_index_cancel_exists_table mt_value_cancel_exists_table. ~(mt_index_cancel_exists_table=0) -> (exists pvs_le_gap_cancel_exists_tabledomain. pvs_le_gap_cancel_exists_tabledomain + (mt_index_cancel_exists_table) = (n)) -> (exists dst_positive_code_cancel_exists_tableentry dst_positive_scale_cancel_exists_tableentry dst_negative_code_cancel_exists_tableentry dst_negative_scale_cancel_exists_tableentry dst_positive_cancel_exists_tableentry dst_negative_cancel_exists_tableentry. (((M) = (((((dst_positive_code_cancel_exists_tableentry) + (dst_positive_scale_cancel_exists_tableentry)) * S ((dst_positive_code_cancel_exists_tableentry) + (dst_positive_scale_cancel_exists_tableentry)) + ((dst_positive_scale_cancel_exists_tableentry) + (dst_positive_scale_cancel_exists_tableentry))) + (((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) * S ((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) + ((dst_negative_scale_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)))) * S ((((dst_positive_code_cancel_exists_tableentry) + (dst_positive_scale_cancel_exists_tableentry)) * S ((dst_positive_code_cancel_exists_tableentry) + (dst_positive_scale_cancel_exists_tableentry)) + ((dst_positive_scale_cancel_exists_tableentry) + (dst_positive_scale_cancel_exists_tableentry))) + (((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) * S ((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) + ((dst_negative_scale_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)))) + ((((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) * S ((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) + ((dst_negative_scale_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry))) + (((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) * S ((dst_negative_code_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)) + ((dst_negative_scale_cancel_exists_tableentry) + (dst_negative_scale_cancel_exists_tableentry)))))) /\ (((((exists ff_h_pvs_cancel_exists_tableentrypositive. ff_h_pvs_cancel_exists_tableentrypositive + S (dst_positive_cancel_exists_tableentry) = S ((S (mt_index_cancel_exists_table)) * dst_positive_scale_cancel_exists_tableentry)) /\ exists ff_q_pvs_cancel_exists_tableentrypositive. dst_positive_code_cancel_exists_tableentry = ff_q_pvs_cancel_exists_tableentrypositive * S ((S (mt_index_cancel_exists_table)) * dst_positive_scale_cancel_exists_tableentry) + (dst_positive_cancel_exists_tableentry))) /\ (((((exists ff_h_pvs_cancel_exists_tableentrynegative. ff_h_pvs_cancel_exists_tableentrynegative + S (dst_negative_cancel_exists_tableentry) = S ((S (mt_index_cancel_exists_table)) * dst_negative_scale_cancel_exists_tableentry)) /\ exists ff_q_pvs_cancel_exists_tableentrynegative. dst_negative_code_cancel_exists_tableentry = ff_q_pvs_cancel_exists_tableentrynegative * S ((S (mt_index_cancel_exists_table)) * dst_negative_scale_cancel_exists_tableentry) + (dst_negative_cancel_exists_tableentry))) /\ (exists ge_balance_positive_cancel_exists_tableentryvalue ge_balance_negative_cancel_exists_tableentryvalue. (((((mt_value_cancel_exists_table) = 2 * (ge_balance_positive_cancel_exists_tableentryvalue) /\ (ge_balance_negative_cancel_exists_tableentryvalue) = 0) \/ exists ge_signed_half_cancel_exists_tableentryvaluedecode. (((mt_value_cancel_exists_table) = 2 * ge_signed_half_cancel_exists_tableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_exists_tableentryvalue) = 0) /\ (ge_balance_negative_cancel_exists_tableentryvalue) = S ge_signed_half_cancel_exists_tableentryvaluedecode))) /\ ((dst_positive_cancel_exists_tableentry) + ge_balance_negative_cancel_exists_tableentryvalue = (dst_negative_cancel_exists_tableentry) + ge_balance_positive_cancel_exists_tableentryvalue))))))))) -> (((~((mt_index_cancel_exists_table) = 0)) /\ ((((exists mv_square_prime_cancel_exists_tablevaluesquare. ((~((mv_square_prime_cancel_exists_tablevaluesquare) = 1) /\ forall pvs_left_cancel_exists_tablevaluesquareprime pvs_right_cancel_exists_tablevaluesquareprime. (mv_square_prime_cancel_exists_tablevaluesquare) = pvs_left_cancel_exists_tablevaluesquareprime * pvs_right_cancel_exists_tablevaluesquareprime -> pvs_left_cancel_exists_tablevaluesquareprime = 1 \/ pvs_right_cancel_exists_tablevaluesquareprime = 1) /\ (exists pvs_factor_cancel_exists_tablevaluesquaredivisor. (mt_index_cancel_exists_table) = (mv_square_prime_cancel_exists_tablevaluesquare * mv_square_prime_cancel_exists_tablevaluesquare) * pvs_factor_cancel_exists_tablevaluesquaredivisor))) /\ ((mt_value_cancel_exists_table) = 0))) \/ (((((~((mt_index_cancel_exists_table) = 0)) /\ (forall sfd_prime_cancel_exists_tablevaluesquarefree. (~((sfd_prime_cancel_exists_tablevaluesquarefree) = 1) /\ forall pvs_left_cancel_exists_tablevaluesquarefreedomain pvs_right_cancel_exists_tablevaluesquarefreedomain. (sfd_prime_cancel_exists_tablevaluesquarefree) = pvs_left_cancel_exists_tablevaluesquarefreedomain * pvs_right_cancel_exists_tablevaluesquarefreedomain -> pvs_left_cancel_exists_tablevaluesquarefreedomain = 1 \/ pvs_right_cancel_exists_tablevaluesquarefreedomain = 1) -> (exists pvs_le_gap_cancel_exists_tablevaluesquarefreebound. pvs_le_gap_cancel_exists_tablevaluesquarefreebound + (sfd_prime_cancel_exists_tablevaluesquarefree) = (mt_index_cancel_exists_table)) -> ~(exists pvs_factor_cancel_exists_tablevaluesquarefreesquare. (mt_index_cancel_exists_table) = (sfd_prime_cancel_exists_tablevaluesquarefree * sfd_prime_cancel_exists_tablevaluesquarefree) * pvs_factor_cancel_exists_tablevaluesquarefreesquare)))) /\ (exists mv_factor_code_cancel_exists_tablevaluefactors mv_factor_scale_cancel_exists_tablevaluefactors mv_factor_count_cancel_exists_tablevaluefactors. (((~(mt_index_cancel_exists_table = 0) /\ ((exists ff_u_fsat_cancel_exists_tablevaluefactorsfactorization_product ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_start. ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_start. ff_u_fsat_cancel_exists_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_terminal. ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_terminal + S (mt_index_cancel_exists_table) = S ((S (mv_factor_count_cancel_exists_tablevaluefactors)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_terminal. ff_u_fsat_cancel_exists_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_cancel_exists_tablevaluefactors)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product) + (mt_index_cancel_exists_table))) /\ forall ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product. (exists ff_lt_fsat_cancel_exists_tablevaluefactorsfactorization_product_bound. ff_lt_fsat_cancel_exists_tablevaluefactorsfactorization_product_bound + S ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product = mv_factor_count_cancel_exists_tablevaluefactors) -> exists ff_p_fsat_cancel_exists_tablevaluefactorsfactorization_product ff_r_fsat_cancel_exists_tablevaluefactorsfactorization_product ff_s_fsat_cancel_exists_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_factor. ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_factor + S (ff_p_fsat_cancel_exists_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product)) * mv_factor_scale_cancel_exists_tablevaluefactors)) /\ exists ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_factor. mv_factor_code_cancel_exists_tablevaluefactors = ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product)) * mv_factor_scale_cancel_exists_tablevaluefactors) + (ff_p_fsat_cancel_exists_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_partial. ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_partial + S (ff_r_fsat_cancel_exists_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_partial. ff_u_fsat_cancel_exists_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product) + (ff_r_fsat_cancel_exists_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_successor. ff_h_fsat_cancel_exists_tablevaluefactorsfactorization_product_successor + S (ff_s_fsat_cancel_exists_tablevaluefactorsfactorization_product) = S ((S (S ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_successor. ff_u_fsat_cancel_exists_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_exists_tablevaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_cancel_exists_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_exists_tablevaluefactorsfactorization_product) + (ff_s_fsat_cancel_exists_tablevaluefactorsfactorization_product))) /\ ff_s_fsat_cancel_exists_tablevaluefactorsfactorization_product = ff_r_fsat_cancel_exists_tablevaluefactorsfactorization_product * ff_p_fsat_cancel_exists_tablevaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_cancel_exists_tablevaluefactorsfactorization_primes. (exists ftsf_gap_fsat_cancel_exists_tablevaluefactorsfactorization_primes_bound. ftsf_gap_fsat_cancel_exists_tablevaluefactorsfactorization_primes_bound + S ftsf_index_fsat_cancel_exists_tablevaluefactorsfactorization_primes = (mv_factor_count_cancel_exists_tablevaluefactors)) -> exists ftsf_factor_fsat_cancel_exists_tablevaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_cancel_exists_tablevaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_cancel_exists_tablevaluefactorsfactorization_primes)) * mv_factor_scale_cancel_exists_tablevaluefactors)) /\ exists ff_q_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_entry. mv_factor_code_cancel_exists_tablevaluefactors = ff_q_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_cancel_exists_tablevaluefactorsfactorization_primes)) * mv_factor_scale_cancel_exists_tablevaluefactors) + (ftsf_factor_fsat_cancel_exists_tablevaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_cancel_exists_tablevaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_prime. ftsf_factor_fsat_cancel_exists_tablevaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_cancel_exists_tablevaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_cancel_exists_tablevaluefactorsparityeven. (mv_factor_count_cancel_exists_tablevaluefactors) = 2 * mv_even_half_cancel_exists_tablevaluefactorsparityeven) /\ ((mt_value_cancel_exists_table) = 2))) \/ (((exists mv_odd_half_cancel_exists_tablevaluefactorsparityodd. (mv_factor_count_cancel_exists_tablevaluefactors) = 2 * mv_odd_half_cancel_exists_tablevaluefactorsparityodd + 1) /\ ((mt_value_cancel_exists_table) = 1)))))))))))))))) /\ (((((~((n)=0)) /\ (exists dm_mask_table_cancel_exists_sum. ((((exists dst_positive_code_cancel_exists_summasktable dst_positive_scale_cancel_exists_summasktable dst_negative_code_cancel_exists_summasktable dst_negative_scale_cancel_exists_summasktable. (((dm_mask_table_cancel_exists_sum) = (((((dst_positive_code_cancel_exists_summasktable) + (dst_positive_scale_cancel_exists_summasktable)) * S ((dst_positive_code_cancel_exists_summasktable) + (dst_positive_scale_cancel_exists_summasktable)) + ((dst_positive_scale_cancel_exists_summasktable) + (dst_positive_scale_cancel_exists_summasktable))) + (((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) * S ((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) + ((dst_negative_scale_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)))) * S ((((dst_positive_code_cancel_exists_summasktable) + (dst_positive_scale_cancel_exists_summasktable)) * S ((dst_positive_code_cancel_exists_summasktable) + (dst_positive_scale_cancel_exists_summasktable)) + ((dst_positive_scale_cancel_exists_summasktable) + (dst_positive_scale_cancel_exists_summasktable))) + (((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) * S ((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) + ((dst_negative_scale_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)))) + ((((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) * S ((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) + ((dst_negative_scale_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable))) + (((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) * S ((dst_negative_code_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)) + ((dst_negative_scale_cancel_exists_summasktable) + (dst_negative_scale_cancel_exists_summasktable)))))) /\ (forall dst_index_cancel_exists_summasktable. (exists pvs_le_gap_cancel_exists_summasktabledomain. pvs_le_gap_cancel_exists_summasktabledomain + (dst_index_cancel_exists_summasktable) = (n)) -> exists dst_positive_cancel_exists_summasktable dst_negative_cancel_exists_summasktable dst_value_cancel_exists_summasktable. ((((exists ff_h_pvs_cancel_exists_summasktableentrypositive. ff_h_pvs_cancel_exists_summasktableentrypositive + S (dst_positive_cancel_exists_summasktable) = S ((S (dst_index_cancel_exists_summasktable)) * dst_positive_scale_cancel_exists_summasktable)) /\ exists ff_q_pvs_cancel_exists_summasktableentrypositive. dst_positive_code_cancel_exists_summasktable = ff_q_pvs_cancel_exists_summasktableentrypositive * S ((S (dst_index_cancel_exists_summasktable)) * dst_positive_scale_cancel_exists_summasktable) + (dst_positive_cancel_exists_summasktable))) /\ (((((exists ff_h_pvs_cancel_exists_summasktableentrynegative. ff_h_pvs_cancel_exists_summasktableentrynegative + S (dst_negative_cancel_exists_summasktable) = S ((S (dst_index_cancel_exists_summasktable)) * dst_negative_scale_cancel_exists_summasktable)) /\ exists ff_q_pvs_cancel_exists_summasktableentrynegative. dst_negative_code_cancel_exists_summasktable = ff_q_pvs_cancel_exists_summasktableentrynegative * S ((S (dst_index_cancel_exists_summasktable)) * dst_negative_scale_cancel_exists_summasktable) + (dst_negative_cancel_exists_summasktable))) /\ (exists ge_balance_positive_cancel_exists_summasktableentryvalue ge_balance_negative_cancel_exists_summasktableentryvalue. (((((dst_value_cancel_exists_summasktable) = 2 * (ge_balance_positive_cancel_exists_summasktableentryvalue) /\ (ge_balance_negative_cancel_exists_summasktableentryvalue) = 0) \/ exists ge_signed_half_cancel_exists_summasktableentryvaluedecode. (((dst_value_cancel_exists_summasktable) = 2 * ge_signed_half_cancel_exists_summasktableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_exists_summasktableentryvalue) = 0) /\ (ge_balance_negative_cancel_exists_summasktableentryvalue) = S ge_signed_half_cancel_exists_summasktableentryvaluedecode))) /\ ((dst_positive_cancel_exists_summasktable) + ge_balance_negative_cancel_exists_summasktableentryvalue = (dst_negative_cancel_exists_summasktable) + ge_balance_positive_cancel_exists_summasktableentryvalue))))))))) /\ (forall dm_index_cancel_exists_summask dm_value_cancel_exists_summask. (exists pvs_le_gap_cancel_exists_summaskdomain. pvs_le_gap_cancel_exists_summaskdomain + (dm_index_cancel_exists_summask) = (n)) -> (exists dst_positive_code_cancel_exists_summasklookup dst_positive_scale_cancel_exists_summasklookup dst_negative_code_cancel_exists_summasklookup dst_negative_scale_cancel_exists_summasklookup dst_positive_cancel_exists_summasklookup dst_negative_cancel_exists_summasklookup. (((dm_mask_table_cancel_exists_sum) = (((((dst_positive_code_cancel_exists_summasklookup) + (dst_positive_scale_cancel_exists_summasklookup)) * S ((dst_positive_code_cancel_exists_summasklookup) + (dst_positive_scale_cancel_exists_summasklookup)) + ((dst_positive_scale_cancel_exists_summasklookup) + (dst_positive_scale_cancel_exists_summasklookup))) + (((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) * S ((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) + ((dst_negative_scale_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)))) * S ((((dst_positive_code_cancel_exists_summasklookup) + (dst_positive_scale_cancel_exists_summasklookup)) * S ((dst_positive_code_cancel_exists_summasklookup) + (dst_positive_scale_cancel_exists_summasklookup)) + ((dst_positive_scale_cancel_exists_summasklookup) + (dst_positive_scale_cancel_exists_summasklookup))) + (((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) * S ((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) + ((dst_negative_scale_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)))) + ((((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) * S ((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) + ((dst_negative_scale_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup))) + (((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) * S ((dst_negative_code_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)) + ((dst_negative_scale_cancel_exists_summasklookup) + (dst_negative_scale_cancel_exists_summasklookup)))))) /\ (((((exists ff_h_pvs_cancel_exists_summasklookuppositive. ff_h_pvs_cancel_exists_summasklookuppositive + S (dst_positive_cancel_exists_summasklookup) = S ((S (dm_index_cancel_exists_summask)) * dst_positive_scale_cancel_exists_summasklookup)) /\ exists ff_q_pvs_cancel_exists_summasklookuppositive. dst_positive_code_cancel_exists_summasklookup = ff_q_pvs_cancel_exists_summasklookuppositive * S ((S (dm_index_cancel_exists_summask)) * dst_positive_scale_cancel_exists_summasklookup) + (dst_positive_cancel_exists_summasklookup))) /\ (((((exists ff_h_pvs_cancel_exists_summasklookupnegative. ff_h_pvs_cancel_exists_summasklookupnegative + S (dst_negative_cancel_exists_summasklookup) = S ((S (dm_index_cancel_exists_summask)) * dst_negative_scale_cancel_exists_summasklookup)) /\ exists ff_q_pvs_cancel_exists_summasklookupnegative. dst_negative_code_cancel_exists_summasklookup = ff_q_pvs_cancel_exists_summasklookupnegative * S ((S (dm_index_cancel_exists_summask)) * dst_negative_scale_cancel_exists_summasklookup) + (dst_negative_cancel_exists_summasklookup))) /\ (exists ge_balance_positive_cancel_exists_summasklookupvalue ge_balance_negative_cancel_exists_summasklookupvalue. (((((dm_value_cancel_exists_summask) = 2 * (ge_balance_positive_cancel_exists_summasklookupvalue) /\ (ge_balance_negative_cancel_exists_summasklookupvalue) = 0) \/ exists ge_signed_half_cancel_exists_summasklookupvaluedecode. (((dm_value_cancel_exists_summask) = 2 * ge_signed_half_cancel_exists_summasklookupvaluedecode + 1 /\ (ge_balance_positive_cancel_exists_summasklookupvalue) = 0) /\ (ge_balance_negative_cancel_exists_summasklookupvalue) = S ge_signed_half_cancel_exists_summasklookupvaluedecode))) /\ ((dst_positive_cancel_exists_summasklookup) + ge_balance_negative_cancel_exists_summasklookupvalue = (dst_negative_cancel_exists_summasklookup) + ge_balance_positive_cancel_exists_summasklookupvalue))))))))) -> ((((~((dm_index_cancel_exists_summask)=0)) /\ (exists dm_quotient_cancel_exists_summaskentry. (((n)=(dm_index_cancel_exists_summask)*dm_quotient_cancel_exists_summaskentry) /\ (exists dst_positive_code_cancel_exists_summaskentryinput dst_positive_scale_cancel_exists_summaskentryinput dst_negative_code_cancel_exists_summaskentryinput dst_negative_scale_cancel_exists_summaskentryinput dst_positive_cancel_exists_summaskentryinput dst_negative_cancel_exists_summaskentryinput. (((M) = (((((dst_positive_code_cancel_exists_summaskentryinput) + (dst_positive_scale_cancel_exists_summaskentryinput)) * S ((dst_positive_code_cancel_exists_summaskentryinput) + (dst_positive_scale_cancel_exists_summaskentryinput)) + ((dst_positive_scale_cancel_exists_summaskentryinput) + (dst_positive_scale_cancel_exists_summaskentryinput))) + (((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) * S ((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) + ((dst_negative_scale_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)))) * S ((((dst_positive_code_cancel_exists_summaskentryinput) + (dst_positive_scale_cancel_exists_summaskentryinput)) * S ((dst_positive_code_cancel_exists_summaskentryinput) + (dst_positive_scale_cancel_exists_summaskentryinput)) + ((dst_positive_scale_cancel_exists_summaskentryinput) + (dst_positive_scale_cancel_exists_summaskentryinput))) + (((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) * S ((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) + ((dst_negative_scale_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)))) + ((((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) * S ((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) + ((dst_negative_scale_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput))) + (((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) * S ((dst_negative_code_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)) + ((dst_negative_scale_cancel_exists_summaskentryinput) + (dst_negative_scale_cancel_exists_summaskentryinput)))))) /\ (((((exists ff_h_pvs_cancel_exists_summaskentryinputpositive. ff_h_pvs_cancel_exists_summaskentryinputpositive + S (dst_positive_cancel_exists_summaskentryinput) = S ((S (dm_index_cancel_exists_summask)) * dst_positive_scale_cancel_exists_summaskentryinput)) /\ exists ff_q_pvs_cancel_exists_summaskentryinputpositive. dst_positive_code_cancel_exists_summaskentryinput = ff_q_pvs_cancel_exists_summaskentryinputpositive * S ((S (dm_index_cancel_exists_summask)) * dst_positive_scale_cancel_exists_summaskentryinput) + (dst_positive_cancel_exists_summaskentryinput))) /\ (((((exists ff_h_pvs_cancel_exists_summaskentryinputnegative. ff_h_pvs_cancel_exists_summaskentryinputnegative + S (dst_negative_cancel_exists_summaskentryinput) = S ((S (dm_index_cancel_exists_summask)) * dst_negative_scale_cancel_exists_summaskentryinput)) /\ exists ff_q_pvs_cancel_exists_summaskentryinputnegative. dst_negative_code_cancel_exists_summaskentryinput = ff_q_pvs_cancel_exists_summaskentryinputnegative * S ((S (dm_index_cancel_exists_summask)) * dst_negative_scale_cancel_exists_summaskentryinput) + (dst_negative_cancel_exists_summaskentryinput))) /\ (exists ge_balance_positive_cancel_exists_summaskentryinputvalue ge_balance_negative_cancel_exists_summaskentryinputvalue. (((((dm_value_cancel_exists_summask) = 2 * (ge_balance_positive_cancel_exists_summaskentryinputvalue) /\ (ge_balance_negative_cancel_exists_summaskentryinputvalue) = 0) \/ exists ge_signed_half_cancel_exists_summaskentryinputvaluedecode. (((dm_value_cancel_exists_summask) = 2 * ge_signed_half_cancel_exists_summaskentryinputvaluedecode + 1 /\ (ge_balance_positive_cancel_exists_summaskentryinputvalue) = 0) /\ (ge_balance_negative_cancel_exists_summaskentryinputvalue) = S ge_signed_half_cancel_exists_summaskentryinputvaluedecode))) /\ ((dst_positive_cancel_exists_summaskentryinput) + ge_balance_negative_cancel_exists_summaskentryinputvalue = (dst_negative_cancel_exists_summaskentryinput) + ge_balance_positive_cancel_exists_summaskentryinputvalue))))))))))))) \/ ((((dm_index_cancel_exists_summask)=0 \/ ~(exists pvs_factor_cancel_exists_summaskentrynondivisor. (n) = (dm_index_cancel_exists_summask) * pvs_factor_cancel_exists_summaskentrynondivisor)) /\ ((dm_value_cancel_exists_summask)=0))))))) /\ (exists dst_positive_code_cancel_exists_sumfold dst_positive_scale_cancel_exists_sumfold dst_negative_code_cancel_exists_sumfold dst_negative_scale_cancel_exists_sumfold dst_positive_sum_cancel_exists_sumfold dst_negative_sum_cancel_exists_sumfold. (((dm_mask_table_cancel_exists_sum) = (((((dst_positive_code_cancel_exists_sumfold) + (dst_positive_scale_cancel_exists_sumfold)) * S ((dst_positive_code_cancel_exists_sumfold) + (dst_positive_scale_cancel_exists_sumfold)) + ((dst_positive_scale_cancel_exists_sumfold) + (dst_positive_scale_cancel_exists_sumfold))) + (((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) * S ((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) + ((dst_negative_scale_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)))) * S ((((dst_positive_code_cancel_exists_sumfold) + (dst_positive_scale_cancel_exists_sumfold)) * S ((dst_positive_code_cancel_exists_sumfold) + (dst_positive_scale_cancel_exists_sumfold)) + ((dst_positive_scale_cancel_exists_sumfold) + (dst_positive_scale_cancel_exists_sumfold))) + (((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) * S ((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) + ((dst_negative_scale_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)))) + ((((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) * S ((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) + ((dst_negative_scale_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold))) + (((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) * S ((dst_negative_code_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)) + ((dst_negative_scale_cancel_exists_sumfold) + (dst_negative_scale_cancel_exists_sumfold)))))) /\ (((exists fs_u_dst_cancel_exists_sumfoldpositive fs_v_dst_cancel_exists_sumfoldpositive. ((((exists fs_h_dst_cancel_exists_sumfoldpositive_body_start. fs_h_dst_cancel_exists_sumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_exists_sumfoldpositive)) /\ exists fs_q_dst_cancel_exists_sumfoldpositive_body_start. fs_u_dst_cancel_exists_sumfoldpositive = fs_q_dst_cancel_exists_sumfoldpositive_body_start * S ((S (0)) * fs_v_dst_cancel_exists_sumfoldpositive) + (0))) /\ ((((exists fs_h_dst_cancel_exists_sumfoldpositive_body_terminal. fs_h_dst_cancel_exists_sumfoldpositive_body_terminal + S (dst_positive_sum_cancel_exists_sumfold) = S ((S (S (n))) * fs_v_dst_cancel_exists_sumfoldpositive)) /\ exists fs_q_dst_cancel_exists_sumfoldpositive_body_terminal. fs_u_dst_cancel_exists_sumfoldpositive = fs_q_dst_cancel_exists_sumfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_cancel_exists_sumfoldpositive) + (dst_positive_sum_cancel_exists_sumfold))) /\ forall fs_i_dst_cancel_exists_sumfoldpositive_body_steps. (exists fs_lt_dst_cancel_exists_sumfoldpositive_body_steps_bound. fs_lt_dst_cancel_exists_sumfoldpositive_body_steps_bound + S fs_i_dst_cancel_exists_sumfoldpositive_body_steps = S (n)) -> exists fs_a_dst_cancel_exists_sumfoldpositive_body_steps fs_r_dst_cancel_exists_sumfoldpositive_body_steps fs_s_dst_cancel_exists_sumfoldpositive_body_steps. ((((exists fs_h_dst_cancel_exists_sumfoldpositive_body_steps_summand. fs_h_dst_cancel_exists_sumfoldpositive_body_steps_summand + S (fs_a_dst_cancel_exists_sumfoldpositive_body_steps) = S ((S (fs_i_dst_cancel_exists_sumfoldpositive_body_steps)) * dst_positive_scale_cancel_exists_sumfold)) /\ exists fs_q_dst_cancel_exists_sumfoldpositive_body_steps_summand. dst_positive_code_cancel_exists_sumfold = fs_q_dst_cancel_exists_sumfoldpositive_body_steps_summand * S ((S (fs_i_dst_cancel_exists_sumfoldpositive_body_steps)) * dst_positive_scale_cancel_exists_sumfold) + (fs_a_dst_cancel_exists_sumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_exists_sumfoldpositive_body_steps_partial. fs_h_dst_cancel_exists_sumfoldpositive_body_steps_partial + S (fs_r_dst_cancel_exists_sumfoldpositive_body_steps) = S ((S (fs_i_dst_cancel_exists_sumfoldpositive_body_steps)) * fs_v_dst_cancel_exists_sumfoldpositive)) /\ exists fs_q_dst_cancel_exists_sumfoldpositive_body_steps_partial. fs_u_dst_cancel_exists_sumfoldpositive = fs_q_dst_cancel_exists_sumfoldpositive_body_steps_partial * S ((S (fs_i_dst_cancel_exists_sumfoldpositive_body_steps)) * fs_v_dst_cancel_exists_sumfoldpositive) + (fs_r_dst_cancel_exists_sumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_exists_sumfoldpositive_body_steps_successor. fs_h_dst_cancel_exists_sumfoldpositive_body_steps_successor + S (fs_s_dst_cancel_exists_sumfoldpositive_body_steps) = S ((S (S fs_i_dst_cancel_exists_sumfoldpositive_body_steps)) * fs_v_dst_cancel_exists_sumfoldpositive)) /\ exists fs_q_dst_cancel_exists_sumfoldpositive_body_steps_successor. fs_u_dst_cancel_exists_sumfoldpositive = fs_q_dst_cancel_exists_sumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_cancel_exists_sumfoldpositive_body_steps)) * fs_v_dst_cancel_exists_sumfoldpositive) + (fs_s_dst_cancel_exists_sumfoldpositive_body_steps))) /\ fs_s_dst_cancel_exists_sumfoldpositive_body_steps = fs_r_dst_cancel_exists_sumfoldpositive_body_steps + fs_a_dst_cancel_exists_sumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_cancel_exists_sumfoldnegative fs_v_dst_cancel_exists_sumfoldnegative. ((((exists fs_h_dst_cancel_exists_sumfoldnegative_body_start. fs_h_dst_cancel_exists_sumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_exists_sumfoldnegative)) /\ exists fs_q_dst_cancel_exists_sumfoldnegative_body_start. fs_u_dst_cancel_exists_sumfoldnegative = fs_q_dst_cancel_exists_sumfoldnegative_body_start * S ((S (0)) * fs_v_dst_cancel_exists_sumfoldnegative) + (0))) /\ ((((exists fs_h_dst_cancel_exists_sumfoldnegative_body_terminal. fs_h_dst_cancel_exists_sumfoldnegative_body_terminal + S (dst_negative_sum_cancel_exists_sumfold) = S ((S (S (n))) * fs_v_dst_cancel_exists_sumfoldnegative)) /\ exists fs_q_dst_cancel_exists_sumfoldnegative_body_terminal. fs_u_dst_cancel_exists_sumfoldnegative = fs_q_dst_cancel_exists_sumfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_cancel_exists_sumfoldnegative) + (dst_negative_sum_cancel_exists_sumfold))) /\ forall fs_i_dst_cancel_exists_sumfoldnegative_body_steps. (exists fs_lt_dst_cancel_exists_sumfoldnegative_body_steps_bound. fs_lt_dst_cancel_exists_sumfoldnegative_body_steps_bound + S fs_i_dst_cancel_exists_sumfoldnegative_body_steps = S (n)) -> exists fs_a_dst_cancel_exists_sumfoldnegative_body_steps fs_r_dst_cancel_exists_sumfoldnegative_body_steps fs_s_dst_cancel_exists_sumfoldnegative_body_steps. ((((exists fs_h_dst_cancel_exists_sumfoldnegative_body_steps_summand. fs_h_dst_cancel_exists_sumfoldnegative_body_steps_summand + S (fs_a_dst_cancel_exists_sumfoldnegative_body_steps) = S ((S (fs_i_dst_cancel_exists_sumfoldnegative_body_steps)) * dst_negative_scale_cancel_exists_sumfold)) /\ exists fs_q_dst_cancel_exists_sumfoldnegative_body_steps_summand. dst_negative_code_cancel_exists_sumfold = fs_q_dst_cancel_exists_sumfoldnegative_body_steps_summand * S ((S (fs_i_dst_cancel_exists_sumfoldnegative_body_steps)) * dst_negative_scale_cancel_exists_sumfold) + (fs_a_dst_cancel_exists_sumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_exists_sumfoldnegative_body_steps_partial. fs_h_dst_cancel_exists_sumfoldnegative_body_steps_partial + S (fs_r_dst_cancel_exists_sumfoldnegative_body_steps) = S ((S (fs_i_dst_cancel_exists_sumfoldnegative_body_steps)) * fs_v_dst_cancel_exists_sumfoldnegative)) /\ exists fs_q_dst_cancel_exists_sumfoldnegative_body_steps_partial. fs_u_dst_cancel_exists_sumfoldnegative = fs_q_dst_cancel_exists_sumfoldnegative_body_steps_partial * S ((S (fs_i_dst_cancel_exists_sumfoldnegative_body_steps)) * fs_v_dst_cancel_exists_sumfoldnegative) + (fs_r_dst_cancel_exists_sumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_exists_sumfoldnegative_body_steps_successor. fs_h_dst_cancel_exists_sumfoldnegative_body_steps_successor + S (fs_s_dst_cancel_exists_sumfoldnegative_body_steps) = S ((S (S fs_i_dst_cancel_exists_sumfoldnegative_body_steps)) * fs_v_dst_cancel_exists_sumfoldnegative)) /\ exists fs_q_dst_cancel_exists_sumfoldnegative_body_steps_successor. fs_u_dst_cancel_exists_sumfoldnegative = fs_q_dst_cancel_exists_sumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_cancel_exists_sumfoldnegative_body_steps)) * fs_v_dst_cancel_exists_sumfoldnegative) + (fs_s_dst_cancel_exists_sumfoldnegative_body_steps))) /\ fs_s_dst_cancel_exists_sumfoldnegative_body_steps = fs_r_dst_cancel_exists_sumfoldnegative_body_steps + fs_a_dst_cancel_exists_sumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_cancel_exists_sumfoldresult ge_balance_negative_cancel_exists_sumfoldresult. (((((z) = 2 * (ge_balance_positive_cancel_exists_sumfoldresult) /\ (ge_balance_negative_cancel_exists_sumfoldresult) = 0) \/ exists ge_signed_half_cancel_exists_sumfoldresultdecode. (((z) = 2 * ge_signed_half_cancel_exists_sumfoldresultdecode + 1 /\ (ge_balance_positive_cancel_exists_sumfoldresult) = 0) /\ (ge_balance_negative_cancel_exists_sumfoldresult) = S ge_signed_half_cancel_exists_sumfoldresultdecode))) /\ ((dst_positive_sum_cancel_exists_sumfold) + ge_balance_negative_cancel_exists_sumfoldresult = (dst_negative_sum_cancel_exists_sumfold) + ge_balance_positive_cancel_exists_sumfoldresult))))))))))))) /\ (((n)=1 /\ (z)=2) \/ (~((n)=1) /\ (z)=0))))))