mobius_inversion_reconstructs_divisor_transform

forall N F G M. (exists dst_positive_code_reverse_source dst_positive_scale_reverse_source dst_negative_code_reverse_source dst_negative_scale_reverse_source. (((F) = (((((dst_positive_code_reverse_source) + (dst_positive_scale_reverse_source)) * S ((dst_positive_code_reverse_source) + (dst_positive_scale_reverse_source)) + ((dst_positive_scale_reverse_source) + (dst_positive_scale_reverse_source))) + (((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) * S ((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) + ((dst_negative_scale_reverse_source) + (dst_negative_scale_reverse_source)))) * S ((((dst_positive_code_reverse_source) + (dst_positive_scale_reverse_source)) * S ((dst_positive_code_reverse_source) + (dst_positive_scale_reverse_source)) + ((dst_positive_scale_reverse_source) + (dst_positive_scale_reverse_source))) + (((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) * S ((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) + ((dst_negative_scale_reverse_source) + (dst_negative_scale_reverse_source)))) + ((((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) * S ((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) + ((dst_negative_scale_reverse_source) + (dst_negative_scale_reverse_source))) + (((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) * S ((dst_negative_code_reverse_source) + (dst_negative_scale_reverse_source)) + ((dst_negative_scale_reverse_source) + (dst_negative_scale_reverse_source)))))) /\ (forall dst_index_reverse_source. (exists pvs_le_gap_reverse_sourcedomain. pvs_le_gap_reverse_sourcedomain + (dst_index_reverse_source) = (N)) -> exists dst_positive_reverse_source dst_negative_reverse_source dst_value_reverse_source. ((((exists ff_h_pvs_reverse_sourceentrypositive. ff_h_pvs_reverse_sourceentrypositive + S (dst_positive_reverse_source) = S ((S (dst_index_reverse_source)) * dst_positive_scale_reverse_source)) /\ exists ff_q_pvs_reverse_sourceentrypositive. dst_positive_code_reverse_source = ff_q_pvs_reverse_sourceentrypositive * S ((S (dst_index_reverse_source)) * dst_positive_scale_reverse_source) + (dst_positive_reverse_source))) /\ (((((exists ff_h_pvs_reverse_sourceentrynegative. ff_h_pvs_reverse_sourceentrynegative + S (dst_negative_reverse_source) = S ((S (dst_index_reverse_source)) * dst_negative_scale_reverse_source)) /\ exists ff_q_pvs_reverse_sourceentrynegative. dst_negative_code_reverse_source = ff_q_pvs_reverse_sourceentrynegative * S ((S (dst_index_reverse_source)) * dst_negative_scale_reverse_source) + (dst_negative_reverse_source))) /\ (exists ge_balance_positive_reverse_sourceentryvalue ge_balance_negative_reverse_sourceentryvalue. (((((dst_value_reverse_source) = 2 * (ge_balance_positive_reverse_sourceentryvalue) /\ (ge_balance_negative_reverse_sourceentryvalue) = 0) \/ exists ge_signed_half_reverse_sourceentryvaluedecode. (((dst_value_reverse_source) = 2 * ge_signed_half_reverse_sourceentryvaluedecode + 1 /\ (ge_balance_positive_reverse_sourceentryvalue) = 0) /\ (ge_balance_negative_reverse_sourceentryvalue) = S ge_signed_half_reverse_sourceentryvaluedecode))) /\ ((dst_positive_reverse_source) + ge_balance_negative_reverse_sourceentryvalue = (dst_negative_reverse_source) + ge_balance_positive_reverse_sourceentryvalue))))))))) -> (exists dst_positive_code_reverse_transform_table dst_positive_scale_reverse_transform_table dst_negative_code_reverse_transform_table dst_negative_scale_reverse_transform_table. (((G) = (((((dst_positive_code_reverse_transform_table) + (dst_positive_scale_reverse_transform_table)) * S ((dst_positive_code_reverse_transform_table) + (dst_positive_scale_reverse_transform_table)) + ((dst_positive_scale_reverse_transform_table) + (dst_positive_scale_reverse_transform_table))) + (((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) * S ((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) + ((dst_negative_scale_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)))) * S ((((dst_positive_code_reverse_transform_table) + (dst_positive_scale_reverse_transform_table)) * S ((dst_positive_code_reverse_transform_table) + (dst_positive_scale_reverse_transform_table)) + ((dst_positive_scale_reverse_transform_table) + (dst_positive_scale_reverse_transform_table))) + (((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) * S ((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) + ((dst_negative_scale_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)))) + ((((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) * S ((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) + ((dst_negative_scale_reverse_transform_table) + (dst_negative_scale_reverse_transform_table))) + (((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) * S ((dst_negative_code_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)) + ((dst_negative_scale_reverse_transform_table) + (dst_negative_scale_reverse_transform_table)))))) /\ (forall dst_index_reverse_transform_table. (exists pvs_le_gap_reverse_transform_tabledomain. pvs_le_gap_reverse_transform_tabledomain + (dst_index_reverse_transform_table) = (N)) -> exists dst_positive_reverse_transform_table dst_negative_reverse_transform_table dst_value_reverse_transform_table. ((((exists ff_h_pvs_reverse_transform_tableentrypositive. ff_h_pvs_reverse_transform_tableentrypositive + S (dst_positive_reverse_transform_table) = S ((S (dst_index_reverse_transform_table)) * dst_positive_scale_reverse_transform_table)) /\ exists ff_q_pvs_reverse_transform_tableentrypositive. dst_positive_code_reverse_transform_table = ff_q_pvs_reverse_transform_tableentrypositive * S ((S (dst_index_reverse_transform_table)) * dst_positive_scale_reverse_transform_table) + (dst_positive_reverse_transform_table))) /\ (((((exists ff_h_pvs_reverse_transform_tableentrynegative. ff_h_pvs_reverse_transform_tableentrynegative + S (dst_negative_reverse_transform_table) = S ((S (dst_index_reverse_transform_table)) * dst_negative_scale_reverse_transform_table)) /\ exists ff_q_pvs_reverse_transform_tableentrynegative. dst_negative_code_reverse_transform_table = ff_q_pvs_reverse_transform_tableentrynegative * S ((S (dst_index_reverse_transform_table)) * dst_negative_scale_reverse_transform_table) + (dst_negative_reverse_transform_table))) /\ (exists ge_balance_positive_reverse_transform_tableentryvalue ge_balance_negative_reverse_transform_tableentryvalue. (((((dst_value_reverse_transform_table) = 2 * (ge_balance_positive_reverse_transform_tableentryvalue) /\ (ge_balance_negative_reverse_transform_tableentryvalue) = 0) \/ exists ge_signed_half_reverse_transform_tableentryvaluedecode. (((dst_value_reverse_transform_table) = 2 * ge_signed_half_reverse_transform_tableentryvaluedecode + 1 /\ (ge_balance_positive_reverse_transform_tableentryvalue) = 0) /\ (ge_balance_negative_reverse_transform_tableentryvalue) = S ge_signed_half_reverse_transform_tableentryvaluedecode))) /\ ((dst_positive_reverse_transform_table) + ge_balance_negative_reverse_transform_tableentryvalue = (dst_negative_reverse_transform_table) + ge_balance_positive_reverse_transform_tableentryvalue))))))))) -> (((exists dst_positive_code_reverse_mobiustable dst_positive_scale_reverse_mobiustable dst_negative_code_reverse_mobiustable dst_negative_scale_reverse_mobiustable. (((M) = (((((dst_positive_code_reverse_mobiustable) + (dst_positive_scale_reverse_mobiustable)) * S ((dst_positive_code_reverse_mobiustable) + (dst_positive_scale_reverse_mobiustable)) + ((dst_positive_scale_reverse_mobiustable) + (dst_positive_scale_reverse_mobiustable))) + (((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) * S ((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) + ((dst_negative_scale_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)))) * S ((((dst_positive_code_reverse_mobiustable) + (dst_positive_scale_reverse_mobiustable)) * S ((dst_positive_code_reverse_mobiustable) + (dst_positive_scale_reverse_mobiustable)) + ((dst_positive_scale_reverse_mobiustable) + (dst_positive_scale_reverse_mobiustable))) + (((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) * S ((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) + ((dst_negative_scale_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)))) + ((((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) * S ((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) + ((dst_negative_scale_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable))) + (((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) * S ((dst_negative_code_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)) + ((dst_negative_scale_reverse_mobiustable) + (dst_negative_scale_reverse_mobiustable)))))) /\ (forall dst_index_reverse_mobiustable. (exists pvs_le_gap_reverse_mobiustabledomain. pvs_le_gap_reverse_mobiustabledomain + (dst_index_reverse_mobiustable) = (N)) -> exists dst_positive_reverse_mobiustable dst_negative_reverse_mobiustable dst_value_reverse_mobiustable. ((((exists ff_h_pvs_reverse_mobiustableentrypositive. ff_h_pvs_reverse_mobiustableentrypositive + S (dst_positive_reverse_mobiustable) = S ((S (dst_index_reverse_mobiustable)) * dst_positive_scale_reverse_mobiustable)) /\ exists ff_q_pvs_reverse_mobiustableentrypositive. dst_positive_code_reverse_mobiustable = ff_q_pvs_reverse_mobiustableentrypositive * S ((S (dst_index_reverse_mobiustable)) * dst_positive_scale_reverse_mobiustable) + (dst_positive_reverse_mobiustable))) /\ (((((exists ff_h_pvs_reverse_mobiustableentrynegative. ff_h_pvs_reverse_mobiustableentrynegative + S (dst_negative_reverse_mobiustable) = S ((S (dst_index_reverse_mobiustable)) * dst_negative_scale_reverse_mobiustable)) /\ exists ff_q_pvs_reverse_mobiustableentrynegative. dst_negative_code_reverse_mobiustable = ff_q_pvs_reverse_mobiustableentrynegative * S ((S (dst_index_reverse_mobiustable)) * dst_negative_scale_reverse_mobiustable) + (dst_negative_reverse_mobiustable))) /\ (exists ge_balance_positive_reverse_mobiustableentryvalue ge_balance_negative_reverse_mobiustableentryvalue. (((((dst_value_reverse_mobiustable) = 2 * (ge_balance_positive_reverse_mobiustableentryvalue) /\ (ge_balance_negative_reverse_mobiustableentryvalue) = 0) \/ exists ge_signed_half_reverse_mobiustableentryvaluedecode. (((dst_value_reverse_mobiustable) = 2 * ge_signed_half_reverse_mobiustableentryvaluedecode + 1 /\ (ge_balance_positive_reverse_mobiustableentryvalue) = 0) /\ (ge_balance_negative_reverse_mobiustableentryvalue) = S ge_signed_half_reverse_mobiustableentryvaluedecode))) /\ ((dst_positive_reverse_mobiustable) + ge_balance_negative_reverse_mobiustableentryvalue = (dst_negative_reverse_mobiustable) + ge_balance_positive_reverse_mobiustableentryvalue))))))))) /\ (((exists dst_positive_code_reverse_mobiuszero dst_positive_scale_reverse_mobiuszero dst_negative_code_reverse_mobiuszero dst_negative_scale_reverse_mobiuszero dst_positive_reverse_mobiuszero dst_negative_reverse_mobiuszero. (((M) = (((((dst_positive_code_reverse_mobiuszero) + (dst_positive_scale_reverse_mobiuszero)) * S ((dst_positive_code_reverse_mobiuszero) + (dst_positive_scale_reverse_mobiuszero)) + ((dst_positive_scale_reverse_mobiuszero) + (dst_positive_scale_reverse_mobiuszero))) + (((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) * S ((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) + ((dst_negative_scale_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)))) * S ((((dst_positive_code_reverse_mobiuszero) + (dst_positive_scale_reverse_mobiuszero)) * S ((dst_positive_code_reverse_mobiuszero) + (dst_positive_scale_reverse_mobiuszero)) + ((dst_positive_scale_reverse_mobiuszero) + (dst_positive_scale_reverse_mobiuszero))) + (((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) * S ((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) + ((dst_negative_scale_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)))) + ((((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) * S ((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) + ((dst_negative_scale_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero))) + (((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) * S ((dst_negative_code_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)) + ((dst_negative_scale_reverse_mobiuszero) + (dst_negative_scale_reverse_mobiuszero)))))) /\ (((((exists ff_h_pvs_reverse_mobiuszeropositive. ff_h_pvs_reverse_mobiuszeropositive + S (dst_positive_reverse_mobiuszero) = S ((S (0)) * dst_positive_scale_reverse_mobiuszero)) /\ exists ff_q_pvs_reverse_mobiuszeropositive. dst_positive_code_reverse_mobiuszero = ff_q_pvs_reverse_mobiuszeropositive * S ((S (0)) * dst_positive_scale_reverse_mobiuszero) + (dst_positive_reverse_mobiuszero))) /\ (((((exists ff_h_pvs_reverse_mobiuszeronegative. ff_h_pvs_reverse_mobiuszeronegative + S (dst_negative_reverse_mobiuszero) = S ((S (0)) * dst_negative_scale_reverse_mobiuszero)) /\ exists ff_q_pvs_reverse_mobiuszeronegative. dst_negative_code_reverse_mobiuszero = ff_q_pvs_reverse_mobiuszeronegative * S ((S (0)) * dst_negative_scale_reverse_mobiuszero) + (dst_negative_reverse_mobiuszero))) /\ (exists ge_balance_positive_reverse_mobiuszerovalue ge_balance_negative_reverse_mobiuszerovalue. (((((0) = 2 * (ge_balance_positive_reverse_mobiuszerovalue) /\ (ge_balance_negative_reverse_mobiuszerovalue) = 0) \/ exists ge_signed_half_reverse_mobiuszerovaluedecode. (((0) = 2 * ge_signed_half_reverse_mobiuszerovaluedecode + 1 /\ (ge_balance_positive_reverse_mobiuszerovalue) = 0) /\ (ge_balance_negative_reverse_mobiuszerovalue) = S ge_signed_half_reverse_mobiuszerovaluedecode))) /\ ((dst_positive_reverse_mobiuszero) + ge_balance_negative_reverse_mobiuszerovalue = (dst_negative_reverse_mobiuszero) + ge_balance_positive_reverse_mobiuszerovalue))))))))) /\ (forall mt_index_reverse_mobius mt_value_reverse_mobius. ~(mt_index_reverse_mobius=0) -> (exists pvs_le_gap_reverse_mobiusdomain. pvs_le_gap_reverse_mobiusdomain + (mt_index_reverse_mobius) = (N)) -> (exists dst_positive_code_reverse_mobiusentry dst_positive_scale_reverse_mobiusentry dst_negative_code_reverse_mobiusentry dst_negative_scale_reverse_mobiusentry dst_positive_reverse_mobiusentry dst_negative_reverse_mobiusentry. (((M) = (((((dst_positive_code_reverse_mobiusentry) + (dst_positive_scale_reverse_mobiusentry)) * S ((dst_positive_code_reverse_mobiusentry) + (dst_positive_scale_reverse_mobiusentry)) + ((dst_positive_scale_reverse_mobiusentry) + (dst_positive_scale_reverse_mobiusentry))) + (((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) * S ((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) + ((dst_negative_scale_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)))) * S ((((dst_positive_code_reverse_mobiusentry) + (dst_positive_scale_reverse_mobiusentry)) * S ((dst_positive_code_reverse_mobiusentry) + (dst_positive_scale_reverse_mobiusentry)) + ((dst_positive_scale_reverse_mobiusentry) + (dst_positive_scale_reverse_mobiusentry))) + (((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) * S ((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) + ((dst_negative_scale_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)))) + ((((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) * S ((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) + ((dst_negative_scale_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry))) + (((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) * S ((dst_negative_code_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)) + ((dst_negative_scale_reverse_mobiusentry) + (dst_negative_scale_reverse_mobiusentry)))))) /\ (((((exists ff_h_pvs_reverse_mobiusentrypositive. ff_h_pvs_reverse_mobiusentrypositive + S (dst_positive_reverse_mobiusentry) = S ((S (mt_index_reverse_mobius)) * dst_positive_scale_reverse_mobiusentry)) /\ exists ff_q_pvs_reverse_mobiusentrypositive. dst_positive_code_reverse_mobiusentry = ff_q_pvs_reverse_mobiusentrypositive * S ((S (mt_index_reverse_mobius)) * dst_positive_scale_reverse_mobiusentry) + (dst_positive_reverse_mobiusentry))) /\ (((((exists ff_h_pvs_reverse_mobiusentrynegative. ff_h_pvs_reverse_mobiusentrynegative + S (dst_negative_reverse_mobiusentry) = S ((S (mt_index_reverse_mobius)) * dst_negative_scale_reverse_mobiusentry)) /\ exists ff_q_pvs_reverse_mobiusentrynegative. dst_negative_code_reverse_mobiusentry = ff_q_pvs_reverse_mobiusentrynegative * S ((S (mt_index_reverse_mobius)) * dst_negative_scale_reverse_mobiusentry) + (dst_negative_reverse_mobiusentry))) /\ (exists ge_balance_positive_reverse_mobiusentryvalue ge_balance_negative_reverse_mobiusentryvalue. (((((mt_value_reverse_mobius) = 2 * (ge_balance_positive_reverse_mobiusentryvalue) /\ (ge_balance_negative_reverse_mobiusentryvalue) = 0) \/ exists ge_signed_half_reverse_mobiusentryvaluedecode. (((mt_value_reverse_mobius) = 2 * ge_signed_half_reverse_mobiusentryvaluedecode + 1 /\ (ge_balance_positive_reverse_mobiusentryvalue) = 0) /\ (ge_balance_negative_reverse_mobiusentryvalue) = S ge_signed_half_reverse_mobiusentryvaluedecode))) /\ ((dst_positive_reverse_mobiusentry) + ge_balance_negative_reverse_mobiusentryvalue = (dst_negative_reverse_mobiusentry) + ge_balance_positive_reverse_mobiusentryvalue))))))))) -> (((~((mt_index_reverse_mobius) = 0)) /\ ((((exists mv_square_prime_reverse_mobiusvaluesquare. ((~((mv_square_prime_reverse_mobiusvaluesquare) = 1) /\ forall pvs_left_reverse_mobiusvaluesquareprime pvs_right_reverse_mobiusvaluesquareprime. (mv_square_prime_reverse_mobiusvaluesquare) = pvs_left_reverse_mobiusvaluesquareprime * pvs_right_reverse_mobiusvaluesquareprime -> pvs_left_reverse_mobiusvaluesquareprime = 1 \/ pvs_right_reverse_mobiusvaluesquareprime = 1) /\ (exists pvs_factor_reverse_mobiusvaluesquaredivisor. (mt_index_reverse_mobius) = (mv_square_prime_reverse_mobiusvaluesquare * mv_square_prime_reverse_mobiusvaluesquare) * pvs_factor_reverse_mobiusvaluesquaredivisor))) /\ ((mt_value_reverse_mobius) = 0))) \/ (((((~((mt_index_reverse_mobius) = 0)) /\ (forall sfd_prime_reverse_mobiusvaluesquarefree. (~((sfd_prime_reverse_mobiusvaluesquarefree) = 1) /\ forall pvs_left_reverse_mobiusvaluesquarefreedomain pvs_right_reverse_mobiusvaluesquarefreedomain. (sfd_prime_reverse_mobiusvaluesquarefree) = pvs_left_reverse_mobiusvaluesquarefreedomain * pvs_right_reverse_mobiusvaluesquarefreedomain -> pvs_left_reverse_mobiusvaluesquarefreedomain = 1 \/ pvs_right_reverse_mobiusvaluesquarefreedomain = 1) -> (exists pvs_le_gap_reverse_mobiusvaluesquarefreebound. pvs_le_gap_reverse_mobiusvaluesquarefreebound + (sfd_prime_reverse_mobiusvaluesquarefree) = (mt_index_reverse_mobius)) -> ~(exists pvs_factor_reverse_mobiusvaluesquarefreesquare. (mt_index_reverse_mobius) = (sfd_prime_reverse_mobiusvaluesquarefree * sfd_prime_reverse_mobiusvaluesquarefree) * pvs_factor_reverse_mobiusvaluesquarefreesquare)))) /\ (exists mv_factor_code_reverse_mobiusvaluefactors mv_factor_scale_reverse_mobiusvaluefactors mv_factor_count_reverse_mobiusvaluefactors. (((~(mt_index_reverse_mobius = 0) /\ ((exists ff_u_fsat_reverse_mobiusvaluefactorsfactorization_product ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_start. ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_start. ff_u_fsat_reverse_mobiusvaluefactorsfactorization_product = ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_terminal. ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_terminal + S (mt_index_reverse_mobius) = S ((S (mv_factor_count_reverse_mobiusvaluefactors)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_terminal. ff_u_fsat_reverse_mobiusvaluefactorsfactorization_product = ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_reverse_mobiusvaluefactors)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product) + (mt_index_reverse_mobius))) /\ forall ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product. (exists ff_lt_fsat_reverse_mobiusvaluefactorsfactorization_product_bound. ff_lt_fsat_reverse_mobiusvaluefactorsfactorization_product_bound + S ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product = mv_factor_count_reverse_mobiusvaluefactors) -> exists ff_p_fsat_reverse_mobiusvaluefactorsfactorization_product ff_r_fsat_reverse_mobiusvaluefactorsfactorization_product ff_s_fsat_reverse_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_factor. ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_factor + S (ff_p_fsat_reverse_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_reverse_mobiusvaluefactors)) /\ exists ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_factor. mv_factor_code_reverse_mobiusvaluefactors = ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_reverse_mobiusvaluefactors) + (ff_p_fsat_reverse_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_partial. ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_partial + S (ff_r_fsat_reverse_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_partial. ff_u_fsat_reverse_mobiusvaluefactorsfactorization_product = ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product) + (ff_r_fsat_reverse_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_successor. ff_h_fsat_reverse_mobiusvaluefactorsfactorization_product_successor + S (ff_s_fsat_reverse_mobiusvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_successor. ff_u_fsat_reverse_mobiusvaluefactorsfactorization_product = ff_q_fsat_reverse_mobiusvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_reverse_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_reverse_mobiusvaluefactorsfactorization_product) + (ff_s_fsat_reverse_mobiusvaluefactorsfactorization_product))) /\ ff_s_fsat_reverse_mobiusvaluefactorsfactorization_product = ff_r_fsat_reverse_mobiusvaluefactorsfactorization_product * ff_p_fsat_reverse_mobiusvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_reverse_mobiusvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_reverse_mobiusvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_reverse_mobiusvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_reverse_mobiusvaluefactorsfactorization_primes = (mv_factor_count_reverse_mobiusvaluefactors)) -> exists ftsf_factor_fsat_reverse_mobiusvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_reverse_mobiusvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_reverse_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_reverse_mobiusvaluefactors)) /\ exists ff_q_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_entry. mv_factor_code_reverse_mobiusvaluefactors = ff_q_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_reverse_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_reverse_mobiusvaluefactors) + (ftsf_factor_fsat_reverse_mobiusvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_reverse_mobiusvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_reverse_mobiusvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_reverse_mobiusvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_reverse_mobiusvaluefactorsparityeven. (mv_factor_count_reverse_mobiusvaluefactors) = 2 * mv_even_half_reverse_mobiusvaluefactorsparityeven) /\ ((mt_value_reverse_mobius) = 2))) \/ (((exists mv_odd_half_reverse_mobiusvaluefactorsparityodd. (mv_factor_count_reverse_mobiusvaluefactors) = 2 * mv_odd_half_reverse_mobiusvaluefactorsparityodd + 1) /\ ((mt_value_reverse_mobius) = 1)))))))))))))))) -> (((exists dst_positive_code_reverse_inverseleft dst_positive_scale_reverse_inverseleft dst_negative_code_reverse_inverseleft dst_negative_scale_reverse_inverseleft. (((M) = (((((dst_positive_code_reverse_inverseleft) + (dst_positive_scale_reverse_inverseleft)) * S ((dst_positive_code_reverse_inverseleft) + (dst_positive_scale_reverse_inverseleft)) + ((dst_positive_scale_reverse_inverseleft) + (dst_positive_scale_reverse_inverseleft))) + (((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) * S ((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) + ((dst_negative_scale_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)))) * S ((((dst_positive_code_reverse_inverseleft) + (dst_positive_scale_reverse_inverseleft)) * S ((dst_positive_code_reverse_inverseleft) + (dst_positive_scale_reverse_inverseleft)) + ((dst_positive_scale_reverse_inverseleft) + (dst_positive_scale_reverse_inverseleft))) + (((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) * S ((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) + ((dst_negative_scale_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)))) + ((((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) * S ((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) + ((dst_negative_scale_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft))) + (((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) * S ((dst_negative_code_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)) + ((dst_negative_scale_reverse_inverseleft) + (dst_negative_scale_reverse_inverseleft)))))) /\ (forall dst_index_reverse_inverseleft. (exists pvs_le_gap_reverse_inverseleftdomain. pvs_le_gap_reverse_inverseleftdomain + (dst_index_reverse_inverseleft) = (N)) -> exists dst_positive_reverse_inverseleft dst_negative_reverse_inverseleft dst_value_reverse_inverseleft. ((((exists ff_h_pvs_reverse_inverseleftentrypositive. ff_h_pvs_reverse_inverseleftentrypositive + S (dst_positive_reverse_inverseleft) = S ((S (dst_index_reverse_inverseleft)) * dst_positive_scale_reverse_inverseleft)) /\ exists ff_q_pvs_reverse_inverseleftentrypositive. dst_positive_code_reverse_inverseleft = ff_q_pvs_reverse_inverseleftentrypositive * S ((S (dst_index_reverse_inverseleft)) * dst_positive_scale_reverse_inverseleft) + (dst_positive_reverse_inverseleft))) /\ (((((exists ff_h_pvs_reverse_inverseleftentrynegative. ff_h_pvs_reverse_inverseleftentrynegative + S (dst_negative_reverse_inverseleft) = S ((S (dst_index_reverse_inverseleft)) * dst_negative_scale_reverse_inverseleft)) /\ exists ff_q_pvs_reverse_inverseleftentrynegative. dst_negative_code_reverse_inverseleft = ff_q_pvs_reverse_inverseleftentrynegative * S ((S (dst_index_reverse_inverseleft)) * dst_negative_scale_reverse_inverseleft) + (dst_negative_reverse_inverseleft))) /\ (exists ge_balance_positive_reverse_inverseleftentryvalue ge_balance_negative_reverse_inverseleftentryvalue. (((((dst_value_reverse_inverseleft) = 2 * (ge_balance_positive_reverse_inverseleftentryvalue) /\ (ge_balance_negative_reverse_inverseleftentryvalue) = 0) \/ exists ge_signed_half_reverse_inverseleftentryvaluedecode. (((dst_value_reverse_inverseleft) = 2 * ge_signed_half_reverse_inverseleftentryvaluedecode + 1 /\ (ge_balance_positive_reverse_inverseleftentryvalue) = 0) /\ (ge_balance_negative_reverse_inverseleftentryvalue) = S ge_signed_half_reverse_inverseleftentryvaluedecode))) /\ ((dst_positive_reverse_inverseleft) + ge_balance_negative_reverse_inverseleftentryvalue = (dst_negative_reverse_inverseleft) + ge_balance_positive_reverse_inverseleftentryvalue))))))))) /\ (((exists dst_positive_code_reverse_inverseright dst_positive_scale_reverse_inverseright dst_negative_code_reverse_inverseright dst_negative_scale_reverse_inverseright. (((G) = (((((dst_positive_code_reverse_inverseright) + (dst_positive_scale_reverse_inverseright)) * S ((dst_positive_code_reverse_inverseright) + (dst_positive_scale_reverse_inverseright)) + ((dst_positive_scale_reverse_inverseright) + (dst_positive_scale_reverse_inverseright))) + (((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) * S ((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) + ((dst_negative_scale_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)))) * S ((((dst_positive_code_reverse_inverseright) + (dst_positive_scale_reverse_inverseright)) * S ((dst_positive_code_reverse_inverseright) + (dst_positive_scale_reverse_inverseright)) + ((dst_positive_scale_reverse_inverseright) + (dst_positive_scale_reverse_inverseright))) + (((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) * S ((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) + ((dst_negative_scale_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)))) + ((((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) * S ((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) + ((dst_negative_scale_reverse_inverseright) + (dst_negative_scale_reverse_inverseright))) + (((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) * S ((dst_negative_code_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)) + ((dst_negative_scale_reverse_inverseright) + (dst_negative_scale_reverse_inverseright)))))) /\ (forall dst_index_reverse_inverseright. (exists pvs_le_gap_reverse_inverserightdomain. pvs_le_gap_reverse_inverserightdomain + (dst_index_reverse_inverseright) = (N)) -> exists dst_positive_reverse_inverseright dst_negative_reverse_inverseright dst_value_reverse_inverseright. ((((exists ff_h_pvs_reverse_inverserightentrypositive. ff_h_pvs_reverse_inverserightentrypositive + S (dst_positive_reverse_inverseright) = S ((S (dst_index_reverse_inverseright)) * dst_positive_scale_reverse_inverseright)) /\ exists ff_q_pvs_reverse_inverserightentrypositive. dst_positive_code_reverse_inverseright = ff_q_pvs_reverse_inverserightentrypositive * S ((S (dst_index_reverse_inverseright)) * dst_positive_scale_reverse_inverseright) + (dst_positive_reverse_inverseright))) /\ (((((exists ff_h_pvs_reverse_inverserightentrynegative. ff_h_pvs_reverse_inverserightentrynegative + S (dst_negative_reverse_inverseright) = S ((S (dst_index_reverse_inverseright)) * dst_negative_scale_reverse_inverseright)) /\ exists ff_q_pvs_reverse_inverserightentrynegative. dst_negative_code_reverse_inverseright = ff_q_pvs_reverse_inverserightentrynegative * S ((S (dst_index_reverse_inverseright)) * dst_negative_scale_reverse_inverseright) + (dst_negative_reverse_inverseright))) /\ (exists ge_balance_positive_reverse_inverserightentryvalue ge_balance_negative_reverse_inverserightentryvalue. (((((dst_value_reverse_inverseright) = 2 * (ge_balance_positive_reverse_inverserightentryvalue) /\ (ge_balance_negative_reverse_inverserightentryvalue) = 0) \/ exists ge_signed_half_reverse_inverserightentryvaluedecode. (((dst_value_reverse_inverseright) = 2 * ge_signed_half_reverse_inverserightentryvaluedecode + 1 /\ (ge_balance_positive_reverse_inverserightentryvalue) = 0) /\ (ge_balance_negative_reverse_inverserightentryvalue) = S ge_signed_half_reverse_inverserightentryvaluedecode))) /\ ((dst_positive_reverse_inverseright) + ge_balance_negative_reverse_inverserightentryvalue = (dst_negative_reverse_inverseright) + ge_balance_positive_reverse_inverserightentryvalue))))))))) /\ (((exists dst_positive_code_reverse_inversetable dst_positive_scale_reverse_inversetable dst_negative_code_reverse_inversetable dst_negative_scale_reverse_inversetable. (((F) = (((((dst_positive_code_reverse_inversetable) + (dst_positive_scale_reverse_inversetable)) * S ((dst_positive_code_reverse_inversetable) + (dst_positive_scale_reverse_inversetable)) + ((dst_positive_scale_reverse_inversetable) + (dst_positive_scale_reverse_inversetable))) + (((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) * S ((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) + ((dst_negative_scale_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)))) * S ((((dst_positive_code_reverse_inversetable) + (dst_positive_scale_reverse_inversetable)) * S ((dst_positive_code_reverse_inversetable) + (dst_positive_scale_reverse_inversetable)) + ((dst_positive_scale_reverse_inversetable) + (dst_positive_scale_reverse_inversetable))) + (((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) * S ((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) + ((dst_negative_scale_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)))) + ((((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) * S ((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) + ((dst_negative_scale_reverse_inversetable) + (dst_negative_scale_reverse_inversetable))) + (((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) * S ((dst_negative_code_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)) + ((dst_negative_scale_reverse_inversetable) + (dst_negative_scale_reverse_inversetable)))))) /\ (forall dst_index_reverse_inversetable. (exists pvs_le_gap_reverse_inversetabledomain. pvs_le_gap_reverse_inversetabledomain + (dst_index_reverse_inversetable) = (N)) -> exists dst_positive_reverse_inversetable dst_negative_reverse_inversetable dst_value_reverse_inversetable. ((((exists ff_h_pvs_reverse_inversetableentrypositive. ff_h_pvs_reverse_inversetableentrypositive + S (dst_positive_reverse_inversetable) = S ((S (dst_index_reverse_inversetable)) * dst_positive_scale_reverse_inversetable)) /\ exists ff_q_pvs_reverse_inversetableentrypositive. dst_positive_code_reverse_inversetable = ff_q_pvs_reverse_inversetableentrypositive * S ((S (dst_index_reverse_inversetable)) * dst_positive_scale_reverse_inversetable) + (dst_positive_reverse_inversetable))) /\ (((((exists ff_h_pvs_reverse_inversetableentrynegative. ff_h_pvs_reverse_inversetableentrynegative + S (dst_negative_reverse_inversetable) = S ((S (dst_index_reverse_inversetable)) * dst_negative_scale_reverse_inversetable)) /\ exists ff_q_pvs_reverse_inversetableentrynegative. dst_negative_code_reverse_inversetable = ff_q_pvs_reverse_inversetableentrynegative * S ((S (dst_index_reverse_inversetable)) * dst_negative_scale_reverse_inversetable) + (dst_negative_reverse_inversetable))) /\ (exists ge_balance_positive_reverse_inversetableentryvalue ge_balance_negative_reverse_inversetableentryvalue. (((((dst_value_reverse_inversetable) = 2 * (ge_balance_positive_reverse_inversetableentryvalue) /\ (ge_balance_negative_reverse_inversetableentryvalue) = 0) \/ exists ge_signed_half_reverse_inversetableentryvaluedecode. (((dst_value_reverse_inversetable) = 2 * ge_signed_half_reverse_inversetableentryvaluedecode + 1 /\ (ge_balance_positive_reverse_inversetableentryvalue) = 0) /\ (ge_balance_negative_reverse_inversetableentryvalue) = S ge_signed_half_reverse_inversetableentryvaluedecode))) /\ ((dst_positive_reverse_inversetable) + ge_balance_negative_reverse_inversetableentryvalue = (dst_negative_reverse_inversetable) + ge_balance_positive_reverse_inversetableentryvalue))))))))) /\ (forall dc_input_reverse_inverse dc_output_reverse_inverse. ~(dc_input_reverse_inverse=0) -> (exists pvs_le_gap_reverse_inversedomain. pvs_le_gap_reverse_inversedomain + (dc_input_reverse_inverse) = (N)) -> (exists dst_positive_code_reverse_inverselookup dst_positive_scale_reverse_inverselookup dst_negative_code_reverse_inverselookup dst_negative_scale_reverse_inverselookup dst_positive_reverse_inverselookup dst_negative_reverse_inverselookup. (((F) = (((((dst_positive_code_reverse_inverselookup) + (dst_positive_scale_reverse_inverselookup)) * S ((dst_positive_code_reverse_inverselookup) + (dst_positive_scale_reverse_inverselookup)) + ((dst_positive_scale_reverse_inverselookup) + (dst_positive_scale_reverse_inverselookup))) + (((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) * S ((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) + ((dst_negative_scale_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)))) * S ((((dst_positive_code_reverse_inverselookup) + (dst_positive_scale_reverse_inverselookup)) * S ((dst_positive_code_reverse_inverselookup) + (dst_positive_scale_reverse_inverselookup)) + ((dst_positive_scale_reverse_inverselookup) + (dst_positive_scale_reverse_inverselookup))) + (((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) * S ((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) + ((dst_negative_scale_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)))) + ((((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) * S ((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) + ((dst_negative_scale_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup))) + (((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) * S ((dst_negative_code_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)) + ((dst_negative_scale_reverse_inverselookup) + (dst_negative_scale_reverse_inverselookup)))))) /\ (((((exists ff_h_pvs_reverse_inverselookuppositive. ff_h_pvs_reverse_inverselookuppositive + S (dst_positive_reverse_inverselookup) = S ((S (dc_input_reverse_inverse)) * dst_positive_scale_reverse_inverselookup)) /\ exists ff_q_pvs_reverse_inverselookuppositive. dst_positive_code_reverse_inverselookup = ff_q_pvs_reverse_inverselookuppositive * S ((S (dc_input_reverse_inverse)) * dst_positive_scale_reverse_inverselookup) + (dst_positive_reverse_inverselookup))) /\ (((((exists ff_h_pvs_reverse_inverselookupnegative. ff_h_pvs_reverse_inverselookupnegative + S (dst_negative_reverse_inverselookup) = S ((S (dc_input_reverse_inverse)) * dst_negative_scale_reverse_inverselookup)) /\ exists ff_q_pvs_reverse_inverselookupnegative. dst_negative_code_reverse_inverselookup = ff_q_pvs_reverse_inverselookupnegative * S ((S (dc_input_reverse_inverse)) * dst_negative_scale_reverse_inverselookup) + (dst_negative_reverse_inverselookup))) /\ (exists ge_balance_positive_reverse_inverselookupvalue ge_balance_negative_reverse_inverselookupvalue. (((((dc_output_reverse_inverse) = 2 * (ge_balance_positive_reverse_inverselookupvalue) /\ (ge_balance_negative_reverse_inverselookupvalue) = 0) \/ exists ge_signed_half_reverse_inverselookupvaluedecode. (((dc_output_reverse_inverse) = 2 * ge_signed_half_reverse_inverselookupvaluedecode + 1 /\ (ge_balance_positive_reverse_inverselookupvalue) = 0) /\ (ge_balance_negative_reverse_inverselookupvalue) = S ge_signed_half_reverse_inverselookupvaluedecode))) /\ ((dst_positive_reverse_inverselookup) + ge_balance_negative_reverse_inverselookupvalue = (dst_negative_reverse_inverselookup) + ge_balance_positive_reverse_inverselookupvalue))))))))) -> (((~((dc_input_reverse_inverse)=0)) /\ (exists dc_mask_reverse_inversevalue. ((((exists dst_positive_code_reverse_inversevaluemasktable dst_positive_scale_reverse_inversevaluemasktable dst_negative_code_reverse_inversevaluemasktable dst_negative_scale_reverse_inversevaluemasktable. (((dc_mask_reverse_inversevalue) = (((((dst_positive_code_reverse_inversevaluemasktable) + (dst_positive_scale_reverse_inversevaluemasktable)) * S ((dst_positive_code_reverse_inversevaluemasktable) + (dst_positive_scale_reverse_inversevaluemasktable)) + ((dst_positive_scale_reverse_inversevaluemasktable) + (dst_positive_scale_reverse_inversevaluemasktable))) + (((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) * S ((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) + ((dst_negative_scale_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)))) * S ((((dst_positive_code_reverse_inversevaluemasktable) + (dst_positive_scale_reverse_inversevaluemasktable)) * S ((dst_positive_code_reverse_inversevaluemasktable) + (dst_positive_scale_reverse_inversevaluemasktable)) + ((dst_positive_scale_reverse_inversevaluemasktable) + (dst_positive_scale_reverse_inversevaluemasktable))) + (((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) * S ((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) + ((dst_negative_scale_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)))) + ((((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) * S ((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) + ((dst_negative_scale_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable))) + (((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) * S ((dst_negative_code_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)) + ((dst_negative_scale_reverse_inversevaluemasktable) + (dst_negative_scale_reverse_inversevaluemasktable)))))) /\ (forall dst_index_reverse_inversevaluemasktable. (exists pvs_le_gap_reverse_inversevaluemasktabledomain. pvs_le_gap_reverse_inversevaluemasktabledomain + (dst_index_reverse_inversevaluemasktable) = (dc_input_reverse_inverse)) -> exists dst_positive_reverse_inversevaluemasktable dst_negative_reverse_inversevaluemasktable dst_value_reverse_inversevaluemasktable. ((((exists ff_h_pvs_reverse_inversevaluemasktableentrypositive. ff_h_pvs_reverse_inversevaluemasktableentrypositive + S (dst_positive_reverse_inversevaluemasktable) = S ((S (dst_index_reverse_inversevaluemasktable)) * dst_positive_scale_reverse_inversevaluemasktable)) /\ exists ff_q_pvs_reverse_inversevaluemasktableentrypositive. dst_positive_code_reverse_inversevaluemasktable = ff_q_pvs_reverse_inversevaluemasktableentrypositive * S ((S (dst_index_reverse_inversevaluemasktable)) * dst_positive_scale_reverse_inversevaluemasktable) + (dst_positive_reverse_inversevaluemasktable))) /\ (((((exists ff_h_pvs_reverse_inversevaluemasktableentrynegative. ff_h_pvs_reverse_inversevaluemasktableentrynegative + S (dst_negative_reverse_inversevaluemasktable) = S ((S (dst_index_reverse_inversevaluemasktable)) * dst_negative_scale_reverse_inversevaluemasktable)) /\ exists ff_q_pvs_reverse_inversevaluemasktableentrynegative. dst_negative_code_reverse_inversevaluemasktable = ff_q_pvs_reverse_inversevaluemasktableentrynegative * S ((S (dst_index_reverse_inversevaluemasktable)) * dst_negative_scale_reverse_inversevaluemasktable) + (dst_negative_reverse_inversevaluemasktable))) /\ (exists ge_balance_positive_reverse_inversevaluemasktableentryvalue ge_balance_negative_reverse_inversevaluemasktableentryvalue. (((((dst_value_reverse_inversevaluemasktable) = 2 * (ge_balance_positive_reverse_inversevaluemasktableentryvalue) /\ (ge_balance_negative_reverse_inversevaluemasktableentryvalue) = 0) \/ exists ge_signed_half_reverse_inversevaluemasktableentryvaluedecode. (((dst_value_reverse_inversevaluemasktable) = 2 * ge_signed_half_reverse_inversevaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_reverse_inversevaluemasktableentryvalue) = 0) /\ (ge_balance_negative_reverse_inversevaluemasktableentryvalue) = S ge_signed_half_reverse_inversevaluemasktableentryvaluedecode))) /\ ((dst_positive_reverse_inversevaluemasktable) + ge_balance_negative_reverse_inversevaluemasktableentryvalue = (dst_negative_reverse_inversevaluemasktable) + ge_balance_positive_reverse_inversevaluemasktableentryvalue))))))))) /\ (forall dc_index_reverse_inversevaluemask dc_value_reverse_inversevaluemask. (exists pvs_le_gap_reverse_inversevaluemaskdomain. pvs_le_gap_reverse_inversevaluemaskdomain + (dc_index_reverse_inversevaluemask) = (dc_input_reverse_inverse)) -> (exists dst_positive_code_reverse_inversevaluemasklookup dst_positive_scale_reverse_inversevaluemasklookup dst_negative_code_reverse_inversevaluemasklookup dst_negative_scale_reverse_inversevaluemasklookup dst_positive_reverse_inversevaluemasklookup dst_negative_reverse_inversevaluemasklookup. (((dc_mask_reverse_inversevalue) = (((((dst_positive_code_reverse_inversevaluemasklookup) + (dst_positive_scale_reverse_inversevaluemasklookup)) * S ((dst_positive_code_reverse_inversevaluemasklookup) + (dst_positive_scale_reverse_inversevaluemasklookup)) + ((dst_positive_scale_reverse_inversevaluemasklookup) + (dst_positive_scale_reverse_inversevaluemasklookup))) + (((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) * S ((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) + ((dst_negative_scale_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)))) * S ((((dst_positive_code_reverse_inversevaluemasklookup) + (dst_positive_scale_reverse_inversevaluemasklookup)) * S ((dst_positive_code_reverse_inversevaluemasklookup) + (dst_positive_scale_reverse_inversevaluemasklookup)) + ((dst_positive_scale_reverse_inversevaluemasklookup) + (dst_positive_scale_reverse_inversevaluemasklookup))) + (((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) * S ((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) + ((dst_negative_scale_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)))) + ((((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) * S ((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) + ((dst_negative_scale_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup))) + (((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) * S ((dst_negative_code_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)) + ((dst_negative_scale_reverse_inversevaluemasklookup) + (dst_negative_scale_reverse_inversevaluemasklookup)))))) /\ (((((exists ff_h_pvs_reverse_inversevaluemasklookuppositive. ff_h_pvs_reverse_inversevaluemasklookuppositive + S (dst_positive_reverse_inversevaluemasklookup) = S ((S (dc_index_reverse_inversevaluemask)) * dst_positive_scale_reverse_inversevaluemasklookup)) /\ exists ff_q_pvs_reverse_inversevaluemasklookuppositive. dst_positive_code_reverse_inversevaluemasklookup = ff_q_pvs_reverse_inversevaluemasklookuppositive * S ((S (dc_index_reverse_inversevaluemask)) * dst_positive_scale_reverse_inversevaluemasklookup) + (dst_positive_reverse_inversevaluemasklookup))) /\ (((((exists ff_h_pvs_reverse_inversevaluemasklookupnegative. ff_h_pvs_reverse_inversevaluemasklookupnegative + S (dst_negative_reverse_inversevaluemasklookup) = S ((S (dc_index_reverse_inversevaluemask)) * dst_negative_scale_reverse_inversevaluemasklookup)) /\ exists ff_q_pvs_reverse_inversevaluemasklookupnegative. dst_negative_code_reverse_inversevaluemasklookup = ff_q_pvs_reverse_inversevaluemasklookupnegative * S ((S (dc_index_reverse_inversevaluemask)) * dst_negative_scale_reverse_inversevaluemasklookup) + (dst_negative_reverse_inversevaluemasklookup))) /\ (exists ge_balance_positive_reverse_inversevaluemasklookupvalue ge_balance_negative_reverse_inversevaluemasklookupvalue. (((((dc_value_reverse_inversevaluemask) = 2 * (ge_balance_positive_reverse_inversevaluemasklookupvalue) /\ (ge_balance_negative_reverse_inversevaluemasklookupvalue) = 0) \/ exists ge_signed_half_reverse_inversevaluemasklookupvaluedecode. (((dc_value_reverse_inversevaluemask) = 2 * ge_signed_half_reverse_inversevaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_reverse_inversevaluemasklookupvalue) = 0) /\ (ge_balance_negative_reverse_inversevaluemasklookupvalue) = S ge_signed_half_reverse_inversevaluemasklookupvaluedecode))) /\ ((dst_positive_reverse_inversevaluemasklookup) + ge_balance_negative_reverse_inversevaluemasklookupvalue = (dst_negative_reverse_inversevaluemasklookup) + ge_balance_positive_reverse_inversevaluemasklookupvalue))))))))) -> ((((~((dc_index_reverse_inversevaluemask)=0)) /\ (exists dc_quotient_reverse_inversevaluemaskentry dc_left_reverse_inversevaluemaskentry dc_right_reverse_inversevaluemaskentry. (((dc_input_reverse_inverse)=(dc_index_reverse_inversevaluemask)*dc_quotient_reverse_inversevaluemaskentry) /\ (((exists dst_positive_code_reverse_inversevaluemaskentryleft dst_positive_scale_reverse_inversevaluemaskentryleft dst_negative_code_reverse_inversevaluemaskentryleft dst_negative_scale_reverse_inversevaluemaskentryleft dst_positive_reverse_inversevaluemaskentryleft dst_negative_reverse_inversevaluemaskentryleft. (((M) = (((((dst_positive_code_reverse_inversevaluemaskentryleft) + (dst_positive_scale_reverse_inversevaluemaskentryleft)) * S ((dst_positive_code_reverse_inversevaluemaskentryleft) + (dst_positive_scale_reverse_inversevaluemaskentryleft)) + ((dst_positive_scale_reverse_inversevaluemaskentryleft) + (dst_positive_scale_reverse_inversevaluemaskentryleft))) + (((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) * S ((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) + ((dst_negative_scale_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)))) * S ((((dst_positive_code_reverse_inversevaluemaskentryleft) + (dst_positive_scale_reverse_inversevaluemaskentryleft)) * S ((dst_positive_code_reverse_inversevaluemaskentryleft) + (dst_positive_scale_reverse_inversevaluemaskentryleft)) + ((dst_positive_scale_reverse_inversevaluemaskentryleft) + (dst_positive_scale_reverse_inversevaluemaskentryleft))) + (((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) * S ((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) + ((dst_negative_scale_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)))) + ((((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) * S ((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) + ((dst_negative_scale_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft))) + (((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) * S ((dst_negative_code_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)) + ((dst_negative_scale_reverse_inversevaluemaskentryleft) + (dst_negative_scale_reverse_inversevaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_reverse_inversevaluemaskentryleftpositive. ff_h_pvs_reverse_inversevaluemaskentryleftpositive + S (dst_positive_reverse_inversevaluemaskentryleft) = S ((S (dc_index_reverse_inversevaluemask)) * dst_positive_scale_reverse_inversevaluemaskentryleft)) /\ exists ff_q_pvs_reverse_inversevaluemaskentryleftpositive. dst_positive_code_reverse_inversevaluemaskentryleft = ff_q_pvs_reverse_inversevaluemaskentryleftpositive * S ((S (dc_index_reverse_inversevaluemask)) * dst_positive_scale_reverse_inversevaluemaskentryleft) + (dst_positive_reverse_inversevaluemaskentryleft))) /\ (((((exists ff_h_pvs_reverse_inversevaluemaskentryleftnegative. ff_h_pvs_reverse_inversevaluemaskentryleftnegative + S (dst_negative_reverse_inversevaluemaskentryleft) = S ((S (dc_index_reverse_inversevaluemask)) * dst_negative_scale_reverse_inversevaluemaskentryleft)) /\ exists ff_q_pvs_reverse_inversevaluemaskentryleftnegative. dst_negative_code_reverse_inversevaluemaskentryleft = ff_q_pvs_reverse_inversevaluemaskentryleftnegative * S ((S (dc_index_reverse_inversevaluemask)) * dst_negative_scale_reverse_inversevaluemaskentryleft) + (dst_negative_reverse_inversevaluemaskentryleft))) /\ (exists ge_balance_positive_reverse_inversevaluemaskentryleftvalue ge_balance_negative_reverse_inversevaluemaskentryleftvalue. (((((dc_left_reverse_inversevaluemaskentry) = 2 * (ge_balance_positive_reverse_inversevaluemaskentryleftvalue) /\ (ge_balance_negative_reverse_inversevaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_reverse_inversevaluemaskentryleftvaluedecode. (((dc_left_reverse_inversevaluemaskentry) = 2 * ge_signed_half_reverse_inversevaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_reverse_inversevaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_reverse_inversevaluemaskentryleftvalue) = S ge_signed_half_reverse_inversevaluemaskentryleftvaluedecode))) /\ ((dst_positive_reverse_inversevaluemaskentryleft) + ge_balance_negative_reverse_inversevaluemaskentryleftvalue = (dst_negative_reverse_inversevaluemaskentryleft) + ge_balance_positive_reverse_inversevaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_reverse_inversevaluemaskentryright dst_positive_scale_reverse_inversevaluemaskentryright dst_negative_code_reverse_inversevaluemaskentryright dst_negative_scale_reverse_inversevaluemaskentryright dst_positive_reverse_inversevaluemaskentryright dst_negative_reverse_inversevaluemaskentryright. (((G) = (((((dst_positive_code_reverse_inversevaluemaskentryright) + (dst_positive_scale_reverse_inversevaluemaskentryright)) * S ((dst_positive_code_reverse_inversevaluemaskentryright) + (dst_positive_scale_reverse_inversevaluemaskentryright)) + ((dst_positive_scale_reverse_inversevaluemaskentryright) + (dst_positive_scale_reverse_inversevaluemaskentryright))) + (((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) * S ((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) + ((dst_negative_scale_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)))) * S ((((dst_positive_code_reverse_inversevaluemaskentryright) + (dst_positive_scale_reverse_inversevaluemaskentryright)) * S ((dst_positive_code_reverse_inversevaluemaskentryright) + (dst_positive_scale_reverse_inversevaluemaskentryright)) + ((dst_positive_scale_reverse_inversevaluemaskentryright) + (dst_positive_scale_reverse_inversevaluemaskentryright))) + (((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) * S ((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) + ((dst_negative_scale_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)))) + ((((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) * S ((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) + ((dst_negative_scale_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright))) + (((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) * S ((dst_negative_code_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)) + ((dst_negative_scale_reverse_inversevaluemaskentryright) + (dst_negative_scale_reverse_inversevaluemaskentryright)))))) /\ (((((exists ff_h_pvs_reverse_inversevaluemaskentryrightpositive. ff_h_pvs_reverse_inversevaluemaskentryrightpositive + S (dst_positive_reverse_inversevaluemaskentryright) = S ((S (dc_quotient_reverse_inversevaluemaskentry)) * dst_positive_scale_reverse_inversevaluemaskentryright)) /\ exists ff_q_pvs_reverse_inversevaluemaskentryrightpositive. dst_positive_code_reverse_inversevaluemaskentryright = ff_q_pvs_reverse_inversevaluemaskentryrightpositive * S ((S (dc_quotient_reverse_inversevaluemaskentry)) * dst_positive_scale_reverse_inversevaluemaskentryright) + (dst_positive_reverse_inversevaluemaskentryright))) /\ (((((exists ff_h_pvs_reverse_inversevaluemaskentryrightnegative. ff_h_pvs_reverse_inversevaluemaskentryrightnegative + S (dst_negative_reverse_inversevaluemaskentryright) = S ((S (dc_quotient_reverse_inversevaluemaskentry)) * dst_negative_scale_reverse_inversevaluemaskentryright)) /\ exists ff_q_pvs_reverse_inversevaluemaskentryrightnegative. dst_negative_code_reverse_inversevaluemaskentryright = ff_q_pvs_reverse_inversevaluemaskentryrightnegative * S ((S (dc_quotient_reverse_inversevaluemaskentry)) * dst_negative_scale_reverse_inversevaluemaskentryright) + (dst_negative_reverse_inversevaluemaskentryright))) /\ (exists ge_balance_positive_reverse_inversevaluemaskentryrightvalue ge_balance_negative_reverse_inversevaluemaskentryrightvalue. (((((dc_right_reverse_inversevaluemaskentry) = 2 * (ge_balance_positive_reverse_inversevaluemaskentryrightvalue) /\ (ge_balance_negative_reverse_inversevaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_reverse_inversevaluemaskentryrightvaluedecode. (((dc_right_reverse_inversevaluemaskentry) = 2 * ge_signed_half_reverse_inversevaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_reverse_inversevaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_reverse_inversevaluemaskentryrightvalue) = S ge_signed_half_reverse_inversevaluemaskentryrightvaluedecode))) /\ ((dst_positive_reverse_inversevaluemaskentryright) + ge_balance_negative_reverse_inversevaluemaskentryrightvalue = (dst_negative_reverse_inversevaluemaskentryright) + ge_balance_positive_reverse_inversevaluemaskentryrightvalue))))))))) /\ (exists sto_ap_reverse_inversevaluemaskentryproduct sto_an_reverse_inversevaluemaskentryproduct sto_bp_reverse_inversevaluemaskentryproduct sto_bn_reverse_inversevaluemaskentryproduct sto_cp_reverse_inversevaluemaskentryproduct sto_cn_reverse_inversevaluemaskentryproduct. (((((dc_left_reverse_inversevaluemaskentry) = 2 * (sto_ap_reverse_inversevaluemaskentryproduct) /\ (sto_an_reverse_inversevaluemaskentryproduct) = 0) \/ exists ge_signed_half_reverse_inversevaluemaskentryproductleft. (((dc_left_reverse_inversevaluemaskentry) = 2 * ge_signed_half_reverse_inversevaluemaskentryproductleft + 1 /\ (sto_ap_reverse_inversevaluemaskentryproduct) = 0) /\ (sto_an_reverse_inversevaluemaskentryproduct) = S ge_signed_half_reverse_inversevaluemaskentryproductleft))) /\ ((((((dc_right_reverse_inversevaluemaskentry) = 2 * (sto_bp_reverse_inversevaluemaskentryproduct) /\ (sto_bn_reverse_inversevaluemaskentryproduct) = 0) \/ exists ge_signed_half_reverse_inversevaluemaskentryproductright. (((dc_right_reverse_inversevaluemaskentry) = 2 * ge_signed_half_reverse_inversevaluemaskentryproductright + 1 /\ (sto_bp_reverse_inversevaluemaskentryproduct) = 0) /\ (sto_bn_reverse_inversevaluemaskentryproduct) = S ge_signed_half_reverse_inversevaluemaskentryproductright))) /\ ((((((dc_value_reverse_inversevaluemask) = 2 * (sto_cp_reverse_inversevaluemaskentryproduct) /\ (sto_cn_reverse_inversevaluemaskentryproduct) = 0) \/ exists ge_signed_half_reverse_inversevaluemaskentryproductoutput. (((dc_value_reverse_inversevaluemask) = 2 * ge_signed_half_reverse_inversevaluemaskentryproductoutput + 1 /\ (sto_cp_reverse_inversevaluemaskentryproduct) = 0) /\ (sto_cn_reverse_inversevaluemaskentryproduct) = S ge_signed_half_reverse_inversevaluemaskentryproductoutput))) /\ ((sto_ap_reverse_inversevaluemaskentryproduct * sto_bp_reverse_inversevaluemaskentryproduct + sto_an_reverse_inversevaluemaskentryproduct * sto_bn_reverse_inversevaluemaskentryproduct) + sto_cn_reverse_inversevaluemaskentryproduct = (sto_ap_reverse_inversevaluemaskentryproduct * sto_bn_reverse_inversevaluemaskentryproduct + sto_an_reverse_inversevaluemaskentryproduct * sto_bp_reverse_inversevaluemaskentryproduct) + sto_cp_reverse_inversevaluemaskentryproduct))))))))))))))) \/ ((((dc_index_reverse_inversevaluemask)=0 \/ ~(exists pvs_factor_reverse_inversevaluemaskentrynondivisor. (dc_input_reverse_inverse) = (dc_index_reverse_inversevaluemask) * pvs_factor_reverse_inversevaluemaskentrynondivisor)) /\ ((dc_value_reverse_inversevaluemask)=0))))))) /\ (exists dst_positive_code_reverse_inversevaluefold dst_positive_scale_reverse_inversevaluefold dst_negative_code_reverse_inversevaluefold dst_negative_scale_reverse_inversevaluefold dst_positive_sum_reverse_inversevaluefold dst_negative_sum_reverse_inversevaluefold. (((dc_mask_reverse_inversevalue) = (((((dst_positive_code_reverse_inversevaluefold) + (dst_positive_scale_reverse_inversevaluefold)) * S ((dst_positive_code_reverse_inversevaluefold) + (dst_positive_scale_reverse_inversevaluefold)) + ((dst_positive_scale_reverse_inversevaluefold) + (dst_positive_scale_reverse_inversevaluefold))) + (((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) * S ((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) + ((dst_negative_scale_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)))) * S ((((dst_positive_code_reverse_inversevaluefold) + (dst_positive_scale_reverse_inversevaluefold)) * S ((dst_positive_code_reverse_inversevaluefold) + (dst_positive_scale_reverse_inversevaluefold)) + ((dst_positive_scale_reverse_inversevaluefold) + (dst_positive_scale_reverse_inversevaluefold))) + (((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) * S ((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) + ((dst_negative_scale_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)))) + ((((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) * S ((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) + ((dst_negative_scale_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold))) + (((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) * S ((dst_negative_code_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)) + ((dst_negative_scale_reverse_inversevaluefold) + (dst_negative_scale_reverse_inversevaluefold)))))) /\ (((exists fs_u_dst_reverse_inversevaluefoldpositive fs_v_dst_reverse_inversevaluefoldpositive. ((((exists fs_h_dst_reverse_inversevaluefoldpositive_body_start. fs_h_dst_reverse_inversevaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_reverse_inversevaluefoldpositive)) /\ exists fs_q_dst_reverse_inversevaluefoldpositive_body_start. fs_u_dst_reverse_inversevaluefoldpositive = fs_q_dst_reverse_inversevaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_reverse_inversevaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_reverse_inversevaluefoldpositive_body_terminal. fs_h_dst_reverse_inversevaluefoldpositive_body_terminal + S (dst_positive_sum_reverse_inversevaluefold) = S ((S (S (dc_input_reverse_inverse))) * fs_v_dst_reverse_inversevaluefoldpositive)) /\ exists fs_q_dst_reverse_inversevaluefoldpositive_body_terminal. fs_u_dst_reverse_inversevaluefoldpositive = fs_q_dst_reverse_inversevaluefoldpositive_body_terminal * S ((S (S (dc_input_reverse_inverse))) * fs_v_dst_reverse_inversevaluefoldpositive) + (dst_positive_sum_reverse_inversevaluefold))) /\ forall fs_i_dst_reverse_inversevaluefoldpositive_body_steps. (exists fs_lt_dst_reverse_inversevaluefoldpositive_body_steps_bound. fs_lt_dst_reverse_inversevaluefoldpositive_body_steps_bound + S fs_i_dst_reverse_inversevaluefoldpositive_body_steps = S (dc_input_reverse_inverse)) -> exists fs_a_dst_reverse_inversevaluefoldpositive_body_steps fs_r_dst_reverse_inversevaluefoldpositive_body_steps fs_s_dst_reverse_inversevaluefoldpositive_body_steps. ((((exists fs_h_dst_reverse_inversevaluefoldpositive_body_steps_summand. fs_h_dst_reverse_inversevaluefoldpositive_body_steps_summand + S (fs_a_dst_reverse_inversevaluefoldpositive_body_steps) = S ((S (fs_i_dst_reverse_inversevaluefoldpositive_body_steps)) * dst_positive_scale_reverse_inversevaluefold)) /\ exists fs_q_dst_reverse_inversevaluefoldpositive_body_steps_summand. dst_positive_code_reverse_inversevaluefold = fs_q_dst_reverse_inversevaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_reverse_inversevaluefoldpositive_body_steps)) * dst_positive_scale_reverse_inversevaluefold) + (fs_a_dst_reverse_inversevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_reverse_inversevaluefoldpositive_body_steps_partial. fs_h_dst_reverse_inversevaluefoldpositive_body_steps_partial + S (fs_r_dst_reverse_inversevaluefoldpositive_body_steps) = S ((S (fs_i_dst_reverse_inversevaluefoldpositive_body_steps)) * fs_v_dst_reverse_inversevaluefoldpositive)) /\ exists fs_q_dst_reverse_inversevaluefoldpositive_body_steps_partial. fs_u_dst_reverse_inversevaluefoldpositive = fs_q_dst_reverse_inversevaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_reverse_inversevaluefoldpositive_body_steps)) * fs_v_dst_reverse_inversevaluefoldpositive) + (fs_r_dst_reverse_inversevaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_reverse_inversevaluefoldpositive_body_steps_successor. fs_h_dst_reverse_inversevaluefoldpositive_body_steps_successor + S (fs_s_dst_reverse_inversevaluefoldpositive_body_steps) = S ((S (S fs_i_dst_reverse_inversevaluefoldpositive_body_steps)) * fs_v_dst_reverse_inversevaluefoldpositive)) /\ exists fs_q_dst_reverse_inversevaluefoldpositive_body_steps_successor. fs_u_dst_reverse_inversevaluefoldpositive = fs_q_dst_reverse_inversevaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_reverse_inversevaluefoldpositive_body_steps)) * fs_v_dst_reverse_inversevaluefoldpositive) + (fs_s_dst_reverse_inversevaluefoldpositive_body_steps))) /\ fs_s_dst_reverse_inversevaluefoldpositive_body_steps = fs_r_dst_reverse_inversevaluefoldpositive_body_steps + fs_a_dst_reverse_inversevaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_reverse_inversevaluefoldnegative fs_v_dst_reverse_inversevaluefoldnegative. ((((exists fs_h_dst_reverse_inversevaluefoldnegative_body_start. fs_h_dst_reverse_inversevaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_reverse_inversevaluefoldnegative)) /\ exists fs_q_dst_reverse_inversevaluefoldnegative_body_start. fs_u_dst_reverse_inversevaluefoldnegative = fs_q_dst_reverse_inversevaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_reverse_inversevaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_reverse_inversevaluefoldnegative_body_terminal. fs_h_dst_reverse_inversevaluefoldnegative_body_terminal + S (dst_negative_sum_reverse_inversevaluefold) = S ((S (S (dc_input_reverse_inverse))) * fs_v_dst_reverse_inversevaluefoldnegative)) /\ exists fs_q_dst_reverse_inversevaluefoldnegative_body_terminal. fs_u_dst_reverse_inversevaluefoldnegative = fs_q_dst_reverse_inversevaluefoldnegative_body_terminal * S ((S (S (dc_input_reverse_inverse))) * fs_v_dst_reverse_inversevaluefoldnegative) + (dst_negative_sum_reverse_inversevaluefold))) /\ forall fs_i_dst_reverse_inversevaluefoldnegative_body_steps. (exists fs_lt_dst_reverse_inversevaluefoldnegative_body_steps_bound. fs_lt_dst_reverse_inversevaluefoldnegative_body_steps_bound + S fs_i_dst_reverse_inversevaluefoldnegative_body_steps = S (dc_input_reverse_inverse)) -> exists fs_a_dst_reverse_inversevaluefoldnegative_body_steps fs_r_dst_reverse_inversevaluefoldnegative_body_steps fs_s_dst_reverse_inversevaluefoldnegative_body_steps. ((((exists fs_h_dst_reverse_inversevaluefoldnegative_body_steps_summand. fs_h_dst_reverse_inversevaluefoldnegative_body_steps_summand + S (fs_a_dst_reverse_inversevaluefoldnegative_body_steps) = S ((S (fs_i_dst_reverse_inversevaluefoldnegative_body_steps)) * dst_negative_scale_reverse_inversevaluefold)) /\ exists fs_q_dst_reverse_inversevaluefoldnegative_body_steps_summand. dst_negative_code_reverse_inversevaluefold = fs_q_dst_reverse_inversevaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_reverse_inversevaluefoldnegative_body_steps)) * dst_negative_scale_reverse_inversevaluefold) + (fs_a_dst_reverse_inversevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_reverse_inversevaluefoldnegative_body_steps_partial. fs_h_dst_reverse_inversevaluefoldnegative_body_steps_partial + S (fs_r_dst_reverse_inversevaluefoldnegative_body_steps) = S ((S (fs_i_dst_reverse_inversevaluefoldnegative_body_steps)) * fs_v_dst_reverse_inversevaluefoldnegative)) /\ exists fs_q_dst_reverse_inversevaluefoldnegative_body_steps_partial. fs_u_dst_reverse_inversevaluefoldnegative = fs_q_dst_reverse_inversevaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_reverse_inversevaluefoldnegative_body_steps)) * fs_v_dst_reverse_inversevaluefoldnegative) + (fs_r_dst_reverse_inversevaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_reverse_inversevaluefoldnegative_body_steps_successor. fs_h_dst_reverse_inversevaluefoldnegative_body_steps_successor + S (fs_s_dst_reverse_inversevaluefoldnegative_body_steps) = S ((S (S fs_i_dst_reverse_inversevaluefoldnegative_body_steps)) * fs_v_dst_reverse_inversevaluefoldnegative)) /\ exists fs_q_dst_reverse_inversevaluefoldnegative_body_steps_successor. fs_u_dst_reverse_inversevaluefoldnegative = fs_q_dst_reverse_inversevaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_reverse_inversevaluefoldnegative_body_steps)) * fs_v_dst_reverse_inversevaluefoldnegative) + (fs_s_dst_reverse_inversevaluefoldnegative_body_steps))) /\ fs_s_dst_reverse_inversevaluefoldnegative_body_steps = fs_r_dst_reverse_inversevaluefoldnegative_body_steps + fs_a_dst_reverse_inversevaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_reverse_inversevaluefoldresult ge_balance_negative_reverse_inversevaluefoldresult. (((((dc_output_reverse_inverse) = 2 * (ge_balance_positive_reverse_inversevaluefoldresult) /\ (ge_balance_negative_reverse_inversevaluefoldresult) = 0) \/ exists ge_signed_half_reverse_inversevaluefoldresultdecode. (((dc_output_reverse_inverse) = 2 * ge_signed_half_reverse_inversevaluefoldresultdecode + 1 /\ (ge_balance_positive_reverse_inversevaluefoldresult) = 0) /\ (ge_balance_negative_reverse_inversevaluefoldresult) = S ge_signed_half_reverse_inversevaluefoldresultdecode))) /\ ((dst_positive_sum_reverse_inversevaluefold) + ge_balance_negative_reverse_inversevaluefoldresult = (dst_negative_sum_reverse_inversevaluefold) + ge_balance_positive_reverse_inversevaluefoldresult)))))))))))))))))))) -> (forall mi_index_reverse_result mi_value_reverse_result. ~(mi_index_reverse_result=0) -> (exists pvs_le_gap_reverse_resultbound. pvs_le_gap_reverse_resultbound + (mi_index_reverse_result) = (N)) -> (exists dst_positive_code_reverse_resultentry dst_positive_scale_reverse_resultentry dst_negative_code_reverse_resultentry dst_negative_scale_reverse_resultentry dst_positive_reverse_resultentry dst_negative_reverse_resultentry. (((G) = (((((dst_positive_code_reverse_resultentry) + (dst_positive_scale_reverse_resultentry)) * S ((dst_positive_code_reverse_resultentry) + (dst_positive_scale_reverse_resultentry)) + ((dst_positive_scale_reverse_resultentry) + (dst_positive_scale_reverse_resultentry))) + (((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) * S ((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) + ((dst_negative_scale_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)))) * S ((((dst_positive_code_reverse_resultentry) + (dst_positive_scale_reverse_resultentry)) * S ((dst_positive_code_reverse_resultentry) + (dst_positive_scale_reverse_resultentry)) + ((dst_positive_scale_reverse_resultentry) + (dst_positive_scale_reverse_resultentry))) + (((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) * S ((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) + ((dst_negative_scale_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)))) + ((((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) * S ((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) + ((dst_negative_scale_reverse_resultentry) + (dst_negative_scale_reverse_resultentry))) + (((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) * S ((dst_negative_code_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)) + ((dst_negative_scale_reverse_resultentry) + (dst_negative_scale_reverse_resultentry)))))) /\ (((((exists ff_h_pvs_reverse_resultentrypositive. ff_h_pvs_reverse_resultentrypositive + S (dst_positive_reverse_resultentry) = S ((S (mi_index_reverse_result)) * dst_positive_scale_reverse_resultentry)) /\ exists ff_q_pvs_reverse_resultentrypositive. dst_positive_code_reverse_resultentry = ff_q_pvs_reverse_resultentrypositive * S ((S (mi_index_reverse_result)) * dst_positive_scale_reverse_resultentry) + (dst_positive_reverse_resultentry))) /\ (((((exists ff_h_pvs_reverse_resultentrynegative. ff_h_pvs_reverse_resultentrynegative + S (dst_negative_reverse_resultentry) = S ((S (mi_index_reverse_result)) * dst_negative_scale_reverse_resultentry)) /\ exists ff_q_pvs_reverse_resultentrynegative. dst_negative_code_reverse_resultentry = ff_q_pvs_reverse_resultentrynegative * S ((S (mi_index_reverse_result)) * dst_negative_scale_reverse_resultentry) + (dst_negative_reverse_resultentry))) /\ (exists ge_balance_positive_reverse_resultentryvalue ge_balance_negative_reverse_resultentryvalue. (((((mi_value_reverse_result) = 2 * (ge_balance_positive_reverse_resultentryvalue) /\ (ge_balance_negative_reverse_resultentryvalue) = 0) \/ exists ge_signed_half_reverse_resultentryvaluedecode. (((mi_value_reverse_result) = 2 * ge_signed_half_reverse_resultentryvaluedecode + 1 /\ (ge_balance_positive_reverse_resultentryvalue) = 0) /\ (ge_balance_negative_reverse_resultentryvalue) = S ge_signed_half_reverse_resultentryvaluedecode))) /\ ((dst_positive_reverse_resultentry) + ge_balance_negative_reverse_resultentryvalue = (dst_negative_reverse_resultentry) + ge_balance_positive_reverse_resultentryvalue))))))))) -> (((~((mi_index_reverse_result)=0)) /\ (exists dm_mask_table_reverse_resultsum. ((((exists dst_positive_code_reverse_resultsummasktable dst_positive_scale_reverse_resultsummasktable dst_negative_code_reverse_resultsummasktable dst_negative_scale_reverse_resultsummasktable. (((dm_mask_table_reverse_resultsum) = (((((dst_positive_code_reverse_resultsummasktable) + (dst_positive_scale_reverse_resultsummasktable)) * S ((dst_positive_code_reverse_resultsummasktable) + (dst_positive_scale_reverse_resultsummasktable)) + ((dst_positive_scale_reverse_resultsummasktable) + (dst_positive_scale_reverse_resultsummasktable))) + (((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) * S ((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) + ((dst_negative_scale_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)))) * S ((((dst_positive_code_reverse_resultsummasktable) + (dst_positive_scale_reverse_resultsummasktable)) * S ((dst_positive_code_reverse_resultsummasktable) + (dst_positive_scale_reverse_resultsummasktable)) + ((dst_positive_scale_reverse_resultsummasktable) + (dst_positive_scale_reverse_resultsummasktable))) + (((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) * S ((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) + ((dst_negative_scale_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)))) + ((((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) * S ((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) + ((dst_negative_scale_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable))) + (((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) * S ((dst_negative_code_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)) + ((dst_negative_scale_reverse_resultsummasktable) + (dst_negative_scale_reverse_resultsummasktable)))))) /\ (forall dst_index_reverse_resultsummasktable. (exists pvs_le_gap_reverse_resultsummasktabledomain. pvs_le_gap_reverse_resultsummasktabledomain + (dst_index_reverse_resultsummasktable) = (mi_index_reverse_result)) -> exists dst_positive_reverse_resultsummasktable dst_negative_reverse_resultsummasktable dst_value_reverse_resultsummasktable. ((((exists ff_h_pvs_reverse_resultsummasktableentrypositive. ff_h_pvs_reverse_resultsummasktableentrypositive + S (dst_positive_reverse_resultsummasktable) = S ((S (dst_index_reverse_resultsummasktable)) * dst_positive_scale_reverse_resultsummasktable)) /\ exists ff_q_pvs_reverse_resultsummasktableentrypositive. dst_positive_code_reverse_resultsummasktable = ff_q_pvs_reverse_resultsummasktableentrypositive * S ((S (dst_index_reverse_resultsummasktable)) * dst_positive_scale_reverse_resultsummasktable) + (dst_positive_reverse_resultsummasktable))) /\ (((((exists ff_h_pvs_reverse_resultsummasktableentrynegative. ff_h_pvs_reverse_resultsummasktableentrynegative + S (dst_negative_reverse_resultsummasktable) = S ((S (dst_index_reverse_resultsummasktable)) * dst_negative_scale_reverse_resultsummasktable)) /\ exists ff_q_pvs_reverse_resultsummasktableentrynegative. dst_negative_code_reverse_resultsummasktable = ff_q_pvs_reverse_resultsummasktableentrynegative * S ((S (dst_index_reverse_resultsummasktable)) * dst_negative_scale_reverse_resultsummasktable) + (dst_negative_reverse_resultsummasktable))) /\ (exists ge_balance_positive_reverse_resultsummasktableentryvalue ge_balance_negative_reverse_resultsummasktableentryvalue. (((((dst_value_reverse_resultsummasktable) = 2 * (ge_balance_positive_reverse_resultsummasktableentryvalue) /\ (ge_balance_negative_reverse_resultsummasktableentryvalue) = 0) \/ exists ge_signed_half_reverse_resultsummasktableentryvaluedecode. (((dst_value_reverse_resultsummasktable) = 2 * ge_signed_half_reverse_resultsummasktableentryvaluedecode + 1 /\ (ge_balance_positive_reverse_resultsummasktableentryvalue) = 0) /\ (ge_balance_negative_reverse_resultsummasktableentryvalue) = S ge_signed_half_reverse_resultsummasktableentryvaluedecode))) /\ ((dst_positive_reverse_resultsummasktable) + ge_balance_negative_reverse_resultsummasktableentryvalue = (dst_negative_reverse_resultsummasktable) + ge_balance_positive_reverse_resultsummasktableentryvalue))))))))) /\ (forall dm_index_reverse_resultsummask dm_value_reverse_resultsummask. (exists pvs_le_gap_reverse_resultsummaskdomain. pvs_le_gap_reverse_resultsummaskdomain + (dm_index_reverse_resultsummask) = (mi_index_reverse_result)) -> (exists dst_positive_code_reverse_resultsummasklookup dst_positive_scale_reverse_resultsummasklookup dst_negative_code_reverse_resultsummasklookup dst_negative_scale_reverse_resultsummasklookup dst_positive_reverse_resultsummasklookup dst_negative_reverse_resultsummasklookup. (((dm_mask_table_reverse_resultsum) = (((((dst_positive_code_reverse_resultsummasklookup) + (dst_positive_scale_reverse_resultsummasklookup)) * S ((dst_positive_code_reverse_resultsummasklookup) + (dst_positive_scale_reverse_resultsummasklookup)) + ((dst_positive_scale_reverse_resultsummasklookup) + (dst_positive_scale_reverse_resultsummasklookup))) + (((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) * S ((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) + ((dst_negative_scale_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)))) * S ((((dst_positive_code_reverse_resultsummasklookup) + (dst_positive_scale_reverse_resultsummasklookup)) * S ((dst_positive_code_reverse_resultsummasklookup) + (dst_positive_scale_reverse_resultsummasklookup)) + ((dst_positive_scale_reverse_resultsummasklookup) + (dst_positive_scale_reverse_resultsummasklookup))) + (((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) * S ((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) + ((dst_negative_scale_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)))) + ((((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) * S ((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) + ((dst_negative_scale_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup))) + (((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) * S ((dst_negative_code_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)) + ((dst_negative_scale_reverse_resultsummasklookup) + (dst_negative_scale_reverse_resultsummasklookup)))))) /\ (((((exists ff_h_pvs_reverse_resultsummasklookuppositive. ff_h_pvs_reverse_resultsummasklookuppositive + S (dst_positive_reverse_resultsummasklookup) = S ((S (dm_index_reverse_resultsummask)) * dst_positive_scale_reverse_resultsummasklookup)) /\ exists ff_q_pvs_reverse_resultsummasklookuppositive. dst_positive_code_reverse_resultsummasklookup = ff_q_pvs_reverse_resultsummasklookuppositive * S ((S (dm_index_reverse_resultsummask)) * dst_positive_scale_reverse_resultsummasklookup) + (dst_positive_reverse_resultsummasklookup))) /\ (((((exists ff_h_pvs_reverse_resultsummasklookupnegative. ff_h_pvs_reverse_resultsummasklookupnegative + S (dst_negative_reverse_resultsummasklookup) = S ((S (dm_index_reverse_resultsummask)) * dst_negative_scale_reverse_resultsummasklookup)) /\ exists ff_q_pvs_reverse_resultsummasklookupnegative. dst_negative_code_reverse_resultsummasklookup = ff_q_pvs_reverse_resultsummasklookupnegative * S ((S (dm_index_reverse_resultsummask)) * dst_negative_scale_reverse_resultsummasklookup) + (dst_negative_reverse_resultsummasklookup))) /\ (exists ge_balance_positive_reverse_resultsummasklookupvalue ge_balance_negative_reverse_resultsummasklookupvalue. (((((dm_value_reverse_resultsummask) = 2 * (ge_balance_positive_reverse_resultsummasklookupvalue) /\ (ge_balance_negative_reverse_resultsummasklookupvalue) = 0) \/ exists ge_signed_half_reverse_resultsummasklookupvaluedecode. (((dm_value_reverse_resultsummask) = 2 * ge_signed_half_reverse_resultsummasklookupvaluedecode + 1 /\ (ge_balance_positive_reverse_resultsummasklookupvalue) = 0) /\ (ge_balance_negative_reverse_resultsummasklookupvalue) = S ge_signed_half_reverse_resultsummasklookupvaluedecode))) /\ ((dst_positive_reverse_resultsummasklookup) + ge_balance_negative_reverse_resultsummasklookupvalue = (dst_negative_reverse_resultsummasklookup) + ge_balance_positive_reverse_resultsummasklookupvalue))))))))) -> ((((~((dm_index_reverse_resultsummask)=0)) /\ (exists dm_quotient_reverse_resultsummaskentry. (((mi_index_reverse_result)=(dm_index_reverse_resultsummask)*dm_quotient_reverse_resultsummaskentry) /\ (exists dst_positive_code_reverse_resultsummaskentryinput dst_positive_scale_reverse_resultsummaskentryinput dst_negative_code_reverse_resultsummaskentryinput dst_negative_scale_reverse_resultsummaskentryinput dst_positive_reverse_resultsummaskentryinput dst_negative_reverse_resultsummaskentryinput. (((F) = (((((dst_positive_code_reverse_resultsummaskentryinput) + (dst_positive_scale_reverse_resultsummaskentryinput)) * S ((dst_positive_code_reverse_resultsummaskentryinput) + (dst_positive_scale_reverse_resultsummaskentryinput)) + ((dst_positive_scale_reverse_resultsummaskentryinput) + (dst_positive_scale_reverse_resultsummaskentryinput))) + (((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) * S ((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) + ((dst_negative_scale_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)))) * S ((((dst_positive_code_reverse_resultsummaskentryinput) + (dst_positive_scale_reverse_resultsummaskentryinput)) * S ((dst_positive_code_reverse_resultsummaskentryinput) + (dst_positive_scale_reverse_resultsummaskentryinput)) + ((dst_positive_scale_reverse_resultsummaskentryinput) + (dst_positive_scale_reverse_resultsummaskentryinput))) + (((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) * S ((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) + ((dst_negative_scale_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)))) + ((((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) * S ((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) + ((dst_negative_scale_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput))) + (((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) * S ((dst_negative_code_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)) + ((dst_negative_scale_reverse_resultsummaskentryinput) + (dst_negative_scale_reverse_resultsummaskentryinput)))))) /\ (((((exists ff_h_pvs_reverse_resultsummaskentryinputpositive. ff_h_pvs_reverse_resultsummaskentryinputpositive + S (dst_positive_reverse_resultsummaskentryinput) = S ((S (dm_index_reverse_resultsummask)) * dst_positive_scale_reverse_resultsummaskentryinput)) /\ exists ff_q_pvs_reverse_resultsummaskentryinputpositive. dst_positive_code_reverse_resultsummaskentryinput = ff_q_pvs_reverse_resultsummaskentryinputpositive * S ((S (dm_index_reverse_resultsummask)) * dst_positive_scale_reverse_resultsummaskentryinput) + (dst_positive_reverse_resultsummaskentryinput))) /\ (((((exists ff_h_pvs_reverse_resultsummaskentryinputnegative. ff_h_pvs_reverse_resultsummaskentryinputnegative + S (dst_negative_reverse_resultsummaskentryinput) = S ((S (dm_index_reverse_resultsummask)) * dst_negative_scale_reverse_resultsummaskentryinput)) /\ exists ff_q_pvs_reverse_resultsummaskentryinputnegative. dst_negative_code_reverse_resultsummaskentryinput = ff_q_pvs_reverse_resultsummaskentryinputnegative * S ((S (dm_index_reverse_resultsummask)) * dst_negative_scale_reverse_resultsummaskentryinput) + (dst_negative_reverse_resultsummaskentryinput))) /\ (exists ge_balance_positive_reverse_resultsummaskentryinputvalue ge_balance_negative_reverse_resultsummaskentryinputvalue. (((((dm_value_reverse_resultsummask) = 2 * (ge_balance_positive_reverse_resultsummaskentryinputvalue) /\ (ge_balance_negative_reverse_resultsummaskentryinputvalue) = 0) \/ exists ge_signed_half_reverse_resultsummaskentryinputvaluedecode. (((dm_value_reverse_resultsummask) = 2 * ge_signed_half_reverse_resultsummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_reverse_resultsummaskentryinputvalue) = 0) /\ (ge_balance_negative_reverse_resultsummaskentryinputvalue) = S ge_signed_half_reverse_resultsummaskentryinputvaluedecode))) /\ ((dst_positive_reverse_resultsummaskentryinput) + ge_balance_negative_reverse_resultsummaskentryinputvalue = (dst_negative_reverse_resultsummaskentryinput) + ge_balance_positive_reverse_resultsummaskentryinputvalue))))))))))))) \/ ((((dm_index_reverse_resultsummask)=0 \/ ~(exists pvs_factor_reverse_resultsummaskentrynondivisor. (mi_index_reverse_result) = (dm_index_reverse_resultsummask) * pvs_factor_reverse_resultsummaskentrynondivisor)) /\ ((dm_value_reverse_resultsummask)=0))))))) /\ (exists dst_positive_code_reverse_resultsumfold dst_positive_scale_reverse_resultsumfold dst_negative_code_reverse_resultsumfold dst_negative_scale_reverse_resultsumfold dst_positive_sum_reverse_resultsumfold dst_negative_sum_reverse_resultsumfold. (((dm_mask_table_reverse_resultsum) = (((((dst_positive_code_reverse_resultsumfold) + (dst_positive_scale_reverse_resultsumfold)) * S ((dst_positive_code_reverse_resultsumfold) + (dst_positive_scale_reverse_resultsumfold)) + ((dst_positive_scale_reverse_resultsumfold) + (dst_positive_scale_reverse_resultsumfold))) + (((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) * S ((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) + ((dst_negative_scale_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)))) * S ((((dst_positive_code_reverse_resultsumfold) + (dst_positive_scale_reverse_resultsumfold)) * S ((dst_positive_code_reverse_resultsumfold) + (dst_positive_scale_reverse_resultsumfold)) + ((dst_positive_scale_reverse_resultsumfold) + (dst_positive_scale_reverse_resultsumfold))) + (((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) * S ((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) + ((dst_negative_scale_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)))) + ((((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) * S ((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) + ((dst_negative_scale_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold))) + (((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) * S ((dst_negative_code_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)) + ((dst_negative_scale_reverse_resultsumfold) + (dst_negative_scale_reverse_resultsumfold)))))) /\ (((exists fs_u_dst_reverse_resultsumfoldpositive fs_v_dst_reverse_resultsumfoldpositive. ((((exists fs_h_dst_reverse_resultsumfoldpositive_body_start. fs_h_dst_reverse_resultsumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_reverse_resultsumfoldpositive_body_start. fs_u_dst_reverse_resultsumfoldpositive = fs_q_dst_reverse_resultsumfoldpositive_body_start * S ((S (0)) * fs_v_dst_reverse_resultsumfoldpositive) + (0))) /\ ((((exists fs_h_dst_reverse_resultsumfoldpositive_body_terminal. fs_h_dst_reverse_resultsumfoldpositive_body_terminal + S (dst_positive_sum_reverse_resultsumfold) = S ((S (S (mi_index_reverse_result))) * fs_v_dst_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_reverse_resultsumfoldpositive_body_terminal. fs_u_dst_reverse_resultsumfoldpositive = fs_q_dst_reverse_resultsumfoldpositive_body_terminal * S ((S (S (mi_index_reverse_result))) * fs_v_dst_reverse_resultsumfoldpositive) + (dst_positive_sum_reverse_resultsumfold))) /\ forall fs_i_dst_reverse_resultsumfoldpositive_body_steps. (exists fs_lt_dst_reverse_resultsumfoldpositive_body_steps_bound. fs_lt_dst_reverse_resultsumfoldpositive_body_steps_bound + S fs_i_dst_reverse_resultsumfoldpositive_body_steps = S (mi_index_reverse_result)) -> exists fs_a_dst_reverse_resultsumfoldpositive_body_steps fs_r_dst_reverse_resultsumfoldpositive_body_steps fs_s_dst_reverse_resultsumfoldpositive_body_steps. ((((exists fs_h_dst_reverse_resultsumfoldpositive_body_steps_summand. fs_h_dst_reverse_resultsumfoldpositive_body_steps_summand + S (fs_a_dst_reverse_resultsumfoldpositive_body_steps) = S ((S (fs_i_dst_reverse_resultsumfoldpositive_body_steps)) * dst_positive_scale_reverse_resultsumfold)) /\ exists fs_q_dst_reverse_resultsumfoldpositive_body_steps_summand. dst_positive_code_reverse_resultsumfold = fs_q_dst_reverse_resultsumfoldpositive_body_steps_summand * S ((S (fs_i_dst_reverse_resultsumfoldpositive_body_steps)) * dst_positive_scale_reverse_resultsumfold) + (fs_a_dst_reverse_resultsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_reverse_resultsumfoldpositive_body_steps_partial. fs_h_dst_reverse_resultsumfoldpositive_body_steps_partial + S (fs_r_dst_reverse_resultsumfoldpositive_body_steps) = S ((S (fs_i_dst_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_reverse_resultsumfoldpositive_body_steps_partial. fs_u_dst_reverse_resultsumfoldpositive = fs_q_dst_reverse_resultsumfoldpositive_body_steps_partial * S ((S (fs_i_dst_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_reverse_resultsumfoldpositive) + (fs_r_dst_reverse_resultsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_reverse_resultsumfoldpositive_body_steps_successor. fs_h_dst_reverse_resultsumfoldpositive_body_steps_successor + S (fs_s_dst_reverse_resultsumfoldpositive_body_steps) = S ((S (S fs_i_dst_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_reverse_resultsumfoldpositive)) /\ exists fs_q_dst_reverse_resultsumfoldpositive_body_steps_successor. fs_u_dst_reverse_resultsumfoldpositive = fs_q_dst_reverse_resultsumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_reverse_resultsumfoldpositive_body_steps)) * fs_v_dst_reverse_resultsumfoldpositive) + (fs_s_dst_reverse_resultsumfoldpositive_body_steps))) /\ fs_s_dst_reverse_resultsumfoldpositive_body_steps = fs_r_dst_reverse_resultsumfoldpositive_body_steps + fs_a_dst_reverse_resultsumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_reverse_resultsumfoldnegative fs_v_dst_reverse_resultsumfoldnegative. ((((exists fs_h_dst_reverse_resultsumfoldnegative_body_start. fs_h_dst_reverse_resultsumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_reverse_resultsumfoldnegative_body_start. fs_u_dst_reverse_resultsumfoldnegative = fs_q_dst_reverse_resultsumfoldnegative_body_start * S ((S (0)) * fs_v_dst_reverse_resultsumfoldnegative) + (0))) /\ ((((exists fs_h_dst_reverse_resultsumfoldnegative_body_terminal. fs_h_dst_reverse_resultsumfoldnegative_body_terminal + S (dst_negative_sum_reverse_resultsumfold) = S ((S (S (mi_index_reverse_result))) * fs_v_dst_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_reverse_resultsumfoldnegative_body_terminal. fs_u_dst_reverse_resultsumfoldnegative = fs_q_dst_reverse_resultsumfoldnegative_body_terminal * S ((S (S (mi_index_reverse_result))) * fs_v_dst_reverse_resultsumfoldnegative) + (dst_negative_sum_reverse_resultsumfold))) /\ forall fs_i_dst_reverse_resultsumfoldnegative_body_steps. (exists fs_lt_dst_reverse_resultsumfoldnegative_body_steps_bound. fs_lt_dst_reverse_resultsumfoldnegative_body_steps_bound + S fs_i_dst_reverse_resultsumfoldnegative_body_steps = S (mi_index_reverse_result)) -> exists fs_a_dst_reverse_resultsumfoldnegative_body_steps fs_r_dst_reverse_resultsumfoldnegative_body_steps fs_s_dst_reverse_resultsumfoldnegative_body_steps. ((((exists fs_h_dst_reverse_resultsumfoldnegative_body_steps_summand. fs_h_dst_reverse_resultsumfoldnegative_body_steps_summand + S (fs_a_dst_reverse_resultsumfoldnegative_body_steps) = S ((S (fs_i_dst_reverse_resultsumfoldnegative_body_steps)) * dst_negative_scale_reverse_resultsumfold)) /\ exists fs_q_dst_reverse_resultsumfoldnegative_body_steps_summand. dst_negative_code_reverse_resultsumfold = fs_q_dst_reverse_resultsumfoldnegative_body_steps_summand * S ((S (fs_i_dst_reverse_resultsumfoldnegative_body_steps)) * dst_negative_scale_reverse_resultsumfold) + (fs_a_dst_reverse_resultsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_reverse_resultsumfoldnegative_body_steps_partial. fs_h_dst_reverse_resultsumfoldnegative_body_steps_partial + S (fs_r_dst_reverse_resultsumfoldnegative_body_steps) = S ((S (fs_i_dst_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_reverse_resultsumfoldnegative_body_steps_partial. fs_u_dst_reverse_resultsumfoldnegative = fs_q_dst_reverse_resultsumfoldnegative_body_steps_partial * S ((S (fs_i_dst_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_reverse_resultsumfoldnegative) + (fs_r_dst_reverse_resultsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_reverse_resultsumfoldnegative_body_steps_successor. fs_h_dst_reverse_resultsumfoldnegative_body_steps_successor + S (fs_s_dst_reverse_resultsumfoldnegative_body_steps) = S ((S (S fs_i_dst_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_reverse_resultsumfoldnegative)) /\ exists fs_q_dst_reverse_resultsumfoldnegative_body_steps_successor. fs_u_dst_reverse_resultsumfoldnegative = fs_q_dst_reverse_resultsumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_reverse_resultsumfoldnegative_body_steps)) * fs_v_dst_reverse_resultsumfoldnegative) + (fs_s_dst_reverse_resultsumfoldnegative_body_steps))) /\ fs_s_dst_reverse_resultsumfoldnegative_body_steps = fs_r_dst_reverse_resultsumfoldnegative_body_steps + fs_a_dst_reverse_resultsumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_reverse_resultsumfoldresult ge_balance_negative_reverse_resultsumfoldresult. (((((mi_value_reverse_result) = 2 * (ge_balance_positive_reverse_resultsumfoldresult) /\ (ge_balance_negative_reverse_resultsumfoldresult) = 0) \/ exists ge_signed_half_reverse_resultsumfoldresultdecode. (((mi_value_reverse_result) = 2 * ge_signed_half_reverse_resultsumfoldresultdecode + 1 /\ (ge_balance_positive_reverse_resultsumfoldresult) = 0) /\ (ge_balance_negative_reverse_resultsumfoldresult) = S ge_signed_half_reverse_resultsumfoldresultdecode))) /\ ((dst_positive_sum_reverse_resultsumfold) + ge_balance_negative_reverse_resultsumfoldresult = (dst_negative_sum_reverse_resultsumfold) + ge_balance_positive_reverse_resultsumfoldresult))))))))))))))