mobius_constant_one_convolution_delta

forall N M U E. (((exists dst_positive_code_mu_one_mobiustable dst_positive_scale_mu_one_mobiustable dst_negative_code_mu_one_mobiustable dst_negative_scale_mu_one_mobiustable. (((M) = (((((dst_positive_code_mu_one_mobiustable) + (dst_positive_scale_mu_one_mobiustable)) * S ((dst_positive_code_mu_one_mobiustable) + (dst_positive_scale_mu_one_mobiustable)) + ((dst_positive_scale_mu_one_mobiustable) + (dst_positive_scale_mu_one_mobiustable))) + (((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) * S ((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) + ((dst_negative_scale_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)))) * S ((((dst_positive_code_mu_one_mobiustable) + (dst_positive_scale_mu_one_mobiustable)) * S ((dst_positive_code_mu_one_mobiustable) + (dst_positive_scale_mu_one_mobiustable)) + ((dst_positive_scale_mu_one_mobiustable) + (dst_positive_scale_mu_one_mobiustable))) + (((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) * S ((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) + ((dst_negative_scale_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)))) + ((((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) * S ((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) + ((dst_negative_scale_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable))) + (((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) * S ((dst_negative_code_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)) + ((dst_negative_scale_mu_one_mobiustable) + (dst_negative_scale_mu_one_mobiustable)))))) /\ (forall dst_index_mu_one_mobiustable. (exists pvs_le_gap_mu_one_mobiustabledomain. pvs_le_gap_mu_one_mobiustabledomain + (dst_index_mu_one_mobiustable) = (N)) -> exists dst_positive_mu_one_mobiustable dst_negative_mu_one_mobiustable dst_value_mu_one_mobiustable. ((((exists ff_h_pvs_mu_one_mobiustableentrypositive. ff_h_pvs_mu_one_mobiustableentrypositive + S (dst_positive_mu_one_mobiustable) = S ((S (dst_index_mu_one_mobiustable)) * dst_positive_scale_mu_one_mobiustable)) /\ exists ff_q_pvs_mu_one_mobiustableentrypositive. dst_positive_code_mu_one_mobiustable = ff_q_pvs_mu_one_mobiustableentrypositive * S ((S (dst_index_mu_one_mobiustable)) * dst_positive_scale_mu_one_mobiustable) + (dst_positive_mu_one_mobiustable))) /\ (((((exists ff_h_pvs_mu_one_mobiustableentrynegative. ff_h_pvs_mu_one_mobiustableentrynegative + S (dst_negative_mu_one_mobiustable) = S ((S (dst_index_mu_one_mobiustable)) * dst_negative_scale_mu_one_mobiustable)) /\ exists ff_q_pvs_mu_one_mobiustableentrynegative. dst_negative_code_mu_one_mobiustable = ff_q_pvs_mu_one_mobiustableentrynegative * S ((S (dst_index_mu_one_mobiustable)) * dst_negative_scale_mu_one_mobiustable) + (dst_negative_mu_one_mobiustable))) /\ (exists ge_balance_positive_mu_one_mobiustableentryvalue ge_balance_negative_mu_one_mobiustableentryvalue. (((((dst_value_mu_one_mobiustable) = 2 * (ge_balance_positive_mu_one_mobiustableentryvalue) /\ (ge_balance_negative_mu_one_mobiustableentryvalue) = 0) \/ exists ge_signed_half_mu_one_mobiustableentryvaluedecode. (((dst_value_mu_one_mobiustable) = 2 * ge_signed_half_mu_one_mobiustableentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_mobiustableentryvalue) = 0) /\ (ge_balance_negative_mu_one_mobiustableentryvalue) = S ge_signed_half_mu_one_mobiustableentryvaluedecode))) /\ ((dst_positive_mu_one_mobiustable) + ge_balance_negative_mu_one_mobiustableentryvalue = (dst_negative_mu_one_mobiustable) + ge_balance_positive_mu_one_mobiustableentryvalue))))))))) /\ (((exists dst_positive_code_mu_one_mobiuszero dst_positive_scale_mu_one_mobiuszero dst_negative_code_mu_one_mobiuszero dst_negative_scale_mu_one_mobiuszero dst_positive_mu_one_mobiuszero dst_negative_mu_one_mobiuszero. (((M) = (((((dst_positive_code_mu_one_mobiuszero) + (dst_positive_scale_mu_one_mobiuszero)) * S ((dst_positive_code_mu_one_mobiuszero) + (dst_positive_scale_mu_one_mobiuszero)) + ((dst_positive_scale_mu_one_mobiuszero) + (dst_positive_scale_mu_one_mobiuszero))) + (((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) * S ((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) + ((dst_negative_scale_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)))) * S ((((dst_positive_code_mu_one_mobiuszero) + (dst_positive_scale_mu_one_mobiuszero)) * S ((dst_positive_code_mu_one_mobiuszero) + (dst_positive_scale_mu_one_mobiuszero)) + ((dst_positive_scale_mu_one_mobiuszero) + (dst_positive_scale_mu_one_mobiuszero))) + (((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) * S ((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) + ((dst_negative_scale_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)))) + ((((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) * S ((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) + ((dst_negative_scale_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero))) + (((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) * S ((dst_negative_code_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)) + ((dst_negative_scale_mu_one_mobiuszero) + (dst_negative_scale_mu_one_mobiuszero)))))) /\ (((((exists ff_h_pvs_mu_one_mobiuszeropositive. ff_h_pvs_mu_one_mobiuszeropositive + S (dst_positive_mu_one_mobiuszero) = S ((S (0)) * dst_positive_scale_mu_one_mobiuszero)) /\ exists ff_q_pvs_mu_one_mobiuszeropositive. dst_positive_code_mu_one_mobiuszero = ff_q_pvs_mu_one_mobiuszeropositive * S ((S (0)) * dst_positive_scale_mu_one_mobiuszero) + (dst_positive_mu_one_mobiuszero))) /\ (((((exists ff_h_pvs_mu_one_mobiuszeronegative. ff_h_pvs_mu_one_mobiuszeronegative + S (dst_negative_mu_one_mobiuszero) = S ((S (0)) * dst_negative_scale_mu_one_mobiuszero)) /\ exists ff_q_pvs_mu_one_mobiuszeronegative. dst_negative_code_mu_one_mobiuszero = ff_q_pvs_mu_one_mobiuszeronegative * S ((S (0)) * dst_negative_scale_mu_one_mobiuszero) + (dst_negative_mu_one_mobiuszero))) /\ (exists ge_balance_positive_mu_one_mobiuszerovalue ge_balance_negative_mu_one_mobiuszerovalue. (((((0) = 2 * (ge_balance_positive_mu_one_mobiuszerovalue) /\ (ge_balance_negative_mu_one_mobiuszerovalue) = 0) \/ exists ge_signed_half_mu_one_mobiuszerovaluedecode. (((0) = 2 * ge_signed_half_mu_one_mobiuszerovaluedecode + 1 /\ (ge_balance_positive_mu_one_mobiuszerovalue) = 0) /\ (ge_balance_negative_mu_one_mobiuszerovalue) = S ge_signed_half_mu_one_mobiuszerovaluedecode))) /\ ((dst_positive_mu_one_mobiuszero) + ge_balance_negative_mu_one_mobiuszerovalue = (dst_negative_mu_one_mobiuszero) + ge_balance_positive_mu_one_mobiuszerovalue))))))))) /\ (forall mt_index_mu_one_mobius mt_value_mu_one_mobius. ~(mt_index_mu_one_mobius=0) -> (exists pvs_le_gap_mu_one_mobiusdomain. pvs_le_gap_mu_one_mobiusdomain + (mt_index_mu_one_mobius) = (N)) -> (exists dst_positive_code_mu_one_mobiusentry dst_positive_scale_mu_one_mobiusentry dst_negative_code_mu_one_mobiusentry dst_negative_scale_mu_one_mobiusentry dst_positive_mu_one_mobiusentry dst_negative_mu_one_mobiusentry. (((M) = (((((dst_positive_code_mu_one_mobiusentry) + (dst_positive_scale_mu_one_mobiusentry)) * S ((dst_positive_code_mu_one_mobiusentry) + (dst_positive_scale_mu_one_mobiusentry)) + ((dst_positive_scale_mu_one_mobiusentry) + (dst_positive_scale_mu_one_mobiusentry))) + (((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) * S ((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) + ((dst_negative_scale_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)))) * S ((((dst_positive_code_mu_one_mobiusentry) + (dst_positive_scale_mu_one_mobiusentry)) * S ((dst_positive_code_mu_one_mobiusentry) + (dst_positive_scale_mu_one_mobiusentry)) + ((dst_positive_scale_mu_one_mobiusentry) + (dst_positive_scale_mu_one_mobiusentry))) + (((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) * S ((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) + ((dst_negative_scale_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)))) + ((((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) * S ((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) + ((dst_negative_scale_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry))) + (((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) * S ((dst_negative_code_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)) + ((dst_negative_scale_mu_one_mobiusentry) + (dst_negative_scale_mu_one_mobiusentry)))))) /\ (((((exists ff_h_pvs_mu_one_mobiusentrypositive. ff_h_pvs_mu_one_mobiusentrypositive + S (dst_positive_mu_one_mobiusentry) = S ((S (mt_index_mu_one_mobius)) * dst_positive_scale_mu_one_mobiusentry)) /\ exists ff_q_pvs_mu_one_mobiusentrypositive. dst_positive_code_mu_one_mobiusentry = ff_q_pvs_mu_one_mobiusentrypositive * S ((S (mt_index_mu_one_mobius)) * dst_positive_scale_mu_one_mobiusentry) + (dst_positive_mu_one_mobiusentry))) /\ (((((exists ff_h_pvs_mu_one_mobiusentrynegative. ff_h_pvs_mu_one_mobiusentrynegative + S (dst_negative_mu_one_mobiusentry) = S ((S (mt_index_mu_one_mobius)) * dst_negative_scale_mu_one_mobiusentry)) /\ exists ff_q_pvs_mu_one_mobiusentrynegative. dst_negative_code_mu_one_mobiusentry = ff_q_pvs_mu_one_mobiusentrynegative * S ((S (mt_index_mu_one_mobius)) * dst_negative_scale_mu_one_mobiusentry) + (dst_negative_mu_one_mobiusentry))) /\ (exists ge_balance_positive_mu_one_mobiusentryvalue ge_balance_negative_mu_one_mobiusentryvalue. (((((mt_value_mu_one_mobius) = 2 * (ge_balance_positive_mu_one_mobiusentryvalue) /\ (ge_balance_negative_mu_one_mobiusentryvalue) = 0) \/ exists ge_signed_half_mu_one_mobiusentryvaluedecode. (((mt_value_mu_one_mobius) = 2 * ge_signed_half_mu_one_mobiusentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_mobiusentryvalue) = 0) /\ (ge_balance_negative_mu_one_mobiusentryvalue) = S ge_signed_half_mu_one_mobiusentryvaluedecode))) /\ ((dst_positive_mu_one_mobiusentry) + ge_balance_negative_mu_one_mobiusentryvalue = (dst_negative_mu_one_mobiusentry) + ge_balance_positive_mu_one_mobiusentryvalue))))))))) -> (((~((mt_index_mu_one_mobius) = 0)) /\ ((((exists mv_square_prime_mu_one_mobiusvaluesquare. ((~((mv_square_prime_mu_one_mobiusvaluesquare) = 1) /\ forall pvs_left_mu_one_mobiusvaluesquareprime pvs_right_mu_one_mobiusvaluesquareprime. (mv_square_prime_mu_one_mobiusvaluesquare) = pvs_left_mu_one_mobiusvaluesquareprime * pvs_right_mu_one_mobiusvaluesquareprime -> pvs_left_mu_one_mobiusvaluesquareprime = 1 \/ pvs_right_mu_one_mobiusvaluesquareprime = 1) /\ (exists pvs_factor_mu_one_mobiusvaluesquaredivisor. (mt_index_mu_one_mobius) = (mv_square_prime_mu_one_mobiusvaluesquare * mv_square_prime_mu_one_mobiusvaluesquare) * pvs_factor_mu_one_mobiusvaluesquaredivisor))) /\ ((mt_value_mu_one_mobius) = 0))) \/ (((((~((mt_index_mu_one_mobius) = 0)) /\ (forall sfd_prime_mu_one_mobiusvaluesquarefree. (~((sfd_prime_mu_one_mobiusvaluesquarefree) = 1) /\ forall pvs_left_mu_one_mobiusvaluesquarefreedomain pvs_right_mu_one_mobiusvaluesquarefreedomain. (sfd_prime_mu_one_mobiusvaluesquarefree) = pvs_left_mu_one_mobiusvaluesquarefreedomain * pvs_right_mu_one_mobiusvaluesquarefreedomain -> pvs_left_mu_one_mobiusvaluesquarefreedomain = 1 \/ pvs_right_mu_one_mobiusvaluesquarefreedomain = 1) -> (exists pvs_le_gap_mu_one_mobiusvaluesquarefreebound. pvs_le_gap_mu_one_mobiusvaluesquarefreebound + (sfd_prime_mu_one_mobiusvaluesquarefree) = (mt_index_mu_one_mobius)) -> ~(exists pvs_factor_mu_one_mobiusvaluesquarefreesquare. (mt_index_mu_one_mobius) = (sfd_prime_mu_one_mobiusvaluesquarefree * sfd_prime_mu_one_mobiusvaluesquarefree) * pvs_factor_mu_one_mobiusvaluesquarefreesquare)))) /\ (exists mv_factor_code_mu_one_mobiusvaluefactors mv_factor_scale_mu_one_mobiusvaluefactors mv_factor_count_mu_one_mobiusvaluefactors. (((~(mt_index_mu_one_mobius = 0) /\ ((exists ff_u_fsat_mu_one_mobiusvaluefactorsfactorization_product ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_start. ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_start. ff_u_fsat_mu_one_mobiusvaluefactorsfactorization_product = ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_terminal. ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_terminal + S (mt_index_mu_one_mobius) = S ((S (mv_factor_count_mu_one_mobiusvaluefactors)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_terminal. ff_u_fsat_mu_one_mobiusvaluefactorsfactorization_product = ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_mu_one_mobiusvaluefactors)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product) + (mt_index_mu_one_mobius))) /\ forall ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product. (exists ff_lt_fsat_mu_one_mobiusvaluefactorsfactorization_product_bound. ff_lt_fsat_mu_one_mobiusvaluefactorsfactorization_product_bound + S ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product = mv_factor_count_mu_one_mobiusvaluefactors) -> exists ff_p_fsat_mu_one_mobiusvaluefactorsfactorization_product ff_r_fsat_mu_one_mobiusvaluefactorsfactorization_product ff_s_fsat_mu_one_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_factor. ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_factor + S (ff_p_fsat_mu_one_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_mu_one_mobiusvaluefactors)) /\ exists ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_factor. mv_factor_code_mu_one_mobiusvaluefactors = ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_mu_one_mobiusvaluefactors) + (ff_p_fsat_mu_one_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_partial. ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_partial + S (ff_r_fsat_mu_one_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_partial. ff_u_fsat_mu_one_mobiusvaluefactorsfactorization_product = ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product) + (ff_r_fsat_mu_one_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_successor. ff_h_fsat_mu_one_mobiusvaluefactorsfactorization_product_successor + S (ff_s_fsat_mu_one_mobiusvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_successor. ff_u_fsat_mu_one_mobiusvaluefactorsfactorization_product = ff_q_fsat_mu_one_mobiusvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_mu_one_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_mu_one_mobiusvaluefactorsfactorization_product) + (ff_s_fsat_mu_one_mobiusvaluefactorsfactorization_product))) /\ ff_s_fsat_mu_one_mobiusvaluefactorsfactorization_product = ff_r_fsat_mu_one_mobiusvaluefactorsfactorization_product * ff_p_fsat_mu_one_mobiusvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_mu_one_mobiusvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_mu_one_mobiusvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_mu_one_mobiusvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_mu_one_mobiusvaluefactorsfactorization_primes = (mv_factor_count_mu_one_mobiusvaluefactors)) -> exists ftsf_factor_fsat_mu_one_mobiusvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_mu_one_mobiusvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_mu_one_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_mu_one_mobiusvaluefactors)) /\ exists ff_q_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_entry. mv_factor_code_mu_one_mobiusvaluefactors = ff_q_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_mu_one_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_mu_one_mobiusvaluefactors) + (ftsf_factor_fsat_mu_one_mobiusvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_mu_one_mobiusvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_mu_one_mobiusvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mu_one_mobiusvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_mu_one_mobiusvaluefactorsparityeven. (mv_factor_count_mu_one_mobiusvaluefactors) = 2 * mv_even_half_mu_one_mobiusvaluefactorsparityeven) /\ ((mt_value_mu_one_mobius) = 2))) \/ (((exists mv_odd_half_mu_one_mobiusvaluefactorsparityodd. (mv_factor_count_mu_one_mobiusvaluefactors) = 2 * mv_odd_half_mu_one_mobiusvaluefactorsparityodd + 1) /\ ((mt_value_mu_one_mobius) = 1)))))))))))))))) -> (((exists dst_positive_code_mu_one_onetable dst_positive_scale_mu_one_onetable dst_negative_code_mu_one_onetable dst_negative_scale_mu_one_onetable. (((U) = (((((dst_positive_code_mu_one_onetable) + (dst_positive_scale_mu_one_onetable)) * S ((dst_positive_code_mu_one_onetable) + (dst_positive_scale_mu_one_onetable)) + ((dst_positive_scale_mu_one_onetable) + (dst_positive_scale_mu_one_onetable))) + (((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) * S ((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) + ((dst_negative_scale_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)))) * S ((((dst_positive_code_mu_one_onetable) + (dst_positive_scale_mu_one_onetable)) * S ((dst_positive_code_mu_one_onetable) + (dst_positive_scale_mu_one_onetable)) + ((dst_positive_scale_mu_one_onetable) + (dst_positive_scale_mu_one_onetable))) + (((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) * S ((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) + ((dst_negative_scale_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)))) + ((((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) * S ((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) + ((dst_negative_scale_mu_one_onetable) + (dst_negative_scale_mu_one_onetable))) + (((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) * S ((dst_negative_code_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)) + ((dst_negative_scale_mu_one_onetable) + (dst_negative_scale_mu_one_onetable)))))) /\ (forall dst_index_mu_one_onetable. (exists pvs_le_gap_mu_one_onetabledomain. pvs_le_gap_mu_one_onetabledomain + (dst_index_mu_one_onetable) = (N)) -> exists dst_positive_mu_one_onetable dst_negative_mu_one_onetable dst_value_mu_one_onetable. ((((exists ff_h_pvs_mu_one_onetableentrypositive. ff_h_pvs_mu_one_onetableentrypositive + S (dst_positive_mu_one_onetable) = S ((S (dst_index_mu_one_onetable)) * dst_positive_scale_mu_one_onetable)) /\ exists ff_q_pvs_mu_one_onetableentrypositive. dst_positive_code_mu_one_onetable = ff_q_pvs_mu_one_onetableentrypositive * S ((S (dst_index_mu_one_onetable)) * dst_positive_scale_mu_one_onetable) + (dst_positive_mu_one_onetable))) /\ (((((exists ff_h_pvs_mu_one_onetableentrynegative. ff_h_pvs_mu_one_onetableentrynegative + S (dst_negative_mu_one_onetable) = S ((S (dst_index_mu_one_onetable)) * dst_negative_scale_mu_one_onetable)) /\ exists ff_q_pvs_mu_one_onetableentrynegative. dst_negative_code_mu_one_onetable = ff_q_pvs_mu_one_onetableentrynegative * S ((S (dst_index_mu_one_onetable)) * dst_negative_scale_mu_one_onetable) + (dst_negative_mu_one_onetable))) /\ (exists ge_balance_positive_mu_one_onetableentryvalue ge_balance_negative_mu_one_onetableentryvalue. (((((dst_value_mu_one_onetable) = 2 * (ge_balance_positive_mu_one_onetableentryvalue) /\ (ge_balance_negative_mu_one_onetableentryvalue) = 0) \/ exists ge_signed_half_mu_one_onetableentryvaluedecode. (((dst_value_mu_one_onetable) = 2 * ge_signed_half_mu_one_onetableentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_onetableentryvalue) = 0) /\ (ge_balance_negative_mu_one_onetableentryvalue) = S ge_signed_half_mu_one_onetableentryvaluedecode))) /\ ((dst_positive_mu_one_onetable) + ge_balance_negative_mu_one_onetableentryvalue = (dst_negative_mu_one_onetable) + ge_balance_positive_mu_one_onetableentryvalue))))))))) /\ (forall du_index_mu_one_one du_value_mu_one_one. ~(du_index_mu_one_one=0) -> (exists pvs_le_gap_mu_one_onebound. pvs_le_gap_mu_one_onebound + (du_index_mu_one_one) = (N)) -> (exists dst_positive_code_mu_one_oneentry dst_positive_scale_mu_one_oneentry dst_negative_code_mu_one_oneentry dst_negative_scale_mu_one_oneentry dst_positive_mu_one_oneentry dst_negative_mu_one_oneentry. (((U) = (((((dst_positive_code_mu_one_oneentry) + (dst_positive_scale_mu_one_oneentry)) * S ((dst_positive_code_mu_one_oneentry) + (dst_positive_scale_mu_one_oneentry)) + ((dst_positive_scale_mu_one_oneentry) + (dst_positive_scale_mu_one_oneentry))) + (((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) * S ((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) + ((dst_negative_scale_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)))) * S ((((dst_positive_code_mu_one_oneentry) + (dst_positive_scale_mu_one_oneentry)) * S ((dst_positive_code_mu_one_oneentry) + (dst_positive_scale_mu_one_oneentry)) + ((dst_positive_scale_mu_one_oneentry) + (dst_positive_scale_mu_one_oneentry))) + (((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) * S ((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) + ((dst_negative_scale_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)))) + ((((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) * S ((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) + ((dst_negative_scale_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry))) + (((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) * S ((dst_negative_code_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)) + ((dst_negative_scale_mu_one_oneentry) + (dst_negative_scale_mu_one_oneentry)))))) /\ (((((exists ff_h_pvs_mu_one_oneentrypositive. ff_h_pvs_mu_one_oneentrypositive + S (dst_positive_mu_one_oneentry) = S ((S (du_index_mu_one_one)) * dst_positive_scale_mu_one_oneentry)) /\ exists ff_q_pvs_mu_one_oneentrypositive. dst_positive_code_mu_one_oneentry = ff_q_pvs_mu_one_oneentrypositive * S ((S (du_index_mu_one_one)) * dst_positive_scale_mu_one_oneentry) + (dst_positive_mu_one_oneentry))) /\ (((((exists ff_h_pvs_mu_one_oneentrynegative. ff_h_pvs_mu_one_oneentrynegative + S (dst_negative_mu_one_oneentry) = S ((S (du_index_mu_one_one)) * dst_negative_scale_mu_one_oneentry)) /\ exists ff_q_pvs_mu_one_oneentrynegative. dst_negative_code_mu_one_oneentry = ff_q_pvs_mu_one_oneentrynegative * S ((S (du_index_mu_one_one)) * dst_negative_scale_mu_one_oneentry) + (dst_negative_mu_one_oneentry))) /\ (exists ge_balance_positive_mu_one_oneentryvalue ge_balance_negative_mu_one_oneentryvalue. (((((du_value_mu_one_one) = 2 * (ge_balance_positive_mu_one_oneentryvalue) /\ (ge_balance_negative_mu_one_oneentryvalue) = 0) \/ exists ge_signed_half_mu_one_oneentryvaluedecode. (((du_value_mu_one_one) = 2 * ge_signed_half_mu_one_oneentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_oneentryvalue) = 0) /\ (ge_balance_negative_mu_one_oneentryvalue) = S ge_signed_half_mu_one_oneentryvaluedecode))) /\ ((dst_positive_mu_one_oneentry) + ge_balance_negative_mu_one_oneentryvalue = (dst_negative_mu_one_oneentry) + ge_balance_positive_mu_one_oneentryvalue))))))))) -> du_value_mu_one_one=2))) -> (((exists dst_positive_code_mu_one_deltatable dst_positive_scale_mu_one_deltatable dst_negative_code_mu_one_deltatable dst_negative_scale_mu_one_deltatable. (((E) = (((((dst_positive_code_mu_one_deltatable) + (dst_positive_scale_mu_one_deltatable)) * S ((dst_positive_code_mu_one_deltatable) + (dst_positive_scale_mu_one_deltatable)) + ((dst_positive_scale_mu_one_deltatable) + (dst_positive_scale_mu_one_deltatable))) + (((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) * S ((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) + ((dst_negative_scale_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)))) * S ((((dst_positive_code_mu_one_deltatable) + (dst_positive_scale_mu_one_deltatable)) * S ((dst_positive_code_mu_one_deltatable) + (dst_positive_scale_mu_one_deltatable)) + ((dst_positive_scale_mu_one_deltatable) + (dst_positive_scale_mu_one_deltatable))) + (((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) * S ((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) + ((dst_negative_scale_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)))) + ((((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) * S ((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) + ((dst_negative_scale_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable))) + (((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) * S ((dst_negative_code_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)) + ((dst_negative_scale_mu_one_deltatable) + (dst_negative_scale_mu_one_deltatable)))))) /\ (forall dst_index_mu_one_deltatable. (exists pvs_le_gap_mu_one_deltatabledomain. pvs_le_gap_mu_one_deltatabledomain + (dst_index_mu_one_deltatable) = (N)) -> exists dst_positive_mu_one_deltatable dst_negative_mu_one_deltatable dst_value_mu_one_deltatable. ((((exists ff_h_pvs_mu_one_deltatableentrypositive. ff_h_pvs_mu_one_deltatableentrypositive + S (dst_positive_mu_one_deltatable) = S ((S (dst_index_mu_one_deltatable)) * dst_positive_scale_mu_one_deltatable)) /\ exists ff_q_pvs_mu_one_deltatableentrypositive. dst_positive_code_mu_one_deltatable = ff_q_pvs_mu_one_deltatableentrypositive * S ((S (dst_index_mu_one_deltatable)) * dst_positive_scale_mu_one_deltatable) + (dst_positive_mu_one_deltatable))) /\ (((((exists ff_h_pvs_mu_one_deltatableentrynegative. ff_h_pvs_mu_one_deltatableentrynegative + S (dst_negative_mu_one_deltatable) = S ((S (dst_index_mu_one_deltatable)) * dst_negative_scale_mu_one_deltatable)) /\ exists ff_q_pvs_mu_one_deltatableentrynegative. dst_negative_code_mu_one_deltatable = ff_q_pvs_mu_one_deltatableentrynegative * S ((S (dst_index_mu_one_deltatable)) * dst_negative_scale_mu_one_deltatable) + (dst_negative_mu_one_deltatable))) /\ (exists ge_balance_positive_mu_one_deltatableentryvalue ge_balance_negative_mu_one_deltatableentryvalue. (((((dst_value_mu_one_deltatable) = 2 * (ge_balance_positive_mu_one_deltatableentryvalue) /\ (ge_balance_negative_mu_one_deltatableentryvalue) = 0) \/ exists ge_signed_half_mu_one_deltatableentryvaluedecode. (((dst_value_mu_one_deltatable) = 2 * ge_signed_half_mu_one_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_deltatableentryvalue) = 0) /\ (ge_balance_negative_mu_one_deltatableentryvalue) = S ge_signed_half_mu_one_deltatableentryvaluedecode))) /\ ((dst_positive_mu_one_deltatable) + ge_balance_negative_mu_one_deltatableentryvalue = (dst_negative_mu_one_deltatable) + ge_balance_positive_mu_one_deltatableentryvalue))))))))) /\ (forall du_index_mu_one_delta du_value_mu_one_delta. ~(du_index_mu_one_delta=0) -> (exists pvs_le_gap_mu_one_deltabound. pvs_le_gap_mu_one_deltabound + (du_index_mu_one_delta) = (N)) -> (exists dst_positive_code_mu_one_deltaentry dst_positive_scale_mu_one_deltaentry dst_negative_code_mu_one_deltaentry dst_negative_scale_mu_one_deltaentry dst_positive_mu_one_deltaentry dst_negative_mu_one_deltaentry. (((E) = (((((dst_positive_code_mu_one_deltaentry) + (dst_positive_scale_mu_one_deltaentry)) * S ((dst_positive_code_mu_one_deltaentry) + (dst_positive_scale_mu_one_deltaentry)) + ((dst_positive_scale_mu_one_deltaentry) + (dst_positive_scale_mu_one_deltaentry))) + (((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) * S ((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) + ((dst_negative_scale_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)))) * S ((((dst_positive_code_mu_one_deltaentry) + (dst_positive_scale_mu_one_deltaentry)) * S ((dst_positive_code_mu_one_deltaentry) + (dst_positive_scale_mu_one_deltaentry)) + ((dst_positive_scale_mu_one_deltaentry) + (dst_positive_scale_mu_one_deltaentry))) + (((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) * S ((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) + ((dst_negative_scale_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)))) + ((((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) * S ((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) + ((dst_negative_scale_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry))) + (((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) * S ((dst_negative_code_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)) + ((dst_negative_scale_mu_one_deltaentry) + (dst_negative_scale_mu_one_deltaentry)))))) /\ (((((exists ff_h_pvs_mu_one_deltaentrypositive. ff_h_pvs_mu_one_deltaentrypositive + S (dst_positive_mu_one_deltaentry) = S ((S (du_index_mu_one_delta)) * dst_positive_scale_mu_one_deltaentry)) /\ exists ff_q_pvs_mu_one_deltaentrypositive. dst_positive_code_mu_one_deltaentry = ff_q_pvs_mu_one_deltaentrypositive * S ((S (du_index_mu_one_delta)) * dst_positive_scale_mu_one_deltaentry) + (dst_positive_mu_one_deltaentry))) /\ (((((exists ff_h_pvs_mu_one_deltaentrynegative. ff_h_pvs_mu_one_deltaentrynegative + S (dst_negative_mu_one_deltaentry) = S ((S (du_index_mu_one_delta)) * dst_negative_scale_mu_one_deltaentry)) /\ exists ff_q_pvs_mu_one_deltaentrynegative. dst_negative_code_mu_one_deltaentry = ff_q_pvs_mu_one_deltaentrynegative * S ((S (du_index_mu_one_delta)) * dst_negative_scale_mu_one_deltaentry) + (dst_negative_mu_one_deltaentry))) /\ (exists ge_balance_positive_mu_one_deltaentryvalue ge_balance_negative_mu_one_deltaentryvalue. (((((du_value_mu_one_delta) = 2 * (ge_balance_positive_mu_one_deltaentryvalue) /\ (ge_balance_negative_mu_one_deltaentryvalue) = 0) \/ exists ge_signed_half_mu_one_deltaentryvaluedecode. (((du_value_mu_one_delta) = 2 * ge_signed_half_mu_one_deltaentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_deltaentryvalue) = 0) /\ (ge_balance_negative_mu_one_deltaentryvalue) = S ge_signed_half_mu_one_deltaentryvaluedecode))) /\ ((dst_positive_mu_one_deltaentry) + ge_balance_negative_mu_one_deltaentryvalue = (dst_negative_mu_one_deltaentry) + ge_balance_positive_mu_one_deltaentryvalue))))))))) -> ((((du_index_mu_one_delta)=1 -> (du_value_mu_one_delta)=2) /\ (~((du_index_mu_one_delta)=1) -> (du_value_mu_one_delta)=0)))))) -> (((exists dst_positive_code_mu_one_resultleft dst_positive_scale_mu_one_resultleft dst_negative_code_mu_one_resultleft dst_negative_scale_mu_one_resultleft. (((M) = (((((dst_positive_code_mu_one_resultleft) + (dst_positive_scale_mu_one_resultleft)) * S ((dst_positive_code_mu_one_resultleft) + (dst_positive_scale_mu_one_resultleft)) + ((dst_positive_scale_mu_one_resultleft) + (dst_positive_scale_mu_one_resultleft))) + (((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) * S ((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) + ((dst_negative_scale_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)))) * S ((((dst_positive_code_mu_one_resultleft) + (dst_positive_scale_mu_one_resultleft)) * S ((dst_positive_code_mu_one_resultleft) + (dst_positive_scale_mu_one_resultleft)) + ((dst_positive_scale_mu_one_resultleft) + (dst_positive_scale_mu_one_resultleft))) + (((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) * S ((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) + ((dst_negative_scale_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)))) + ((((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) * S ((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) + ((dst_negative_scale_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft))) + (((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) * S ((dst_negative_code_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)) + ((dst_negative_scale_mu_one_resultleft) + (dst_negative_scale_mu_one_resultleft)))))) /\ (forall dst_index_mu_one_resultleft. (exists pvs_le_gap_mu_one_resultleftdomain. pvs_le_gap_mu_one_resultleftdomain + (dst_index_mu_one_resultleft) = (N)) -> exists dst_positive_mu_one_resultleft dst_negative_mu_one_resultleft dst_value_mu_one_resultleft. ((((exists ff_h_pvs_mu_one_resultleftentrypositive. ff_h_pvs_mu_one_resultleftentrypositive + S (dst_positive_mu_one_resultleft) = S ((S (dst_index_mu_one_resultleft)) * dst_positive_scale_mu_one_resultleft)) /\ exists ff_q_pvs_mu_one_resultleftentrypositive. dst_positive_code_mu_one_resultleft = ff_q_pvs_mu_one_resultleftentrypositive * S ((S (dst_index_mu_one_resultleft)) * dst_positive_scale_mu_one_resultleft) + (dst_positive_mu_one_resultleft))) /\ (((((exists ff_h_pvs_mu_one_resultleftentrynegative. ff_h_pvs_mu_one_resultleftentrynegative + S (dst_negative_mu_one_resultleft) = S ((S (dst_index_mu_one_resultleft)) * dst_negative_scale_mu_one_resultleft)) /\ exists ff_q_pvs_mu_one_resultleftentrynegative. dst_negative_code_mu_one_resultleft = ff_q_pvs_mu_one_resultleftentrynegative * S ((S (dst_index_mu_one_resultleft)) * dst_negative_scale_mu_one_resultleft) + (dst_negative_mu_one_resultleft))) /\ (exists ge_balance_positive_mu_one_resultleftentryvalue ge_balance_negative_mu_one_resultleftentryvalue. (((((dst_value_mu_one_resultleft) = 2 * (ge_balance_positive_mu_one_resultleftentryvalue) /\ (ge_balance_negative_mu_one_resultleftentryvalue) = 0) \/ exists ge_signed_half_mu_one_resultleftentryvaluedecode. (((dst_value_mu_one_resultleft) = 2 * ge_signed_half_mu_one_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultleftentryvalue) = 0) /\ (ge_balance_negative_mu_one_resultleftentryvalue) = S ge_signed_half_mu_one_resultleftentryvaluedecode))) /\ ((dst_positive_mu_one_resultleft) + ge_balance_negative_mu_one_resultleftentryvalue = (dst_negative_mu_one_resultleft) + ge_balance_positive_mu_one_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_mu_one_resultright dst_positive_scale_mu_one_resultright dst_negative_code_mu_one_resultright dst_negative_scale_mu_one_resultright. (((U) = (((((dst_positive_code_mu_one_resultright) + (dst_positive_scale_mu_one_resultright)) * S ((dst_positive_code_mu_one_resultright) + (dst_positive_scale_mu_one_resultright)) + ((dst_positive_scale_mu_one_resultright) + (dst_positive_scale_mu_one_resultright))) + (((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) * S ((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) + ((dst_negative_scale_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)))) * S ((((dst_positive_code_mu_one_resultright) + (dst_positive_scale_mu_one_resultright)) * S ((dst_positive_code_mu_one_resultright) + (dst_positive_scale_mu_one_resultright)) + ((dst_positive_scale_mu_one_resultright) + (dst_positive_scale_mu_one_resultright))) + (((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) * S ((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) + ((dst_negative_scale_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)))) + ((((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) * S ((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) + ((dst_negative_scale_mu_one_resultright) + (dst_negative_scale_mu_one_resultright))) + (((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) * S ((dst_negative_code_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)) + ((dst_negative_scale_mu_one_resultright) + (dst_negative_scale_mu_one_resultright)))))) /\ (forall dst_index_mu_one_resultright. (exists pvs_le_gap_mu_one_resultrightdomain. pvs_le_gap_mu_one_resultrightdomain + (dst_index_mu_one_resultright) = (N)) -> exists dst_positive_mu_one_resultright dst_negative_mu_one_resultright dst_value_mu_one_resultright. ((((exists ff_h_pvs_mu_one_resultrightentrypositive. ff_h_pvs_mu_one_resultrightentrypositive + S (dst_positive_mu_one_resultright) = S ((S (dst_index_mu_one_resultright)) * dst_positive_scale_mu_one_resultright)) /\ exists ff_q_pvs_mu_one_resultrightentrypositive. dst_positive_code_mu_one_resultright = ff_q_pvs_mu_one_resultrightentrypositive * S ((S (dst_index_mu_one_resultright)) * dst_positive_scale_mu_one_resultright) + (dst_positive_mu_one_resultright))) /\ (((((exists ff_h_pvs_mu_one_resultrightentrynegative. ff_h_pvs_mu_one_resultrightentrynegative + S (dst_negative_mu_one_resultright) = S ((S (dst_index_mu_one_resultright)) * dst_negative_scale_mu_one_resultright)) /\ exists ff_q_pvs_mu_one_resultrightentrynegative. dst_negative_code_mu_one_resultright = ff_q_pvs_mu_one_resultrightentrynegative * S ((S (dst_index_mu_one_resultright)) * dst_negative_scale_mu_one_resultright) + (dst_negative_mu_one_resultright))) /\ (exists ge_balance_positive_mu_one_resultrightentryvalue ge_balance_negative_mu_one_resultrightentryvalue. (((((dst_value_mu_one_resultright) = 2 * (ge_balance_positive_mu_one_resultrightentryvalue) /\ (ge_balance_negative_mu_one_resultrightentryvalue) = 0) \/ exists ge_signed_half_mu_one_resultrightentryvaluedecode. (((dst_value_mu_one_resultright) = 2 * ge_signed_half_mu_one_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultrightentryvalue) = 0) /\ (ge_balance_negative_mu_one_resultrightentryvalue) = S ge_signed_half_mu_one_resultrightentryvaluedecode))) /\ ((dst_positive_mu_one_resultright) + ge_balance_negative_mu_one_resultrightentryvalue = (dst_negative_mu_one_resultright) + ge_balance_positive_mu_one_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_mu_one_resulttable dst_positive_scale_mu_one_resulttable dst_negative_code_mu_one_resulttable dst_negative_scale_mu_one_resulttable. (((E) = (((((dst_positive_code_mu_one_resulttable) + (dst_positive_scale_mu_one_resulttable)) * S ((dst_positive_code_mu_one_resulttable) + (dst_positive_scale_mu_one_resulttable)) + ((dst_positive_scale_mu_one_resulttable) + (dst_positive_scale_mu_one_resulttable))) + (((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) * S ((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) + ((dst_negative_scale_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)))) * S ((((dst_positive_code_mu_one_resulttable) + (dst_positive_scale_mu_one_resulttable)) * S ((dst_positive_code_mu_one_resulttable) + (dst_positive_scale_mu_one_resulttable)) + ((dst_positive_scale_mu_one_resulttable) + (dst_positive_scale_mu_one_resulttable))) + (((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) * S ((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) + ((dst_negative_scale_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)))) + ((((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) * S ((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) + ((dst_negative_scale_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable))) + (((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) * S ((dst_negative_code_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)) + ((dst_negative_scale_mu_one_resulttable) + (dst_negative_scale_mu_one_resulttable)))))) /\ (forall dst_index_mu_one_resulttable. (exists pvs_le_gap_mu_one_resulttabledomain. pvs_le_gap_mu_one_resulttabledomain + (dst_index_mu_one_resulttable) = (N)) -> exists dst_positive_mu_one_resulttable dst_negative_mu_one_resulttable dst_value_mu_one_resulttable. ((((exists ff_h_pvs_mu_one_resulttableentrypositive. ff_h_pvs_mu_one_resulttableentrypositive + S (dst_positive_mu_one_resulttable) = S ((S (dst_index_mu_one_resulttable)) * dst_positive_scale_mu_one_resulttable)) /\ exists ff_q_pvs_mu_one_resulttableentrypositive. dst_positive_code_mu_one_resulttable = ff_q_pvs_mu_one_resulttableentrypositive * S ((S (dst_index_mu_one_resulttable)) * dst_positive_scale_mu_one_resulttable) + (dst_positive_mu_one_resulttable))) /\ (((((exists ff_h_pvs_mu_one_resulttableentrynegative. ff_h_pvs_mu_one_resulttableentrynegative + S (dst_negative_mu_one_resulttable) = S ((S (dst_index_mu_one_resulttable)) * dst_negative_scale_mu_one_resulttable)) /\ exists ff_q_pvs_mu_one_resulttableentrynegative. dst_negative_code_mu_one_resulttable = ff_q_pvs_mu_one_resulttableentrynegative * S ((S (dst_index_mu_one_resulttable)) * dst_negative_scale_mu_one_resulttable) + (dst_negative_mu_one_resulttable))) /\ (exists ge_balance_positive_mu_one_resulttableentryvalue ge_balance_negative_mu_one_resulttableentryvalue. (((((dst_value_mu_one_resulttable) = 2 * (ge_balance_positive_mu_one_resulttableentryvalue) /\ (ge_balance_negative_mu_one_resulttableentryvalue) = 0) \/ exists ge_signed_half_mu_one_resulttableentryvaluedecode. (((dst_value_mu_one_resulttable) = 2 * ge_signed_half_mu_one_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_resulttableentryvalue) = 0) /\ (ge_balance_negative_mu_one_resulttableentryvalue) = S ge_signed_half_mu_one_resulttableentryvaluedecode))) /\ ((dst_positive_mu_one_resulttable) + ge_balance_negative_mu_one_resulttableentryvalue = (dst_negative_mu_one_resulttable) + ge_balance_positive_mu_one_resulttableentryvalue))))))))) /\ (forall dc_input_mu_one_result dc_output_mu_one_result. ~(dc_input_mu_one_result=0) -> (exists pvs_le_gap_mu_one_resultdomain. pvs_le_gap_mu_one_resultdomain + (dc_input_mu_one_result) = (N)) -> (exists dst_positive_code_mu_one_resultlookup dst_positive_scale_mu_one_resultlookup dst_negative_code_mu_one_resultlookup dst_negative_scale_mu_one_resultlookup dst_positive_mu_one_resultlookup dst_negative_mu_one_resultlookup. (((E) = (((((dst_positive_code_mu_one_resultlookup) + (dst_positive_scale_mu_one_resultlookup)) * S ((dst_positive_code_mu_one_resultlookup) + (dst_positive_scale_mu_one_resultlookup)) + ((dst_positive_scale_mu_one_resultlookup) + (dst_positive_scale_mu_one_resultlookup))) + (((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) * S ((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) + ((dst_negative_scale_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)))) * S ((((dst_positive_code_mu_one_resultlookup) + (dst_positive_scale_mu_one_resultlookup)) * S ((dst_positive_code_mu_one_resultlookup) + (dst_positive_scale_mu_one_resultlookup)) + ((dst_positive_scale_mu_one_resultlookup) + (dst_positive_scale_mu_one_resultlookup))) + (((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) * S ((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) + ((dst_negative_scale_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)))) + ((((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) * S ((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) + ((dst_negative_scale_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup))) + (((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) * S ((dst_negative_code_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)) + ((dst_negative_scale_mu_one_resultlookup) + (dst_negative_scale_mu_one_resultlookup)))))) /\ (((((exists ff_h_pvs_mu_one_resultlookuppositive. ff_h_pvs_mu_one_resultlookuppositive + S (dst_positive_mu_one_resultlookup) = S ((S (dc_input_mu_one_result)) * dst_positive_scale_mu_one_resultlookup)) /\ exists ff_q_pvs_mu_one_resultlookuppositive. dst_positive_code_mu_one_resultlookup = ff_q_pvs_mu_one_resultlookuppositive * S ((S (dc_input_mu_one_result)) * dst_positive_scale_mu_one_resultlookup) + (dst_positive_mu_one_resultlookup))) /\ (((((exists ff_h_pvs_mu_one_resultlookupnegative. ff_h_pvs_mu_one_resultlookupnegative + S (dst_negative_mu_one_resultlookup) = S ((S (dc_input_mu_one_result)) * dst_negative_scale_mu_one_resultlookup)) /\ exists ff_q_pvs_mu_one_resultlookupnegative. dst_negative_code_mu_one_resultlookup = ff_q_pvs_mu_one_resultlookupnegative * S ((S (dc_input_mu_one_result)) * dst_negative_scale_mu_one_resultlookup) + (dst_negative_mu_one_resultlookup))) /\ (exists ge_balance_positive_mu_one_resultlookupvalue ge_balance_negative_mu_one_resultlookupvalue. (((((dc_output_mu_one_result) = 2 * (ge_balance_positive_mu_one_resultlookupvalue) /\ (ge_balance_negative_mu_one_resultlookupvalue) = 0) \/ exists ge_signed_half_mu_one_resultlookupvaluedecode. (((dc_output_mu_one_result) = 2 * ge_signed_half_mu_one_resultlookupvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultlookupvalue) = 0) /\ (ge_balance_negative_mu_one_resultlookupvalue) = S ge_signed_half_mu_one_resultlookupvaluedecode))) /\ ((dst_positive_mu_one_resultlookup) + ge_balance_negative_mu_one_resultlookupvalue = (dst_negative_mu_one_resultlookup) + ge_balance_positive_mu_one_resultlookupvalue))))))))) -> (((~((dc_input_mu_one_result)=0)) /\ (exists dc_mask_mu_one_resultvalue. ((((exists dst_positive_code_mu_one_resultvaluemasktable dst_positive_scale_mu_one_resultvaluemasktable dst_negative_code_mu_one_resultvaluemasktable dst_negative_scale_mu_one_resultvaluemasktable. (((dc_mask_mu_one_resultvalue) = (((((dst_positive_code_mu_one_resultvaluemasktable) + (dst_positive_scale_mu_one_resultvaluemasktable)) * S ((dst_positive_code_mu_one_resultvaluemasktable) + (dst_positive_scale_mu_one_resultvaluemasktable)) + ((dst_positive_scale_mu_one_resultvaluemasktable) + (dst_positive_scale_mu_one_resultvaluemasktable))) + (((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) * S ((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) + ((dst_negative_scale_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)))) * S ((((dst_positive_code_mu_one_resultvaluemasktable) + (dst_positive_scale_mu_one_resultvaluemasktable)) * S ((dst_positive_code_mu_one_resultvaluemasktable) + (dst_positive_scale_mu_one_resultvaluemasktable)) + ((dst_positive_scale_mu_one_resultvaluemasktable) + (dst_positive_scale_mu_one_resultvaluemasktable))) + (((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) * S ((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) + ((dst_negative_scale_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)))) + ((((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) * S ((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) + ((dst_negative_scale_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable))) + (((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) * S ((dst_negative_code_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)) + ((dst_negative_scale_mu_one_resultvaluemasktable) + (dst_negative_scale_mu_one_resultvaluemasktable)))))) /\ (forall dst_index_mu_one_resultvaluemasktable. (exists pvs_le_gap_mu_one_resultvaluemasktabledomain. pvs_le_gap_mu_one_resultvaluemasktabledomain + (dst_index_mu_one_resultvaluemasktable) = (dc_input_mu_one_result)) -> exists dst_positive_mu_one_resultvaluemasktable dst_negative_mu_one_resultvaluemasktable dst_value_mu_one_resultvaluemasktable. ((((exists ff_h_pvs_mu_one_resultvaluemasktableentrypositive. ff_h_pvs_mu_one_resultvaluemasktableentrypositive + S (dst_positive_mu_one_resultvaluemasktable) = S ((S (dst_index_mu_one_resultvaluemasktable)) * dst_positive_scale_mu_one_resultvaluemasktable)) /\ exists ff_q_pvs_mu_one_resultvaluemasktableentrypositive. dst_positive_code_mu_one_resultvaluemasktable = ff_q_pvs_mu_one_resultvaluemasktableentrypositive * S ((S (dst_index_mu_one_resultvaluemasktable)) * dst_positive_scale_mu_one_resultvaluemasktable) + (dst_positive_mu_one_resultvaluemasktable))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemasktableentrynegative. ff_h_pvs_mu_one_resultvaluemasktableentrynegative + S (dst_negative_mu_one_resultvaluemasktable) = S ((S (dst_index_mu_one_resultvaluemasktable)) * dst_negative_scale_mu_one_resultvaluemasktable)) /\ exists ff_q_pvs_mu_one_resultvaluemasktableentrynegative. dst_negative_code_mu_one_resultvaluemasktable = ff_q_pvs_mu_one_resultvaluemasktableentrynegative * S ((S (dst_index_mu_one_resultvaluemasktable)) * dst_negative_scale_mu_one_resultvaluemasktable) + (dst_negative_mu_one_resultvaluemasktable))) /\ (exists ge_balance_positive_mu_one_resultvaluemasktableentryvalue ge_balance_negative_mu_one_resultvaluemasktableentryvalue. (((((dst_value_mu_one_resultvaluemasktable) = 2 * (ge_balance_positive_mu_one_resultvaluemasktableentryvalue) /\ (ge_balance_negative_mu_one_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_mu_one_resultvaluemasktableentryvaluedecode. (((dst_value_mu_one_resultvaluemasktable) = 2 * ge_signed_half_mu_one_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_mu_one_resultvaluemasktableentryvalue) = S ge_signed_half_mu_one_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_mu_one_resultvaluemasktable) + ge_balance_negative_mu_one_resultvaluemasktableentryvalue = (dst_negative_mu_one_resultvaluemasktable) + ge_balance_positive_mu_one_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_mu_one_resultvaluemask dc_value_mu_one_resultvaluemask. (exists pvs_le_gap_mu_one_resultvaluemaskdomain. pvs_le_gap_mu_one_resultvaluemaskdomain + (dc_index_mu_one_resultvaluemask) = (dc_input_mu_one_result)) -> (exists dst_positive_code_mu_one_resultvaluemasklookup dst_positive_scale_mu_one_resultvaluemasklookup dst_negative_code_mu_one_resultvaluemasklookup dst_negative_scale_mu_one_resultvaluemasklookup dst_positive_mu_one_resultvaluemasklookup dst_negative_mu_one_resultvaluemasklookup. (((dc_mask_mu_one_resultvalue) = (((((dst_positive_code_mu_one_resultvaluemasklookup) + (dst_positive_scale_mu_one_resultvaluemasklookup)) * S ((dst_positive_code_mu_one_resultvaluemasklookup) + (dst_positive_scale_mu_one_resultvaluemasklookup)) + ((dst_positive_scale_mu_one_resultvaluemasklookup) + (dst_positive_scale_mu_one_resultvaluemasklookup))) + (((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) * S ((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) + ((dst_negative_scale_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)))) * S ((((dst_positive_code_mu_one_resultvaluemasklookup) + (dst_positive_scale_mu_one_resultvaluemasklookup)) * S ((dst_positive_code_mu_one_resultvaluemasklookup) + (dst_positive_scale_mu_one_resultvaluemasklookup)) + ((dst_positive_scale_mu_one_resultvaluemasklookup) + (dst_positive_scale_mu_one_resultvaluemasklookup))) + (((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) * S ((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) + ((dst_negative_scale_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)))) + ((((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) * S ((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) + ((dst_negative_scale_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup))) + (((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) * S ((dst_negative_code_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)) + ((dst_negative_scale_mu_one_resultvaluemasklookup) + (dst_negative_scale_mu_one_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemasklookuppositive. ff_h_pvs_mu_one_resultvaluemasklookuppositive + S (dst_positive_mu_one_resultvaluemasklookup) = S ((S (dc_index_mu_one_resultvaluemask)) * dst_positive_scale_mu_one_resultvaluemasklookup)) /\ exists ff_q_pvs_mu_one_resultvaluemasklookuppositive. dst_positive_code_mu_one_resultvaluemasklookup = ff_q_pvs_mu_one_resultvaluemasklookuppositive * S ((S (dc_index_mu_one_resultvaluemask)) * dst_positive_scale_mu_one_resultvaluemasklookup) + (dst_positive_mu_one_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemasklookupnegative. ff_h_pvs_mu_one_resultvaluemasklookupnegative + S (dst_negative_mu_one_resultvaluemasklookup) = S ((S (dc_index_mu_one_resultvaluemask)) * dst_negative_scale_mu_one_resultvaluemasklookup)) /\ exists ff_q_pvs_mu_one_resultvaluemasklookupnegative. dst_negative_code_mu_one_resultvaluemasklookup = ff_q_pvs_mu_one_resultvaluemasklookupnegative * S ((S (dc_index_mu_one_resultvaluemask)) * dst_negative_scale_mu_one_resultvaluemasklookup) + (dst_negative_mu_one_resultvaluemasklookup))) /\ (exists ge_balance_positive_mu_one_resultvaluemasklookupvalue ge_balance_negative_mu_one_resultvaluemasklookupvalue. (((((dc_value_mu_one_resultvaluemask) = 2 * (ge_balance_positive_mu_one_resultvaluemasklookupvalue) /\ (ge_balance_negative_mu_one_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_mu_one_resultvaluemasklookupvaluedecode. (((dc_value_mu_one_resultvaluemask) = 2 * ge_signed_half_mu_one_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_mu_one_resultvaluemasklookupvalue) = S ge_signed_half_mu_one_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_mu_one_resultvaluemasklookup) + ge_balance_negative_mu_one_resultvaluemasklookupvalue = (dst_negative_mu_one_resultvaluemasklookup) + ge_balance_positive_mu_one_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_mu_one_resultvaluemask)=0)) /\ (exists dc_quotient_mu_one_resultvaluemaskentry dc_left_mu_one_resultvaluemaskentry dc_right_mu_one_resultvaluemaskentry. (((dc_input_mu_one_result)=(dc_index_mu_one_resultvaluemask)*dc_quotient_mu_one_resultvaluemaskentry) /\ (((exists dst_positive_code_mu_one_resultvaluemaskentryleft dst_positive_scale_mu_one_resultvaluemaskentryleft dst_negative_code_mu_one_resultvaluemaskentryleft dst_negative_scale_mu_one_resultvaluemaskentryleft dst_positive_mu_one_resultvaluemaskentryleft dst_negative_mu_one_resultvaluemaskentryleft. (((M) = (((((dst_positive_code_mu_one_resultvaluemaskentryleft) + (dst_positive_scale_mu_one_resultvaluemaskentryleft)) * S ((dst_positive_code_mu_one_resultvaluemaskentryleft) + (dst_positive_scale_mu_one_resultvaluemaskentryleft)) + ((dst_positive_scale_mu_one_resultvaluemaskentryleft) + (dst_positive_scale_mu_one_resultvaluemaskentryleft))) + (((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) * S ((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) + ((dst_negative_scale_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)))) * S ((((dst_positive_code_mu_one_resultvaluemaskentryleft) + (dst_positive_scale_mu_one_resultvaluemaskentryleft)) * S ((dst_positive_code_mu_one_resultvaluemaskentryleft) + (dst_positive_scale_mu_one_resultvaluemaskentryleft)) + ((dst_positive_scale_mu_one_resultvaluemaskentryleft) + (dst_positive_scale_mu_one_resultvaluemaskentryleft))) + (((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) * S ((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) + ((dst_negative_scale_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)))) + ((((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) * S ((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) + ((dst_negative_scale_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft))) + (((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) * S ((dst_negative_code_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)) + ((dst_negative_scale_mu_one_resultvaluemaskentryleft) + (dst_negative_scale_mu_one_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemaskentryleftpositive. ff_h_pvs_mu_one_resultvaluemaskentryleftpositive + S (dst_positive_mu_one_resultvaluemaskentryleft) = S ((S (dc_index_mu_one_resultvaluemask)) * dst_positive_scale_mu_one_resultvaluemaskentryleft)) /\ exists ff_q_pvs_mu_one_resultvaluemaskentryleftpositive. dst_positive_code_mu_one_resultvaluemaskentryleft = ff_q_pvs_mu_one_resultvaluemaskentryleftpositive * S ((S (dc_index_mu_one_resultvaluemask)) * dst_positive_scale_mu_one_resultvaluemaskentryleft) + (dst_positive_mu_one_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemaskentryleftnegative. ff_h_pvs_mu_one_resultvaluemaskentryleftnegative + S (dst_negative_mu_one_resultvaluemaskentryleft) = S ((S (dc_index_mu_one_resultvaluemask)) * dst_negative_scale_mu_one_resultvaluemaskentryleft)) /\ exists ff_q_pvs_mu_one_resultvaluemaskentryleftnegative. dst_negative_code_mu_one_resultvaluemaskentryleft = ff_q_pvs_mu_one_resultvaluemaskentryleftnegative * S ((S (dc_index_mu_one_resultvaluemask)) * dst_negative_scale_mu_one_resultvaluemaskentryleft) + (dst_negative_mu_one_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_mu_one_resultvaluemaskentryleftvalue ge_balance_negative_mu_one_resultvaluemaskentryleftvalue. (((((dc_left_mu_one_resultvaluemaskentry) = 2 * (ge_balance_positive_mu_one_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_mu_one_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_mu_one_resultvaluemaskentryleftvaluedecode. (((dc_left_mu_one_resultvaluemaskentry) = 2 * ge_signed_half_mu_one_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_mu_one_resultvaluemaskentryleftvalue) = S ge_signed_half_mu_one_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_mu_one_resultvaluemaskentryleft) + ge_balance_negative_mu_one_resultvaluemaskentryleftvalue = (dst_negative_mu_one_resultvaluemaskentryleft) + ge_balance_positive_mu_one_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_mu_one_resultvaluemaskentryright dst_positive_scale_mu_one_resultvaluemaskentryright dst_negative_code_mu_one_resultvaluemaskentryright dst_negative_scale_mu_one_resultvaluemaskentryright dst_positive_mu_one_resultvaluemaskentryright dst_negative_mu_one_resultvaluemaskentryright. (((U) = (((((dst_positive_code_mu_one_resultvaluemaskentryright) + (dst_positive_scale_mu_one_resultvaluemaskentryright)) * S ((dst_positive_code_mu_one_resultvaluemaskentryright) + (dst_positive_scale_mu_one_resultvaluemaskentryright)) + ((dst_positive_scale_mu_one_resultvaluemaskentryright) + (dst_positive_scale_mu_one_resultvaluemaskentryright))) + (((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) * S ((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) + ((dst_negative_scale_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)))) * S ((((dst_positive_code_mu_one_resultvaluemaskentryright) + (dst_positive_scale_mu_one_resultvaluemaskentryright)) * S ((dst_positive_code_mu_one_resultvaluemaskentryright) + (dst_positive_scale_mu_one_resultvaluemaskentryright)) + ((dst_positive_scale_mu_one_resultvaluemaskentryright) + (dst_positive_scale_mu_one_resultvaluemaskentryright))) + (((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) * S ((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) + ((dst_negative_scale_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)))) + ((((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) * S ((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) + ((dst_negative_scale_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright))) + (((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) * S ((dst_negative_code_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)) + ((dst_negative_scale_mu_one_resultvaluemaskentryright) + (dst_negative_scale_mu_one_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemaskentryrightpositive. ff_h_pvs_mu_one_resultvaluemaskentryrightpositive + S (dst_positive_mu_one_resultvaluemaskentryright) = S ((S (dc_quotient_mu_one_resultvaluemaskentry)) * dst_positive_scale_mu_one_resultvaluemaskentryright)) /\ exists ff_q_pvs_mu_one_resultvaluemaskentryrightpositive. dst_positive_code_mu_one_resultvaluemaskentryright = ff_q_pvs_mu_one_resultvaluemaskentryrightpositive * S ((S (dc_quotient_mu_one_resultvaluemaskentry)) * dst_positive_scale_mu_one_resultvaluemaskentryright) + (dst_positive_mu_one_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_mu_one_resultvaluemaskentryrightnegative. ff_h_pvs_mu_one_resultvaluemaskentryrightnegative + S (dst_negative_mu_one_resultvaluemaskentryright) = S ((S (dc_quotient_mu_one_resultvaluemaskentry)) * dst_negative_scale_mu_one_resultvaluemaskentryright)) /\ exists ff_q_pvs_mu_one_resultvaluemaskentryrightnegative. dst_negative_code_mu_one_resultvaluemaskentryright = ff_q_pvs_mu_one_resultvaluemaskentryrightnegative * S ((S (dc_quotient_mu_one_resultvaluemaskentry)) * dst_negative_scale_mu_one_resultvaluemaskentryright) + (dst_negative_mu_one_resultvaluemaskentryright))) /\ (exists ge_balance_positive_mu_one_resultvaluemaskentryrightvalue ge_balance_negative_mu_one_resultvaluemaskentryrightvalue. (((((dc_right_mu_one_resultvaluemaskentry) = 2 * (ge_balance_positive_mu_one_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_mu_one_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_mu_one_resultvaluemaskentryrightvaluedecode. (((dc_right_mu_one_resultvaluemaskentry) = 2 * ge_signed_half_mu_one_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_mu_one_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_mu_one_resultvaluemaskentryrightvalue) = S ge_signed_half_mu_one_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_mu_one_resultvaluemaskentryright) + ge_balance_negative_mu_one_resultvaluemaskentryrightvalue = (dst_negative_mu_one_resultvaluemaskentryright) + ge_balance_positive_mu_one_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_mu_one_resultvaluemaskentryproduct sto_an_mu_one_resultvaluemaskentryproduct sto_bp_mu_one_resultvaluemaskentryproduct sto_bn_mu_one_resultvaluemaskentryproduct sto_cp_mu_one_resultvaluemaskentryproduct sto_cn_mu_one_resultvaluemaskentryproduct. (((((dc_left_mu_one_resultvaluemaskentry) = 2 * (sto_ap_mu_one_resultvaluemaskentryproduct) /\ (sto_an_mu_one_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_mu_one_resultvaluemaskentryproductleft. (((dc_left_mu_one_resultvaluemaskentry) = 2 * ge_signed_half_mu_one_resultvaluemaskentryproductleft + 1 /\ (sto_ap_mu_one_resultvaluemaskentryproduct) = 0) /\ (sto_an_mu_one_resultvaluemaskentryproduct) = S ge_signed_half_mu_one_resultvaluemaskentryproductleft))) /\ ((((((dc_right_mu_one_resultvaluemaskentry) = 2 * (sto_bp_mu_one_resultvaluemaskentryproduct) /\ (sto_bn_mu_one_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_mu_one_resultvaluemaskentryproductright. (((dc_right_mu_one_resultvaluemaskentry) = 2 * ge_signed_half_mu_one_resultvaluemaskentryproductright + 1 /\ (sto_bp_mu_one_resultvaluemaskentryproduct) = 0) /\ (sto_bn_mu_one_resultvaluemaskentryproduct) = S ge_signed_half_mu_one_resultvaluemaskentryproductright))) /\ ((((((dc_value_mu_one_resultvaluemask) = 2 * (sto_cp_mu_one_resultvaluemaskentryproduct) /\ (sto_cn_mu_one_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_mu_one_resultvaluemaskentryproductoutput. (((dc_value_mu_one_resultvaluemask) = 2 * ge_signed_half_mu_one_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_mu_one_resultvaluemaskentryproduct) = 0) /\ (sto_cn_mu_one_resultvaluemaskentryproduct) = S ge_signed_half_mu_one_resultvaluemaskentryproductoutput))) /\ ((sto_ap_mu_one_resultvaluemaskentryproduct * sto_bp_mu_one_resultvaluemaskentryproduct + sto_an_mu_one_resultvaluemaskentryproduct * sto_bn_mu_one_resultvaluemaskentryproduct) + sto_cn_mu_one_resultvaluemaskentryproduct = (sto_ap_mu_one_resultvaluemaskentryproduct * sto_bn_mu_one_resultvaluemaskentryproduct + sto_an_mu_one_resultvaluemaskentryproduct * sto_bp_mu_one_resultvaluemaskentryproduct) + sto_cp_mu_one_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_mu_one_resultvaluemask)=0 \/ ~(exists pvs_factor_mu_one_resultvaluemaskentrynondivisor. (dc_input_mu_one_result) = (dc_index_mu_one_resultvaluemask) * pvs_factor_mu_one_resultvaluemaskentrynondivisor)) /\ ((dc_value_mu_one_resultvaluemask)=0))))))) /\ (exists dst_positive_code_mu_one_resultvaluefold dst_positive_scale_mu_one_resultvaluefold dst_negative_code_mu_one_resultvaluefold dst_negative_scale_mu_one_resultvaluefold dst_positive_sum_mu_one_resultvaluefold dst_negative_sum_mu_one_resultvaluefold. (((dc_mask_mu_one_resultvalue) = (((((dst_positive_code_mu_one_resultvaluefold) + (dst_positive_scale_mu_one_resultvaluefold)) * S ((dst_positive_code_mu_one_resultvaluefold) + (dst_positive_scale_mu_one_resultvaluefold)) + ((dst_positive_scale_mu_one_resultvaluefold) + (dst_positive_scale_mu_one_resultvaluefold))) + (((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) * S ((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) + ((dst_negative_scale_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)))) * S ((((dst_positive_code_mu_one_resultvaluefold) + (dst_positive_scale_mu_one_resultvaluefold)) * S ((dst_positive_code_mu_one_resultvaluefold) + (dst_positive_scale_mu_one_resultvaluefold)) + ((dst_positive_scale_mu_one_resultvaluefold) + (dst_positive_scale_mu_one_resultvaluefold))) + (((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) * S ((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) + ((dst_negative_scale_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)))) + ((((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) * S ((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) + ((dst_negative_scale_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold))) + (((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) * S ((dst_negative_code_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)) + ((dst_negative_scale_mu_one_resultvaluefold) + (dst_negative_scale_mu_one_resultvaluefold)))))) /\ (((exists fs_u_dst_mu_one_resultvaluefoldpositive fs_v_dst_mu_one_resultvaluefoldpositive. ((((exists fs_h_dst_mu_one_resultvaluefoldpositive_body_start. fs_h_dst_mu_one_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_mu_one_resultvaluefoldpositive)) /\ exists fs_q_dst_mu_one_resultvaluefoldpositive_body_start. fs_u_dst_mu_one_resultvaluefoldpositive = fs_q_dst_mu_one_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_mu_one_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_mu_one_resultvaluefoldpositive_body_terminal. fs_h_dst_mu_one_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_mu_one_resultvaluefold) = S ((S (S (dc_input_mu_one_result))) * fs_v_dst_mu_one_resultvaluefoldpositive)) /\ exists fs_q_dst_mu_one_resultvaluefoldpositive_body_terminal. fs_u_dst_mu_one_resultvaluefoldpositive = fs_q_dst_mu_one_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_mu_one_result))) * fs_v_dst_mu_one_resultvaluefoldpositive) + (dst_positive_sum_mu_one_resultvaluefold))) /\ forall fs_i_dst_mu_one_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_mu_one_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_mu_one_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_mu_one_resultvaluefoldpositive_body_steps = S (dc_input_mu_one_result)) -> exists fs_a_dst_mu_one_resultvaluefoldpositive_body_steps fs_r_dst_mu_one_resultvaluefoldpositive_body_steps fs_s_dst_mu_one_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_mu_one_resultvaluefoldpositive_body_steps_summand. fs_h_dst_mu_one_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_mu_one_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_mu_one_resultvaluefoldpositive_body_steps)) * dst_positive_scale_mu_one_resultvaluefold)) /\ exists fs_q_dst_mu_one_resultvaluefoldpositive_body_steps_summand. dst_positive_code_mu_one_resultvaluefold = fs_q_dst_mu_one_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_mu_one_resultvaluefoldpositive_body_steps)) * dst_positive_scale_mu_one_resultvaluefold) + (fs_a_dst_mu_one_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_mu_one_resultvaluefoldpositive_body_steps_partial. fs_h_dst_mu_one_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_mu_one_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_mu_one_resultvaluefoldpositive_body_steps)) * fs_v_dst_mu_one_resultvaluefoldpositive)) /\ exists fs_q_dst_mu_one_resultvaluefoldpositive_body_steps_partial. fs_u_dst_mu_one_resultvaluefoldpositive = fs_q_dst_mu_one_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_mu_one_resultvaluefoldpositive_body_steps)) * fs_v_dst_mu_one_resultvaluefoldpositive) + (fs_r_dst_mu_one_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_mu_one_resultvaluefoldpositive_body_steps_successor. fs_h_dst_mu_one_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_mu_one_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_mu_one_resultvaluefoldpositive_body_steps)) * fs_v_dst_mu_one_resultvaluefoldpositive)) /\ exists fs_q_dst_mu_one_resultvaluefoldpositive_body_steps_successor. fs_u_dst_mu_one_resultvaluefoldpositive = fs_q_dst_mu_one_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_mu_one_resultvaluefoldpositive_body_steps)) * fs_v_dst_mu_one_resultvaluefoldpositive) + (fs_s_dst_mu_one_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_mu_one_resultvaluefoldpositive_body_steps = fs_r_dst_mu_one_resultvaluefoldpositive_body_steps + fs_a_dst_mu_one_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_mu_one_resultvaluefoldnegative fs_v_dst_mu_one_resultvaluefoldnegative. ((((exists fs_h_dst_mu_one_resultvaluefoldnegative_body_start. fs_h_dst_mu_one_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_mu_one_resultvaluefoldnegative)) /\ exists fs_q_dst_mu_one_resultvaluefoldnegative_body_start. fs_u_dst_mu_one_resultvaluefoldnegative = fs_q_dst_mu_one_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_mu_one_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_mu_one_resultvaluefoldnegative_body_terminal. fs_h_dst_mu_one_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_mu_one_resultvaluefold) = S ((S (S (dc_input_mu_one_result))) * fs_v_dst_mu_one_resultvaluefoldnegative)) /\ exists fs_q_dst_mu_one_resultvaluefoldnegative_body_terminal. fs_u_dst_mu_one_resultvaluefoldnegative = fs_q_dst_mu_one_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_mu_one_result))) * fs_v_dst_mu_one_resultvaluefoldnegative) + (dst_negative_sum_mu_one_resultvaluefold))) /\ forall fs_i_dst_mu_one_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_mu_one_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_mu_one_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_mu_one_resultvaluefoldnegative_body_steps = S (dc_input_mu_one_result)) -> exists fs_a_dst_mu_one_resultvaluefoldnegative_body_steps fs_r_dst_mu_one_resultvaluefoldnegative_body_steps fs_s_dst_mu_one_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_mu_one_resultvaluefoldnegative_body_steps_summand. fs_h_dst_mu_one_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_mu_one_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_mu_one_resultvaluefoldnegative_body_steps)) * dst_negative_scale_mu_one_resultvaluefold)) /\ exists fs_q_dst_mu_one_resultvaluefoldnegative_body_steps_summand. dst_negative_code_mu_one_resultvaluefold = fs_q_dst_mu_one_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_mu_one_resultvaluefoldnegative_body_steps)) * dst_negative_scale_mu_one_resultvaluefold) + (fs_a_dst_mu_one_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_mu_one_resultvaluefoldnegative_body_steps_partial. fs_h_dst_mu_one_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_mu_one_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_mu_one_resultvaluefoldnegative_body_steps)) * fs_v_dst_mu_one_resultvaluefoldnegative)) /\ exists fs_q_dst_mu_one_resultvaluefoldnegative_body_steps_partial. fs_u_dst_mu_one_resultvaluefoldnegative = fs_q_dst_mu_one_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_mu_one_resultvaluefoldnegative_body_steps)) * fs_v_dst_mu_one_resultvaluefoldnegative) + (fs_r_dst_mu_one_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_mu_one_resultvaluefoldnegative_body_steps_successor. fs_h_dst_mu_one_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_mu_one_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_mu_one_resultvaluefoldnegative_body_steps)) * fs_v_dst_mu_one_resultvaluefoldnegative)) /\ exists fs_q_dst_mu_one_resultvaluefoldnegative_body_steps_successor. fs_u_dst_mu_one_resultvaluefoldnegative = fs_q_dst_mu_one_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_mu_one_resultvaluefoldnegative_body_steps)) * fs_v_dst_mu_one_resultvaluefoldnegative) + (fs_s_dst_mu_one_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_mu_one_resultvaluefoldnegative_body_steps = fs_r_dst_mu_one_resultvaluefoldnegative_body_steps + fs_a_dst_mu_one_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_mu_one_resultvaluefoldresult ge_balance_negative_mu_one_resultvaluefoldresult. (((((dc_output_mu_one_result) = 2 * (ge_balance_positive_mu_one_resultvaluefoldresult) /\ (ge_balance_negative_mu_one_resultvaluefoldresult) = 0) \/ exists ge_signed_half_mu_one_resultvaluefoldresultdecode. (((dc_output_mu_one_result) = 2 * ge_signed_half_mu_one_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_mu_one_resultvaluefoldresult) = 0) /\ (ge_balance_negative_mu_one_resultvaluefoldresult) = S ge_signed_half_mu_one_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_mu_one_resultvaluefold) + ge_balance_negative_mu_one_resultvaluefoldresult = (dst_negative_sum_mu_one_resultvaluefold) + ge_balance_positive_mu_one_resultvaluefoldresult))))))))))))))))))))