mobius_divisor_sum_unit_one

Exact expanded first-order arithmetic statement

forall N M. (((exists dst_positive_code_cancel_unit_tabletable dst_positive_scale_cancel_unit_tabletable dst_negative_code_cancel_unit_tabletable dst_negative_scale_cancel_unit_tabletable. (((M) = (((((dst_positive_code_cancel_unit_tabletable) + (dst_positive_scale_cancel_unit_tabletable)) * S ((dst_positive_code_cancel_unit_tabletable) + (dst_positive_scale_cancel_unit_tabletable)) + ((dst_positive_scale_cancel_unit_tabletable) + (dst_positive_scale_cancel_unit_tabletable))) + (((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) * S ((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) + ((dst_negative_scale_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)))) * S ((((dst_positive_code_cancel_unit_tabletable) + (dst_positive_scale_cancel_unit_tabletable)) * S ((dst_positive_code_cancel_unit_tabletable) + (dst_positive_scale_cancel_unit_tabletable)) + ((dst_positive_scale_cancel_unit_tabletable) + (dst_positive_scale_cancel_unit_tabletable))) + (((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) * S ((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) + ((dst_negative_scale_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)))) + ((((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) * S ((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) + ((dst_negative_scale_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable))) + (((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) * S ((dst_negative_code_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)) + ((dst_negative_scale_cancel_unit_tabletable) + (dst_negative_scale_cancel_unit_tabletable)))))) /\ (forall dst_index_cancel_unit_tabletable. (exists pvs_le_gap_cancel_unit_tabletabledomain. pvs_le_gap_cancel_unit_tabletabledomain + (dst_index_cancel_unit_tabletable) = (N)) -> exists dst_positive_cancel_unit_tabletable dst_negative_cancel_unit_tabletable dst_value_cancel_unit_tabletable. ((((exists ff_h_pvs_cancel_unit_tabletableentrypositive. ff_h_pvs_cancel_unit_tabletableentrypositive + S (dst_positive_cancel_unit_tabletable) = S ((S (dst_index_cancel_unit_tabletable)) * dst_positive_scale_cancel_unit_tabletable)) /\ exists ff_q_pvs_cancel_unit_tabletableentrypositive. dst_positive_code_cancel_unit_tabletable = ff_q_pvs_cancel_unit_tabletableentrypositive * S ((S (dst_index_cancel_unit_tabletable)) * dst_positive_scale_cancel_unit_tabletable) + (dst_positive_cancel_unit_tabletable))) /\ (((((exists ff_h_pvs_cancel_unit_tabletableentrynegative. ff_h_pvs_cancel_unit_tabletableentrynegative + S (dst_negative_cancel_unit_tabletable) = S ((S (dst_index_cancel_unit_tabletable)) * dst_negative_scale_cancel_unit_tabletable)) /\ exists ff_q_pvs_cancel_unit_tabletableentrynegative. dst_negative_code_cancel_unit_tabletable = ff_q_pvs_cancel_unit_tabletableentrynegative * S ((S (dst_index_cancel_unit_tabletable)) * dst_negative_scale_cancel_unit_tabletable) + (dst_negative_cancel_unit_tabletable))) /\ (exists ge_balance_positive_cancel_unit_tabletableentryvalue ge_balance_negative_cancel_unit_tabletableentryvalue. (((((dst_value_cancel_unit_tabletable) = 2 * (ge_balance_positive_cancel_unit_tabletableentryvalue) /\ (ge_balance_negative_cancel_unit_tabletableentryvalue) = 0) \/ exists ge_signed_half_cancel_unit_tabletableentryvaluedecode. (((dst_value_cancel_unit_tabletable) = 2 * ge_signed_half_cancel_unit_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_unit_tabletableentryvalue) = 0) /\ (ge_balance_negative_cancel_unit_tabletableentryvalue) = S ge_signed_half_cancel_unit_tabletableentryvaluedecode))) /\ ((dst_positive_cancel_unit_tabletable) + ge_balance_negative_cancel_unit_tabletableentryvalue = (dst_negative_cancel_unit_tabletable) + ge_balance_positive_cancel_unit_tabletableentryvalue))))))))) /\ (((exists dst_positive_code_cancel_unit_tablezero dst_positive_scale_cancel_unit_tablezero dst_negative_code_cancel_unit_tablezero dst_negative_scale_cancel_unit_tablezero dst_positive_cancel_unit_tablezero dst_negative_cancel_unit_tablezero. (((M) = (((((dst_positive_code_cancel_unit_tablezero) + (dst_positive_scale_cancel_unit_tablezero)) * S ((dst_positive_code_cancel_unit_tablezero) + (dst_positive_scale_cancel_unit_tablezero)) + ((dst_positive_scale_cancel_unit_tablezero) + (dst_positive_scale_cancel_unit_tablezero))) + (((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) * S ((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) + ((dst_negative_scale_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)))) * S ((((dst_positive_code_cancel_unit_tablezero) + (dst_positive_scale_cancel_unit_tablezero)) * S ((dst_positive_code_cancel_unit_tablezero) + (dst_positive_scale_cancel_unit_tablezero)) + ((dst_positive_scale_cancel_unit_tablezero) + (dst_positive_scale_cancel_unit_tablezero))) + (((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) * S ((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) + ((dst_negative_scale_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)))) + ((((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) * S ((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) + ((dst_negative_scale_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero))) + (((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) * S ((dst_negative_code_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)) + ((dst_negative_scale_cancel_unit_tablezero) + (dst_negative_scale_cancel_unit_tablezero)))))) /\ (((((exists ff_h_pvs_cancel_unit_tablezeropositive. ff_h_pvs_cancel_unit_tablezeropositive + S (dst_positive_cancel_unit_tablezero) = S ((S (0)) * dst_positive_scale_cancel_unit_tablezero)) /\ exists ff_q_pvs_cancel_unit_tablezeropositive. dst_positive_code_cancel_unit_tablezero = ff_q_pvs_cancel_unit_tablezeropositive * S ((S (0)) * dst_positive_scale_cancel_unit_tablezero) + (dst_positive_cancel_unit_tablezero))) /\ (((((exists ff_h_pvs_cancel_unit_tablezeronegative. ff_h_pvs_cancel_unit_tablezeronegative + S (dst_negative_cancel_unit_tablezero) = S ((S (0)) * dst_negative_scale_cancel_unit_tablezero)) /\ exists ff_q_pvs_cancel_unit_tablezeronegative. dst_negative_code_cancel_unit_tablezero = ff_q_pvs_cancel_unit_tablezeronegative * S ((S (0)) * dst_negative_scale_cancel_unit_tablezero) + (dst_negative_cancel_unit_tablezero))) /\ (exists ge_balance_positive_cancel_unit_tablezerovalue ge_balance_negative_cancel_unit_tablezerovalue. (((((0) = 2 * (ge_balance_positive_cancel_unit_tablezerovalue) /\ (ge_balance_negative_cancel_unit_tablezerovalue) = 0) \/ exists ge_signed_half_cancel_unit_tablezerovaluedecode. (((0) = 2 * ge_signed_half_cancel_unit_tablezerovaluedecode + 1 /\ (ge_balance_positive_cancel_unit_tablezerovalue) = 0) /\ (ge_balance_negative_cancel_unit_tablezerovalue) = S ge_signed_half_cancel_unit_tablezerovaluedecode))) /\ ((dst_positive_cancel_unit_tablezero) + ge_balance_negative_cancel_unit_tablezerovalue = (dst_negative_cancel_unit_tablezero) + ge_balance_positive_cancel_unit_tablezerovalue))))))))) /\ (forall mt_index_cancel_unit_table mt_value_cancel_unit_table. ~(mt_index_cancel_unit_table=0) -> (exists pvs_le_gap_cancel_unit_tabledomain. pvs_le_gap_cancel_unit_tabledomain + (mt_index_cancel_unit_table) = (N)) -> (exists dst_positive_code_cancel_unit_tableentry dst_positive_scale_cancel_unit_tableentry dst_negative_code_cancel_unit_tableentry dst_negative_scale_cancel_unit_tableentry dst_positive_cancel_unit_tableentry dst_negative_cancel_unit_tableentry. (((M) = (((((dst_positive_code_cancel_unit_tableentry) + (dst_positive_scale_cancel_unit_tableentry)) * S ((dst_positive_code_cancel_unit_tableentry) + (dst_positive_scale_cancel_unit_tableentry)) + ((dst_positive_scale_cancel_unit_tableentry) + (dst_positive_scale_cancel_unit_tableentry))) + (((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) * S ((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) + ((dst_negative_scale_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)))) * S ((((dst_positive_code_cancel_unit_tableentry) + (dst_positive_scale_cancel_unit_tableentry)) * S ((dst_positive_code_cancel_unit_tableentry) + (dst_positive_scale_cancel_unit_tableentry)) + ((dst_positive_scale_cancel_unit_tableentry) + (dst_positive_scale_cancel_unit_tableentry))) + (((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) * S ((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) + ((dst_negative_scale_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)))) + ((((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) * S ((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) + ((dst_negative_scale_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry))) + (((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) * S ((dst_negative_code_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)) + ((dst_negative_scale_cancel_unit_tableentry) + (dst_negative_scale_cancel_unit_tableentry)))))) /\ (((((exists ff_h_pvs_cancel_unit_tableentrypositive. ff_h_pvs_cancel_unit_tableentrypositive + S (dst_positive_cancel_unit_tableentry) = S ((S (mt_index_cancel_unit_table)) * dst_positive_scale_cancel_unit_tableentry)) /\ exists ff_q_pvs_cancel_unit_tableentrypositive. dst_positive_code_cancel_unit_tableentry = ff_q_pvs_cancel_unit_tableentrypositive * S ((S (mt_index_cancel_unit_table)) * dst_positive_scale_cancel_unit_tableentry) + (dst_positive_cancel_unit_tableentry))) /\ (((((exists ff_h_pvs_cancel_unit_tableentrynegative. ff_h_pvs_cancel_unit_tableentrynegative + S (dst_negative_cancel_unit_tableentry) = S ((S (mt_index_cancel_unit_table)) * dst_negative_scale_cancel_unit_tableentry)) /\ exists ff_q_pvs_cancel_unit_tableentrynegative. dst_negative_code_cancel_unit_tableentry = ff_q_pvs_cancel_unit_tableentrynegative * S ((S (mt_index_cancel_unit_table)) * dst_negative_scale_cancel_unit_tableentry) + (dst_negative_cancel_unit_tableentry))) /\ (exists ge_balance_positive_cancel_unit_tableentryvalue ge_balance_negative_cancel_unit_tableentryvalue. (((((mt_value_cancel_unit_table) = 2 * (ge_balance_positive_cancel_unit_tableentryvalue) /\ (ge_balance_negative_cancel_unit_tableentryvalue) = 0) \/ exists ge_signed_half_cancel_unit_tableentryvaluedecode. (((mt_value_cancel_unit_table) = 2 * ge_signed_half_cancel_unit_tableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_unit_tableentryvalue) = 0) /\ (ge_balance_negative_cancel_unit_tableentryvalue) = S ge_signed_half_cancel_unit_tableentryvaluedecode))) /\ ((dst_positive_cancel_unit_tableentry) + ge_balance_negative_cancel_unit_tableentryvalue = (dst_negative_cancel_unit_tableentry) + ge_balance_positive_cancel_unit_tableentryvalue))))))))) -> (((~((mt_index_cancel_unit_table) = 0)) /\ ((((exists mv_square_prime_cancel_unit_tablevaluesquare. ((~((mv_square_prime_cancel_unit_tablevaluesquare) = 1) /\ forall pvs_left_cancel_unit_tablevaluesquareprime pvs_right_cancel_unit_tablevaluesquareprime. (mv_square_prime_cancel_unit_tablevaluesquare) = pvs_left_cancel_unit_tablevaluesquareprime * pvs_right_cancel_unit_tablevaluesquareprime -> pvs_left_cancel_unit_tablevaluesquareprime = 1 \/ pvs_right_cancel_unit_tablevaluesquareprime = 1) /\ (exists pvs_factor_cancel_unit_tablevaluesquaredivisor. (mt_index_cancel_unit_table) = (mv_square_prime_cancel_unit_tablevaluesquare * mv_square_prime_cancel_unit_tablevaluesquare) * pvs_factor_cancel_unit_tablevaluesquaredivisor))) /\ ((mt_value_cancel_unit_table) = 0))) \/ (((((~((mt_index_cancel_unit_table) = 0)) /\ (forall sfd_prime_cancel_unit_tablevaluesquarefree. (~((sfd_prime_cancel_unit_tablevaluesquarefree) = 1) /\ forall pvs_left_cancel_unit_tablevaluesquarefreedomain pvs_right_cancel_unit_tablevaluesquarefreedomain. (sfd_prime_cancel_unit_tablevaluesquarefree) = pvs_left_cancel_unit_tablevaluesquarefreedomain * pvs_right_cancel_unit_tablevaluesquarefreedomain -> pvs_left_cancel_unit_tablevaluesquarefreedomain = 1 \/ pvs_right_cancel_unit_tablevaluesquarefreedomain = 1) -> (exists pvs_le_gap_cancel_unit_tablevaluesquarefreebound. pvs_le_gap_cancel_unit_tablevaluesquarefreebound + (sfd_prime_cancel_unit_tablevaluesquarefree) = (mt_index_cancel_unit_table)) -> ~(exists pvs_factor_cancel_unit_tablevaluesquarefreesquare. (mt_index_cancel_unit_table) = (sfd_prime_cancel_unit_tablevaluesquarefree * sfd_prime_cancel_unit_tablevaluesquarefree) * pvs_factor_cancel_unit_tablevaluesquarefreesquare)))) /\ (exists mv_factor_code_cancel_unit_tablevaluefactors mv_factor_scale_cancel_unit_tablevaluefactors mv_factor_count_cancel_unit_tablevaluefactors. (((~(mt_index_cancel_unit_table = 0) /\ ((exists ff_u_fsat_cancel_unit_tablevaluefactorsfactorization_product ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_start. ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_start. ff_u_fsat_cancel_unit_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_terminal. ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_terminal + S (mt_index_cancel_unit_table) = S ((S (mv_factor_count_cancel_unit_tablevaluefactors)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_terminal. ff_u_fsat_cancel_unit_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_cancel_unit_tablevaluefactors)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product) + (mt_index_cancel_unit_table))) /\ forall ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product. (exists ff_lt_fsat_cancel_unit_tablevaluefactorsfactorization_product_bound. ff_lt_fsat_cancel_unit_tablevaluefactorsfactorization_product_bound + S ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product = mv_factor_count_cancel_unit_tablevaluefactors) -> exists ff_p_fsat_cancel_unit_tablevaluefactorsfactorization_product ff_r_fsat_cancel_unit_tablevaluefactorsfactorization_product ff_s_fsat_cancel_unit_tablevaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_factor. ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_factor + S (ff_p_fsat_cancel_unit_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product)) * mv_factor_scale_cancel_unit_tablevaluefactors)) /\ exists ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_factor. mv_factor_code_cancel_unit_tablevaluefactors = ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product)) * mv_factor_scale_cancel_unit_tablevaluefactors) + (ff_p_fsat_cancel_unit_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_partial. ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_partial + S (ff_r_fsat_cancel_unit_tablevaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_partial. ff_u_fsat_cancel_unit_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product) + (ff_r_fsat_cancel_unit_tablevaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_successor. ff_h_fsat_cancel_unit_tablevaluefactorsfactorization_product_successor + S (ff_s_fsat_cancel_unit_tablevaluefactorsfactorization_product) = S ((S (S ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_successor. ff_u_fsat_cancel_unit_tablevaluefactorsfactorization_product = ff_q_fsat_cancel_unit_tablevaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_cancel_unit_tablevaluefactorsfactorization_product)) * ff_v_fsat_cancel_unit_tablevaluefactorsfactorization_product) + (ff_s_fsat_cancel_unit_tablevaluefactorsfactorization_product))) /\ ff_s_fsat_cancel_unit_tablevaluefactorsfactorization_product = ff_r_fsat_cancel_unit_tablevaluefactorsfactorization_product * ff_p_fsat_cancel_unit_tablevaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_cancel_unit_tablevaluefactorsfactorization_primes. (exists ftsf_gap_fsat_cancel_unit_tablevaluefactorsfactorization_primes_bound. ftsf_gap_fsat_cancel_unit_tablevaluefactorsfactorization_primes_bound + S ftsf_index_fsat_cancel_unit_tablevaluefactorsfactorization_primes = (mv_factor_count_cancel_unit_tablevaluefactors)) -> exists ftsf_factor_fsat_cancel_unit_tablevaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_cancel_unit_tablevaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_cancel_unit_tablevaluefactorsfactorization_primes)) * mv_factor_scale_cancel_unit_tablevaluefactors)) /\ exists ff_q_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_entry. mv_factor_code_cancel_unit_tablevaluefactors = ff_q_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_cancel_unit_tablevaluefactorsfactorization_primes)) * mv_factor_scale_cancel_unit_tablevaluefactors) + (ftsf_factor_fsat_cancel_unit_tablevaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_cancel_unit_tablevaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_prime. ftsf_factor_fsat_cancel_unit_tablevaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_cancel_unit_tablevaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_cancel_unit_tablevaluefactorsparityeven. (mv_factor_count_cancel_unit_tablevaluefactors) = 2 * mv_even_half_cancel_unit_tablevaluefactorsparityeven) /\ ((mt_value_cancel_unit_table) = 2))) \/ (((exists mv_odd_half_cancel_unit_tablevaluefactorsparityodd. (mv_factor_count_cancel_unit_tablevaluefactors) = 2 * mv_odd_half_cancel_unit_tablevaluefactorsparityodd + 1) /\ ((mt_value_cancel_unit_table) = 1)))))))))))))))) -> (exists pvs_le_gap_cancel_unit_bound. pvs_le_gap_cancel_unit_bound + (1) = (N)) -> (((~((1)=0)) /\ (exists dm_mask_table_cancel_unit_result. ((((exists dst_positive_code_cancel_unit_resultmasktable dst_positive_scale_cancel_unit_resultmasktable dst_negative_code_cancel_unit_resultmasktable dst_negative_scale_cancel_unit_resultmasktable. (((dm_mask_table_cancel_unit_result) = (((((dst_positive_code_cancel_unit_resultmasktable) + (dst_positive_scale_cancel_unit_resultmasktable)) * S ((dst_positive_code_cancel_unit_resultmasktable) + (dst_positive_scale_cancel_unit_resultmasktable)) + ((dst_positive_scale_cancel_unit_resultmasktable) + (dst_positive_scale_cancel_unit_resultmasktable))) + (((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) * S ((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) + ((dst_negative_scale_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)))) * S ((((dst_positive_code_cancel_unit_resultmasktable) + (dst_positive_scale_cancel_unit_resultmasktable)) * S ((dst_positive_code_cancel_unit_resultmasktable) + (dst_positive_scale_cancel_unit_resultmasktable)) + ((dst_positive_scale_cancel_unit_resultmasktable) + (dst_positive_scale_cancel_unit_resultmasktable))) + (((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) * S ((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) + ((dst_negative_scale_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)))) + ((((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) * S ((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) + ((dst_negative_scale_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable))) + (((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) * S ((dst_negative_code_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)) + ((dst_negative_scale_cancel_unit_resultmasktable) + (dst_negative_scale_cancel_unit_resultmasktable)))))) /\ (forall dst_index_cancel_unit_resultmasktable. (exists pvs_le_gap_cancel_unit_resultmasktabledomain. pvs_le_gap_cancel_unit_resultmasktabledomain + (dst_index_cancel_unit_resultmasktable) = (1)) -> exists dst_positive_cancel_unit_resultmasktable dst_negative_cancel_unit_resultmasktable dst_value_cancel_unit_resultmasktable. ((((exists ff_h_pvs_cancel_unit_resultmasktableentrypositive. ff_h_pvs_cancel_unit_resultmasktableentrypositive + S (dst_positive_cancel_unit_resultmasktable) = S ((S (dst_index_cancel_unit_resultmasktable)) * dst_positive_scale_cancel_unit_resultmasktable)) /\ exists ff_q_pvs_cancel_unit_resultmasktableentrypositive. dst_positive_code_cancel_unit_resultmasktable = ff_q_pvs_cancel_unit_resultmasktableentrypositive * S ((S (dst_index_cancel_unit_resultmasktable)) * dst_positive_scale_cancel_unit_resultmasktable) + (dst_positive_cancel_unit_resultmasktable))) /\ (((((exists ff_h_pvs_cancel_unit_resultmasktableentrynegative. ff_h_pvs_cancel_unit_resultmasktableentrynegative + S (dst_negative_cancel_unit_resultmasktable) = S ((S (dst_index_cancel_unit_resultmasktable)) * dst_negative_scale_cancel_unit_resultmasktable)) /\ exists ff_q_pvs_cancel_unit_resultmasktableentrynegative. dst_negative_code_cancel_unit_resultmasktable = ff_q_pvs_cancel_unit_resultmasktableentrynegative * S ((S (dst_index_cancel_unit_resultmasktable)) * dst_negative_scale_cancel_unit_resultmasktable) + (dst_negative_cancel_unit_resultmasktable))) /\ (exists ge_balance_positive_cancel_unit_resultmasktableentryvalue ge_balance_negative_cancel_unit_resultmasktableentryvalue. (((((dst_value_cancel_unit_resultmasktable) = 2 * (ge_balance_positive_cancel_unit_resultmasktableentryvalue) /\ (ge_balance_negative_cancel_unit_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_cancel_unit_resultmasktableentryvaluedecode. (((dst_value_cancel_unit_resultmasktable) = 2 * ge_signed_half_cancel_unit_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_unit_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_cancel_unit_resultmasktableentryvalue) = S ge_signed_half_cancel_unit_resultmasktableentryvaluedecode))) /\ ((dst_positive_cancel_unit_resultmasktable) + ge_balance_negative_cancel_unit_resultmasktableentryvalue = (dst_negative_cancel_unit_resultmasktable) + ge_balance_positive_cancel_unit_resultmasktableentryvalue))))))))) /\ (forall dm_index_cancel_unit_resultmask dm_value_cancel_unit_resultmask. (exists pvs_le_gap_cancel_unit_resultmaskdomain. pvs_le_gap_cancel_unit_resultmaskdomain + (dm_index_cancel_unit_resultmask) = (1)) -> (exists dst_positive_code_cancel_unit_resultmasklookup dst_positive_scale_cancel_unit_resultmasklookup dst_negative_code_cancel_unit_resultmasklookup dst_negative_scale_cancel_unit_resultmasklookup dst_positive_cancel_unit_resultmasklookup dst_negative_cancel_unit_resultmasklookup. (((dm_mask_table_cancel_unit_result) = (((((dst_positive_code_cancel_unit_resultmasklookup) + (dst_positive_scale_cancel_unit_resultmasklookup)) * S ((dst_positive_code_cancel_unit_resultmasklookup) + (dst_positive_scale_cancel_unit_resultmasklookup)) + ((dst_positive_scale_cancel_unit_resultmasklookup) + (dst_positive_scale_cancel_unit_resultmasklookup))) + (((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) * S ((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) + ((dst_negative_scale_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)))) * S ((((dst_positive_code_cancel_unit_resultmasklookup) + (dst_positive_scale_cancel_unit_resultmasklookup)) * S ((dst_positive_code_cancel_unit_resultmasklookup) + (dst_positive_scale_cancel_unit_resultmasklookup)) + ((dst_positive_scale_cancel_unit_resultmasklookup) + (dst_positive_scale_cancel_unit_resultmasklookup))) + (((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) * S ((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) + ((dst_negative_scale_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)))) + ((((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) * S ((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) + ((dst_negative_scale_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup))) + (((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) * S ((dst_negative_code_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)) + ((dst_negative_scale_cancel_unit_resultmasklookup) + (dst_negative_scale_cancel_unit_resultmasklookup)))))) /\ (((((exists ff_h_pvs_cancel_unit_resultmasklookuppositive. ff_h_pvs_cancel_unit_resultmasklookuppositive + S (dst_positive_cancel_unit_resultmasklookup) = S ((S (dm_index_cancel_unit_resultmask)) * dst_positive_scale_cancel_unit_resultmasklookup)) /\ exists ff_q_pvs_cancel_unit_resultmasklookuppositive. dst_positive_code_cancel_unit_resultmasklookup = ff_q_pvs_cancel_unit_resultmasklookuppositive * S ((S (dm_index_cancel_unit_resultmask)) * dst_positive_scale_cancel_unit_resultmasklookup) + (dst_positive_cancel_unit_resultmasklookup))) /\ (((((exists ff_h_pvs_cancel_unit_resultmasklookupnegative. ff_h_pvs_cancel_unit_resultmasklookupnegative + S (dst_negative_cancel_unit_resultmasklookup) = S ((S (dm_index_cancel_unit_resultmask)) * dst_negative_scale_cancel_unit_resultmasklookup)) /\ exists ff_q_pvs_cancel_unit_resultmasklookupnegative. dst_negative_code_cancel_unit_resultmasklookup = ff_q_pvs_cancel_unit_resultmasklookupnegative * S ((S (dm_index_cancel_unit_resultmask)) * dst_negative_scale_cancel_unit_resultmasklookup) + (dst_negative_cancel_unit_resultmasklookup))) /\ (exists ge_balance_positive_cancel_unit_resultmasklookupvalue ge_balance_negative_cancel_unit_resultmasklookupvalue. (((((dm_value_cancel_unit_resultmask) = 2 * (ge_balance_positive_cancel_unit_resultmasklookupvalue) /\ (ge_balance_negative_cancel_unit_resultmasklookupvalue) = 0) \/ exists ge_signed_half_cancel_unit_resultmasklookupvaluedecode. (((dm_value_cancel_unit_resultmask) = 2 * ge_signed_half_cancel_unit_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_cancel_unit_resultmasklookupvalue) = 0) /\ (ge_balance_negative_cancel_unit_resultmasklookupvalue) = S ge_signed_half_cancel_unit_resultmasklookupvaluedecode))) /\ ((dst_positive_cancel_unit_resultmasklookup) + ge_balance_negative_cancel_unit_resultmasklookupvalue = (dst_negative_cancel_unit_resultmasklookup) + ge_balance_positive_cancel_unit_resultmasklookupvalue))))))))) -> ((((~((dm_index_cancel_unit_resultmask)=0)) /\ (exists dm_quotient_cancel_unit_resultmaskentry. (((1)=(dm_index_cancel_unit_resultmask)*dm_quotient_cancel_unit_resultmaskentry) /\ (exists dst_positive_code_cancel_unit_resultmaskentryinput dst_positive_scale_cancel_unit_resultmaskentryinput dst_negative_code_cancel_unit_resultmaskentryinput dst_negative_scale_cancel_unit_resultmaskentryinput dst_positive_cancel_unit_resultmaskentryinput dst_negative_cancel_unit_resultmaskentryinput. (((M) = (((((dst_positive_code_cancel_unit_resultmaskentryinput) + (dst_positive_scale_cancel_unit_resultmaskentryinput)) * S ((dst_positive_code_cancel_unit_resultmaskentryinput) + (dst_positive_scale_cancel_unit_resultmaskentryinput)) + ((dst_positive_scale_cancel_unit_resultmaskentryinput) + (dst_positive_scale_cancel_unit_resultmaskentryinput))) + (((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) * S ((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) + ((dst_negative_scale_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)))) * S ((((dst_positive_code_cancel_unit_resultmaskentryinput) + (dst_positive_scale_cancel_unit_resultmaskentryinput)) * S ((dst_positive_code_cancel_unit_resultmaskentryinput) + (dst_positive_scale_cancel_unit_resultmaskentryinput)) + ((dst_positive_scale_cancel_unit_resultmaskentryinput) + (dst_positive_scale_cancel_unit_resultmaskentryinput))) + (((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) * S ((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) + ((dst_negative_scale_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)))) + ((((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) * S ((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) + ((dst_negative_scale_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput))) + (((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) * S ((dst_negative_code_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)) + ((dst_negative_scale_cancel_unit_resultmaskentryinput) + (dst_negative_scale_cancel_unit_resultmaskentryinput)))))) /\ (((((exists ff_h_pvs_cancel_unit_resultmaskentryinputpositive. ff_h_pvs_cancel_unit_resultmaskentryinputpositive + S (dst_positive_cancel_unit_resultmaskentryinput) = S ((S (dm_index_cancel_unit_resultmask)) * dst_positive_scale_cancel_unit_resultmaskentryinput)) /\ exists ff_q_pvs_cancel_unit_resultmaskentryinputpositive. dst_positive_code_cancel_unit_resultmaskentryinput = ff_q_pvs_cancel_unit_resultmaskentryinputpositive * S ((S (dm_index_cancel_unit_resultmask)) * dst_positive_scale_cancel_unit_resultmaskentryinput) + (dst_positive_cancel_unit_resultmaskentryinput))) /\ (((((exists ff_h_pvs_cancel_unit_resultmaskentryinputnegative. ff_h_pvs_cancel_unit_resultmaskentryinputnegative + S (dst_negative_cancel_unit_resultmaskentryinput) = S ((S (dm_index_cancel_unit_resultmask)) * dst_negative_scale_cancel_unit_resultmaskentryinput)) /\ exists ff_q_pvs_cancel_unit_resultmaskentryinputnegative. dst_negative_code_cancel_unit_resultmaskentryinput = ff_q_pvs_cancel_unit_resultmaskentryinputnegative * S ((S (dm_index_cancel_unit_resultmask)) * dst_negative_scale_cancel_unit_resultmaskentryinput) + (dst_negative_cancel_unit_resultmaskentryinput))) /\ (exists ge_balance_positive_cancel_unit_resultmaskentryinputvalue ge_balance_negative_cancel_unit_resultmaskentryinputvalue. (((((dm_value_cancel_unit_resultmask) = 2 * (ge_balance_positive_cancel_unit_resultmaskentryinputvalue) /\ (ge_balance_negative_cancel_unit_resultmaskentryinputvalue) = 0) \/ exists ge_signed_half_cancel_unit_resultmaskentryinputvaluedecode. (((dm_value_cancel_unit_resultmask) = 2 * ge_signed_half_cancel_unit_resultmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_cancel_unit_resultmaskentryinputvalue) = 0) /\ (ge_balance_negative_cancel_unit_resultmaskentryinputvalue) = S ge_signed_half_cancel_unit_resultmaskentryinputvaluedecode))) /\ ((dst_positive_cancel_unit_resultmaskentryinput) + ge_balance_negative_cancel_unit_resultmaskentryinputvalue = (dst_negative_cancel_unit_resultmaskentryinput) + ge_balance_positive_cancel_unit_resultmaskentryinputvalue))))))))))))) \/ ((((dm_index_cancel_unit_resultmask)=0 \/ ~(exists pvs_factor_cancel_unit_resultmaskentrynondivisor. (1) = (dm_index_cancel_unit_resultmask) * pvs_factor_cancel_unit_resultmaskentrynondivisor)) /\ ((dm_value_cancel_unit_resultmask)=0))))))) /\ (exists dst_positive_code_cancel_unit_resultfold dst_positive_scale_cancel_unit_resultfold dst_negative_code_cancel_unit_resultfold dst_negative_scale_cancel_unit_resultfold dst_positive_sum_cancel_unit_resultfold dst_negative_sum_cancel_unit_resultfold. (((dm_mask_table_cancel_unit_result) = (((((dst_positive_code_cancel_unit_resultfold) + (dst_positive_scale_cancel_unit_resultfold)) * S ((dst_positive_code_cancel_unit_resultfold) + (dst_positive_scale_cancel_unit_resultfold)) + ((dst_positive_scale_cancel_unit_resultfold) + (dst_positive_scale_cancel_unit_resultfold))) + (((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) * S ((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) + ((dst_negative_scale_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)))) * S ((((dst_positive_code_cancel_unit_resultfold) + (dst_positive_scale_cancel_unit_resultfold)) * S ((dst_positive_code_cancel_unit_resultfold) + (dst_positive_scale_cancel_unit_resultfold)) + ((dst_positive_scale_cancel_unit_resultfold) + (dst_positive_scale_cancel_unit_resultfold))) + (((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) * S ((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) + ((dst_negative_scale_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)))) + ((((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) * S ((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) + ((dst_negative_scale_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold))) + (((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) * S ((dst_negative_code_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)) + ((dst_negative_scale_cancel_unit_resultfold) + (dst_negative_scale_cancel_unit_resultfold)))))) /\ (((exists fs_u_dst_cancel_unit_resultfoldpositive fs_v_dst_cancel_unit_resultfoldpositive. ((((exists fs_h_dst_cancel_unit_resultfoldpositive_body_start. fs_h_dst_cancel_unit_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_unit_resultfoldpositive)) /\ exists fs_q_dst_cancel_unit_resultfoldpositive_body_start. fs_u_dst_cancel_unit_resultfoldpositive = fs_q_dst_cancel_unit_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_cancel_unit_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_cancel_unit_resultfoldpositive_body_terminal. fs_h_dst_cancel_unit_resultfoldpositive_body_terminal + S (dst_positive_sum_cancel_unit_resultfold) = S ((S (S (1))) * fs_v_dst_cancel_unit_resultfoldpositive)) /\ exists fs_q_dst_cancel_unit_resultfoldpositive_body_terminal. fs_u_dst_cancel_unit_resultfoldpositive = fs_q_dst_cancel_unit_resultfoldpositive_body_terminal * S ((S (S (1))) * fs_v_dst_cancel_unit_resultfoldpositive) + (dst_positive_sum_cancel_unit_resultfold))) /\ forall fs_i_dst_cancel_unit_resultfoldpositive_body_steps. (exists fs_lt_dst_cancel_unit_resultfoldpositive_body_steps_bound. fs_lt_dst_cancel_unit_resultfoldpositive_body_steps_bound + S fs_i_dst_cancel_unit_resultfoldpositive_body_steps = S (1)) -> exists fs_a_dst_cancel_unit_resultfoldpositive_body_steps fs_r_dst_cancel_unit_resultfoldpositive_body_steps fs_s_dst_cancel_unit_resultfoldpositive_body_steps. ((((exists fs_h_dst_cancel_unit_resultfoldpositive_body_steps_summand. fs_h_dst_cancel_unit_resultfoldpositive_body_steps_summand + S (fs_a_dst_cancel_unit_resultfoldpositive_body_steps) = S ((S (fs_i_dst_cancel_unit_resultfoldpositive_body_steps)) * dst_positive_scale_cancel_unit_resultfold)) /\ exists fs_q_dst_cancel_unit_resultfoldpositive_body_steps_summand. dst_positive_code_cancel_unit_resultfold = fs_q_dst_cancel_unit_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_cancel_unit_resultfoldpositive_body_steps)) * dst_positive_scale_cancel_unit_resultfold) + (fs_a_dst_cancel_unit_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_unit_resultfoldpositive_body_steps_partial. fs_h_dst_cancel_unit_resultfoldpositive_body_steps_partial + S (fs_r_dst_cancel_unit_resultfoldpositive_body_steps) = S ((S (fs_i_dst_cancel_unit_resultfoldpositive_body_steps)) * fs_v_dst_cancel_unit_resultfoldpositive)) /\ exists fs_q_dst_cancel_unit_resultfoldpositive_body_steps_partial. fs_u_dst_cancel_unit_resultfoldpositive = fs_q_dst_cancel_unit_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_cancel_unit_resultfoldpositive_body_steps)) * fs_v_dst_cancel_unit_resultfoldpositive) + (fs_r_dst_cancel_unit_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_unit_resultfoldpositive_body_steps_successor. fs_h_dst_cancel_unit_resultfoldpositive_body_steps_successor + S (fs_s_dst_cancel_unit_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_cancel_unit_resultfoldpositive_body_steps)) * fs_v_dst_cancel_unit_resultfoldpositive)) /\ exists fs_q_dst_cancel_unit_resultfoldpositive_body_steps_successor. fs_u_dst_cancel_unit_resultfoldpositive = fs_q_dst_cancel_unit_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_cancel_unit_resultfoldpositive_body_steps)) * fs_v_dst_cancel_unit_resultfoldpositive) + (fs_s_dst_cancel_unit_resultfoldpositive_body_steps))) /\ fs_s_dst_cancel_unit_resultfoldpositive_body_steps = fs_r_dst_cancel_unit_resultfoldpositive_body_steps + fs_a_dst_cancel_unit_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_cancel_unit_resultfoldnegative fs_v_dst_cancel_unit_resultfoldnegative. ((((exists fs_h_dst_cancel_unit_resultfoldnegative_body_start. fs_h_dst_cancel_unit_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_unit_resultfoldnegative)) /\ exists fs_q_dst_cancel_unit_resultfoldnegative_body_start. fs_u_dst_cancel_unit_resultfoldnegative = fs_q_dst_cancel_unit_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_cancel_unit_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_cancel_unit_resultfoldnegative_body_terminal. fs_h_dst_cancel_unit_resultfoldnegative_body_terminal + S (dst_negative_sum_cancel_unit_resultfold) = S ((S (S (1))) * fs_v_dst_cancel_unit_resultfoldnegative)) /\ exists fs_q_dst_cancel_unit_resultfoldnegative_body_terminal. fs_u_dst_cancel_unit_resultfoldnegative = fs_q_dst_cancel_unit_resultfoldnegative_body_terminal * S ((S (S (1))) * fs_v_dst_cancel_unit_resultfoldnegative) + (dst_negative_sum_cancel_unit_resultfold))) /\ forall fs_i_dst_cancel_unit_resultfoldnegative_body_steps. (exists fs_lt_dst_cancel_unit_resultfoldnegative_body_steps_bound. fs_lt_dst_cancel_unit_resultfoldnegative_body_steps_bound + S fs_i_dst_cancel_unit_resultfoldnegative_body_steps = S (1)) -> exists fs_a_dst_cancel_unit_resultfoldnegative_body_steps fs_r_dst_cancel_unit_resultfoldnegative_body_steps fs_s_dst_cancel_unit_resultfoldnegative_body_steps. ((((exists fs_h_dst_cancel_unit_resultfoldnegative_body_steps_summand. fs_h_dst_cancel_unit_resultfoldnegative_body_steps_summand + S (fs_a_dst_cancel_unit_resultfoldnegative_body_steps) = S ((S (fs_i_dst_cancel_unit_resultfoldnegative_body_steps)) * dst_negative_scale_cancel_unit_resultfold)) /\ exists fs_q_dst_cancel_unit_resultfoldnegative_body_steps_summand. dst_negative_code_cancel_unit_resultfold = fs_q_dst_cancel_unit_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_cancel_unit_resultfoldnegative_body_steps)) * dst_negative_scale_cancel_unit_resultfold) + (fs_a_dst_cancel_unit_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_unit_resultfoldnegative_body_steps_partial. fs_h_dst_cancel_unit_resultfoldnegative_body_steps_partial + S (fs_r_dst_cancel_unit_resultfoldnegative_body_steps) = S ((S (fs_i_dst_cancel_unit_resultfoldnegative_body_steps)) * fs_v_dst_cancel_unit_resultfoldnegative)) /\ exists fs_q_dst_cancel_unit_resultfoldnegative_body_steps_partial. fs_u_dst_cancel_unit_resultfoldnegative = fs_q_dst_cancel_unit_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_cancel_unit_resultfoldnegative_body_steps)) * fs_v_dst_cancel_unit_resultfoldnegative) + (fs_r_dst_cancel_unit_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_unit_resultfoldnegative_body_steps_successor. fs_h_dst_cancel_unit_resultfoldnegative_body_steps_successor + S (fs_s_dst_cancel_unit_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_cancel_unit_resultfoldnegative_body_steps)) * fs_v_dst_cancel_unit_resultfoldnegative)) /\ exists fs_q_dst_cancel_unit_resultfoldnegative_body_steps_successor. fs_u_dst_cancel_unit_resultfoldnegative = fs_q_dst_cancel_unit_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_cancel_unit_resultfoldnegative_body_steps)) * fs_v_dst_cancel_unit_resultfoldnegative) + (fs_s_dst_cancel_unit_resultfoldnegative_body_steps))) /\ fs_s_dst_cancel_unit_resultfoldnegative_body_steps = fs_r_dst_cancel_unit_resultfoldnegative_body_steps + fs_a_dst_cancel_unit_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_cancel_unit_resultfoldresult ge_balance_negative_cancel_unit_resultfoldresult. (((((2) = 2 * (ge_balance_positive_cancel_unit_resultfoldresult) /\ (ge_balance_negative_cancel_unit_resultfoldresult) = 0) \/ exists ge_signed_half_cancel_unit_resultfoldresultdecode. (((2) = 2 * ge_signed_half_cancel_unit_resultfoldresultdecode + 1 /\ (ge_balance_positive_cancel_unit_resultfoldresult) = 0) /\ (ge_balance_negative_cancel_unit_resultfoldresult) = S ge_signed_half_cancel_unit_resultfoldresultdecode))) /\ ((dst_positive_sum_cancel_unit_resultfold) + ge_balance_negative_cancel_unit_resultfoldresult = (dst_negative_sum_cancel_unit_resultfold) + ge_balance_positive_cancel_unit_resultfoldresult)))))))))))))