mobius_divisor_sum_cancellation_on_positive_values

Exact expanded first-order arithmetic statement

forall N F n z. (exists dst_positive_code_arbitrary_zero_table dst_positive_scale_arbitrary_zero_table dst_negative_code_arbitrary_zero_table dst_negative_scale_arbitrary_zero_table. (((F) = (((((dst_positive_code_arbitrary_zero_table) + (dst_positive_scale_arbitrary_zero_table)) * S ((dst_positive_code_arbitrary_zero_table) + (dst_positive_scale_arbitrary_zero_table)) + ((dst_positive_scale_arbitrary_zero_table) + (dst_positive_scale_arbitrary_zero_table))) + (((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) * S ((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) + ((dst_negative_scale_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)))) * S ((((dst_positive_code_arbitrary_zero_table) + (dst_positive_scale_arbitrary_zero_table)) * S ((dst_positive_code_arbitrary_zero_table) + (dst_positive_scale_arbitrary_zero_table)) + ((dst_positive_scale_arbitrary_zero_table) + (dst_positive_scale_arbitrary_zero_table))) + (((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) * S ((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) + ((dst_negative_scale_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)))) + ((((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) * S ((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) + ((dst_negative_scale_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table))) + (((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) * S ((dst_negative_code_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)) + ((dst_negative_scale_arbitrary_zero_table) + (dst_negative_scale_arbitrary_zero_table)))))) /\ (forall dst_index_arbitrary_zero_table. (exists pvs_le_gap_arbitrary_zero_tabledomain. pvs_le_gap_arbitrary_zero_tabledomain + (dst_index_arbitrary_zero_table) = (N)) -> exists dst_positive_arbitrary_zero_table dst_negative_arbitrary_zero_table dst_value_arbitrary_zero_table. ((((exists ff_h_pvs_arbitrary_zero_tableentrypositive. ff_h_pvs_arbitrary_zero_tableentrypositive + S (dst_positive_arbitrary_zero_table) = S ((S (dst_index_arbitrary_zero_table)) * dst_positive_scale_arbitrary_zero_table)) /\ exists ff_q_pvs_arbitrary_zero_tableentrypositive. dst_positive_code_arbitrary_zero_table = ff_q_pvs_arbitrary_zero_tableentrypositive * S ((S (dst_index_arbitrary_zero_table)) * dst_positive_scale_arbitrary_zero_table) + (dst_positive_arbitrary_zero_table))) /\ (((((exists ff_h_pvs_arbitrary_zero_tableentrynegative. ff_h_pvs_arbitrary_zero_tableentrynegative + S (dst_negative_arbitrary_zero_table) = S ((S (dst_index_arbitrary_zero_table)) * dst_negative_scale_arbitrary_zero_table)) /\ exists ff_q_pvs_arbitrary_zero_tableentrynegative. dst_negative_code_arbitrary_zero_table = ff_q_pvs_arbitrary_zero_tableentrynegative * S ((S (dst_index_arbitrary_zero_table)) * dst_negative_scale_arbitrary_zero_table) + (dst_negative_arbitrary_zero_table))) /\ (exists ge_balance_positive_arbitrary_zero_tableentryvalue ge_balance_negative_arbitrary_zero_tableentryvalue. (((((dst_value_arbitrary_zero_table) = 2 * (ge_balance_positive_arbitrary_zero_tableentryvalue) /\ (ge_balance_negative_arbitrary_zero_tableentryvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_tableentryvaluedecode. (((dst_value_arbitrary_zero_table) = 2 * ge_signed_half_arbitrary_zero_tableentryvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_tableentryvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_tableentryvalue) = S ge_signed_half_arbitrary_zero_tableentryvaluedecode))) /\ ((dst_positive_arbitrary_zero_table) + ge_balance_negative_arbitrary_zero_tableentryvalue = (dst_negative_arbitrary_zero_table) + ge_balance_positive_arbitrary_zero_tableentryvalue))))))))) -> (forall mdc_positive_index_arbitrary_zero_values mdc_positive_value_arbitrary_zero_values. ~(mdc_positive_index_arbitrary_zero_values=0) -> (exists pvs_le_gap_arbitrary_zero_valuesbound. pvs_le_gap_arbitrary_zero_valuesbound + (mdc_positive_index_arbitrary_zero_values) = (N)) -> (exists dst_positive_code_arbitrary_zero_valuesentry dst_positive_scale_arbitrary_zero_valuesentry dst_negative_code_arbitrary_zero_valuesentry dst_negative_scale_arbitrary_zero_valuesentry dst_positive_arbitrary_zero_valuesentry dst_negative_arbitrary_zero_valuesentry. (((F) = (((((dst_positive_code_arbitrary_zero_valuesentry) + (dst_positive_scale_arbitrary_zero_valuesentry)) * S ((dst_positive_code_arbitrary_zero_valuesentry) + (dst_positive_scale_arbitrary_zero_valuesentry)) + ((dst_positive_scale_arbitrary_zero_valuesentry) + (dst_positive_scale_arbitrary_zero_valuesentry))) + (((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) * S ((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) + ((dst_negative_scale_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)))) * S ((((dst_positive_code_arbitrary_zero_valuesentry) + (dst_positive_scale_arbitrary_zero_valuesentry)) * S ((dst_positive_code_arbitrary_zero_valuesentry) + (dst_positive_scale_arbitrary_zero_valuesentry)) + ((dst_positive_scale_arbitrary_zero_valuesentry) + (dst_positive_scale_arbitrary_zero_valuesentry))) + (((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) * S ((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) + ((dst_negative_scale_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)))) + ((((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) * S ((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) + ((dst_negative_scale_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry))) + (((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) * S ((dst_negative_code_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)) + ((dst_negative_scale_arbitrary_zero_valuesentry) + (dst_negative_scale_arbitrary_zero_valuesentry)))))) /\ (((((exists ff_h_pvs_arbitrary_zero_valuesentrypositive. ff_h_pvs_arbitrary_zero_valuesentrypositive + S (dst_positive_arbitrary_zero_valuesentry) = S ((S (mdc_positive_index_arbitrary_zero_values)) * dst_positive_scale_arbitrary_zero_valuesentry)) /\ exists ff_q_pvs_arbitrary_zero_valuesentrypositive. dst_positive_code_arbitrary_zero_valuesentry = ff_q_pvs_arbitrary_zero_valuesentrypositive * S ((S (mdc_positive_index_arbitrary_zero_values)) * dst_positive_scale_arbitrary_zero_valuesentry) + (dst_positive_arbitrary_zero_valuesentry))) /\ (((((exists ff_h_pvs_arbitrary_zero_valuesentrynegative. ff_h_pvs_arbitrary_zero_valuesentrynegative + S (dst_negative_arbitrary_zero_valuesentry) = S ((S (mdc_positive_index_arbitrary_zero_values)) * dst_negative_scale_arbitrary_zero_valuesentry)) /\ exists ff_q_pvs_arbitrary_zero_valuesentrynegative. dst_negative_code_arbitrary_zero_valuesentry = ff_q_pvs_arbitrary_zero_valuesentrynegative * S ((S (mdc_positive_index_arbitrary_zero_values)) * dst_negative_scale_arbitrary_zero_valuesentry) + (dst_negative_arbitrary_zero_valuesentry))) /\ (exists ge_balance_positive_arbitrary_zero_valuesentryvalue ge_balance_negative_arbitrary_zero_valuesentryvalue. (((((mdc_positive_value_arbitrary_zero_values) = 2 * (ge_balance_positive_arbitrary_zero_valuesentryvalue) /\ (ge_balance_negative_arbitrary_zero_valuesentryvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_valuesentryvaluedecode. (((mdc_positive_value_arbitrary_zero_values) = 2 * ge_signed_half_arbitrary_zero_valuesentryvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_valuesentryvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_valuesentryvalue) = S ge_signed_half_arbitrary_zero_valuesentryvaluedecode))) /\ ((dst_positive_arbitrary_zero_valuesentry) + ge_balance_negative_arbitrary_zero_valuesentryvalue = (dst_negative_arbitrary_zero_valuesentry) + ge_balance_positive_arbitrary_zero_valuesentryvalue))))))))) -> (((~((mdc_positive_index_arbitrary_zero_values) = 0)) /\ ((((exists mv_square_prime_arbitrary_zero_valuesmobiussquare. ((~((mv_square_prime_arbitrary_zero_valuesmobiussquare) = 1) /\ forall pvs_left_arbitrary_zero_valuesmobiussquareprime pvs_right_arbitrary_zero_valuesmobiussquareprime. (mv_square_prime_arbitrary_zero_valuesmobiussquare) = pvs_left_arbitrary_zero_valuesmobiussquareprime * pvs_right_arbitrary_zero_valuesmobiussquareprime -> pvs_left_arbitrary_zero_valuesmobiussquareprime = 1 \/ pvs_right_arbitrary_zero_valuesmobiussquareprime = 1) /\ (exists pvs_factor_arbitrary_zero_valuesmobiussquaredivisor. (mdc_positive_index_arbitrary_zero_values) = (mv_square_prime_arbitrary_zero_valuesmobiussquare * mv_square_prime_arbitrary_zero_valuesmobiussquare) * pvs_factor_arbitrary_zero_valuesmobiussquaredivisor))) /\ ((mdc_positive_value_arbitrary_zero_values) = 0))) \/ (((((~((mdc_positive_index_arbitrary_zero_values) = 0)) /\ (forall sfd_prime_arbitrary_zero_valuesmobiussquarefree. (~((sfd_prime_arbitrary_zero_valuesmobiussquarefree) = 1) /\ forall pvs_left_arbitrary_zero_valuesmobiussquarefreedomain pvs_right_arbitrary_zero_valuesmobiussquarefreedomain. (sfd_prime_arbitrary_zero_valuesmobiussquarefree) = pvs_left_arbitrary_zero_valuesmobiussquarefreedomain * pvs_right_arbitrary_zero_valuesmobiussquarefreedomain -> pvs_left_arbitrary_zero_valuesmobiussquarefreedomain = 1 \/ pvs_right_arbitrary_zero_valuesmobiussquarefreedomain = 1) -> (exists pvs_le_gap_arbitrary_zero_valuesmobiussquarefreebound. pvs_le_gap_arbitrary_zero_valuesmobiussquarefreebound + (sfd_prime_arbitrary_zero_valuesmobiussquarefree) = (mdc_positive_index_arbitrary_zero_values)) -> ~(exists pvs_factor_arbitrary_zero_valuesmobiussquarefreesquare. (mdc_positive_index_arbitrary_zero_values) = (sfd_prime_arbitrary_zero_valuesmobiussquarefree * sfd_prime_arbitrary_zero_valuesmobiussquarefree) * pvs_factor_arbitrary_zero_valuesmobiussquarefreesquare)))) /\ (exists mv_factor_code_arbitrary_zero_valuesmobiusfactors mv_factor_scale_arbitrary_zero_valuesmobiusfactors mv_factor_count_arbitrary_zero_valuesmobiusfactors. (((~(mdc_positive_index_arbitrary_zero_values = 0) /\ ((exists ff_u_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product. ((((exists ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_start. ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_start. ff_u_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product = ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_terminal. ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_terminal + S (mdc_positive_index_arbitrary_zero_values) = S ((S (mv_factor_count_arbitrary_zero_valuesmobiusfactors)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_terminal. ff_u_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product = ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_terminal * S ((S (mv_factor_count_arbitrary_zero_valuesmobiusfactors)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) + (mdc_positive_index_arbitrary_zero_values))) /\ forall ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product. (exists ff_lt_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_bound. ff_lt_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_bound + S ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product = mv_factor_count_arbitrary_zero_valuesmobiusfactors) -> exists ff_p_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product ff_r_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product ff_s_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product. ((((exists ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_factor. ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_factor + S (ff_p_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) = S ((S (ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) * mv_factor_scale_arbitrary_zero_valuesmobiusfactors)) /\ exists ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_factor. mv_factor_code_arbitrary_zero_valuesmobiusfactors = ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_factor * S ((S (ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) * mv_factor_scale_arbitrary_zero_valuesmobiusfactors) + (ff_p_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product))) /\ ((((exists ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_partial. ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_partial + S (ff_r_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) = S ((S (ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_partial. ff_u_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product = ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_partial * S ((S (ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) + (ff_r_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product))) /\ ((((exists ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_successor. ff_h_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_successor + S (ff_s_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) = S ((S (S ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) /\ exists ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_successor. ff_u_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product = ff_q_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product_successor * S ((S (S ff_i_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)) * ff_v_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product) + (ff_s_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product))) /\ ff_s_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product = ff_r_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product * ff_p_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes. (exists ftsf_gap_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_bound. ftsf_gap_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_bound + S ftsf_index_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes = (mv_factor_count_arbitrary_zero_valuesmobiusfactors)) -> exists ftsf_factor_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_entry. ff_h_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_entry + S (ftsf_factor_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes) = S ((S (ftsf_index_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes)) * mv_factor_scale_arbitrary_zero_valuesmobiusfactors)) /\ exists ff_q_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_entry. mv_factor_code_arbitrary_zero_valuesmobiusfactors = ff_q_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes)) * mv_factor_scale_arbitrary_zero_valuesmobiusfactors) + (ftsf_factor_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_prime. ftsf_factor_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes = frm_prime_left_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_arbitrary_zero_valuesmobiusfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_arbitrary_zero_valuesmobiusfactorsparityeven. (mv_factor_count_arbitrary_zero_valuesmobiusfactors) = 2 * mv_even_half_arbitrary_zero_valuesmobiusfactorsparityeven) /\ ((mdc_positive_value_arbitrary_zero_values) = 2))) \/ (((exists mv_odd_half_arbitrary_zero_valuesmobiusfactorsparityodd. (mv_factor_count_arbitrary_zero_valuesmobiusfactors) = 2 * mv_odd_half_arbitrary_zero_valuesmobiusfactorsparityodd + 1) /\ ((mdc_positive_value_arbitrary_zero_values) = 1)))))))))))) -> ~(n=0) -> (exists pvs_le_gap_arbitrary_zero_bound. pvs_le_gap_arbitrary_zero_bound + (n) = (N)) -> ((((((~((n)=0)) /\ (exists dm_mask_table_arbitrary_zero_resultforward. ((((exists dst_positive_code_arbitrary_zero_resultforwardmasktable dst_positive_scale_arbitrary_zero_resultforwardmasktable dst_negative_code_arbitrary_zero_resultforwardmasktable dst_negative_scale_arbitrary_zero_resultforwardmasktable. (((dm_mask_table_arbitrary_zero_resultforward) = (((((dst_positive_code_arbitrary_zero_resultforwardmasktable) + (dst_positive_scale_arbitrary_zero_resultforwardmasktable)) * S ((dst_positive_code_arbitrary_zero_resultforwardmasktable) + (dst_positive_scale_arbitrary_zero_resultforwardmasktable)) + ((dst_positive_scale_arbitrary_zero_resultforwardmasktable) + (dst_positive_scale_arbitrary_zero_resultforwardmasktable))) + (((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)))) * S ((((dst_positive_code_arbitrary_zero_resultforwardmasktable) + (dst_positive_scale_arbitrary_zero_resultforwardmasktable)) * S ((dst_positive_code_arbitrary_zero_resultforwardmasktable) + (dst_positive_scale_arbitrary_zero_resultforwardmasktable)) + ((dst_positive_scale_arbitrary_zero_resultforwardmasktable) + (dst_positive_scale_arbitrary_zero_resultforwardmasktable))) + (((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)))) + ((((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable))) + (((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasktable) + (dst_negative_scale_arbitrary_zero_resultforwardmasktable)))))) /\ (forall dst_index_arbitrary_zero_resultforwardmasktable. (exists pvs_le_gap_arbitrary_zero_resultforwardmasktabledomain. pvs_le_gap_arbitrary_zero_resultforwardmasktabledomain + (dst_index_arbitrary_zero_resultforwardmasktable) = (n)) -> exists dst_positive_arbitrary_zero_resultforwardmasktable dst_negative_arbitrary_zero_resultforwardmasktable dst_value_arbitrary_zero_resultforwardmasktable. ((((exists ff_h_pvs_arbitrary_zero_resultforwardmasktableentrypositive. ff_h_pvs_arbitrary_zero_resultforwardmasktableentrypositive + S (dst_positive_arbitrary_zero_resultforwardmasktable) = S ((S (dst_index_arbitrary_zero_resultforwardmasktable)) * dst_positive_scale_arbitrary_zero_resultforwardmasktable)) /\ exists ff_q_pvs_arbitrary_zero_resultforwardmasktableentrypositive. dst_positive_code_arbitrary_zero_resultforwardmasktable = ff_q_pvs_arbitrary_zero_resultforwardmasktableentrypositive * S ((S (dst_index_arbitrary_zero_resultforwardmasktable)) * dst_positive_scale_arbitrary_zero_resultforwardmasktable) + (dst_positive_arbitrary_zero_resultforwardmasktable))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultforwardmasktableentrynegative. ff_h_pvs_arbitrary_zero_resultforwardmasktableentrynegative + S (dst_negative_arbitrary_zero_resultforwardmasktable) = S ((S (dst_index_arbitrary_zero_resultforwardmasktable)) * dst_negative_scale_arbitrary_zero_resultforwardmasktable)) /\ exists ff_q_pvs_arbitrary_zero_resultforwardmasktableentrynegative. dst_negative_code_arbitrary_zero_resultforwardmasktable = ff_q_pvs_arbitrary_zero_resultforwardmasktableentrynegative * S ((S (dst_index_arbitrary_zero_resultforwardmasktable)) * dst_negative_scale_arbitrary_zero_resultforwardmasktable) + (dst_negative_arbitrary_zero_resultforwardmasktable))) /\ (exists ge_balance_positive_arbitrary_zero_resultforwardmasktableentryvalue ge_balance_negative_arbitrary_zero_resultforwardmasktableentryvalue. (((((dst_value_arbitrary_zero_resultforwardmasktable) = 2 * (ge_balance_positive_arbitrary_zero_resultforwardmasktableentryvalue) /\ (ge_balance_negative_arbitrary_zero_resultforwardmasktableentryvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_resultforwardmasktableentryvaluedecode. (((dst_value_arbitrary_zero_resultforwardmasktable) = 2 * ge_signed_half_arbitrary_zero_resultforwardmasktableentryvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultforwardmasktableentryvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_resultforwardmasktableentryvalue) = S ge_signed_half_arbitrary_zero_resultforwardmasktableentryvaluedecode))) /\ ((dst_positive_arbitrary_zero_resultforwardmasktable) + ge_balance_negative_arbitrary_zero_resultforwardmasktableentryvalue = (dst_negative_arbitrary_zero_resultforwardmasktable) + ge_balance_positive_arbitrary_zero_resultforwardmasktableentryvalue))))))))) /\ (forall dm_index_arbitrary_zero_resultforwardmask dm_value_arbitrary_zero_resultforwardmask. (exists pvs_le_gap_arbitrary_zero_resultforwardmaskdomain. pvs_le_gap_arbitrary_zero_resultforwardmaskdomain + (dm_index_arbitrary_zero_resultforwardmask) = (n)) -> (exists dst_positive_code_arbitrary_zero_resultforwardmasklookup dst_positive_scale_arbitrary_zero_resultforwardmasklookup dst_negative_code_arbitrary_zero_resultforwardmasklookup dst_negative_scale_arbitrary_zero_resultforwardmasklookup dst_positive_arbitrary_zero_resultforwardmasklookup dst_negative_arbitrary_zero_resultforwardmasklookup. (((dm_mask_table_arbitrary_zero_resultforward) = (((((dst_positive_code_arbitrary_zero_resultforwardmasklookup) + (dst_positive_scale_arbitrary_zero_resultforwardmasklookup)) * S ((dst_positive_code_arbitrary_zero_resultforwardmasklookup) + (dst_positive_scale_arbitrary_zero_resultforwardmasklookup)) + ((dst_positive_scale_arbitrary_zero_resultforwardmasklookup) + (dst_positive_scale_arbitrary_zero_resultforwardmasklookup))) + (((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)))) * S ((((dst_positive_code_arbitrary_zero_resultforwardmasklookup) + (dst_positive_scale_arbitrary_zero_resultforwardmasklookup)) * S ((dst_positive_code_arbitrary_zero_resultforwardmasklookup) + (dst_positive_scale_arbitrary_zero_resultforwardmasklookup)) + ((dst_positive_scale_arbitrary_zero_resultforwardmasklookup) + (dst_positive_scale_arbitrary_zero_resultforwardmasklookup))) + (((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)))) + ((((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup))) + (((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) * S ((dst_negative_code_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) + ((dst_negative_scale_arbitrary_zero_resultforwardmasklookup) + (dst_negative_scale_arbitrary_zero_resultforwardmasklookup)))))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultforwardmasklookuppositive. ff_h_pvs_arbitrary_zero_resultforwardmasklookuppositive + S (dst_positive_arbitrary_zero_resultforwardmasklookup) = S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_positive_scale_arbitrary_zero_resultforwardmasklookup)) /\ exists ff_q_pvs_arbitrary_zero_resultforwardmasklookuppositive. dst_positive_code_arbitrary_zero_resultforwardmasklookup = ff_q_pvs_arbitrary_zero_resultforwardmasklookuppositive * S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_positive_scale_arbitrary_zero_resultforwardmasklookup) + (dst_positive_arbitrary_zero_resultforwardmasklookup))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultforwardmasklookupnegative. ff_h_pvs_arbitrary_zero_resultforwardmasklookupnegative + S (dst_negative_arbitrary_zero_resultforwardmasklookup) = S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_negative_scale_arbitrary_zero_resultforwardmasklookup)) /\ exists ff_q_pvs_arbitrary_zero_resultforwardmasklookupnegative. dst_negative_code_arbitrary_zero_resultforwardmasklookup = ff_q_pvs_arbitrary_zero_resultforwardmasklookupnegative * S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_negative_scale_arbitrary_zero_resultforwardmasklookup) + (dst_negative_arbitrary_zero_resultforwardmasklookup))) /\ (exists ge_balance_positive_arbitrary_zero_resultforwardmasklookupvalue ge_balance_negative_arbitrary_zero_resultforwardmasklookupvalue. (((((dm_value_arbitrary_zero_resultforwardmask) = 2 * (ge_balance_positive_arbitrary_zero_resultforwardmasklookupvalue) /\ (ge_balance_negative_arbitrary_zero_resultforwardmasklookupvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_resultforwardmasklookupvaluedecode. (((dm_value_arbitrary_zero_resultforwardmask) = 2 * ge_signed_half_arbitrary_zero_resultforwardmasklookupvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultforwardmasklookupvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_resultforwardmasklookupvalue) = S ge_signed_half_arbitrary_zero_resultforwardmasklookupvaluedecode))) /\ ((dst_positive_arbitrary_zero_resultforwardmasklookup) + ge_balance_negative_arbitrary_zero_resultforwardmasklookupvalue = (dst_negative_arbitrary_zero_resultforwardmasklookup) + ge_balance_positive_arbitrary_zero_resultforwardmasklookupvalue))))))))) -> ((((~((dm_index_arbitrary_zero_resultforwardmask)=0)) /\ (exists dm_quotient_arbitrary_zero_resultforwardmaskentry. (((n)=(dm_index_arbitrary_zero_resultforwardmask)*dm_quotient_arbitrary_zero_resultforwardmaskentry) /\ (exists dst_positive_code_arbitrary_zero_resultforwardmaskentryinput dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput dst_negative_code_arbitrary_zero_resultforwardmaskentryinput dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput dst_positive_arbitrary_zero_resultforwardmaskentryinput dst_negative_arbitrary_zero_resultforwardmaskentryinput. (((F) = (((((dst_positive_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput)) * S ((dst_positive_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput)) + ((dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput))) + (((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)))) * S ((((dst_positive_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput)) * S ((dst_positive_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput)) + ((dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput))) + (((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)))) + ((((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput))) + (((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)))))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultforwardmaskentryinputpositive. ff_h_pvs_arbitrary_zero_resultforwardmaskentryinputpositive + S (dst_positive_arbitrary_zero_resultforwardmaskentryinput) = S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput)) /\ exists ff_q_pvs_arbitrary_zero_resultforwardmaskentryinputpositive. dst_positive_code_arbitrary_zero_resultforwardmaskentryinput = ff_q_pvs_arbitrary_zero_resultforwardmaskentryinputpositive * S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_positive_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_positive_arbitrary_zero_resultforwardmaskentryinput))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultforwardmaskentryinputnegative. ff_h_pvs_arbitrary_zero_resultforwardmaskentryinputnegative + S (dst_negative_arbitrary_zero_resultforwardmaskentryinput) = S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput)) /\ exists ff_q_pvs_arbitrary_zero_resultforwardmaskentryinputnegative. dst_negative_code_arbitrary_zero_resultforwardmaskentryinput = ff_q_pvs_arbitrary_zero_resultforwardmaskentryinputnegative * S ((S (dm_index_arbitrary_zero_resultforwardmask)) * dst_negative_scale_arbitrary_zero_resultforwardmaskentryinput) + (dst_negative_arbitrary_zero_resultforwardmaskentryinput))) /\ (exists ge_balance_positive_arbitrary_zero_resultforwardmaskentryinputvalue ge_balance_negative_arbitrary_zero_resultforwardmaskentryinputvalue. (((((dm_value_arbitrary_zero_resultforwardmask) = 2 * (ge_balance_positive_arbitrary_zero_resultforwardmaskentryinputvalue) /\ (ge_balance_negative_arbitrary_zero_resultforwardmaskentryinputvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_resultforwardmaskentryinputvaluedecode. (((dm_value_arbitrary_zero_resultforwardmask) = 2 * ge_signed_half_arbitrary_zero_resultforwardmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultforwardmaskentryinputvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_resultforwardmaskentryinputvalue) = S ge_signed_half_arbitrary_zero_resultforwardmaskentryinputvaluedecode))) /\ ((dst_positive_arbitrary_zero_resultforwardmaskentryinput) + ge_balance_negative_arbitrary_zero_resultforwardmaskentryinputvalue = (dst_negative_arbitrary_zero_resultforwardmaskentryinput) + ge_balance_positive_arbitrary_zero_resultforwardmaskentryinputvalue))))))))))))) \/ ((((dm_index_arbitrary_zero_resultforwardmask)=0 \/ ~(exists pvs_factor_arbitrary_zero_resultforwardmaskentrynondivisor. (n) = (dm_index_arbitrary_zero_resultforwardmask) * pvs_factor_arbitrary_zero_resultforwardmaskentrynondivisor)) /\ ((dm_value_arbitrary_zero_resultforwardmask)=0))))))) /\ (exists dst_positive_code_arbitrary_zero_resultforwardfold dst_positive_scale_arbitrary_zero_resultforwardfold dst_negative_code_arbitrary_zero_resultforwardfold dst_negative_scale_arbitrary_zero_resultforwardfold dst_positive_sum_arbitrary_zero_resultforwardfold dst_negative_sum_arbitrary_zero_resultforwardfold. (((dm_mask_table_arbitrary_zero_resultforward) = (((((dst_positive_code_arbitrary_zero_resultforwardfold) + (dst_positive_scale_arbitrary_zero_resultforwardfold)) * S ((dst_positive_code_arbitrary_zero_resultforwardfold) + (dst_positive_scale_arbitrary_zero_resultforwardfold)) + ((dst_positive_scale_arbitrary_zero_resultforwardfold) + (dst_positive_scale_arbitrary_zero_resultforwardfold))) + (((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) * S ((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) + ((dst_negative_scale_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)))) * S ((((dst_positive_code_arbitrary_zero_resultforwardfold) + (dst_positive_scale_arbitrary_zero_resultforwardfold)) * S ((dst_positive_code_arbitrary_zero_resultforwardfold) + (dst_positive_scale_arbitrary_zero_resultforwardfold)) + ((dst_positive_scale_arbitrary_zero_resultforwardfold) + (dst_positive_scale_arbitrary_zero_resultforwardfold))) + (((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) * S ((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) + ((dst_negative_scale_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)))) + ((((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) * S ((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) + ((dst_negative_scale_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold))) + (((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) * S ((dst_negative_code_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)) + ((dst_negative_scale_arbitrary_zero_resultforwardfold) + (dst_negative_scale_arbitrary_zero_resultforwardfold)))))) /\ (((exists fs_u_dst_arbitrary_zero_resultforwardfoldpositive fs_v_dst_arbitrary_zero_resultforwardfoldpositive. ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_start. fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_start. fs_u_dst_arbitrary_zero_resultforwardfoldpositive = fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_start * S ((S (0)) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive) + (0))) /\ ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_terminal. fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_terminal + S (dst_positive_sum_arbitrary_zero_resultforwardfold) = S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_terminal. fs_u_dst_arbitrary_zero_resultforwardfoldpositive = fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive) + (dst_positive_sum_arbitrary_zero_resultforwardfold))) /\ forall fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps. (exists fs_lt_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_bound. fs_lt_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_bound + S fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps = S (n)) -> exists fs_a_dst_arbitrary_zero_resultforwardfoldpositive_body_steps fs_r_dst_arbitrary_zero_resultforwardfoldpositive_body_steps fs_s_dst_arbitrary_zero_resultforwardfoldpositive_body_steps. ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_summand. fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_summand + S (fs_a_dst_arbitrary_zero_resultforwardfoldpositive_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)) * dst_positive_scale_arbitrary_zero_resultforwardfold)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_summand. dst_positive_code_arbitrary_zero_resultforwardfold = fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_summand * S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)) * dst_positive_scale_arbitrary_zero_resultforwardfold) + (fs_a_dst_arbitrary_zero_resultforwardfoldpositive_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_partial. fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_partial + S (fs_r_dst_arbitrary_zero_resultforwardfoldpositive_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_partial. fs_u_dst_arbitrary_zero_resultforwardfoldpositive = fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_partial * S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive) + (fs_r_dst_arbitrary_zero_resultforwardfoldpositive_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_successor. fs_h_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_successor + S (fs_s_dst_arbitrary_zero_resultforwardfoldpositive_body_steps) = S ((S (S fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_successor. fs_u_dst_arbitrary_zero_resultforwardfoldpositive = fs_q_dst_arbitrary_zero_resultforwardfoldpositive_body_steps_successor * S ((S (S fs_i_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldpositive) + (fs_s_dst_arbitrary_zero_resultforwardfoldpositive_body_steps))) /\ fs_s_dst_arbitrary_zero_resultforwardfoldpositive_body_steps = fs_r_dst_arbitrary_zero_resultforwardfoldpositive_body_steps + fs_a_dst_arbitrary_zero_resultforwardfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_arbitrary_zero_resultforwardfoldnegative fs_v_dst_arbitrary_zero_resultforwardfoldnegative. ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_start. fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_start. fs_u_dst_arbitrary_zero_resultforwardfoldnegative = fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_start * S ((S (0)) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative) + (0))) /\ ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_terminal. fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_terminal + S (dst_negative_sum_arbitrary_zero_resultforwardfold) = S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_terminal. fs_u_dst_arbitrary_zero_resultforwardfoldnegative = fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative) + (dst_negative_sum_arbitrary_zero_resultforwardfold))) /\ forall fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps. (exists fs_lt_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_bound. fs_lt_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_bound + S fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps = S (n)) -> exists fs_a_dst_arbitrary_zero_resultforwardfoldnegative_body_steps fs_r_dst_arbitrary_zero_resultforwardfoldnegative_body_steps fs_s_dst_arbitrary_zero_resultforwardfoldnegative_body_steps. ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_summand. fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_summand + S (fs_a_dst_arbitrary_zero_resultforwardfoldnegative_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)) * dst_negative_scale_arbitrary_zero_resultforwardfold)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_summand. dst_negative_code_arbitrary_zero_resultforwardfold = fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_summand * S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)) * dst_negative_scale_arbitrary_zero_resultforwardfold) + (fs_a_dst_arbitrary_zero_resultforwardfoldnegative_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_partial. fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_partial + S (fs_r_dst_arbitrary_zero_resultforwardfoldnegative_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_partial. fs_u_dst_arbitrary_zero_resultforwardfoldnegative = fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_partial * S ((S (fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative) + (fs_r_dst_arbitrary_zero_resultforwardfoldnegative_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_successor. fs_h_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_successor + S (fs_s_dst_arbitrary_zero_resultforwardfoldnegative_body_steps) = S ((S (S fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_successor. fs_u_dst_arbitrary_zero_resultforwardfoldnegative = fs_q_dst_arbitrary_zero_resultforwardfoldnegative_body_steps_successor * S ((S (S fs_i_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultforwardfoldnegative) + (fs_s_dst_arbitrary_zero_resultforwardfoldnegative_body_steps))) /\ fs_s_dst_arbitrary_zero_resultforwardfoldnegative_body_steps = fs_r_dst_arbitrary_zero_resultforwardfoldnegative_body_steps + fs_a_dst_arbitrary_zero_resultforwardfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_arbitrary_zero_resultforwardfoldresult ge_balance_negative_arbitrary_zero_resultforwardfoldresult. (((((z) = 2 * (ge_balance_positive_arbitrary_zero_resultforwardfoldresult) /\ (ge_balance_negative_arbitrary_zero_resultforwardfoldresult) = 0) \/ exists ge_signed_half_arbitrary_zero_resultforwardfoldresultdecode. (((z) = 2 * ge_signed_half_arbitrary_zero_resultforwardfoldresultdecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultforwardfoldresult) = 0) /\ (ge_balance_negative_arbitrary_zero_resultforwardfoldresult) = S ge_signed_half_arbitrary_zero_resultforwardfoldresultdecode))) /\ ((dst_positive_sum_arbitrary_zero_resultforwardfold) + ge_balance_negative_arbitrary_zero_resultforwardfoldresult = (dst_negative_sum_arbitrary_zero_resultforwardfold) + ge_balance_positive_arbitrary_zero_resultforwardfoldresult))))))))))))) -> (((n)=1 /\ (z)=2) \/ (~((n)=1) /\ (z)=0))) /\ ((((n)=1 /\ (z)=2) \/ (~((n)=1) /\ (z)=0)) -> (((~((n)=0)) /\ (exists dm_mask_table_arbitrary_zero_resultreverse. ((((exists dst_positive_code_arbitrary_zero_resultreversemasktable dst_positive_scale_arbitrary_zero_resultreversemasktable dst_negative_code_arbitrary_zero_resultreversemasktable dst_negative_scale_arbitrary_zero_resultreversemasktable. (((dm_mask_table_arbitrary_zero_resultreverse) = (((((dst_positive_code_arbitrary_zero_resultreversemasktable) + (dst_positive_scale_arbitrary_zero_resultreversemasktable)) * S ((dst_positive_code_arbitrary_zero_resultreversemasktable) + (dst_positive_scale_arbitrary_zero_resultreversemasktable)) + ((dst_positive_scale_arbitrary_zero_resultreversemasktable) + (dst_positive_scale_arbitrary_zero_resultreversemasktable))) + (((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) * S ((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) + ((dst_negative_scale_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)))) * S ((((dst_positive_code_arbitrary_zero_resultreversemasktable) + (dst_positive_scale_arbitrary_zero_resultreversemasktable)) * S ((dst_positive_code_arbitrary_zero_resultreversemasktable) + (dst_positive_scale_arbitrary_zero_resultreversemasktable)) + ((dst_positive_scale_arbitrary_zero_resultreversemasktable) + (dst_positive_scale_arbitrary_zero_resultreversemasktable))) + (((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) * S ((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) + ((dst_negative_scale_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)))) + ((((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) * S ((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) + ((dst_negative_scale_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable))) + (((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) * S ((dst_negative_code_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)) + ((dst_negative_scale_arbitrary_zero_resultreversemasktable) + (dst_negative_scale_arbitrary_zero_resultreversemasktable)))))) /\ (forall dst_index_arbitrary_zero_resultreversemasktable. (exists pvs_le_gap_arbitrary_zero_resultreversemasktabledomain. pvs_le_gap_arbitrary_zero_resultreversemasktabledomain + (dst_index_arbitrary_zero_resultreversemasktable) = (n)) -> exists dst_positive_arbitrary_zero_resultreversemasktable dst_negative_arbitrary_zero_resultreversemasktable dst_value_arbitrary_zero_resultreversemasktable. ((((exists ff_h_pvs_arbitrary_zero_resultreversemasktableentrypositive. ff_h_pvs_arbitrary_zero_resultreversemasktableentrypositive + S (dst_positive_arbitrary_zero_resultreversemasktable) = S ((S (dst_index_arbitrary_zero_resultreversemasktable)) * dst_positive_scale_arbitrary_zero_resultreversemasktable)) /\ exists ff_q_pvs_arbitrary_zero_resultreversemasktableentrypositive. dst_positive_code_arbitrary_zero_resultreversemasktable = ff_q_pvs_arbitrary_zero_resultreversemasktableentrypositive * S ((S (dst_index_arbitrary_zero_resultreversemasktable)) * dst_positive_scale_arbitrary_zero_resultreversemasktable) + (dst_positive_arbitrary_zero_resultreversemasktable))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultreversemasktableentrynegative. ff_h_pvs_arbitrary_zero_resultreversemasktableentrynegative + S (dst_negative_arbitrary_zero_resultreversemasktable) = S ((S (dst_index_arbitrary_zero_resultreversemasktable)) * dst_negative_scale_arbitrary_zero_resultreversemasktable)) /\ exists ff_q_pvs_arbitrary_zero_resultreversemasktableentrynegative. dst_negative_code_arbitrary_zero_resultreversemasktable = ff_q_pvs_arbitrary_zero_resultreversemasktableentrynegative * S ((S (dst_index_arbitrary_zero_resultreversemasktable)) * dst_negative_scale_arbitrary_zero_resultreversemasktable) + (dst_negative_arbitrary_zero_resultreversemasktable))) /\ (exists ge_balance_positive_arbitrary_zero_resultreversemasktableentryvalue ge_balance_negative_arbitrary_zero_resultreversemasktableentryvalue. (((((dst_value_arbitrary_zero_resultreversemasktable) = 2 * (ge_balance_positive_arbitrary_zero_resultreversemasktableentryvalue) /\ (ge_balance_negative_arbitrary_zero_resultreversemasktableentryvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_resultreversemasktableentryvaluedecode. (((dst_value_arbitrary_zero_resultreversemasktable) = 2 * ge_signed_half_arbitrary_zero_resultreversemasktableentryvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultreversemasktableentryvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_resultreversemasktableentryvalue) = S ge_signed_half_arbitrary_zero_resultreversemasktableentryvaluedecode))) /\ ((dst_positive_arbitrary_zero_resultreversemasktable) + ge_balance_negative_arbitrary_zero_resultreversemasktableentryvalue = (dst_negative_arbitrary_zero_resultreversemasktable) + ge_balance_positive_arbitrary_zero_resultreversemasktableentryvalue))))))))) /\ (forall dm_index_arbitrary_zero_resultreversemask dm_value_arbitrary_zero_resultreversemask. (exists pvs_le_gap_arbitrary_zero_resultreversemaskdomain. pvs_le_gap_arbitrary_zero_resultreversemaskdomain + (dm_index_arbitrary_zero_resultreversemask) = (n)) -> (exists dst_positive_code_arbitrary_zero_resultreversemasklookup dst_positive_scale_arbitrary_zero_resultreversemasklookup dst_negative_code_arbitrary_zero_resultreversemasklookup dst_negative_scale_arbitrary_zero_resultreversemasklookup dst_positive_arbitrary_zero_resultreversemasklookup dst_negative_arbitrary_zero_resultreversemasklookup. (((dm_mask_table_arbitrary_zero_resultreverse) = (((((dst_positive_code_arbitrary_zero_resultreversemasklookup) + (dst_positive_scale_arbitrary_zero_resultreversemasklookup)) * S ((dst_positive_code_arbitrary_zero_resultreversemasklookup) + (dst_positive_scale_arbitrary_zero_resultreversemasklookup)) + ((dst_positive_scale_arbitrary_zero_resultreversemasklookup) + (dst_positive_scale_arbitrary_zero_resultreversemasklookup))) + (((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) * S ((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) + ((dst_negative_scale_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)))) * S ((((dst_positive_code_arbitrary_zero_resultreversemasklookup) + (dst_positive_scale_arbitrary_zero_resultreversemasklookup)) * S ((dst_positive_code_arbitrary_zero_resultreversemasklookup) + (dst_positive_scale_arbitrary_zero_resultreversemasklookup)) + ((dst_positive_scale_arbitrary_zero_resultreversemasklookup) + (dst_positive_scale_arbitrary_zero_resultreversemasklookup))) + (((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) * S ((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) + ((dst_negative_scale_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)))) + ((((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) * S ((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) + ((dst_negative_scale_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup))) + (((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) * S ((dst_negative_code_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)) + ((dst_negative_scale_arbitrary_zero_resultreversemasklookup) + (dst_negative_scale_arbitrary_zero_resultreversemasklookup)))))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultreversemasklookuppositive. ff_h_pvs_arbitrary_zero_resultreversemasklookuppositive + S (dst_positive_arbitrary_zero_resultreversemasklookup) = S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_positive_scale_arbitrary_zero_resultreversemasklookup)) /\ exists ff_q_pvs_arbitrary_zero_resultreversemasklookuppositive. dst_positive_code_arbitrary_zero_resultreversemasklookup = ff_q_pvs_arbitrary_zero_resultreversemasklookuppositive * S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_positive_scale_arbitrary_zero_resultreversemasklookup) + (dst_positive_arbitrary_zero_resultreversemasklookup))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultreversemasklookupnegative. ff_h_pvs_arbitrary_zero_resultreversemasklookupnegative + S (dst_negative_arbitrary_zero_resultreversemasklookup) = S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_negative_scale_arbitrary_zero_resultreversemasklookup)) /\ exists ff_q_pvs_arbitrary_zero_resultreversemasklookupnegative. dst_negative_code_arbitrary_zero_resultreversemasklookup = ff_q_pvs_arbitrary_zero_resultreversemasklookupnegative * S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_negative_scale_arbitrary_zero_resultreversemasklookup) + (dst_negative_arbitrary_zero_resultreversemasklookup))) /\ (exists ge_balance_positive_arbitrary_zero_resultreversemasklookupvalue ge_balance_negative_arbitrary_zero_resultreversemasklookupvalue. (((((dm_value_arbitrary_zero_resultreversemask) = 2 * (ge_balance_positive_arbitrary_zero_resultreversemasklookupvalue) /\ (ge_balance_negative_arbitrary_zero_resultreversemasklookupvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_resultreversemasklookupvaluedecode. (((dm_value_arbitrary_zero_resultreversemask) = 2 * ge_signed_half_arbitrary_zero_resultreversemasklookupvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultreversemasklookupvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_resultreversemasklookupvalue) = S ge_signed_half_arbitrary_zero_resultreversemasklookupvaluedecode))) /\ ((dst_positive_arbitrary_zero_resultreversemasklookup) + ge_balance_negative_arbitrary_zero_resultreversemasklookupvalue = (dst_negative_arbitrary_zero_resultreversemasklookup) + ge_balance_positive_arbitrary_zero_resultreversemasklookupvalue))))))))) -> ((((~((dm_index_arbitrary_zero_resultreversemask)=0)) /\ (exists dm_quotient_arbitrary_zero_resultreversemaskentry. (((n)=(dm_index_arbitrary_zero_resultreversemask)*dm_quotient_arbitrary_zero_resultreversemaskentry) /\ (exists dst_positive_code_arbitrary_zero_resultreversemaskentryinput dst_positive_scale_arbitrary_zero_resultreversemaskentryinput dst_negative_code_arbitrary_zero_resultreversemaskentryinput dst_negative_scale_arbitrary_zero_resultreversemaskentryinput dst_positive_arbitrary_zero_resultreversemaskentryinput dst_negative_arbitrary_zero_resultreversemaskentryinput. (((F) = (((((dst_positive_code_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_scale_arbitrary_zero_resultreversemaskentryinput)) * S ((dst_positive_code_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_scale_arbitrary_zero_resultreversemaskentryinput)) + ((dst_positive_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_scale_arbitrary_zero_resultreversemaskentryinput))) + (((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)))) * S ((((dst_positive_code_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_scale_arbitrary_zero_resultreversemaskentryinput)) * S ((dst_positive_code_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_scale_arbitrary_zero_resultreversemaskentryinput)) + ((dst_positive_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_scale_arbitrary_zero_resultreversemaskentryinput))) + (((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)))) + ((((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput))) + (((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) * S ((dst_negative_code_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) + ((dst_negative_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)))))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultreversemaskentryinputpositive. ff_h_pvs_arbitrary_zero_resultreversemaskentryinputpositive + S (dst_positive_arbitrary_zero_resultreversemaskentryinput) = S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_positive_scale_arbitrary_zero_resultreversemaskentryinput)) /\ exists ff_q_pvs_arbitrary_zero_resultreversemaskentryinputpositive. dst_positive_code_arbitrary_zero_resultreversemaskentryinput = ff_q_pvs_arbitrary_zero_resultreversemaskentryinputpositive * S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_positive_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_positive_arbitrary_zero_resultreversemaskentryinput))) /\ (((((exists ff_h_pvs_arbitrary_zero_resultreversemaskentryinputnegative. ff_h_pvs_arbitrary_zero_resultreversemaskentryinputnegative + S (dst_negative_arbitrary_zero_resultreversemaskentryinput) = S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_negative_scale_arbitrary_zero_resultreversemaskentryinput)) /\ exists ff_q_pvs_arbitrary_zero_resultreversemaskentryinputnegative. dst_negative_code_arbitrary_zero_resultreversemaskentryinput = ff_q_pvs_arbitrary_zero_resultreversemaskentryinputnegative * S ((S (dm_index_arbitrary_zero_resultreversemask)) * dst_negative_scale_arbitrary_zero_resultreversemaskentryinput) + (dst_negative_arbitrary_zero_resultreversemaskentryinput))) /\ (exists ge_balance_positive_arbitrary_zero_resultreversemaskentryinputvalue ge_balance_negative_arbitrary_zero_resultreversemaskentryinputvalue. (((((dm_value_arbitrary_zero_resultreversemask) = 2 * (ge_balance_positive_arbitrary_zero_resultreversemaskentryinputvalue) /\ (ge_balance_negative_arbitrary_zero_resultreversemaskentryinputvalue) = 0) \/ exists ge_signed_half_arbitrary_zero_resultreversemaskentryinputvaluedecode. (((dm_value_arbitrary_zero_resultreversemask) = 2 * ge_signed_half_arbitrary_zero_resultreversemaskentryinputvaluedecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultreversemaskentryinputvalue) = 0) /\ (ge_balance_negative_arbitrary_zero_resultreversemaskentryinputvalue) = S ge_signed_half_arbitrary_zero_resultreversemaskentryinputvaluedecode))) /\ ((dst_positive_arbitrary_zero_resultreversemaskentryinput) + ge_balance_negative_arbitrary_zero_resultreversemaskentryinputvalue = (dst_negative_arbitrary_zero_resultreversemaskentryinput) + ge_balance_positive_arbitrary_zero_resultreversemaskentryinputvalue))))))))))))) \/ ((((dm_index_arbitrary_zero_resultreversemask)=0 \/ ~(exists pvs_factor_arbitrary_zero_resultreversemaskentrynondivisor. (n) = (dm_index_arbitrary_zero_resultreversemask) * pvs_factor_arbitrary_zero_resultreversemaskentrynondivisor)) /\ ((dm_value_arbitrary_zero_resultreversemask)=0))))))) /\ (exists dst_positive_code_arbitrary_zero_resultreversefold dst_positive_scale_arbitrary_zero_resultreversefold dst_negative_code_arbitrary_zero_resultreversefold dst_negative_scale_arbitrary_zero_resultreversefold dst_positive_sum_arbitrary_zero_resultreversefold dst_negative_sum_arbitrary_zero_resultreversefold. (((dm_mask_table_arbitrary_zero_resultreverse) = (((((dst_positive_code_arbitrary_zero_resultreversefold) + (dst_positive_scale_arbitrary_zero_resultreversefold)) * S ((dst_positive_code_arbitrary_zero_resultreversefold) + (dst_positive_scale_arbitrary_zero_resultreversefold)) + ((dst_positive_scale_arbitrary_zero_resultreversefold) + (dst_positive_scale_arbitrary_zero_resultreversefold))) + (((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) * S ((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) + ((dst_negative_scale_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)))) * S ((((dst_positive_code_arbitrary_zero_resultreversefold) + (dst_positive_scale_arbitrary_zero_resultreversefold)) * S ((dst_positive_code_arbitrary_zero_resultreversefold) + (dst_positive_scale_arbitrary_zero_resultreversefold)) + ((dst_positive_scale_arbitrary_zero_resultreversefold) + (dst_positive_scale_arbitrary_zero_resultreversefold))) + (((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) * S ((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) + ((dst_negative_scale_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)))) + ((((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) * S ((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) + ((dst_negative_scale_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold))) + (((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) * S ((dst_negative_code_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)) + ((dst_negative_scale_arbitrary_zero_resultreversefold) + (dst_negative_scale_arbitrary_zero_resultreversefold)))))) /\ (((exists fs_u_dst_arbitrary_zero_resultreversefoldpositive fs_v_dst_arbitrary_zero_resultreversefoldpositive. ((((exists fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_start. fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_arbitrary_zero_resultreversefoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_start. fs_u_dst_arbitrary_zero_resultreversefoldpositive = fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_start * S ((S (0)) * fs_v_dst_arbitrary_zero_resultreversefoldpositive) + (0))) /\ ((((exists fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_terminal. fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_terminal + S (dst_positive_sum_arbitrary_zero_resultreversefold) = S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultreversefoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_terminal. fs_u_dst_arbitrary_zero_resultreversefoldpositive = fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultreversefoldpositive) + (dst_positive_sum_arbitrary_zero_resultreversefold))) /\ forall fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps. (exists fs_lt_dst_arbitrary_zero_resultreversefoldpositive_body_steps_bound. fs_lt_dst_arbitrary_zero_resultreversefoldpositive_body_steps_bound + S fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps = S (n)) -> exists fs_a_dst_arbitrary_zero_resultreversefoldpositive_body_steps fs_r_dst_arbitrary_zero_resultreversefoldpositive_body_steps fs_s_dst_arbitrary_zero_resultreversefoldpositive_body_steps. ((((exists fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_steps_summand. fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_steps_summand + S (fs_a_dst_arbitrary_zero_resultreversefoldpositive_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps)) * dst_positive_scale_arbitrary_zero_resultreversefold)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_steps_summand. dst_positive_code_arbitrary_zero_resultreversefold = fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_steps_summand * S ((S (fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps)) * dst_positive_scale_arbitrary_zero_resultreversefold) + (fs_a_dst_arbitrary_zero_resultreversefoldpositive_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_steps_partial. fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_steps_partial + S (fs_r_dst_arbitrary_zero_resultreversefoldpositive_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_steps_partial. fs_u_dst_arbitrary_zero_resultreversefoldpositive = fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_steps_partial * S ((S (fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldpositive) + (fs_r_dst_arbitrary_zero_resultreversefoldpositive_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_steps_successor. fs_h_dst_arbitrary_zero_resultreversefoldpositive_body_steps_successor + S (fs_s_dst_arbitrary_zero_resultreversefoldpositive_body_steps) = S ((S (S fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldpositive)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_steps_successor. fs_u_dst_arbitrary_zero_resultreversefoldpositive = fs_q_dst_arbitrary_zero_resultreversefoldpositive_body_steps_successor * S ((S (S fs_i_dst_arbitrary_zero_resultreversefoldpositive_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldpositive) + (fs_s_dst_arbitrary_zero_resultreversefoldpositive_body_steps))) /\ fs_s_dst_arbitrary_zero_resultreversefoldpositive_body_steps = fs_r_dst_arbitrary_zero_resultreversefoldpositive_body_steps + fs_a_dst_arbitrary_zero_resultreversefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_arbitrary_zero_resultreversefoldnegative fs_v_dst_arbitrary_zero_resultreversefoldnegative. ((((exists fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_start. fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_arbitrary_zero_resultreversefoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_start. fs_u_dst_arbitrary_zero_resultreversefoldnegative = fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_start * S ((S (0)) * fs_v_dst_arbitrary_zero_resultreversefoldnegative) + (0))) /\ ((((exists fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_terminal. fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_terminal + S (dst_negative_sum_arbitrary_zero_resultreversefold) = S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultreversefoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_terminal. fs_u_dst_arbitrary_zero_resultreversefoldnegative = fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_arbitrary_zero_resultreversefoldnegative) + (dst_negative_sum_arbitrary_zero_resultreversefold))) /\ forall fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps. (exists fs_lt_dst_arbitrary_zero_resultreversefoldnegative_body_steps_bound. fs_lt_dst_arbitrary_zero_resultreversefoldnegative_body_steps_bound + S fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps = S (n)) -> exists fs_a_dst_arbitrary_zero_resultreversefoldnegative_body_steps fs_r_dst_arbitrary_zero_resultreversefoldnegative_body_steps fs_s_dst_arbitrary_zero_resultreversefoldnegative_body_steps. ((((exists fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_steps_summand. fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_steps_summand + S (fs_a_dst_arbitrary_zero_resultreversefoldnegative_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps)) * dst_negative_scale_arbitrary_zero_resultreversefold)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_steps_summand. dst_negative_code_arbitrary_zero_resultreversefold = fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_steps_summand * S ((S (fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps)) * dst_negative_scale_arbitrary_zero_resultreversefold) + (fs_a_dst_arbitrary_zero_resultreversefoldnegative_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_steps_partial. fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_steps_partial + S (fs_r_dst_arbitrary_zero_resultreversefoldnegative_body_steps) = S ((S (fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_steps_partial. fs_u_dst_arbitrary_zero_resultreversefoldnegative = fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_steps_partial * S ((S (fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldnegative) + (fs_r_dst_arbitrary_zero_resultreversefoldnegative_body_steps))) /\ ((((exists fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_steps_successor. fs_h_dst_arbitrary_zero_resultreversefoldnegative_body_steps_successor + S (fs_s_dst_arbitrary_zero_resultreversefoldnegative_body_steps) = S ((S (S fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldnegative)) /\ exists fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_steps_successor. fs_u_dst_arbitrary_zero_resultreversefoldnegative = fs_q_dst_arbitrary_zero_resultreversefoldnegative_body_steps_successor * S ((S (S fs_i_dst_arbitrary_zero_resultreversefoldnegative_body_steps)) * fs_v_dst_arbitrary_zero_resultreversefoldnegative) + (fs_s_dst_arbitrary_zero_resultreversefoldnegative_body_steps))) /\ fs_s_dst_arbitrary_zero_resultreversefoldnegative_body_steps = fs_r_dst_arbitrary_zero_resultreversefoldnegative_body_steps + fs_a_dst_arbitrary_zero_resultreversefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_arbitrary_zero_resultreversefoldresult ge_balance_negative_arbitrary_zero_resultreversefoldresult. (((((z) = 2 * (ge_balance_positive_arbitrary_zero_resultreversefoldresult) /\ (ge_balance_negative_arbitrary_zero_resultreversefoldresult) = 0) \/ exists ge_signed_half_arbitrary_zero_resultreversefoldresultdecode. (((z) = 2 * ge_signed_half_arbitrary_zero_resultreversefoldresultdecode + 1 /\ (ge_balance_positive_arbitrary_zero_resultreversefoldresult) = 0) /\ (ge_balance_negative_arbitrary_zero_resultreversefoldresult) = S ge_signed_half_arbitrary_zero_resultreversefoldresultdecode))) /\ ((dst_positive_sum_arbitrary_zero_resultreversefold) + ge_balance_negative_arbitrary_zero_resultreversefoldresult = (dst_negative_sum_arbitrary_zero_resultreversefold) + ge_balance_positive_arbitrary_zero_resultreversefoldresult))))))))))))))))