mobius_dirichlet_inversion_value

Exact expanded first-order arithmetic statement

forall N F G M U E n a b. (exists dst_positive_code_value_source dst_positive_scale_value_source dst_negative_code_value_source dst_negative_scale_value_source. (((F) = (((((dst_positive_code_value_source) + (dst_positive_scale_value_source)) * S ((dst_positive_code_value_source) + (dst_positive_scale_value_source)) + ((dst_positive_scale_value_source) + (dst_positive_scale_value_source))) + (((dst_negative_code_value_source) + (dst_negative_scale_value_source)) * S ((dst_negative_code_value_source) + (dst_negative_scale_value_source)) + ((dst_negative_scale_value_source) + (dst_negative_scale_value_source)))) * S ((((dst_positive_code_value_source) + (dst_positive_scale_value_source)) * S ((dst_positive_code_value_source) + (dst_positive_scale_value_source)) + ((dst_positive_scale_value_source) + (dst_positive_scale_value_source))) + (((dst_negative_code_value_source) + (dst_negative_scale_value_source)) * S ((dst_negative_code_value_source) + (dst_negative_scale_value_source)) + ((dst_negative_scale_value_source) + (dst_negative_scale_value_source)))) + ((((dst_negative_code_value_source) + (dst_negative_scale_value_source)) * S ((dst_negative_code_value_source) + (dst_negative_scale_value_source)) + ((dst_negative_scale_value_source) + (dst_negative_scale_value_source))) + (((dst_negative_code_value_source) + (dst_negative_scale_value_source)) * S ((dst_negative_code_value_source) + (dst_negative_scale_value_source)) + ((dst_negative_scale_value_source) + (dst_negative_scale_value_source)))))) /\ (forall dst_index_value_source. (exists pvs_le_gap_value_sourcedomain. pvs_le_gap_value_sourcedomain + (dst_index_value_source) = (N)) -> exists dst_positive_value_source dst_negative_value_source dst_value_value_source. ((((exists ff_h_pvs_value_sourceentrypositive. ff_h_pvs_value_sourceentrypositive + S (dst_positive_value_source) = S ((S (dst_index_value_source)) * dst_positive_scale_value_source)) /\ exists ff_q_pvs_value_sourceentrypositive. dst_positive_code_value_source = ff_q_pvs_value_sourceentrypositive * S ((S (dst_index_value_source)) * dst_positive_scale_value_source) + (dst_positive_value_source))) /\ (((((exists ff_h_pvs_value_sourceentrynegative. ff_h_pvs_value_sourceentrynegative + S (dst_negative_value_source) = S ((S (dst_index_value_source)) * dst_negative_scale_value_source)) /\ exists ff_q_pvs_value_sourceentrynegative. dst_negative_code_value_source = ff_q_pvs_value_sourceentrynegative * S ((S (dst_index_value_source)) * dst_negative_scale_value_source) + (dst_negative_value_source))) /\ (exists ge_balance_positive_value_sourceentryvalue ge_balance_negative_value_sourceentryvalue. (((((dst_value_value_source) = 2 * (ge_balance_positive_value_sourceentryvalue) /\ (ge_balance_negative_value_sourceentryvalue) = 0) \/ exists ge_signed_half_value_sourceentryvaluedecode. (((dst_value_value_source) = 2 * ge_signed_half_value_sourceentryvaluedecode + 1 /\ (ge_balance_positive_value_sourceentryvalue) = 0) /\ (ge_balance_negative_value_sourceentryvalue) = S ge_signed_half_value_sourceentryvaluedecode))) /\ ((dst_positive_value_source) + ge_balance_negative_value_sourceentryvalue = (dst_negative_value_source) + ge_balance_positive_value_sourceentryvalue))))))))) -> (exists dst_positive_code_value_transform_table dst_positive_scale_value_transform_table dst_negative_code_value_transform_table dst_negative_scale_value_transform_table. (((G) = (((((dst_positive_code_value_transform_table) + (dst_positive_scale_value_transform_table)) * S ((dst_positive_code_value_transform_table) + (dst_positive_scale_value_transform_table)) + ((dst_positive_scale_value_transform_table) + (dst_positive_scale_value_transform_table))) + (((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) * S ((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) + ((dst_negative_scale_value_transform_table) + (dst_negative_scale_value_transform_table)))) * S ((((dst_positive_code_value_transform_table) + (dst_positive_scale_value_transform_table)) * S ((dst_positive_code_value_transform_table) + (dst_positive_scale_value_transform_table)) + ((dst_positive_scale_value_transform_table) + (dst_positive_scale_value_transform_table))) + (((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) * S ((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) + ((dst_negative_scale_value_transform_table) + (dst_negative_scale_value_transform_table)))) + ((((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) * S ((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) + ((dst_negative_scale_value_transform_table) + (dst_negative_scale_value_transform_table))) + (((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) * S ((dst_negative_code_value_transform_table) + (dst_negative_scale_value_transform_table)) + ((dst_negative_scale_value_transform_table) + (dst_negative_scale_value_transform_table)))))) /\ (forall dst_index_value_transform_table. (exists pvs_le_gap_value_transform_tabledomain. pvs_le_gap_value_transform_tabledomain + (dst_index_value_transform_table) = (N)) -> exists dst_positive_value_transform_table dst_negative_value_transform_table dst_value_value_transform_table. ((((exists ff_h_pvs_value_transform_tableentrypositive. ff_h_pvs_value_transform_tableentrypositive + S (dst_positive_value_transform_table) = S ((S (dst_index_value_transform_table)) * dst_positive_scale_value_transform_table)) /\ exists ff_q_pvs_value_transform_tableentrypositive. dst_positive_code_value_transform_table = ff_q_pvs_value_transform_tableentrypositive * S ((S (dst_index_value_transform_table)) * dst_positive_scale_value_transform_table) + (dst_positive_value_transform_table))) /\ (((((exists ff_h_pvs_value_transform_tableentrynegative. ff_h_pvs_value_transform_tableentrynegative + S (dst_negative_value_transform_table) = S ((S (dst_index_value_transform_table)) * dst_negative_scale_value_transform_table)) /\ exists ff_q_pvs_value_transform_tableentrynegative. dst_negative_code_value_transform_table = ff_q_pvs_value_transform_tableentrynegative * S ((S (dst_index_value_transform_table)) * dst_negative_scale_value_transform_table) + (dst_negative_value_transform_table))) /\ (exists ge_balance_positive_value_transform_tableentryvalue ge_balance_negative_value_transform_tableentryvalue. (((((dst_value_value_transform_table) = 2 * (ge_balance_positive_value_transform_tableentryvalue) /\ (ge_balance_negative_value_transform_tableentryvalue) = 0) \/ exists ge_signed_half_value_transform_tableentryvaluedecode. (((dst_value_value_transform_table) = 2 * ge_signed_half_value_transform_tableentryvaluedecode + 1 /\ (ge_balance_positive_value_transform_tableentryvalue) = 0) /\ (ge_balance_negative_value_transform_tableentryvalue) = S ge_signed_half_value_transform_tableentryvaluedecode))) /\ ((dst_positive_value_transform_table) + ge_balance_negative_value_transform_tableentryvalue = (dst_negative_value_transform_table) + ge_balance_positive_value_transform_tableentryvalue))))))))) -> (((exists dst_positive_code_value_mobiustable dst_positive_scale_value_mobiustable dst_negative_code_value_mobiustable dst_negative_scale_value_mobiustable. (((M) = (((((dst_positive_code_value_mobiustable) + (dst_positive_scale_value_mobiustable)) * S ((dst_positive_code_value_mobiustable) + (dst_positive_scale_value_mobiustable)) + ((dst_positive_scale_value_mobiustable) + (dst_positive_scale_value_mobiustable))) + (((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) * S ((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) + ((dst_negative_scale_value_mobiustable) + (dst_negative_scale_value_mobiustable)))) * S ((((dst_positive_code_value_mobiustable) + (dst_positive_scale_value_mobiustable)) * S ((dst_positive_code_value_mobiustable) + (dst_positive_scale_value_mobiustable)) + ((dst_positive_scale_value_mobiustable) + (dst_positive_scale_value_mobiustable))) + (((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) * S ((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) + ((dst_negative_scale_value_mobiustable) + (dst_negative_scale_value_mobiustable)))) + ((((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) * S ((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) + ((dst_negative_scale_value_mobiustable) + (dst_negative_scale_value_mobiustable))) + (((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) * S ((dst_negative_code_value_mobiustable) + (dst_negative_scale_value_mobiustable)) + ((dst_negative_scale_value_mobiustable) + (dst_negative_scale_value_mobiustable)))))) /\ (forall dst_index_value_mobiustable. (exists pvs_le_gap_value_mobiustabledomain. pvs_le_gap_value_mobiustabledomain + (dst_index_value_mobiustable) = (N)) -> exists dst_positive_value_mobiustable dst_negative_value_mobiustable dst_value_value_mobiustable. ((((exists ff_h_pvs_value_mobiustableentrypositive. ff_h_pvs_value_mobiustableentrypositive + S (dst_positive_value_mobiustable) = S ((S (dst_index_value_mobiustable)) * dst_positive_scale_value_mobiustable)) /\ exists ff_q_pvs_value_mobiustableentrypositive. dst_positive_code_value_mobiustable = ff_q_pvs_value_mobiustableentrypositive * S ((S (dst_index_value_mobiustable)) * dst_positive_scale_value_mobiustable) + (dst_positive_value_mobiustable))) /\ (((((exists ff_h_pvs_value_mobiustableentrynegative. ff_h_pvs_value_mobiustableentrynegative + S (dst_negative_value_mobiustable) = S ((S (dst_index_value_mobiustable)) * dst_negative_scale_value_mobiustable)) /\ exists ff_q_pvs_value_mobiustableentrynegative. dst_negative_code_value_mobiustable = ff_q_pvs_value_mobiustableentrynegative * S ((S (dst_index_value_mobiustable)) * dst_negative_scale_value_mobiustable) + (dst_negative_value_mobiustable))) /\ (exists ge_balance_positive_value_mobiustableentryvalue ge_balance_negative_value_mobiustableentryvalue. (((((dst_value_value_mobiustable) = 2 * (ge_balance_positive_value_mobiustableentryvalue) /\ (ge_balance_negative_value_mobiustableentryvalue) = 0) \/ exists ge_signed_half_value_mobiustableentryvaluedecode. (((dst_value_value_mobiustable) = 2 * ge_signed_half_value_mobiustableentryvaluedecode + 1 /\ (ge_balance_positive_value_mobiustableentryvalue) = 0) /\ (ge_balance_negative_value_mobiustableentryvalue) = S ge_signed_half_value_mobiustableentryvaluedecode))) /\ ((dst_positive_value_mobiustable) + ge_balance_negative_value_mobiustableentryvalue = (dst_negative_value_mobiustable) + ge_balance_positive_value_mobiustableentryvalue))))))))) /\ (((exists dst_positive_code_value_mobiuszero dst_positive_scale_value_mobiuszero dst_negative_code_value_mobiuszero dst_negative_scale_value_mobiuszero dst_positive_value_mobiuszero dst_negative_value_mobiuszero. (((M) = (((((dst_positive_code_value_mobiuszero) + (dst_positive_scale_value_mobiuszero)) * S ((dst_positive_code_value_mobiuszero) + (dst_positive_scale_value_mobiuszero)) + ((dst_positive_scale_value_mobiuszero) + (dst_positive_scale_value_mobiuszero))) + (((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) * S ((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) + ((dst_negative_scale_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)))) * S ((((dst_positive_code_value_mobiuszero) + (dst_positive_scale_value_mobiuszero)) * S ((dst_positive_code_value_mobiuszero) + (dst_positive_scale_value_mobiuszero)) + ((dst_positive_scale_value_mobiuszero) + (dst_positive_scale_value_mobiuszero))) + (((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) * S ((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) + ((dst_negative_scale_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)))) + ((((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) * S ((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) + ((dst_negative_scale_value_mobiuszero) + (dst_negative_scale_value_mobiuszero))) + (((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) * S ((dst_negative_code_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)) + ((dst_negative_scale_value_mobiuszero) + (dst_negative_scale_value_mobiuszero)))))) /\ (((((exists ff_h_pvs_value_mobiuszeropositive. ff_h_pvs_value_mobiuszeropositive + S (dst_positive_value_mobiuszero) = S ((S (0)) * dst_positive_scale_value_mobiuszero)) /\ exists ff_q_pvs_value_mobiuszeropositive. dst_positive_code_value_mobiuszero = ff_q_pvs_value_mobiuszeropositive * S ((S (0)) * dst_positive_scale_value_mobiuszero) + (dst_positive_value_mobiuszero))) /\ (((((exists ff_h_pvs_value_mobiuszeronegative. ff_h_pvs_value_mobiuszeronegative + S (dst_negative_value_mobiuszero) = S ((S (0)) * dst_negative_scale_value_mobiuszero)) /\ exists ff_q_pvs_value_mobiuszeronegative. dst_negative_code_value_mobiuszero = ff_q_pvs_value_mobiuszeronegative * S ((S (0)) * dst_negative_scale_value_mobiuszero) + (dst_negative_value_mobiuszero))) /\ (exists ge_balance_positive_value_mobiuszerovalue ge_balance_negative_value_mobiuszerovalue. (((((0) = 2 * (ge_balance_positive_value_mobiuszerovalue) /\ (ge_balance_negative_value_mobiuszerovalue) = 0) \/ exists ge_signed_half_value_mobiuszerovaluedecode. (((0) = 2 * ge_signed_half_value_mobiuszerovaluedecode + 1 /\ (ge_balance_positive_value_mobiuszerovalue) = 0) /\ (ge_balance_negative_value_mobiuszerovalue) = S ge_signed_half_value_mobiuszerovaluedecode))) /\ ((dst_positive_value_mobiuszero) + ge_balance_negative_value_mobiuszerovalue = (dst_negative_value_mobiuszero) + ge_balance_positive_value_mobiuszerovalue))))))))) /\ (forall mt_index_value_mobius mt_value_value_mobius. ~(mt_index_value_mobius=0) -> (exists pvs_le_gap_value_mobiusdomain. pvs_le_gap_value_mobiusdomain + (mt_index_value_mobius) = (N)) -> (exists dst_positive_code_value_mobiusentry dst_positive_scale_value_mobiusentry dst_negative_code_value_mobiusentry dst_negative_scale_value_mobiusentry dst_positive_value_mobiusentry dst_negative_value_mobiusentry. (((M) = (((((dst_positive_code_value_mobiusentry) + (dst_positive_scale_value_mobiusentry)) * S ((dst_positive_code_value_mobiusentry) + (dst_positive_scale_value_mobiusentry)) + ((dst_positive_scale_value_mobiusentry) + (dst_positive_scale_value_mobiusentry))) + (((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) * S ((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) + ((dst_negative_scale_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)))) * S ((((dst_positive_code_value_mobiusentry) + (dst_positive_scale_value_mobiusentry)) * S ((dst_positive_code_value_mobiusentry) + (dst_positive_scale_value_mobiusentry)) + ((dst_positive_scale_value_mobiusentry) + (dst_positive_scale_value_mobiusentry))) + (((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) * S ((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) + ((dst_negative_scale_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)))) + ((((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) * S ((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) + ((dst_negative_scale_value_mobiusentry) + (dst_negative_scale_value_mobiusentry))) + (((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) * S ((dst_negative_code_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)) + ((dst_negative_scale_value_mobiusentry) + (dst_negative_scale_value_mobiusentry)))))) /\ (((((exists ff_h_pvs_value_mobiusentrypositive. ff_h_pvs_value_mobiusentrypositive + S (dst_positive_value_mobiusentry) = S ((S (mt_index_value_mobius)) * dst_positive_scale_value_mobiusentry)) /\ exists ff_q_pvs_value_mobiusentrypositive. dst_positive_code_value_mobiusentry = ff_q_pvs_value_mobiusentrypositive * S ((S (mt_index_value_mobius)) * dst_positive_scale_value_mobiusentry) + (dst_positive_value_mobiusentry))) /\ (((((exists ff_h_pvs_value_mobiusentrynegative. ff_h_pvs_value_mobiusentrynegative + S (dst_negative_value_mobiusentry) = S ((S (mt_index_value_mobius)) * dst_negative_scale_value_mobiusentry)) /\ exists ff_q_pvs_value_mobiusentrynegative. dst_negative_code_value_mobiusentry = ff_q_pvs_value_mobiusentrynegative * S ((S (mt_index_value_mobius)) * dst_negative_scale_value_mobiusentry) + (dst_negative_value_mobiusentry))) /\ (exists ge_balance_positive_value_mobiusentryvalue ge_balance_negative_value_mobiusentryvalue. (((((mt_value_value_mobius) = 2 * (ge_balance_positive_value_mobiusentryvalue) /\ (ge_balance_negative_value_mobiusentryvalue) = 0) \/ exists ge_signed_half_value_mobiusentryvaluedecode. (((mt_value_value_mobius) = 2 * ge_signed_half_value_mobiusentryvaluedecode + 1 /\ (ge_balance_positive_value_mobiusentryvalue) = 0) /\ (ge_balance_negative_value_mobiusentryvalue) = S ge_signed_half_value_mobiusentryvaluedecode))) /\ ((dst_positive_value_mobiusentry) + ge_balance_negative_value_mobiusentryvalue = (dst_negative_value_mobiusentry) + ge_balance_positive_value_mobiusentryvalue))))))))) -> (((~((mt_index_value_mobius) = 0)) /\ ((((exists mv_square_prime_value_mobiusvaluesquare. ((~((mv_square_prime_value_mobiusvaluesquare) = 1) /\ forall pvs_left_value_mobiusvaluesquareprime pvs_right_value_mobiusvaluesquareprime. (mv_square_prime_value_mobiusvaluesquare) = pvs_left_value_mobiusvaluesquareprime * pvs_right_value_mobiusvaluesquareprime -> pvs_left_value_mobiusvaluesquareprime = 1 \/ pvs_right_value_mobiusvaluesquareprime = 1) /\ (exists pvs_factor_value_mobiusvaluesquaredivisor. (mt_index_value_mobius) = (mv_square_prime_value_mobiusvaluesquare * mv_square_prime_value_mobiusvaluesquare) * pvs_factor_value_mobiusvaluesquaredivisor))) /\ ((mt_value_value_mobius) = 0))) \/ (((((~((mt_index_value_mobius) = 0)) /\ (forall sfd_prime_value_mobiusvaluesquarefree. (~((sfd_prime_value_mobiusvaluesquarefree) = 1) /\ forall pvs_left_value_mobiusvaluesquarefreedomain pvs_right_value_mobiusvaluesquarefreedomain. (sfd_prime_value_mobiusvaluesquarefree) = pvs_left_value_mobiusvaluesquarefreedomain * pvs_right_value_mobiusvaluesquarefreedomain -> pvs_left_value_mobiusvaluesquarefreedomain = 1 \/ pvs_right_value_mobiusvaluesquarefreedomain = 1) -> (exists pvs_le_gap_value_mobiusvaluesquarefreebound. pvs_le_gap_value_mobiusvaluesquarefreebound + (sfd_prime_value_mobiusvaluesquarefree) = (mt_index_value_mobius)) -> ~(exists pvs_factor_value_mobiusvaluesquarefreesquare. (mt_index_value_mobius) = (sfd_prime_value_mobiusvaluesquarefree * sfd_prime_value_mobiusvaluesquarefree) * pvs_factor_value_mobiusvaluesquarefreesquare)))) /\ (exists mv_factor_code_value_mobiusvaluefactors mv_factor_scale_value_mobiusvaluefactors mv_factor_count_value_mobiusvaluefactors. (((~(mt_index_value_mobius = 0) /\ ((exists ff_u_fsat_value_mobiusvaluefactorsfactorization_product ff_v_fsat_value_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_value_mobiusvaluefactorsfactorization_product_start. ff_h_fsat_value_mobiusvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_value_mobiusvaluefactorsfactorization_product_start. ff_u_fsat_value_mobiusvaluefactorsfactorization_product = ff_q_fsat_value_mobiusvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_value_mobiusvaluefactorsfactorization_product_terminal. ff_h_fsat_value_mobiusvaluefactorsfactorization_product_terminal + S (mt_index_value_mobius) = S ((S (mv_factor_count_value_mobiusvaluefactors)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_value_mobiusvaluefactorsfactorization_product_terminal. ff_u_fsat_value_mobiusvaluefactorsfactorization_product = ff_q_fsat_value_mobiusvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_value_mobiusvaluefactors)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product) + (mt_index_value_mobius))) /\ forall ff_i_fsat_value_mobiusvaluefactorsfactorization_product. (exists ff_lt_fsat_value_mobiusvaluefactorsfactorization_product_bound. ff_lt_fsat_value_mobiusvaluefactorsfactorization_product_bound + S ff_i_fsat_value_mobiusvaluefactorsfactorization_product = mv_factor_count_value_mobiusvaluefactors) -> exists ff_p_fsat_value_mobiusvaluefactorsfactorization_product ff_r_fsat_value_mobiusvaluefactorsfactorization_product ff_s_fsat_value_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_value_mobiusvaluefactorsfactorization_product_factor. ff_h_fsat_value_mobiusvaluefactorsfactorization_product_factor + S (ff_p_fsat_value_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_value_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_value_mobiusvaluefactors)) /\ exists ff_q_fsat_value_mobiusvaluefactorsfactorization_product_factor. mv_factor_code_value_mobiusvaluefactors = ff_q_fsat_value_mobiusvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_value_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_value_mobiusvaluefactors) + (ff_p_fsat_value_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_mobiusvaluefactorsfactorization_product_partial. ff_h_fsat_value_mobiusvaluefactorsfactorization_product_partial + S (ff_r_fsat_value_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_value_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_value_mobiusvaluefactorsfactorization_product_partial. ff_u_fsat_value_mobiusvaluefactorsfactorization_product = ff_q_fsat_value_mobiusvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_value_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product) + (ff_r_fsat_value_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_value_mobiusvaluefactorsfactorization_product_successor. ff_h_fsat_value_mobiusvaluefactorsfactorization_product_successor + S (ff_s_fsat_value_mobiusvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_value_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_value_mobiusvaluefactorsfactorization_product_successor. ff_u_fsat_value_mobiusvaluefactorsfactorization_product = ff_q_fsat_value_mobiusvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_value_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_value_mobiusvaluefactorsfactorization_product) + (ff_s_fsat_value_mobiusvaluefactorsfactorization_product))) /\ ff_s_fsat_value_mobiusvaluefactorsfactorization_product = ff_r_fsat_value_mobiusvaluefactorsfactorization_product * ff_p_fsat_value_mobiusvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_value_mobiusvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_value_mobiusvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_value_mobiusvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_value_mobiusvaluefactorsfactorization_primes = (mv_factor_count_value_mobiusvaluefactors)) -> exists ftsf_factor_fsat_value_mobiusvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_value_mobiusvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_value_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_value_mobiusvaluefactors)) /\ exists ff_q_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_entry. mv_factor_code_value_mobiusvaluefactors = ff_q_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_value_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_value_mobiusvaluefactors) + (ftsf_factor_fsat_value_mobiusvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_value_mobiusvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_value_mobiusvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_value_mobiusvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_value_mobiusvaluefactorsparityeven. (mv_factor_count_value_mobiusvaluefactors) = 2 * mv_even_half_value_mobiusvaluefactorsparityeven) /\ ((mt_value_value_mobius) = 2))) \/ (((exists mv_odd_half_value_mobiusvaluefactorsparityodd. (mv_factor_count_value_mobiusvaluefactors) = 2 * mv_odd_half_value_mobiusvaluefactorsparityodd + 1) /\ ((mt_value_value_mobius) = 1)))))))))))))))) -> (((exists dst_positive_code_value_onetable dst_positive_scale_value_onetable dst_negative_code_value_onetable dst_negative_scale_value_onetable. (((U) = (((((dst_positive_code_value_onetable) + (dst_positive_scale_value_onetable)) * S ((dst_positive_code_value_onetable) + (dst_positive_scale_value_onetable)) + ((dst_positive_scale_value_onetable) + (dst_positive_scale_value_onetable))) + (((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) * S ((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) + ((dst_negative_scale_value_onetable) + (dst_negative_scale_value_onetable)))) * S ((((dst_positive_code_value_onetable) + (dst_positive_scale_value_onetable)) * S ((dst_positive_code_value_onetable) + (dst_positive_scale_value_onetable)) + ((dst_positive_scale_value_onetable) + (dst_positive_scale_value_onetable))) + (((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) * S ((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) + ((dst_negative_scale_value_onetable) + (dst_negative_scale_value_onetable)))) + ((((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) * S ((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) + ((dst_negative_scale_value_onetable) + (dst_negative_scale_value_onetable))) + (((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) * S ((dst_negative_code_value_onetable) + (dst_negative_scale_value_onetable)) + ((dst_negative_scale_value_onetable) + (dst_negative_scale_value_onetable)))))) /\ (forall dst_index_value_onetable. (exists pvs_le_gap_value_onetabledomain. pvs_le_gap_value_onetabledomain + (dst_index_value_onetable) = (N)) -> exists dst_positive_value_onetable dst_negative_value_onetable dst_value_value_onetable. ((((exists ff_h_pvs_value_onetableentrypositive. ff_h_pvs_value_onetableentrypositive + S (dst_positive_value_onetable) = S ((S (dst_index_value_onetable)) * dst_positive_scale_value_onetable)) /\ exists ff_q_pvs_value_onetableentrypositive. dst_positive_code_value_onetable = ff_q_pvs_value_onetableentrypositive * S ((S (dst_index_value_onetable)) * dst_positive_scale_value_onetable) + (dst_positive_value_onetable))) /\ (((((exists ff_h_pvs_value_onetableentrynegative. ff_h_pvs_value_onetableentrynegative + S (dst_negative_value_onetable) = S ((S (dst_index_value_onetable)) * dst_negative_scale_value_onetable)) /\ exists ff_q_pvs_value_onetableentrynegative. dst_negative_code_value_onetable = ff_q_pvs_value_onetableentrynegative * S ((S (dst_index_value_onetable)) * dst_negative_scale_value_onetable) + (dst_negative_value_onetable))) /\ (exists ge_balance_positive_value_onetableentryvalue ge_balance_negative_value_onetableentryvalue. (((((dst_value_value_onetable) = 2 * (ge_balance_positive_value_onetableentryvalue) /\ (ge_balance_negative_value_onetableentryvalue) = 0) \/ exists ge_signed_half_value_onetableentryvaluedecode. (((dst_value_value_onetable) = 2 * ge_signed_half_value_onetableentryvaluedecode + 1 /\ (ge_balance_positive_value_onetableentryvalue) = 0) /\ (ge_balance_negative_value_onetableentryvalue) = S ge_signed_half_value_onetableentryvaluedecode))) /\ ((dst_positive_value_onetable) + ge_balance_negative_value_onetableentryvalue = (dst_negative_value_onetable) + ge_balance_positive_value_onetableentryvalue))))))))) /\ (forall du_index_value_one du_value_value_one. ~(du_index_value_one=0) -> (exists pvs_le_gap_value_onebound. pvs_le_gap_value_onebound + (du_index_value_one) = (N)) -> (exists dst_positive_code_value_oneentry dst_positive_scale_value_oneentry dst_negative_code_value_oneentry dst_negative_scale_value_oneentry dst_positive_value_oneentry dst_negative_value_oneentry. (((U) = (((((dst_positive_code_value_oneentry) + (dst_positive_scale_value_oneentry)) * S ((dst_positive_code_value_oneentry) + (dst_positive_scale_value_oneentry)) + ((dst_positive_scale_value_oneentry) + (dst_positive_scale_value_oneentry))) + (((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) * S ((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) + ((dst_negative_scale_value_oneentry) + (dst_negative_scale_value_oneentry)))) * S ((((dst_positive_code_value_oneentry) + (dst_positive_scale_value_oneentry)) * S ((dst_positive_code_value_oneentry) + (dst_positive_scale_value_oneentry)) + ((dst_positive_scale_value_oneentry) + (dst_positive_scale_value_oneentry))) + (((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) * S ((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) + ((dst_negative_scale_value_oneentry) + (dst_negative_scale_value_oneentry)))) + ((((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) * S ((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) + ((dst_negative_scale_value_oneentry) + (dst_negative_scale_value_oneentry))) + (((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) * S ((dst_negative_code_value_oneentry) + (dst_negative_scale_value_oneentry)) + ((dst_negative_scale_value_oneentry) + (dst_negative_scale_value_oneentry)))))) /\ (((((exists ff_h_pvs_value_oneentrypositive. ff_h_pvs_value_oneentrypositive + S (dst_positive_value_oneentry) = S ((S (du_index_value_one)) * dst_positive_scale_value_oneentry)) /\ exists ff_q_pvs_value_oneentrypositive. dst_positive_code_value_oneentry = ff_q_pvs_value_oneentrypositive * S ((S (du_index_value_one)) * dst_positive_scale_value_oneentry) + (dst_positive_value_oneentry))) /\ (((((exists ff_h_pvs_value_oneentrynegative. ff_h_pvs_value_oneentrynegative + S (dst_negative_value_oneentry) = S ((S (du_index_value_one)) * dst_negative_scale_value_oneentry)) /\ exists ff_q_pvs_value_oneentrynegative. dst_negative_code_value_oneentry = ff_q_pvs_value_oneentrynegative * S ((S (du_index_value_one)) * dst_negative_scale_value_oneentry) + (dst_negative_value_oneentry))) /\ (exists ge_balance_positive_value_oneentryvalue ge_balance_negative_value_oneentryvalue. (((((du_value_value_one) = 2 * (ge_balance_positive_value_oneentryvalue) /\ (ge_balance_negative_value_oneentryvalue) = 0) \/ exists ge_signed_half_value_oneentryvaluedecode. (((du_value_value_one) = 2 * ge_signed_half_value_oneentryvaluedecode + 1 /\ (ge_balance_positive_value_oneentryvalue) = 0) /\ (ge_balance_negative_value_oneentryvalue) = S ge_signed_half_value_oneentryvaluedecode))) /\ ((dst_positive_value_oneentry) + ge_balance_negative_value_oneentryvalue = (dst_negative_value_oneentry) + ge_balance_positive_value_oneentryvalue))))))))) -> du_value_value_one=2))) -> (((exists dst_positive_code_value_deltatable dst_positive_scale_value_deltatable dst_negative_code_value_deltatable dst_negative_scale_value_deltatable. (((E) = (((((dst_positive_code_value_deltatable) + (dst_positive_scale_value_deltatable)) * S ((dst_positive_code_value_deltatable) + (dst_positive_scale_value_deltatable)) + ((dst_positive_scale_value_deltatable) + (dst_positive_scale_value_deltatable))) + (((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) * S ((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) + ((dst_negative_scale_value_deltatable) + (dst_negative_scale_value_deltatable)))) * S ((((dst_positive_code_value_deltatable) + (dst_positive_scale_value_deltatable)) * S ((dst_positive_code_value_deltatable) + (dst_positive_scale_value_deltatable)) + ((dst_positive_scale_value_deltatable) + (dst_positive_scale_value_deltatable))) + (((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) * S ((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) + ((dst_negative_scale_value_deltatable) + (dst_negative_scale_value_deltatable)))) + ((((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) * S ((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) + ((dst_negative_scale_value_deltatable) + (dst_negative_scale_value_deltatable))) + (((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) * S ((dst_negative_code_value_deltatable) + (dst_negative_scale_value_deltatable)) + ((dst_negative_scale_value_deltatable) + (dst_negative_scale_value_deltatable)))))) /\ (forall dst_index_value_deltatable. (exists pvs_le_gap_value_deltatabledomain. pvs_le_gap_value_deltatabledomain + (dst_index_value_deltatable) = (N)) -> exists dst_positive_value_deltatable dst_negative_value_deltatable dst_value_value_deltatable. ((((exists ff_h_pvs_value_deltatableentrypositive. ff_h_pvs_value_deltatableentrypositive + S (dst_positive_value_deltatable) = S ((S (dst_index_value_deltatable)) * dst_positive_scale_value_deltatable)) /\ exists ff_q_pvs_value_deltatableentrypositive. dst_positive_code_value_deltatable = ff_q_pvs_value_deltatableentrypositive * S ((S (dst_index_value_deltatable)) * dst_positive_scale_value_deltatable) + (dst_positive_value_deltatable))) /\ (((((exists ff_h_pvs_value_deltatableentrynegative. ff_h_pvs_value_deltatableentrynegative + S (dst_negative_value_deltatable) = S ((S (dst_index_value_deltatable)) * dst_negative_scale_value_deltatable)) /\ exists ff_q_pvs_value_deltatableentrynegative. dst_negative_code_value_deltatable = ff_q_pvs_value_deltatableentrynegative * S ((S (dst_index_value_deltatable)) * dst_negative_scale_value_deltatable) + (dst_negative_value_deltatable))) /\ (exists ge_balance_positive_value_deltatableentryvalue ge_balance_negative_value_deltatableentryvalue. (((((dst_value_value_deltatable) = 2 * (ge_balance_positive_value_deltatableentryvalue) /\ (ge_balance_negative_value_deltatableentryvalue) = 0) \/ exists ge_signed_half_value_deltatableentryvaluedecode. (((dst_value_value_deltatable) = 2 * ge_signed_half_value_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_value_deltatableentryvalue) = 0) /\ (ge_balance_negative_value_deltatableentryvalue) = S ge_signed_half_value_deltatableentryvaluedecode))) /\ ((dst_positive_value_deltatable) + ge_balance_negative_value_deltatableentryvalue = (dst_negative_value_deltatable) + ge_balance_positive_value_deltatableentryvalue))))))))) /\ (forall du_index_value_delta du_value_value_delta. ~(du_index_value_delta=0) -> (exists pvs_le_gap_value_deltabound. pvs_le_gap_value_deltabound + (du_index_value_delta) = (N)) -> (exists dst_positive_code_value_deltaentry dst_positive_scale_value_deltaentry dst_negative_code_value_deltaentry dst_negative_scale_value_deltaentry dst_positive_value_deltaentry dst_negative_value_deltaentry. (((E) = (((((dst_positive_code_value_deltaentry) + (dst_positive_scale_value_deltaentry)) * S ((dst_positive_code_value_deltaentry) + (dst_positive_scale_value_deltaentry)) + ((dst_positive_scale_value_deltaentry) + (dst_positive_scale_value_deltaentry))) + (((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) * S ((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) + ((dst_negative_scale_value_deltaentry) + (dst_negative_scale_value_deltaentry)))) * S ((((dst_positive_code_value_deltaentry) + (dst_positive_scale_value_deltaentry)) * S ((dst_positive_code_value_deltaentry) + (dst_positive_scale_value_deltaentry)) + ((dst_positive_scale_value_deltaentry) + (dst_positive_scale_value_deltaentry))) + (((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) * S ((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) + ((dst_negative_scale_value_deltaentry) + (dst_negative_scale_value_deltaentry)))) + ((((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) * S ((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) + ((dst_negative_scale_value_deltaentry) + (dst_negative_scale_value_deltaentry))) + (((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) * S ((dst_negative_code_value_deltaentry) + (dst_negative_scale_value_deltaentry)) + ((dst_negative_scale_value_deltaentry) + (dst_negative_scale_value_deltaentry)))))) /\ (((((exists ff_h_pvs_value_deltaentrypositive. ff_h_pvs_value_deltaentrypositive + S (dst_positive_value_deltaentry) = S ((S (du_index_value_delta)) * dst_positive_scale_value_deltaentry)) /\ exists ff_q_pvs_value_deltaentrypositive. dst_positive_code_value_deltaentry = ff_q_pvs_value_deltaentrypositive * S ((S (du_index_value_delta)) * dst_positive_scale_value_deltaentry) + (dst_positive_value_deltaentry))) /\ (((((exists ff_h_pvs_value_deltaentrynegative. ff_h_pvs_value_deltaentrynegative + S (dst_negative_value_deltaentry) = S ((S (du_index_value_delta)) * dst_negative_scale_value_deltaentry)) /\ exists ff_q_pvs_value_deltaentrynegative. dst_negative_code_value_deltaentry = ff_q_pvs_value_deltaentrynegative * S ((S (du_index_value_delta)) * dst_negative_scale_value_deltaentry) + (dst_negative_value_deltaentry))) /\ (exists ge_balance_positive_value_deltaentryvalue ge_balance_negative_value_deltaentryvalue. (((((du_value_value_delta) = 2 * (ge_balance_positive_value_deltaentryvalue) /\ (ge_balance_negative_value_deltaentryvalue) = 0) \/ exists ge_signed_half_value_deltaentryvaluedecode. (((du_value_value_delta) = 2 * ge_signed_half_value_deltaentryvaluedecode + 1 /\ (ge_balance_positive_value_deltaentryvalue) = 0) /\ (ge_balance_negative_value_deltaentryvalue) = S ge_signed_half_value_deltaentryvaluedecode))) /\ ((dst_positive_value_deltaentry) + ge_balance_negative_value_deltaentryvalue = (dst_negative_value_deltaentry) + ge_balance_positive_value_deltaentryvalue))))))))) -> ((((du_index_value_delta)=1 -> (du_value_value_delta)=2) /\ (~((du_index_value_delta)=1) -> (du_value_value_delta)=0)))))) -> (forall mi_index_value_all_quotients mi_value_value_all_quotients. ~(mi_index_value_all_quotients=0) -> (exists pvs_le_gap_value_all_quotientsbound. pvs_le_gap_value_all_quotientsbound + (mi_index_value_all_quotients) = (N)) -> (exists dst_positive_code_value_all_quotientsentry dst_positive_scale_value_all_quotientsentry dst_negative_code_value_all_quotientsentry dst_negative_scale_value_all_quotientsentry dst_positive_value_all_quotientsentry dst_negative_value_all_quotientsentry. (((G) = (((((dst_positive_code_value_all_quotientsentry) + (dst_positive_scale_value_all_quotientsentry)) * S ((dst_positive_code_value_all_quotientsentry) + (dst_positive_scale_value_all_quotientsentry)) + ((dst_positive_scale_value_all_quotientsentry) + (dst_positive_scale_value_all_quotientsentry))) + (((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) * S ((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) + ((dst_negative_scale_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)))) * S ((((dst_positive_code_value_all_quotientsentry) + (dst_positive_scale_value_all_quotientsentry)) * S ((dst_positive_code_value_all_quotientsentry) + (dst_positive_scale_value_all_quotientsentry)) + ((dst_positive_scale_value_all_quotientsentry) + (dst_positive_scale_value_all_quotientsentry))) + (((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) * S ((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) + ((dst_negative_scale_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)))) + ((((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) * S ((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) + ((dst_negative_scale_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry))) + (((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) * S ((dst_negative_code_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)) + ((dst_negative_scale_value_all_quotientsentry) + (dst_negative_scale_value_all_quotientsentry)))))) /\ (((((exists ff_h_pvs_value_all_quotientsentrypositive. ff_h_pvs_value_all_quotientsentrypositive + S (dst_positive_value_all_quotientsentry) = S ((S (mi_index_value_all_quotients)) * dst_positive_scale_value_all_quotientsentry)) /\ exists ff_q_pvs_value_all_quotientsentrypositive. dst_positive_code_value_all_quotientsentry = ff_q_pvs_value_all_quotientsentrypositive * S ((S (mi_index_value_all_quotients)) * dst_positive_scale_value_all_quotientsentry) + (dst_positive_value_all_quotientsentry))) /\ (((((exists ff_h_pvs_value_all_quotientsentrynegative. ff_h_pvs_value_all_quotientsentrynegative + S (dst_negative_value_all_quotientsentry) = S ((S (mi_index_value_all_quotients)) * dst_negative_scale_value_all_quotientsentry)) /\ exists ff_q_pvs_value_all_quotientsentrynegative. dst_negative_code_value_all_quotientsentry = ff_q_pvs_value_all_quotientsentrynegative * S ((S (mi_index_value_all_quotients)) * dst_negative_scale_value_all_quotientsentry) + (dst_negative_value_all_quotientsentry))) /\ (exists ge_balance_positive_value_all_quotientsentryvalue ge_balance_negative_value_all_quotientsentryvalue. (((((mi_value_value_all_quotients) = 2 * (ge_balance_positive_value_all_quotientsentryvalue) /\ (ge_balance_negative_value_all_quotientsentryvalue) = 0) \/ exists ge_signed_half_value_all_quotientsentryvaluedecode. (((mi_value_value_all_quotients) = 2 * ge_signed_half_value_all_quotientsentryvaluedecode + 1 /\ (ge_balance_positive_value_all_quotientsentryvalue) = 0) /\ (ge_balance_negative_value_all_quotientsentryvalue) = S ge_signed_half_value_all_quotientsentryvaluedecode))) /\ ((dst_positive_value_all_quotientsentry) + ge_balance_negative_value_all_quotientsentryvalue = (dst_negative_value_all_quotientsentry) + ge_balance_positive_value_all_quotientsentryvalue))))))))) -> (((~((mi_index_value_all_quotients)=0)) /\ (exists dm_mask_table_value_all_quotientssum. ((((exists dst_positive_code_value_all_quotientssummasktable dst_positive_scale_value_all_quotientssummasktable dst_negative_code_value_all_quotientssummasktable dst_negative_scale_value_all_quotientssummasktable. (((dm_mask_table_value_all_quotientssum) = (((((dst_positive_code_value_all_quotientssummasktable) + (dst_positive_scale_value_all_quotientssummasktable)) * S ((dst_positive_code_value_all_quotientssummasktable) + (dst_positive_scale_value_all_quotientssummasktable)) + ((dst_positive_scale_value_all_quotientssummasktable) + (dst_positive_scale_value_all_quotientssummasktable))) + (((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) * S ((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) + ((dst_negative_scale_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)))) * S ((((dst_positive_code_value_all_quotientssummasktable) + (dst_positive_scale_value_all_quotientssummasktable)) * S ((dst_positive_code_value_all_quotientssummasktable) + (dst_positive_scale_value_all_quotientssummasktable)) + ((dst_positive_scale_value_all_quotientssummasktable) + (dst_positive_scale_value_all_quotientssummasktable))) + (((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) * S ((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) + ((dst_negative_scale_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)))) + ((((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) * S ((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) + ((dst_negative_scale_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable))) + (((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) * S ((dst_negative_code_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)) + ((dst_negative_scale_value_all_quotientssummasktable) + (dst_negative_scale_value_all_quotientssummasktable)))))) /\ (forall dst_index_value_all_quotientssummasktable. (exists pvs_le_gap_value_all_quotientssummasktabledomain. pvs_le_gap_value_all_quotientssummasktabledomain + (dst_index_value_all_quotientssummasktable) = (mi_index_value_all_quotients)) -> exists dst_positive_value_all_quotientssummasktable dst_negative_value_all_quotientssummasktable dst_value_value_all_quotientssummasktable. ((((exists ff_h_pvs_value_all_quotientssummasktableentrypositive. ff_h_pvs_value_all_quotientssummasktableentrypositive + S (dst_positive_value_all_quotientssummasktable) = S ((S (dst_index_value_all_quotientssummasktable)) * dst_positive_scale_value_all_quotientssummasktable)) /\ exists ff_q_pvs_value_all_quotientssummasktableentrypositive. dst_positive_code_value_all_quotientssummasktable = ff_q_pvs_value_all_quotientssummasktableentrypositive * S ((S (dst_index_value_all_quotientssummasktable)) * dst_positive_scale_value_all_quotientssummasktable) + (dst_positive_value_all_quotientssummasktable))) /\ (((((exists ff_h_pvs_value_all_quotientssummasktableentrynegative. ff_h_pvs_value_all_quotientssummasktableentrynegative + S (dst_negative_value_all_quotientssummasktable) = S ((S (dst_index_value_all_quotientssummasktable)) * dst_negative_scale_value_all_quotientssummasktable)) /\ exists ff_q_pvs_value_all_quotientssummasktableentrynegative. dst_negative_code_value_all_quotientssummasktable = ff_q_pvs_value_all_quotientssummasktableentrynegative * S ((S (dst_index_value_all_quotientssummasktable)) * dst_negative_scale_value_all_quotientssummasktable) + (dst_negative_value_all_quotientssummasktable))) /\ (exists ge_balance_positive_value_all_quotientssummasktableentryvalue ge_balance_negative_value_all_quotientssummasktableentryvalue. (((((dst_value_value_all_quotientssummasktable) = 2 * (ge_balance_positive_value_all_quotientssummasktableentryvalue) /\ (ge_balance_negative_value_all_quotientssummasktableentryvalue) = 0) \/ exists ge_signed_half_value_all_quotientssummasktableentryvaluedecode. (((dst_value_value_all_quotientssummasktable) = 2 * ge_signed_half_value_all_quotientssummasktableentryvaluedecode + 1 /\ (ge_balance_positive_value_all_quotientssummasktableentryvalue) = 0) /\ (ge_balance_negative_value_all_quotientssummasktableentryvalue) = S ge_signed_half_value_all_quotientssummasktableentryvaluedecode))) /\ ((dst_positive_value_all_quotientssummasktable) + ge_balance_negative_value_all_quotientssummasktableentryvalue = (dst_negative_value_all_quotientssummasktable) + ge_balance_positive_value_all_quotientssummasktableentryvalue))))))))) /\ (forall dm_index_value_all_quotientssummask dm_value_value_all_quotientssummask. (exists pvs_le_gap_value_all_quotientssummaskdomain. pvs_le_gap_value_all_quotientssummaskdomain + (dm_index_value_all_quotientssummask) = (mi_index_value_all_quotients)) -> (exists dst_positive_code_value_all_quotientssummasklookup dst_positive_scale_value_all_quotientssummasklookup dst_negative_code_value_all_quotientssummasklookup dst_negative_scale_value_all_quotientssummasklookup dst_positive_value_all_quotientssummasklookup dst_negative_value_all_quotientssummasklookup. (((dm_mask_table_value_all_quotientssum) = (((((dst_positive_code_value_all_quotientssummasklookup) + (dst_positive_scale_value_all_quotientssummasklookup)) * S ((dst_positive_code_value_all_quotientssummasklookup) + (dst_positive_scale_value_all_quotientssummasklookup)) + ((dst_positive_scale_value_all_quotientssummasklookup) + (dst_positive_scale_value_all_quotientssummasklookup))) + (((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) * S ((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) + ((dst_negative_scale_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)))) * S ((((dst_positive_code_value_all_quotientssummasklookup) + (dst_positive_scale_value_all_quotientssummasklookup)) * S ((dst_positive_code_value_all_quotientssummasklookup) + (dst_positive_scale_value_all_quotientssummasklookup)) + ((dst_positive_scale_value_all_quotientssummasklookup) + (dst_positive_scale_value_all_quotientssummasklookup))) + (((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) * S ((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) + ((dst_negative_scale_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)))) + ((((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) * S ((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) + ((dst_negative_scale_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup))) + (((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) * S ((dst_negative_code_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)) + ((dst_negative_scale_value_all_quotientssummasklookup) + (dst_negative_scale_value_all_quotientssummasklookup)))))) /\ (((((exists ff_h_pvs_value_all_quotientssummasklookuppositive. ff_h_pvs_value_all_quotientssummasklookuppositive + S (dst_positive_value_all_quotientssummasklookup) = S ((S (dm_index_value_all_quotientssummask)) * dst_positive_scale_value_all_quotientssummasklookup)) /\ exists ff_q_pvs_value_all_quotientssummasklookuppositive. dst_positive_code_value_all_quotientssummasklookup = ff_q_pvs_value_all_quotientssummasklookuppositive * S ((S (dm_index_value_all_quotientssummask)) * dst_positive_scale_value_all_quotientssummasklookup) + (dst_positive_value_all_quotientssummasklookup))) /\ (((((exists ff_h_pvs_value_all_quotientssummasklookupnegative. ff_h_pvs_value_all_quotientssummasklookupnegative + S (dst_negative_value_all_quotientssummasklookup) = S ((S (dm_index_value_all_quotientssummask)) * dst_negative_scale_value_all_quotientssummasklookup)) /\ exists ff_q_pvs_value_all_quotientssummasklookupnegative. dst_negative_code_value_all_quotientssummasklookup = ff_q_pvs_value_all_quotientssummasklookupnegative * S ((S (dm_index_value_all_quotientssummask)) * dst_negative_scale_value_all_quotientssummasklookup) + (dst_negative_value_all_quotientssummasklookup))) /\ (exists ge_balance_positive_value_all_quotientssummasklookupvalue ge_balance_negative_value_all_quotientssummasklookupvalue. (((((dm_value_value_all_quotientssummask) = 2 * (ge_balance_positive_value_all_quotientssummasklookupvalue) /\ (ge_balance_negative_value_all_quotientssummasklookupvalue) = 0) \/ exists ge_signed_half_value_all_quotientssummasklookupvaluedecode. (((dm_value_value_all_quotientssummask) = 2 * ge_signed_half_value_all_quotientssummasklookupvaluedecode + 1 /\ (ge_balance_positive_value_all_quotientssummasklookupvalue) = 0) /\ (ge_balance_negative_value_all_quotientssummasklookupvalue) = S ge_signed_half_value_all_quotientssummasklookupvaluedecode))) /\ ((dst_positive_value_all_quotientssummasklookup) + ge_balance_negative_value_all_quotientssummasklookupvalue = (dst_negative_value_all_quotientssummasklookup) + ge_balance_positive_value_all_quotientssummasklookupvalue))))))))) -> ((((~((dm_index_value_all_quotientssummask)=0)) /\ (exists dm_quotient_value_all_quotientssummaskentry. (((mi_index_value_all_quotients)=(dm_index_value_all_quotientssummask)*dm_quotient_value_all_quotientssummaskentry) /\ (exists dst_positive_code_value_all_quotientssummaskentryinput dst_positive_scale_value_all_quotientssummaskentryinput dst_negative_code_value_all_quotientssummaskentryinput dst_negative_scale_value_all_quotientssummaskentryinput dst_positive_value_all_quotientssummaskentryinput dst_negative_value_all_quotientssummaskentryinput. (((F) = (((((dst_positive_code_value_all_quotientssummaskentryinput) + (dst_positive_scale_value_all_quotientssummaskentryinput)) * S ((dst_positive_code_value_all_quotientssummaskentryinput) + (dst_positive_scale_value_all_quotientssummaskentryinput)) + ((dst_positive_scale_value_all_quotientssummaskentryinput) + (dst_positive_scale_value_all_quotientssummaskentryinput))) + (((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) * S ((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) + ((dst_negative_scale_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)))) * S ((((dst_positive_code_value_all_quotientssummaskentryinput) + (dst_positive_scale_value_all_quotientssummaskentryinput)) * S ((dst_positive_code_value_all_quotientssummaskentryinput) + (dst_positive_scale_value_all_quotientssummaskentryinput)) + ((dst_positive_scale_value_all_quotientssummaskentryinput) + (dst_positive_scale_value_all_quotientssummaskentryinput))) + (((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) * S ((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) + ((dst_negative_scale_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)))) + ((((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) * S ((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) + ((dst_negative_scale_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput))) + (((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) * S ((dst_negative_code_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)) + ((dst_negative_scale_value_all_quotientssummaskentryinput) + (dst_negative_scale_value_all_quotientssummaskentryinput)))))) /\ (((((exists ff_h_pvs_value_all_quotientssummaskentryinputpositive. ff_h_pvs_value_all_quotientssummaskentryinputpositive + S (dst_positive_value_all_quotientssummaskentryinput) = S ((S (dm_index_value_all_quotientssummask)) * dst_positive_scale_value_all_quotientssummaskentryinput)) /\ exists ff_q_pvs_value_all_quotientssummaskentryinputpositive. dst_positive_code_value_all_quotientssummaskentryinput = ff_q_pvs_value_all_quotientssummaskentryinputpositive * S ((S (dm_index_value_all_quotientssummask)) * dst_positive_scale_value_all_quotientssummaskentryinput) + (dst_positive_value_all_quotientssummaskentryinput))) /\ (((((exists ff_h_pvs_value_all_quotientssummaskentryinputnegative. ff_h_pvs_value_all_quotientssummaskentryinputnegative + S (dst_negative_value_all_quotientssummaskentryinput) = S ((S (dm_index_value_all_quotientssummask)) * dst_negative_scale_value_all_quotientssummaskentryinput)) /\ exists ff_q_pvs_value_all_quotientssummaskentryinputnegative. dst_negative_code_value_all_quotientssummaskentryinput = ff_q_pvs_value_all_quotientssummaskentryinputnegative * S ((S (dm_index_value_all_quotientssummask)) * dst_negative_scale_value_all_quotientssummaskentryinput) + (dst_negative_value_all_quotientssummaskentryinput))) /\ (exists ge_balance_positive_value_all_quotientssummaskentryinputvalue ge_balance_negative_value_all_quotientssummaskentryinputvalue. (((((dm_value_value_all_quotientssummask) = 2 * (ge_balance_positive_value_all_quotientssummaskentryinputvalue) /\ (ge_balance_negative_value_all_quotientssummaskentryinputvalue) = 0) \/ exists ge_signed_half_value_all_quotientssummaskentryinputvaluedecode. (((dm_value_value_all_quotientssummask) = 2 * ge_signed_half_value_all_quotientssummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_value_all_quotientssummaskentryinputvalue) = 0) /\ (ge_balance_negative_value_all_quotientssummaskentryinputvalue) = S ge_signed_half_value_all_quotientssummaskentryinputvaluedecode))) /\ ((dst_positive_value_all_quotientssummaskentryinput) + ge_balance_negative_value_all_quotientssummaskentryinputvalue = (dst_negative_value_all_quotientssummaskentryinput) + ge_balance_positive_value_all_quotientssummaskentryinputvalue))))))))))))) \/ ((((dm_index_value_all_quotientssummask)=0 \/ ~(exists pvs_factor_value_all_quotientssummaskentrynondivisor. (mi_index_value_all_quotients) = (dm_index_value_all_quotientssummask) * pvs_factor_value_all_quotientssummaskentrynondivisor)) /\ ((dm_value_value_all_quotientssummask)=0))))))) /\ (exists dst_positive_code_value_all_quotientssumfold dst_positive_scale_value_all_quotientssumfold dst_negative_code_value_all_quotientssumfold dst_negative_scale_value_all_quotientssumfold dst_positive_sum_value_all_quotientssumfold dst_negative_sum_value_all_quotientssumfold. (((dm_mask_table_value_all_quotientssum) = (((((dst_positive_code_value_all_quotientssumfold) + (dst_positive_scale_value_all_quotientssumfold)) * S ((dst_positive_code_value_all_quotientssumfold) + (dst_positive_scale_value_all_quotientssumfold)) + ((dst_positive_scale_value_all_quotientssumfold) + (dst_positive_scale_value_all_quotientssumfold))) + (((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) * S ((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) + ((dst_negative_scale_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)))) * S ((((dst_positive_code_value_all_quotientssumfold) + (dst_positive_scale_value_all_quotientssumfold)) * S ((dst_positive_code_value_all_quotientssumfold) + (dst_positive_scale_value_all_quotientssumfold)) + ((dst_positive_scale_value_all_quotientssumfold) + (dst_positive_scale_value_all_quotientssumfold))) + (((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) * S ((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) + ((dst_negative_scale_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)))) + ((((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) * S ((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) + ((dst_negative_scale_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold))) + (((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) * S ((dst_negative_code_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)) + ((dst_negative_scale_value_all_quotientssumfold) + (dst_negative_scale_value_all_quotientssumfold)))))) /\ (((exists fs_u_dst_value_all_quotientssumfoldpositive fs_v_dst_value_all_quotientssumfoldpositive. ((((exists fs_h_dst_value_all_quotientssumfoldpositive_body_start. fs_h_dst_value_all_quotientssumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_value_all_quotientssumfoldpositive)) /\ exists fs_q_dst_value_all_quotientssumfoldpositive_body_start. fs_u_dst_value_all_quotientssumfoldpositive = fs_q_dst_value_all_quotientssumfoldpositive_body_start * S ((S (0)) * fs_v_dst_value_all_quotientssumfoldpositive) + (0))) /\ ((((exists fs_h_dst_value_all_quotientssumfoldpositive_body_terminal. fs_h_dst_value_all_quotientssumfoldpositive_body_terminal + S (dst_positive_sum_value_all_quotientssumfold) = S ((S (S (mi_index_value_all_quotients))) * fs_v_dst_value_all_quotientssumfoldpositive)) /\ exists fs_q_dst_value_all_quotientssumfoldpositive_body_terminal. fs_u_dst_value_all_quotientssumfoldpositive = fs_q_dst_value_all_quotientssumfoldpositive_body_terminal * S ((S (S (mi_index_value_all_quotients))) * fs_v_dst_value_all_quotientssumfoldpositive) + (dst_positive_sum_value_all_quotientssumfold))) /\ forall fs_i_dst_value_all_quotientssumfoldpositive_body_steps. (exists fs_lt_dst_value_all_quotientssumfoldpositive_body_steps_bound. fs_lt_dst_value_all_quotientssumfoldpositive_body_steps_bound + S fs_i_dst_value_all_quotientssumfoldpositive_body_steps = S (mi_index_value_all_quotients)) -> exists fs_a_dst_value_all_quotientssumfoldpositive_body_steps fs_r_dst_value_all_quotientssumfoldpositive_body_steps fs_s_dst_value_all_quotientssumfoldpositive_body_steps. ((((exists fs_h_dst_value_all_quotientssumfoldpositive_body_steps_summand. fs_h_dst_value_all_quotientssumfoldpositive_body_steps_summand + S (fs_a_dst_value_all_quotientssumfoldpositive_body_steps) = S ((S (fs_i_dst_value_all_quotientssumfoldpositive_body_steps)) * dst_positive_scale_value_all_quotientssumfold)) /\ exists fs_q_dst_value_all_quotientssumfoldpositive_body_steps_summand. dst_positive_code_value_all_quotientssumfold = fs_q_dst_value_all_quotientssumfoldpositive_body_steps_summand * S ((S (fs_i_dst_value_all_quotientssumfoldpositive_body_steps)) * dst_positive_scale_value_all_quotientssumfold) + (fs_a_dst_value_all_quotientssumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_value_all_quotientssumfoldpositive_body_steps_partial. fs_h_dst_value_all_quotientssumfoldpositive_body_steps_partial + S (fs_r_dst_value_all_quotientssumfoldpositive_body_steps) = S ((S (fs_i_dst_value_all_quotientssumfoldpositive_body_steps)) * fs_v_dst_value_all_quotientssumfoldpositive)) /\ exists fs_q_dst_value_all_quotientssumfoldpositive_body_steps_partial. fs_u_dst_value_all_quotientssumfoldpositive = fs_q_dst_value_all_quotientssumfoldpositive_body_steps_partial * S ((S (fs_i_dst_value_all_quotientssumfoldpositive_body_steps)) * fs_v_dst_value_all_quotientssumfoldpositive) + (fs_r_dst_value_all_quotientssumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_value_all_quotientssumfoldpositive_body_steps_successor. fs_h_dst_value_all_quotientssumfoldpositive_body_steps_successor + S (fs_s_dst_value_all_quotientssumfoldpositive_body_steps) = S ((S (S fs_i_dst_value_all_quotientssumfoldpositive_body_steps)) * fs_v_dst_value_all_quotientssumfoldpositive)) /\ exists fs_q_dst_value_all_quotientssumfoldpositive_body_steps_successor. fs_u_dst_value_all_quotientssumfoldpositive = fs_q_dst_value_all_quotientssumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_value_all_quotientssumfoldpositive_body_steps)) * fs_v_dst_value_all_quotientssumfoldpositive) + (fs_s_dst_value_all_quotientssumfoldpositive_body_steps))) /\ fs_s_dst_value_all_quotientssumfoldpositive_body_steps = fs_r_dst_value_all_quotientssumfoldpositive_body_steps + fs_a_dst_value_all_quotientssumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_value_all_quotientssumfoldnegative fs_v_dst_value_all_quotientssumfoldnegative. ((((exists fs_h_dst_value_all_quotientssumfoldnegative_body_start. fs_h_dst_value_all_quotientssumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_value_all_quotientssumfoldnegative)) /\ exists fs_q_dst_value_all_quotientssumfoldnegative_body_start. fs_u_dst_value_all_quotientssumfoldnegative = fs_q_dst_value_all_quotientssumfoldnegative_body_start * S ((S (0)) * fs_v_dst_value_all_quotientssumfoldnegative) + (0))) /\ ((((exists fs_h_dst_value_all_quotientssumfoldnegative_body_terminal. fs_h_dst_value_all_quotientssumfoldnegative_body_terminal + S (dst_negative_sum_value_all_quotientssumfold) = S ((S (S (mi_index_value_all_quotients))) * fs_v_dst_value_all_quotientssumfoldnegative)) /\ exists fs_q_dst_value_all_quotientssumfoldnegative_body_terminal. fs_u_dst_value_all_quotientssumfoldnegative = fs_q_dst_value_all_quotientssumfoldnegative_body_terminal * S ((S (S (mi_index_value_all_quotients))) * fs_v_dst_value_all_quotientssumfoldnegative) + (dst_negative_sum_value_all_quotientssumfold))) /\ forall fs_i_dst_value_all_quotientssumfoldnegative_body_steps. (exists fs_lt_dst_value_all_quotientssumfoldnegative_body_steps_bound. fs_lt_dst_value_all_quotientssumfoldnegative_body_steps_bound + S fs_i_dst_value_all_quotientssumfoldnegative_body_steps = S (mi_index_value_all_quotients)) -> exists fs_a_dst_value_all_quotientssumfoldnegative_body_steps fs_r_dst_value_all_quotientssumfoldnegative_body_steps fs_s_dst_value_all_quotientssumfoldnegative_body_steps. ((((exists fs_h_dst_value_all_quotientssumfoldnegative_body_steps_summand. fs_h_dst_value_all_quotientssumfoldnegative_body_steps_summand + S (fs_a_dst_value_all_quotientssumfoldnegative_body_steps) = S ((S (fs_i_dst_value_all_quotientssumfoldnegative_body_steps)) * dst_negative_scale_value_all_quotientssumfold)) /\ exists fs_q_dst_value_all_quotientssumfoldnegative_body_steps_summand. dst_negative_code_value_all_quotientssumfold = fs_q_dst_value_all_quotientssumfoldnegative_body_steps_summand * S ((S (fs_i_dst_value_all_quotientssumfoldnegative_body_steps)) * dst_negative_scale_value_all_quotientssumfold) + (fs_a_dst_value_all_quotientssumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_value_all_quotientssumfoldnegative_body_steps_partial. fs_h_dst_value_all_quotientssumfoldnegative_body_steps_partial + S (fs_r_dst_value_all_quotientssumfoldnegative_body_steps) = S ((S (fs_i_dst_value_all_quotientssumfoldnegative_body_steps)) * fs_v_dst_value_all_quotientssumfoldnegative)) /\ exists fs_q_dst_value_all_quotientssumfoldnegative_body_steps_partial. fs_u_dst_value_all_quotientssumfoldnegative = fs_q_dst_value_all_quotientssumfoldnegative_body_steps_partial * S ((S (fs_i_dst_value_all_quotientssumfoldnegative_body_steps)) * fs_v_dst_value_all_quotientssumfoldnegative) + (fs_r_dst_value_all_quotientssumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_value_all_quotientssumfoldnegative_body_steps_successor. fs_h_dst_value_all_quotientssumfoldnegative_body_steps_successor + S (fs_s_dst_value_all_quotientssumfoldnegative_body_steps) = S ((S (S fs_i_dst_value_all_quotientssumfoldnegative_body_steps)) * fs_v_dst_value_all_quotientssumfoldnegative)) /\ exists fs_q_dst_value_all_quotientssumfoldnegative_body_steps_successor. fs_u_dst_value_all_quotientssumfoldnegative = fs_q_dst_value_all_quotientssumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_value_all_quotientssumfoldnegative_body_steps)) * fs_v_dst_value_all_quotientssumfoldnegative) + (fs_s_dst_value_all_quotientssumfoldnegative_body_steps))) /\ fs_s_dst_value_all_quotientssumfoldnegative_body_steps = fs_r_dst_value_all_quotientssumfoldnegative_body_steps + fs_a_dst_value_all_quotientssumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_value_all_quotientssumfoldresult ge_balance_negative_value_all_quotientssumfoldresult. (((((mi_value_value_all_quotients) = 2 * (ge_balance_positive_value_all_quotientssumfoldresult) /\ (ge_balance_negative_value_all_quotientssumfoldresult) = 0) \/ exists ge_signed_half_value_all_quotientssumfoldresultdecode. (((mi_value_value_all_quotients) = 2 * ge_signed_half_value_all_quotientssumfoldresultdecode + 1 /\ (ge_balance_positive_value_all_quotientssumfoldresult) = 0) /\ (ge_balance_negative_value_all_quotientssumfoldresult) = S ge_signed_half_value_all_quotientssumfoldresultdecode))) /\ ((dst_positive_sum_value_all_quotientssumfold) + ge_balance_negative_value_all_quotientssumfoldresult = (dst_negative_sum_value_all_quotientssumfold) + ge_balance_positive_value_all_quotientssumfoldresult)))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_value_bound. pvs_le_gap_value_bound + (n) = (N)) -> (exists dst_positive_code_value_original dst_positive_scale_value_original dst_negative_code_value_original dst_negative_scale_value_original dst_positive_value_original dst_negative_value_original. (((F) = (((((dst_positive_code_value_original) + (dst_positive_scale_value_original)) * S ((dst_positive_code_value_original) + (dst_positive_scale_value_original)) + ((dst_positive_scale_value_original) + (dst_positive_scale_value_original))) + (((dst_negative_code_value_original) + (dst_negative_scale_value_original)) * S ((dst_negative_code_value_original) + (dst_negative_scale_value_original)) + ((dst_negative_scale_value_original) + (dst_negative_scale_value_original)))) * S ((((dst_positive_code_value_original) + (dst_positive_scale_value_original)) * S ((dst_positive_code_value_original) + (dst_positive_scale_value_original)) + ((dst_positive_scale_value_original) + (dst_positive_scale_value_original))) + (((dst_negative_code_value_original) + (dst_negative_scale_value_original)) * S ((dst_negative_code_value_original) + (dst_negative_scale_value_original)) + ((dst_negative_scale_value_original) + (dst_negative_scale_value_original)))) + ((((dst_negative_code_value_original) + (dst_negative_scale_value_original)) * S ((dst_negative_code_value_original) + (dst_negative_scale_value_original)) + ((dst_negative_scale_value_original) + (dst_negative_scale_value_original))) + (((dst_negative_code_value_original) + (dst_negative_scale_value_original)) * S ((dst_negative_code_value_original) + (dst_negative_scale_value_original)) + ((dst_negative_scale_value_original) + (dst_negative_scale_value_original)))))) /\ (((((exists ff_h_pvs_value_originalpositive. ff_h_pvs_value_originalpositive + S (dst_positive_value_original) = S ((S (n)) * dst_positive_scale_value_original)) /\ exists ff_q_pvs_value_originalpositive. dst_positive_code_value_original = ff_q_pvs_value_originalpositive * S ((S (n)) * dst_positive_scale_value_original) + (dst_positive_value_original))) /\ (((((exists ff_h_pvs_value_originalnegative. ff_h_pvs_value_originalnegative + S (dst_negative_value_original) = S ((S (n)) * dst_negative_scale_value_original)) /\ exists ff_q_pvs_value_originalnegative. dst_negative_code_value_original = ff_q_pvs_value_originalnegative * S ((S (n)) * dst_negative_scale_value_original) + (dst_negative_value_original))) /\ (exists ge_balance_positive_value_originalvalue ge_balance_negative_value_originalvalue. (((((a) = 2 * (ge_balance_positive_value_originalvalue) /\ (ge_balance_negative_value_originalvalue) = 0) \/ exists ge_signed_half_value_originalvaluedecode. (((a) = 2 * ge_signed_half_value_originalvaluedecode + 1 /\ (ge_balance_positive_value_originalvalue) = 0) /\ (ge_balance_negative_value_originalvalue) = S ge_signed_half_value_originalvaluedecode))) /\ ((dst_positive_value_original) + ge_balance_negative_value_originalvalue = (dst_negative_value_original) + ge_balance_positive_value_originalvalue))))))))) -> (((~((n)=0)) /\ (exists dc_mask_value_weighted_sum. ((((exists dst_positive_code_value_weighted_summasktable dst_positive_scale_value_weighted_summasktable dst_negative_code_value_weighted_summasktable dst_negative_scale_value_weighted_summasktable. (((dc_mask_value_weighted_sum) = (((((dst_positive_code_value_weighted_summasktable) + (dst_positive_scale_value_weighted_summasktable)) * S ((dst_positive_code_value_weighted_summasktable) + (dst_positive_scale_value_weighted_summasktable)) + ((dst_positive_scale_value_weighted_summasktable) + (dst_positive_scale_value_weighted_summasktable))) + (((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) * S ((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) + ((dst_negative_scale_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)))) * S ((((dst_positive_code_value_weighted_summasktable) + (dst_positive_scale_value_weighted_summasktable)) * S ((dst_positive_code_value_weighted_summasktable) + (dst_positive_scale_value_weighted_summasktable)) + ((dst_positive_scale_value_weighted_summasktable) + (dst_positive_scale_value_weighted_summasktable))) + (((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) * S ((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) + ((dst_negative_scale_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)))) + ((((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) * S ((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) + ((dst_negative_scale_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable))) + (((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) * S ((dst_negative_code_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)) + ((dst_negative_scale_value_weighted_summasktable) + (dst_negative_scale_value_weighted_summasktable)))))) /\ (forall dst_index_value_weighted_summasktable. (exists pvs_le_gap_value_weighted_summasktabledomain. pvs_le_gap_value_weighted_summasktabledomain + (dst_index_value_weighted_summasktable) = (n)) -> exists dst_positive_value_weighted_summasktable dst_negative_value_weighted_summasktable dst_value_value_weighted_summasktable. ((((exists ff_h_pvs_value_weighted_summasktableentrypositive. ff_h_pvs_value_weighted_summasktableentrypositive + S (dst_positive_value_weighted_summasktable) = S ((S (dst_index_value_weighted_summasktable)) * dst_positive_scale_value_weighted_summasktable)) /\ exists ff_q_pvs_value_weighted_summasktableentrypositive. dst_positive_code_value_weighted_summasktable = ff_q_pvs_value_weighted_summasktableentrypositive * S ((S (dst_index_value_weighted_summasktable)) * dst_positive_scale_value_weighted_summasktable) + (dst_positive_value_weighted_summasktable))) /\ (((((exists ff_h_pvs_value_weighted_summasktableentrynegative. ff_h_pvs_value_weighted_summasktableentrynegative + S (dst_negative_value_weighted_summasktable) = S ((S (dst_index_value_weighted_summasktable)) * dst_negative_scale_value_weighted_summasktable)) /\ exists ff_q_pvs_value_weighted_summasktableentrynegative. dst_negative_code_value_weighted_summasktable = ff_q_pvs_value_weighted_summasktableentrynegative * S ((S (dst_index_value_weighted_summasktable)) * dst_negative_scale_value_weighted_summasktable) + (dst_negative_value_weighted_summasktable))) /\ (exists ge_balance_positive_value_weighted_summasktableentryvalue ge_balance_negative_value_weighted_summasktableentryvalue. (((((dst_value_value_weighted_summasktable) = 2 * (ge_balance_positive_value_weighted_summasktableentryvalue) /\ (ge_balance_negative_value_weighted_summasktableentryvalue) = 0) \/ exists ge_signed_half_value_weighted_summasktableentryvaluedecode. (((dst_value_value_weighted_summasktable) = 2 * ge_signed_half_value_weighted_summasktableentryvaluedecode + 1 /\ (ge_balance_positive_value_weighted_summasktableentryvalue) = 0) /\ (ge_balance_negative_value_weighted_summasktableentryvalue) = S ge_signed_half_value_weighted_summasktableentryvaluedecode))) /\ ((dst_positive_value_weighted_summasktable) + ge_balance_negative_value_weighted_summasktableentryvalue = (dst_negative_value_weighted_summasktable) + ge_balance_positive_value_weighted_summasktableentryvalue))))))))) /\ (forall dc_index_value_weighted_summask dc_value_value_weighted_summask. (exists pvs_le_gap_value_weighted_summaskdomain. pvs_le_gap_value_weighted_summaskdomain + (dc_index_value_weighted_summask) = (n)) -> (exists dst_positive_code_value_weighted_summasklookup dst_positive_scale_value_weighted_summasklookup dst_negative_code_value_weighted_summasklookup dst_negative_scale_value_weighted_summasklookup dst_positive_value_weighted_summasklookup dst_negative_value_weighted_summasklookup. (((dc_mask_value_weighted_sum) = (((((dst_positive_code_value_weighted_summasklookup) + (dst_positive_scale_value_weighted_summasklookup)) * S ((dst_positive_code_value_weighted_summasklookup) + (dst_positive_scale_value_weighted_summasklookup)) + ((dst_positive_scale_value_weighted_summasklookup) + (dst_positive_scale_value_weighted_summasklookup))) + (((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) * S ((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) + ((dst_negative_scale_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)))) * S ((((dst_positive_code_value_weighted_summasklookup) + (dst_positive_scale_value_weighted_summasklookup)) * S ((dst_positive_code_value_weighted_summasklookup) + (dst_positive_scale_value_weighted_summasklookup)) + ((dst_positive_scale_value_weighted_summasklookup) + (dst_positive_scale_value_weighted_summasklookup))) + (((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) * S ((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) + ((dst_negative_scale_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)))) + ((((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) * S ((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) + ((dst_negative_scale_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup))) + (((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) * S ((dst_negative_code_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)) + ((dst_negative_scale_value_weighted_summasklookup) + (dst_negative_scale_value_weighted_summasklookup)))))) /\ (((((exists ff_h_pvs_value_weighted_summasklookuppositive. ff_h_pvs_value_weighted_summasklookuppositive + S (dst_positive_value_weighted_summasklookup) = S ((S (dc_index_value_weighted_summask)) * dst_positive_scale_value_weighted_summasklookup)) /\ exists ff_q_pvs_value_weighted_summasklookuppositive. dst_positive_code_value_weighted_summasklookup = ff_q_pvs_value_weighted_summasklookuppositive * S ((S (dc_index_value_weighted_summask)) * dst_positive_scale_value_weighted_summasklookup) + (dst_positive_value_weighted_summasklookup))) /\ (((((exists ff_h_pvs_value_weighted_summasklookupnegative. ff_h_pvs_value_weighted_summasklookupnegative + S (dst_negative_value_weighted_summasklookup) = S ((S (dc_index_value_weighted_summask)) * dst_negative_scale_value_weighted_summasklookup)) /\ exists ff_q_pvs_value_weighted_summasklookupnegative. dst_negative_code_value_weighted_summasklookup = ff_q_pvs_value_weighted_summasklookupnegative * S ((S (dc_index_value_weighted_summask)) * dst_negative_scale_value_weighted_summasklookup) + (dst_negative_value_weighted_summasklookup))) /\ (exists ge_balance_positive_value_weighted_summasklookupvalue ge_balance_negative_value_weighted_summasklookupvalue. (((((dc_value_value_weighted_summask) = 2 * (ge_balance_positive_value_weighted_summasklookupvalue) /\ (ge_balance_negative_value_weighted_summasklookupvalue) = 0) \/ exists ge_signed_half_value_weighted_summasklookupvaluedecode. (((dc_value_value_weighted_summask) = 2 * ge_signed_half_value_weighted_summasklookupvaluedecode + 1 /\ (ge_balance_positive_value_weighted_summasklookupvalue) = 0) /\ (ge_balance_negative_value_weighted_summasklookupvalue) = S ge_signed_half_value_weighted_summasklookupvaluedecode))) /\ ((dst_positive_value_weighted_summasklookup) + ge_balance_negative_value_weighted_summasklookupvalue = (dst_negative_value_weighted_summasklookup) + ge_balance_positive_value_weighted_summasklookupvalue))))))))) -> ((((~((dc_index_value_weighted_summask)=0)) /\ (exists dc_quotient_value_weighted_summaskentry dc_left_value_weighted_summaskentry dc_right_value_weighted_summaskentry. (((n)=(dc_index_value_weighted_summask)*dc_quotient_value_weighted_summaskentry) /\ (((exists dst_positive_code_value_weighted_summaskentryleft dst_positive_scale_value_weighted_summaskentryleft dst_negative_code_value_weighted_summaskentryleft dst_negative_scale_value_weighted_summaskentryleft dst_positive_value_weighted_summaskentryleft dst_negative_value_weighted_summaskentryleft. (((M) = (((((dst_positive_code_value_weighted_summaskentryleft) + (dst_positive_scale_value_weighted_summaskentryleft)) * S ((dst_positive_code_value_weighted_summaskentryleft) + (dst_positive_scale_value_weighted_summaskentryleft)) + ((dst_positive_scale_value_weighted_summaskentryleft) + (dst_positive_scale_value_weighted_summaskentryleft))) + (((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) * S ((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) + ((dst_negative_scale_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)))) * S ((((dst_positive_code_value_weighted_summaskentryleft) + (dst_positive_scale_value_weighted_summaskentryleft)) * S ((dst_positive_code_value_weighted_summaskentryleft) + (dst_positive_scale_value_weighted_summaskentryleft)) + ((dst_positive_scale_value_weighted_summaskentryleft) + (dst_positive_scale_value_weighted_summaskentryleft))) + (((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) * S ((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) + ((dst_negative_scale_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)))) + ((((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) * S ((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) + ((dst_negative_scale_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft))) + (((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) * S ((dst_negative_code_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)) + ((dst_negative_scale_value_weighted_summaskentryleft) + (dst_negative_scale_value_weighted_summaskentryleft)))))) /\ (((((exists ff_h_pvs_value_weighted_summaskentryleftpositive. ff_h_pvs_value_weighted_summaskentryleftpositive + S (dst_positive_value_weighted_summaskentryleft) = S ((S (dc_index_value_weighted_summask)) * dst_positive_scale_value_weighted_summaskentryleft)) /\ exists ff_q_pvs_value_weighted_summaskentryleftpositive. dst_positive_code_value_weighted_summaskentryleft = ff_q_pvs_value_weighted_summaskentryleftpositive * S ((S (dc_index_value_weighted_summask)) * dst_positive_scale_value_weighted_summaskentryleft) + (dst_positive_value_weighted_summaskentryleft))) /\ (((((exists ff_h_pvs_value_weighted_summaskentryleftnegative. ff_h_pvs_value_weighted_summaskentryleftnegative + S (dst_negative_value_weighted_summaskentryleft) = S ((S (dc_index_value_weighted_summask)) * dst_negative_scale_value_weighted_summaskentryleft)) /\ exists ff_q_pvs_value_weighted_summaskentryleftnegative. dst_negative_code_value_weighted_summaskentryleft = ff_q_pvs_value_weighted_summaskentryleftnegative * S ((S (dc_index_value_weighted_summask)) * dst_negative_scale_value_weighted_summaskentryleft) + (dst_negative_value_weighted_summaskentryleft))) /\ (exists ge_balance_positive_value_weighted_summaskentryleftvalue ge_balance_negative_value_weighted_summaskentryleftvalue. (((((dc_left_value_weighted_summaskentry) = 2 * (ge_balance_positive_value_weighted_summaskentryleftvalue) /\ (ge_balance_negative_value_weighted_summaskentryleftvalue) = 0) \/ exists ge_signed_half_value_weighted_summaskentryleftvaluedecode. (((dc_left_value_weighted_summaskentry) = 2 * ge_signed_half_value_weighted_summaskentryleftvaluedecode + 1 /\ (ge_balance_positive_value_weighted_summaskentryleftvalue) = 0) /\ (ge_balance_negative_value_weighted_summaskentryleftvalue) = S ge_signed_half_value_weighted_summaskentryleftvaluedecode))) /\ ((dst_positive_value_weighted_summaskentryleft) + ge_balance_negative_value_weighted_summaskentryleftvalue = (dst_negative_value_weighted_summaskentryleft) + ge_balance_positive_value_weighted_summaskentryleftvalue))))))))) /\ (((exists dst_positive_code_value_weighted_summaskentryright dst_positive_scale_value_weighted_summaskentryright dst_negative_code_value_weighted_summaskentryright dst_negative_scale_value_weighted_summaskentryright dst_positive_value_weighted_summaskentryright dst_negative_value_weighted_summaskentryright. (((G) = (((((dst_positive_code_value_weighted_summaskentryright) + (dst_positive_scale_value_weighted_summaskentryright)) * S ((dst_positive_code_value_weighted_summaskentryright) + (dst_positive_scale_value_weighted_summaskentryright)) + ((dst_positive_scale_value_weighted_summaskentryright) + (dst_positive_scale_value_weighted_summaskentryright))) + (((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) * S ((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) + ((dst_negative_scale_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)))) * S ((((dst_positive_code_value_weighted_summaskentryright) + (dst_positive_scale_value_weighted_summaskentryright)) * S ((dst_positive_code_value_weighted_summaskentryright) + (dst_positive_scale_value_weighted_summaskentryright)) + ((dst_positive_scale_value_weighted_summaskentryright) + (dst_positive_scale_value_weighted_summaskentryright))) + (((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) * S ((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) + ((dst_negative_scale_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)))) + ((((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) * S ((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) + ((dst_negative_scale_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright))) + (((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) * S ((dst_negative_code_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)) + ((dst_negative_scale_value_weighted_summaskentryright) + (dst_negative_scale_value_weighted_summaskentryright)))))) /\ (((((exists ff_h_pvs_value_weighted_summaskentryrightpositive. ff_h_pvs_value_weighted_summaskentryrightpositive + S (dst_positive_value_weighted_summaskentryright) = S ((S (dc_quotient_value_weighted_summaskentry)) * dst_positive_scale_value_weighted_summaskentryright)) /\ exists ff_q_pvs_value_weighted_summaskentryrightpositive. dst_positive_code_value_weighted_summaskentryright = ff_q_pvs_value_weighted_summaskentryrightpositive * S ((S (dc_quotient_value_weighted_summaskentry)) * dst_positive_scale_value_weighted_summaskentryright) + (dst_positive_value_weighted_summaskentryright))) /\ (((((exists ff_h_pvs_value_weighted_summaskentryrightnegative. ff_h_pvs_value_weighted_summaskentryrightnegative + S (dst_negative_value_weighted_summaskentryright) = S ((S (dc_quotient_value_weighted_summaskentry)) * dst_negative_scale_value_weighted_summaskentryright)) /\ exists ff_q_pvs_value_weighted_summaskentryrightnegative. dst_negative_code_value_weighted_summaskentryright = ff_q_pvs_value_weighted_summaskentryrightnegative * S ((S (dc_quotient_value_weighted_summaskentry)) * dst_negative_scale_value_weighted_summaskentryright) + (dst_negative_value_weighted_summaskentryright))) /\ (exists ge_balance_positive_value_weighted_summaskentryrightvalue ge_balance_negative_value_weighted_summaskentryrightvalue. (((((dc_right_value_weighted_summaskentry) = 2 * (ge_balance_positive_value_weighted_summaskentryrightvalue) /\ (ge_balance_negative_value_weighted_summaskentryrightvalue) = 0) \/ exists ge_signed_half_value_weighted_summaskentryrightvaluedecode. (((dc_right_value_weighted_summaskentry) = 2 * ge_signed_half_value_weighted_summaskentryrightvaluedecode + 1 /\ (ge_balance_positive_value_weighted_summaskentryrightvalue) = 0) /\ (ge_balance_negative_value_weighted_summaskentryrightvalue) = S ge_signed_half_value_weighted_summaskentryrightvaluedecode))) /\ ((dst_positive_value_weighted_summaskentryright) + ge_balance_negative_value_weighted_summaskentryrightvalue = (dst_negative_value_weighted_summaskentryright) + ge_balance_positive_value_weighted_summaskentryrightvalue))))))))) /\ (exists sto_ap_value_weighted_summaskentryproduct sto_an_value_weighted_summaskentryproduct sto_bp_value_weighted_summaskentryproduct sto_bn_value_weighted_summaskentryproduct sto_cp_value_weighted_summaskentryproduct sto_cn_value_weighted_summaskentryproduct. (((((dc_left_value_weighted_summaskentry) = 2 * (sto_ap_value_weighted_summaskentryproduct) /\ (sto_an_value_weighted_summaskentryproduct) = 0) \/ exists ge_signed_half_value_weighted_summaskentryproductleft. (((dc_left_value_weighted_summaskentry) = 2 * ge_signed_half_value_weighted_summaskentryproductleft + 1 /\ (sto_ap_value_weighted_summaskentryproduct) = 0) /\ (sto_an_value_weighted_summaskentryproduct) = S ge_signed_half_value_weighted_summaskentryproductleft))) /\ ((((((dc_right_value_weighted_summaskentry) = 2 * (sto_bp_value_weighted_summaskentryproduct) /\ (sto_bn_value_weighted_summaskentryproduct) = 0) \/ exists ge_signed_half_value_weighted_summaskentryproductright. (((dc_right_value_weighted_summaskentry) = 2 * ge_signed_half_value_weighted_summaskentryproductright + 1 /\ (sto_bp_value_weighted_summaskentryproduct) = 0) /\ (sto_bn_value_weighted_summaskentryproduct) = S ge_signed_half_value_weighted_summaskentryproductright))) /\ ((((((dc_value_value_weighted_summask) = 2 * (sto_cp_value_weighted_summaskentryproduct) /\ (sto_cn_value_weighted_summaskentryproduct) = 0) \/ exists ge_signed_half_value_weighted_summaskentryproductoutput. (((dc_value_value_weighted_summask) = 2 * ge_signed_half_value_weighted_summaskentryproductoutput + 1 /\ (sto_cp_value_weighted_summaskentryproduct) = 0) /\ (sto_cn_value_weighted_summaskentryproduct) = S ge_signed_half_value_weighted_summaskentryproductoutput))) /\ ((sto_ap_value_weighted_summaskentryproduct * sto_bp_value_weighted_summaskentryproduct + sto_an_value_weighted_summaskentryproduct * sto_bn_value_weighted_summaskentryproduct) + sto_cn_value_weighted_summaskentryproduct = (sto_ap_value_weighted_summaskentryproduct * sto_bn_value_weighted_summaskentryproduct + sto_an_value_weighted_summaskentryproduct * sto_bp_value_weighted_summaskentryproduct) + sto_cp_value_weighted_summaskentryproduct))))))))))))))) \/ ((((dc_index_value_weighted_summask)=0 \/ ~(exists pvs_factor_value_weighted_summaskentrynondivisor. (n) = (dc_index_value_weighted_summask) * pvs_factor_value_weighted_summaskentrynondivisor)) /\ ((dc_value_value_weighted_summask)=0))))))) /\ (exists dst_positive_code_value_weighted_sumfold dst_positive_scale_value_weighted_sumfold dst_negative_code_value_weighted_sumfold dst_negative_scale_value_weighted_sumfold dst_positive_sum_value_weighted_sumfold dst_negative_sum_value_weighted_sumfold. (((dc_mask_value_weighted_sum) = (((((dst_positive_code_value_weighted_sumfold) + (dst_positive_scale_value_weighted_sumfold)) * S ((dst_positive_code_value_weighted_sumfold) + (dst_positive_scale_value_weighted_sumfold)) + ((dst_positive_scale_value_weighted_sumfold) + (dst_positive_scale_value_weighted_sumfold))) + (((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) * S ((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) + ((dst_negative_scale_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)))) * S ((((dst_positive_code_value_weighted_sumfold) + (dst_positive_scale_value_weighted_sumfold)) * S ((dst_positive_code_value_weighted_sumfold) + (dst_positive_scale_value_weighted_sumfold)) + ((dst_positive_scale_value_weighted_sumfold) + (dst_positive_scale_value_weighted_sumfold))) + (((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) * S ((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) + ((dst_negative_scale_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)))) + ((((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) * S ((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) + ((dst_negative_scale_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold))) + (((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) * S ((dst_negative_code_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)) + ((dst_negative_scale_value_weighted_sumfold) + (dst_negative_scale_value_weighted_sumfold)))))) /\ (((exists fs_u_dst_value_weighted_sumfoldpositive fs_v_dst_value_weighted_sumfoldpositive. ((((exists fs_h_dst_value_weighted_sumfoldpositive_body_start. fs_h_dst_value_weighted_sumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_value_weighted_sumfoldpositive)) /\ exists fs_q_dst_value_weighted_sumfoldpositive_body_start. fs_u_dst_value_weighted_sumfoldpositive = fs_q_dst_value_weighted_sumfoldpositive_body_start * S ((S (0)) * fs_v_dst_value_weighted_sumfoldpositive) + (0))) /\ ((((exists fs_h_dst_value_weighted_sumfoldpositive_body_terminal. fs_h_dst_value_weighted_sumfoldpositive_body_terminal + S (dst_positive_sum_value_weighted_sumfold) = S ((S (S (n))) * fs_v_dst_value_weighted_sumfoldpositive)) /\ exists fs_q_dst_value_weighted_sumfoldpositive_body_terminal. fs_u_dst_value_weighted_sumfoldpositive = fs_q_dst_value_weighted_sumfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_value_weighted_sumfoldpositive) + (dst_positive_sum_value_weighted_sumfold))) /\ forall fs_i_dst_value_weighted_sumfoldpositive_body_steps. (exists fs_lt_dst_value_weighted_sumfoldpositive_body_steps_bound. fs_lt_dst_value_weighted_sumfoldpositive_body_steps_bound + S fs_i_dst_value_weighted_sumfoldpositive_body_steps = S (n)) -> exists fs_a_dst_value_weighted_sumfoldpositive_body_steps fs_r_dst_value_weighted_sumfoldpositive_body_steps fs_s_dst_value_weighted_sumfoldpositive_body_steps. ((((exists fs_h_dst_value_weighted_sumfoldpositive_body_steps_summand. fs_h_dst_value_weighted_sumfoldpositive_body_steps_summand + S (fs_a_dst_value_weighted_sumfoldpositive_body_steps) = S ((S (fs_i_dst_value_weighted_sumfoldpositive_body_steps)) * dst_positive_scale_value_weighted_sumfold)) /\ exists fs_q_dst_value_weighted_sumfoldpositive_body_steps_summand. dst_positive_code_value_weighted_sumfold = fs_q_dst_value_weighted_sumfoldpositive_body_steps_summand * S ((S (fs_i_dst_value_weighted_sumfoldpositive_body_steps)) * dst_positive_scale_value_weighted_sumfold) + (fs_a_dst_value_weighted_sumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_value_weighted_sumfoldpositive_body_steps_partial. fs_h_dst_value_weighted_sumfoldpositive_body_steps_partial + S (fs_r_dst_value_weighted_sumfoldpositive_body_steps) = S ((S (fs_i_dst_value_weighted_sumfoldpositive_body_steps)) * fs_v_dst_value_weighted_sumfoldpositive)) /\ exists fs_q_dst_value_weighted_sumfoldpositive_body_steps_partial. fs_u_dst_value_weighted_sumfoldpositive = fs_q_dst_value_weighted_sumfoldpositive_body_steps_partial * S ((S (fs_i_dst_value_weighted_sumfoldpositive_body_steps)) * fs_v_dst_value_weighted_sumfoldpositive) + (fs_r_dst_value_weighted_sumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_value_weighted_sumfoldpositive_body_steps_successor. fs_h_dst_value_weighted_sumfoldpositive_body_steps_successor + S (fs_s_dst_value_weighted_sumfoldpositive_body_steps) = S ((S (S fs_i_dst_value_weighted_sumfoldpositive_body_steps)) * fs_v_dst_value_weighted_sumfoldpositive)) /\ exists fs_q_dst_value_weighted_sumfoldpositive_body_steps_successor. fs_u_dst_value_weighted_sumfoldpositive = fs_q_dst_value_weighted_sumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_value_weighted_sumfoldpositive_body_steps)) * fs_v_dst_value_weighted_sumfoldpositive) + (fs_s_dst_value_weighted_sumfoldpositive_body_steps))) /\ fs_s_dst_value_weighted_sumfoldpositive_body_steps = fs_r_dst_value_weighted_sumfoldpositive_body_steps + fs_a_dst_value_weighted_sumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_value_weighted_sumfoldnegative fs_v_dst_value_weighted_sumfoldnegative. ((((exists fs_h_dst_value_weighted_sumfoldnegative_body_start. fs_h_dst_value_weighted_sumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_value_weighted_sumfoldnegative)) /\ exists fs_q_dst_value_weighted_sumfoldnegative_body_start. fs_u_dst_value_weighted_sumfoldnegative = fs_q_dst_value_weighted_sumfoldnegative_body_start * S ((S (0)) * fs_v_dst_value_weighted_sumfoldnegative) + (0))) /\ ((((exists fs_h_dst_value_weighted_sumfoldnegative_body_terminal. fs_h_dst_value_weighted_sumfoldnegative_body_terminal + S (dst_negative_sum_value_weighted_sumfold) = S ((S (S (n))) * fs_v_dst_value_weighted_sumfoldnegative)) /\ exists fs_q_dst_value_weighted_sumfoldnegative_body_terminal. fs_u_dst_value_weighted_sumfoldnegative = fs_q_dst_value_weighted_sumfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_value_weighted_sumfoldnegative) + (dst_negative_sum_value_weighted_sumfold))) /\ forall fs_i_dst_value_weighted_sumfoldnegative_body_steps. (exists fs_lt_dst_value_weighted_sumfoldnegative_body_steps_bound. fs_lt_dst_value_weighted_sumfoldnegative_body_steps_bound + S fs_i_dst_value_weighted_sumfoldnegative_body_steps = S (n)) -> exists fs_a_dst_value_weighted_sumfoldnegative_body_steps fs_r_dst_value_weighted_sumfoldnegative_body_steps fs_s_dst_value_weighted_sumfoldnegative_body_steps. ((((exists fs_h_dst_value_weighted_sumfoldnegative_body_steps_summand. fs_h_dst_value_weighted_sumfoldnegative_body_steps_summand + S (fs_a_dst_value_weighted_sumfoldnegative_body_steps) = S ((S (fs_i_dst_value_weighted_sumfoldnegative_body_steps)) * dst_negative_scale_value_weighted_sumfold)) /\ exists fs_q_dst_value_weighted_sumfoldnegative_body_steps_summand. dst_negative_code_value_weighted_sumfold = fs_q_dst_value_weighted_sumfoldnegative_body_steps_summand * S ((S (fs_i_dst_value_weighted_sumfoldnegative_body_steps)) * dst_negative_scale_value_weighted_sumfold) + (fs_a_dst_value_weighted_sumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_value_weighted_sumfoldnegative_body_steps_partial. fs_h_dst_value_weighted_sumfoldnegative_body_steps_partial + S (fs_r_dst_value_weighted_sumfoldnegative_body_steps) = S ((S (fs_i_dst_value_weighted_sumfoldnegative_body_steps)) * fs_v_dst_value_weighted_sumfoldnegative)) /\ exists fs_q_dst_value_weighted_sumfoldnegative_body_steps_partial. fs_u_dst_value_weighted_sumfoldnegative = fs_q_dst_value_weighted_sumfoldnegative_body_steps_partial * S ((S (fs_i_dst_value_weighted_sumfoldnegative_body_steps)) * fs_v_dst_value_weighted_sumfoldnegative) + (fs_r_dst_value_weighted_sumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_value_weighted_sumfoldnegative_body_steps_successor. fs_h_dst_value_weighted_sumfoldnegative_body_steps_successor + S (fs_s_dst_value_weighted_sumfoldnegative_body_steps) = S ((S (S fs_i_dst_value_weighted_sumfoldnegative_body_steps)) * fs_v_dst_value_weighted_sumfoldnegative)) /\ exists fs_q_dst_value_weighted_sumfoldnegative_body_steps_successor. fs_u_dst_value_weighted_sumfoldnegative = fs_q_dst_value_weighted_sumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_value_weighted_sumfoldnegative_body_steps)) * fs_v_dst_value_weighted_sumfoldnegative) + (fs_s_dst_value_weighted_sumfoldnegative_body_steps))) /\ fs_s_dst_value_weighted_sumfoldnegative_body_steps = fs_r_dst_value_weighted_sumfoldnegative_body_steps + fs_a_dst_value_weighted_sumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_value_weighted_sumfoldresult ge_balance_negative_value_weighted_sumfoldresult. (((((b) = 2 * (ge_balance_positive_value_weighted_sumfoldresult) /\ (ge_balance_negative_value_weighted_sumfoldresult) = 0) \/ exists ge_signed_half_value_weighted_sumfoldresultdecode. (((b) = 2 * ge_signed_half_value_weighted_sumfoldresultdecode + 1 /\ (ge_balance_positive_value_weighted_sumfoldresult) = 0) /\ (ge_balance_negative_value_weighted_sumfoldresult) = S ge_signed_half_value_weighted_sumfoldresultdecode))) /\ ((dst_positive_sum_value_weighted_sumfold) + ge_balance_negative_value_weighted_sumfoldresult = (dst_negative_sum_value_weighted_sumfold) + ge_balance_positive_value_weighted_sumfoldresult))))))))))))) -> a=b