Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N F G M. (exists dst_positive_code_inversion_source dst_positive_scale_inversion_source dst_negative_code_inversion_source dst_negative_scale_inversion_source. (((F) = (((((dst_positive_code_inversion_source) + (dst_positive_scale_inversion_source)) * S ((dst_positive_code_inversion_source) + (dst_positive_scale_inversion_source)) + ((dst_positive_scale_inversion_source) + (dst_positive_scale_inversion_source))) + (((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) * S ((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) + ((dst_negative_scale_inversion_source) + (dst_negative_scale_inversion_source)))) * S ((((dst_positive_code_inversion_source) + (dst_positive_scale_inversion_source)) * S ((dst_positive_code_inversion_source) + (dst_positive_scale_inversion_source)) + ((dst_positive_scale_inversion_source) + (dst_positive_scale_inversion_source))) + (((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) * S ((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) + ((dst_negative_scale_inversion_source) + (dst_negative_scale_inversion_source)))) + ((((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) * S ((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) + ((dst_negative_scale_inversion_source) + (dst_negative_scale_inversion_source))) + (((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) * S ((dst_negative_code_inversion_source) + (dst_negative_scale_inversion_source)) + ((dst_negative_scale_inversion_source) + (dst_negative_scale_inversion_source)))))) /\ (forall dst_index_inversion_source. (exists pvs_le_gap_inversion_sourcedomain. pvs_le_gap_inversion_sourcedomain + (dst_index_inversion_source) = (N)) -> exists dst_positive_inversion_source dst_negative_inversion_source dst_value_inversion_source. ((((exists ff_h_pvs_inversion_sourceentrypositive. ff_h_pvs_inversion_sourceentrypositive + S (dst_positive_inversion_source) = S ((S (dst_index_inversion_source)) * dst_positive_scale_inversion_source)) /\ exists ff_q_pvs_inversion_sourceentrypositive. dst_positive_code_inversion_source = ff_q_pvs_inversion_sourceentrypositive * S ((S (dst_index_inversion_source)) * dst_positive_scale_inversion_source) + (dst_positive_inversion_source))) /\ (((((exists ff_h_pvs_inversion_sourceentrynegative. ff_h_pvs_inversion_sourceentrynegative + S (dst_negative_inversion_source) = S ((S (dst_index_inversion_source)) * dst_negative_scale_inversion_source)) /\ exists ff_q_pvs_inversion_sourceentrynegative. dst_negative_code_inversion_source = ff_q_pvs_inversion_sourceentrynegative * S ((S (dst_index_inversion_source)) * dst_negative_scale_inversion_source) + (dst_negative_inversion_source))) /\ (exists ge_balance_positive_inversion_sourceentryvalue ge_balance_negative_inversion_sourceentryvalue. (((((dst_value_inversion_source) = 2 * (ge_balance_positive_inversion_sourceentryvalue) /\ (ge_balance_negative_inversion_sourceentryvalue) = 0) \/ exists ge_signed_half_inversion_sourceentryvaluedecode. (((dst_value_inversion_source) = 2 * ge_signed_half_inversion_sourceentryvaluedecode + 1 /\ (ge_balance_positive_inversion_sourceentryvalue) = 0) /\ (ge_balance_negative_inversion_sourceentryvalue) = S ge_signed_half_inversion_sourceentryvaluedecode))) /\ ((dst_positive_inversion_source) + ge_balance_negative_inversion_sourceentryvalue = (dst_negative_inversion_source) + ge_balance_positive_inversion_sourceentryvalue))))))))) -> (exists dst_positive_code_inversion_transform_table dst_positive_scale_inversion_transform_table dst_negative_code_inversion_transform_table dst_negative_scale_inversion_transform_table. (((G) = (((((dst_positive_code_inversion_transform_table) + (dst_positive_scale_inversion_transform_table)) * S ((dst_positive_code_inversion_transform_table) + (dst_positive_scale_inversion_transform_table)) + ((dst_positive_scale_inversion_transform_table) + (dst_positive_scale_inversion_transform_table))) + (((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) * S ((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) + ((dst_negative_scale_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)))) * S ((((dst_positive_code_inversion_transform_table) + (dst_positive_scale_inversion_transform_table)) * S ((dst_positive_code_inversion_transform_table) + (dst_positive_scale_inversion_transform_table)) + ((dst_positive_scale_inversion_transform_table) + (dst_positive_scale_inversion_transform_table))) + (((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) * S ((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) + ((dst_negative_scale_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)))) + ((((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) * S ((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) + ((dst_negative_scale_inversion_transform_table) + (dst_negative_scale_inversion_transform_table))) + (((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) * S ((dst_negative_code_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)) + ((dst_negative_scale_inversion_transform_table) + (dst_negative_scale_inversion_transform_table)))))) /\ (forall dst_index_inversion_transform_table. (exists pvs_le_gap_inversion_transform_tabledomain. pvs_le_gap_inversion_transform_tabledomain + (dst_index_inversion_transform_table) = (N)) -> exists dst_positive_inversion_transform_table dst_negative_inversion_transform_table dst_value_inversion_transform_table. ((((exists ff_h_pvs_inversion_transform_tableentrypositive. ff_h_pvs_inversion_transform_tableentrypositive + S (dst_positive_inversion_transform_table) = S ((S (dst_index_inversion_transform_table)) * dst_positive_scale_inversion_transform_table)) /\ exists ff_q_pvs_inversion_transform_tableentrypositive. dst_positive_code_inversion_transform_table = ff_q_pvs_inversion_transform_tableentrypositive * S ((S (dst_index_inversion_transform_table)) * dst_positive_scale_inversion_transform_table) + (dst_positive_inversion_transform_table))) /\ (((((exists ff_h_pvs_inversion_transform_tableentrynegative. ff_h_pvs_inversion_transform_tableentrynegative + S (dst_negative_inversion_transform_table) = S ((S (dst_index_inversion_transform_table)) * dst_negative_scale_inversion_transform_table)) /\ exists ff_q_pvs_inversion_transform_tableentrynegative. dst_negative_code_inversion_transform_table = ff_q_pvs_inversion_transform_tableentrynegative * S ((S (dst_index_inversion_transform_table)) * dst_negative_scale_inversion_transform_table) + (dst_negative_inversion_transform_table))) /\ (exists ge_balance_positive_inversion_transform_tableentryvalue ge_balance_negative_inversion_transform_tableentryvalue. (((((dst_value_inversion_transform_table) = 2 * (ge_balance_positive_inversion_transform_tableentryvalue) /\ (ge_balance_negative_inversion_transform_tableentryvalue) = 0) \/ exists ge_signed_half_inversion_transform_tableentryvaluedecode. (((dst_value_inversion_transform_table) = 2 * ge_signed_half_inversion_transform_tableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_transform_tableentryvalue) = 0) /\ (ge_balance_negative_inversion_transform_tableentryvalue) = S ge_signed_half_inversion_transform_tableentryvaluedecode))) /\ ((dst_positive_inversion_transform_table) + ge_balance_negative_inversion_transform_tableentryvalue = (dst_negative_inversion_transform_table) + ge_balance_positive_inversion_transform_tableentryvalue))))))))) -> (((exists dst_positive_code_inversion_mobiustable dst_positive_scale_inversion_mobiustable dst_negative_code_inversion_mobiustable dst_negative_scale_inversion_mobiustable. (((M) = (((((dst_positive_code_inversion_mobiustable) + (dst_positive_scale_inversion_mobiustable)) * S ((dst_positive_code_inversion_mobiustable) + (dst_positive_scale_inversion_mobiustable)) + ((dst_positive_scale_inversion_mobiustable) + (dst_positive_scale_inversion_mobiustable))) + (((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) * S ((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) + ((dst_negative_scale_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)))) * S ((((dst_positive_code_inversion_mobiustable) + (dst_positive_scale_inversion_mobiustable)) * S ((dst_positive_code_inversion_mobiustable) + (dst_positive_scale_inversion_mobiustable)) + ((dst_positive_scale_inversion_mobiustable) + (dst_positive_scale_inversion_mobiustable))) + (((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) * S ((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) + ((dst_negative_scale_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)))) + ((((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) * S ((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) + ((dst_negative_scale_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable))) + (((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) * S ((dst_negative_code_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)) + ((dst_negative_scale_inversion_mobiustable) + (dst_negative_scale_inversion_mobiustable)))))) /\ (forall dst_index_inversion_mobiustable. (exists pvs_le_gap_inversion_mobiustabledomain. pvs_le_gap_inversion_mobiustabledomain + (dst_index_inversion_mobiustable) = (N)) -> exists dst_positive_inversion_mobiustable dst_negative_inversion_mobiustable dst_value_inversion_mobiustable. ((((exists ff_h_pvs_inversion_mobiustableentrypositive. ff_h_pvs_inversion_mobiustableentrypositive + S (dst_positive_inversion_mobiustable) = S ((S (dst_index_inversion_mobiustable)) * dst_positive_scale_inversion_mobiustable)) /\ exists ff_q_pvs_inversion_mobiustableentrypositive. dst_positive_code_inversion_mobiustable = ff_q_pvs_inversion_mobiustableentrypositive * S ((S (dst_index_inversion_mobiustable)) * dst_positive_scale_inversion_mobiustable) + (dst_positive_inversion_mobiustable))) /\ (((((exists ff_h_pvs_inversion_mobiustableentrynegative. ff_h_pvs_inversion_mobiustableentrynegative + S (dst_negative_inversion_mobiustable) = S ((S (dst_index_inversion_mobiustable)) * dst_negative_scale_inversion_mobiustable)) /\ exists ff_q_pvs_inversion_mobiustableentrynegative. dst_negative_code_inversion_mobiustable = ff_q_pvs_inversion_mobiustableentrynegative * S ((S (dst_index_inversion_mobiustable)) * dst_negative_scale_inversion_mobiustable) + (dst_negative_inversion_mobiustable))) /\ (exists ge_balance_positive_inversion_mobiustableentryvalue ge_balance_negative_inversion_mobiustableentryvalue. (((((dst_value_inversion_mobiustable) = 2 * (ge_balance_positive_inversion_mobiustableentryvalue) /\ (ge_balance_negative_inversion_mobiustableentryvalue) = 0) \/ exists ge_signed_half_inversion_mobiustableentryvaluedecode. (((dst_value_inversion_mobiustable) = 2 * ge_signed_half_inversion_mobiustableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_mobiustableentryvalue) = 0) /\ (ge_balance_negative_inversion_mobiustableentryvalue) = S ge_signed_half_inversion_mobiustableentryvaluedecode))) /\ ((dst_positive_inversion_mobiustable) + ge_balance_negative_inversion_mobiustableentryvalue = (dst_negative_inversion_mobiustable) + ge_balance_positive_inversion_mobiustableentryvalue))))))))) /\ (((exists dst_positive_code_inversion_mobiuszero dst_positive_scale_inversion_mobiuszero dst_negative_code_inversion_mobiuszero dst_negative_scale_inversion_mobiuszero dst_positive_inversion_mobiuszero dst_negative_inversion_mobiuszero. (((M) = (((((dst_positive_code_inversion_mobiuszero) + (dst_positive_scale_inversion_mobiuszero)) * S ((dst_positive_code_inversion_mobiuszero) + (dst_positive_scale_inversion_mobiuszero)) + ((dst_positive_scale_inversion_mobiuszero) + (dst_positive_scale_inversion_mobiuszero))) + (((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) * S ((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) + ((dst_negative_scale_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)))) * S ((((dst_positive_code_inversion_mobiuszero) + (dst_positive_scale_inversion_mobiuszero)) * S ((dst_positive_code_inversion_mobiuszero) + (dst_positive_scale_inversion_mobiuszero)) + ((dst_positive_scale_inversion_mobiuszero) + (dst_positive_scale_inversion_mobiuszero))) + (((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) * S ((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) + ((dst_negative_scale_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)))) + ((((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) * S ((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) + ((dst_negative_scale_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero))) + (((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) * S ((dst_negative_code_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)) + ((dst_negative_scale_inversion_mobiuszero) + (dst_negative_scale_inversion_mobiuszero)))))) /\ (((((exists ff_h_pvs_inversion_mobiuszeropositive. ff_h_pvs_inversion_mobiuszeropositive + S (dst_positive_inversion_mobiuszero) = S ((S (0)) * dst_positive_scale_inversion_mobiuszero)) /\ exists ff_q_pvs_inversion_mobiuszeropositive. dst_positive_code_inversion_mobiuszero = ff_q_pvs_inversion_mobiuszeropositive * S ((S (0)) * dst_positive_scale_inversion_mobiuszero) + (dst_positive_inversion_mobiuszero))) /\ (((((exists ff_h_pvs_inversion_mobiuszeronegative. ff_h_pvs_inversion_mobiuszeronegative + S (dst_negative_inversion_mobiuszero) = S ((S (0)) * dst_negative_scale_inversion_mobiuszero)) /\ exists ff_q_pvs_inversion_mobiuszeronegative. dst_negative_code_inversion_mobiuszero = ff_q_pvs_inversion_mobiuszeronegative * S ((S (0)) * dst_negative_scale_inversion_mobiuszero) + (dst_negative_inversion_mobiuszero))) /\ (exists ge_balance_positive_inversion_mobiuszerovalue ge_balance_negative_inversion_mobiuszerovalue. (((((0) = 2 * (ge_balance_positive_inversion_mobiuszerovalue) /\ (ge_balance_negative_inversion_mobiuszerovalue) = 0) \/ exists ge_signed_half_inversion_mobiuszerovaluedecode. (((0) = 2 * ge_signed_half_inversion_mobiuszerovaluedecode + 1 /\ (ge_balance_positive_inversion_mobiuszerovalue) = 0) /\ (ge_balance_negative_inversion_mobiuszerovalue) = S ge_signed_half_inversion_mobiuszerovaluedecode))) /\ ((dst_positive_inversion_mobiuszero) + ge_balance_negative_inversion_mobiuszerovalue = (dst_negative_inversion_mobiuszero) + ge_balance_positive_inversion_mobiuszerovalue))))))))) /\ (forall mt_index_inversion_mobius mt_value_inversion_mobius. ~(mt_index_inversion_mobius=0) -> (exists pvs_le_gap_inversion_mobiusdomain. pvs_le_gap_inversion_mobiusdomain + (mt_index_inversion_mobius) = (N)) -> (exists dst_positive_code_inversion_mobiusentry dst_positive_scale_inversion_mobiusentry dst_negative_code_inversion_mobiusentry dst_negative_scale_inversion_mobiusentry dst_positive_inversion_mobiusentry dst_negative_inversion_mobiusentry. (((M) = (((((dst_positive_code_inversion_mobiusentry) + (dst_positive_scale_inversion_mobiusentry)) * S ((dst_positive_code_inversion_mobiusentry) + (dst_positive_scale_inversion_mobiusentry)) + ((dst_positive_scale_inversion_mobiusentry) + (dst_positive_scale_inversion_mobiusentry))) + (((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) * S ((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) + ((dst_negative_scale_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)))) * S ((((dst_positive_code_inversion_mobiusentry) + (dst_positive_scale_inversion_mobiusentry)) * S ((dst_positive_code_inversion_mobiusentry) + (dst_positive_scale_inversion_mobiusentry)) + ((dst_positive_scale_inversion_mobiusentry) + (dst_positive_scale_inversion_mobiusentry))) + (((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) * S ((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) + ((dst_negative_scale_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)))) + ((((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) * S ((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) + ((dst_negative_scale_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry))) + (((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) * S ((dst_negative_code_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)) + ((dst_negative_scale_inversion_mobiusentry) + (dst_negative_scale_inversion_mobiusentry)))))) /\ (((((exists ff_h_pvs_inversion_mobiusentrypositive. ff_h_pvs_inversion_mobiusentrypositive + S (dst_positive_inversion_mobiusentry) = S ((S (mt_index_inversion_mobius)) * dst_positive_scale_inversion_mobiusentry)) /\ exists ff_q_pvs_inversion_mobiusentrypositive. dst_positive_code_inversion_mobiusentry = ff_q_pvs_inversion_mobiusentrypositive * S ((S (mt_index_inversion_mobius)) * dst_positive_scale_inversion_mobiusentry) + (dst_positive_inversion_mobiusentry))) /\ (((((exists ff_h_pvs_inversion_mobiusentrynegative. ff_h_pvs_inversion_mobiusentrynegative + S (dst_negative_inversion_mobiusentry) = S ((S (mt_index_inversion_mobius)) * dst_negative_scale_inversion_mobiusentry)) /\ exists ff_q_pvs_inversion_mobiusentrynegative. dst_negative_code_inversion_mobiusentry = ff_q_pvs_inversion_mobiusentrynegative * S ((S (mt_index_inversion_mobius)) * dst_negative_scale_inversion_mobiusentry) + (dst_negative_inversion_mobiusentry))) /\ (exists ge_balance_positive_inversion_mobiusentryvalue ge_balance_negative_inversion_mobiusentryvalue. (((((mt_value_inversion_mobius) = 2 * (ge_balance_positive_inversion_mobiusentryvalue) /\ (ge_balance_negative_inversion_mobiusentryvalue) = 0) \/ exists ge_signed_half_inversion_mobiusentryvaluedecode. (((mt_value_inversion_mobius) = 2 * ge_signed_half_inversion_mobiusentryvaluedecode + 1 /\ (ge_balance_positive_inversion_mobiusentryvalue) = 0) /\ (ge_balance_negative_inversion_mobiusentryvalue) = S ge_signed_half_inversion_mobiusentryvaluedecode))) /\ ((dst_positive_inversion_mobiusentry) + ge_balance_negative_inversion_mobiusentryvalue = (dst_negative_inversion_mobiusentry) + ge_balance_positive_inversion_mobiusentryvalue))))))))) -> (((~((mt_index_inversion_mobius) = 0)) /\ ((((exists mv_square_prime_inversion_mobiusvaluesquare. ((~((mv_square_prime_inversion_mobiusvaluesquare) = 1) /\ forall pvs_left_inversion_mobiusvaluesquareprime pvs_right_inversion_mobiusvaluesquareprime. (mv_square_prime_inversion_mobiusvaluesquare) = pvs_left_inversion_mobiusvaluesquareprime * pvs_right_inversion_mobiusvaluesquareprime -> pvs_left_inversion_mobiusvaluesquareprime = 1 \/ pvs_right_inversion_mobiusvaluesquareprime = 1) /\ (exists pvs_factor_inversion_mobiusvaluesquaredivisor. (mt_index_inversion_mobius) = (mv_square_prime_inversion_mobiusvaluesquare * mv_square_prime_inversion_mobiusvaluesquare) * pvs_factor_inversion_mobiusvaluesquaredivisor))) /\ ((mt_value_inversion_mobius) = 0))) \/ (((((~((mt_index_inversion_mobius) = 0)) /\ (forall sfd_prime_inversion_mobiusvaluesquarefree. (~((sfd_prime_inversion_mobiusvaluesquarefree) = 1) /\ forall pvs_left_inversion_mobiusvaluesquarefreedomain pvs_right_inversion_mobiusvaluesquarefreedomain. (sfd_prime_inversion_mobiusvaluesquarefree) = pvs_left_inversion_mobiusvaluesquarefreedomain * pvs_right_inversion_mobiusvaluesquarefreedomain -> pvs_left_inversion_mobiusvaluesquarefreedomain = 1 \/ pvs_right_inversion_mobiusvaluesquarefreedomain = 1) -> (exists pvs_le_gap_inversion_mobiusvaluesquarefreebound. pvs_le_gap_inversion_mobiusvaluesquarefreebound + (sfd_prime_inversion_mobiusvaluesquarefree) = (mt_index_inversion_mobius)) -> ~(exists pvs_factor_inversion_mobiusvaluesquarefreesquare. (mt_index_inversion_mobius) = (sfd_prime_inversion_mobiusvaluesquarefree * sfd_prime_inversion_mobiusvaluesquarefree) * pvs_factor_inversion_mobiusvaluesquarefreesquare)))) /\ (exists mv_factor_code_inversion_mobiusvaluefactors mv_factor_scale_inversion_mobiusvaluefactors mv_factor_count_inversion_mobiusvaluefactors. (((~(mt_index_inversion_mobius = 0) /\ ((exists ff_u_fsat_inversion_mobiusvaluefactorsfactorization_product ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_start. ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_start. ff_u_fsat_inversion_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_terminal. ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_terminal + S (mt_index_inversion_mobius) = S ((S (mv_factor_count_inversion_mobiusvaluefactors)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_terminal. ff_u_fsat_inversion_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_inversion_mobiusvaluefactors)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product) + (mt_index_inversion_mobius))) /\ forall ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product. (exists ff_lt_fsat_inversion_mobiusvaluefactorsfactorization_product_bound. ff_lt_fsat_inversion_mobiusvaluefactorsfactorization_product_bound + S ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product = mv_factor_count_inversion_mobiusvaluefactors) -> exists ff_p_fsat_inversion_mobiusvaluefactorsfactorization_product ff_r_fsat_inversion_mobiusvaluefactorsfactorization_product ff_s_fsat_inversion_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_factor. ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_factor + S (ff_p_fsat_inversion_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_inversion_mobiusvaluefactors)) /\ exists ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_factor. mv_factor_code_inversion_mobiusvaluefactors = ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_inversion_mobiusvaluefactors) + (ff_p_fsat_inversion_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_partial. ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_partial + S (ff_r_fsat_inversion_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_partial. ff_u_fsat_inversion_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product) + (ff_r_fsat_inversion_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_successor. ff_h_fsat_inversion_mobiusvaluefactorsfactorization_product_successor + S (ff_s_fsat_inversion_mobiusvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_successor. ff_u_fsat_inversion_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_mobiusvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_inversion_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_mobiusvaluefactorsfactorization_product) + (ff_s_fsat_inversion_mobiusvaluefactorsfactorization_product))) /\ ff_s_fsat_inversion_mobiusvaluefactorsfactorization_product = ff_r_fsat_inversion_mobiusvaluefactorsfactorization_product * ff_p_fsat_inversion_mobiusvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_inversion_mobiusvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_inversion_mobiusvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_inversion_mobiusvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_inversion_mobiusvaluefactorsfactorization_primes = (mv_factor_count_inversion_mobiusvaluefactors)) -> exists ftsf_factor_fsat_inversion_mobiusvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_inversion_mobiusvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_inversion_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_inversion_mobiusvaluefactors)) /\ exists ff_q_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_entry. mv_factor_code_inversion_mobiusvaluefactors = ff_q_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_inversion_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_inversion_mobiusvaluefactors) + (ftsf_factor_fsat_inversion_mobiusvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_inversion_mobiusvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_inversion_mobiusvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_inversion_mobiusvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_inversion_mobiusvaluefactorsparityeven. (mv_factor_count_inversion_mobiusvaluefactors) = 2 * mv_even_half_inversion_mobiusvaluefactorsparityeven) /\ ((mt_value_inversion_mobius) = 2))) \/ (((exists mv_odd_half_inversion_mobiusvaluefactorsparityodd. (mv_factor_count_inversion_mobiusvaluefactors) = 2 * mv_odd_half_inversion_mobiusvaluefactorsparityodd + 1) /\ ((mt_value_inversion_mobius) = 1)))))))))))))))) -> (forall mi_index_inversion_all_inputs mi_value_inversion_all_inputs. ~(mi_index_inversion_all_inputs=0) -> (exists pvs_le_gap_inversion_all_inputsbound. pvs_le_gap_inversion_all_inputsbound + (mi_index_inversion_all_inputs) = (N)) -> (exists dst_positive_code_inversion_all_inputsentry dst_positive_scale_inversion_all_inputsentry dst_negative_code_inversion_all_inputsentry dst_negative_scale_inversion_all_inputsentry dst_positive_inversion_all_inputsentry dst_negative_inversion_all_inputsentry. (((G) = (((((dst_positive_code_inversion_all_inputsentry) + (dst_positive_scale_inversion_all_inputsentry)) * S ((dst_positive_code_inversion_all_inputsentry) + (dst_positive_scale_inversion_all_inputsentry)) + ((dst_positive_scale_inversion_all_inputsentry) + (dst_positive_scale_inversion_all_inputsentry))) + (((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) * S ((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) + ((dst_negative_scale_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)))) * S ((((dst_positive_code_inversion_all_inputsentry) + (dst_positive_scale_inversion_all_inputsentry)) * S ((dst_positive_code_inversion_all_inputsentry) + (dst_positive_scale_inversion_all_inputsentry)) + ((dst_positive_scale_inversion_all_inputsentry) + (dst_positive_scale_inversion_all_inputsentry))) + (((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) * S ((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) + ((dst_negative_scale_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)))) + ((((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) * S ((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) + ((dst_negative_scale_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry))) + (((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) * S ((dst_negative_code_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)) + ((dst_negative_scale_inversion_all_inputsentry) + (dst_negative_scale_inversion_all_inputsentry)))))) /\ (((((exists ff_h_pvs_inversion_all_inputsentrypositive. ff_h_pvs_inversion_all_inputsentrypositive + S (dst_positive_inversion_all_inputsentry) = S ((S (mi_index_inversion_all_inputs)) * dst_positive_scale_inversion_all_inputsentry)) /\ exists ff_q_pvs_inversion_all_inputsentrypositive. dst_positive_code_inversion_all_inputsentry = ff_q_pvs_inversion_all_inputsentrypositive * S ((S (mi_index_inversion_all_inputs)) * dst_positive_scale_inversion_all_inputsentry) + (dst_positive_inversion_all_inputsentry))) /\ (((((exists ff_h_pvs_inversion_all_inputsentrynegative. ff_h_pvs_inversion_all_inputsentrynegative + S (dst_negative_inversion_all_inputsentry) = S ((S (mi_index_inversion_all_inputs)) * dst_negative_scale_inversion_all_inputsentry)) /\ exists ff_q_pvs_inversion_all_inputsentrynegative. dst_negative_code_inversion_all_inputsentry = ff_q_pvs_inversion_all_inputsentrynegative * S ((S (mi_index_inversion_all_inputs)) * dst_negative_scale_inversion_all_inputsentry) + (dst_negative_inversion_all_inputsentry))) /\ (exists ge_balance_positive_inversion_all_inputsentryvalue ge_balance_negative_inversion_all_inputsentryvalue. (((((mi_value_inversion_all_inputs) = 2 * (ge_balance_positive_inversion_all_inputsentryvalue) /\ (ge_balance_negative_inversion_all_inputsentryvalue) = 0) \/ exists ge_signed_half_inversion_all_inputsentryvaluedecode. (((mi_value_inversion_all_inputs) = 2 * ge_signed_half_inversion_all_inputsentryvaluedecode + 1 /\ (ge_balance_positive_inversion_all_inputsentryvalue) = 0) /\ (ge_balance_negative_inversion_all_inputsentryvalue) = S ge_signed_half_inversion_all_inputsentryvaluedecode))) /\ ((dst_positive_inversion_all_inputsentry) + ge_balance_negative_inversion_all_inputsentryvalue = (dst_negative_inversion_all_inputsentry) + ge_balance_positive_inversion_all_inputsentryvalue))))))))) -> (((~((mi_index_inversion_all_inputs)=0)) /\ (exists dm_mask_table_inversion_all_inputssum. ((((exists dst_positive_code_inversion_all_inputssummasktable dst_positive_scale_inversion_all_inputssummasktable dst_negative_code_inversion_all_inputssummasktable dst_negative_scale_inversion_all_inputssummasktable. (((dm_mask_table_inversion_all_inputssum) = (((((dst_positive_code_inversion_all_inputssummasktable) + (dst_positive_scale_inversion_all_inputssummasktable)) * S ((dst_positive_code_inversion_all_inputssummasktable) + (dst_positive_scale_inversion_all_inputssummasktable)) + ((dst_positive_scale_inversion_all_inputssummasktable) + (dst_positive_scale_inversion_all_inputssummasktable))) + (((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) * S ((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) + ((dst_negative_scale_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)))) * S ((((dst_positive_code_inversion_all_inputssummasktable) + (dst_positive_scale_inversion_all_inputssummasktable)) * S ((dst_positive_code_inversion_all_inputssummasktable) + (dst_positive_scale_inversion_all_inputssummasktable)) + ((dst_positive_scale_inversion_all_inputssummasktable) + (dst_positive_scale_inversion_all_inputssummasktable))) + (((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) * S ((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) + ((dst_negative_scale_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)))) + ((((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) * S ((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) + ((dst_negative_scale_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable))) + (((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) * S ((dst_negative_code_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)) + ((dst_negative_scale_inversion_all_inputssummasktable) + (dst_negative_scale_inversion_all_inputssummasktable)))))) /\ (forall dst_index_inversion_all_inputssummasktable. (exists pvs_le_gap_inversion_all_inputssummasktabledomain. pvs_le_gap_inversion_all_inputssummasktabledomain + (dst_index_inversion_all_inputssummasktable) = (mi_index_inversion_all_inputs)) -> exists dst_positive_inversion_all_inputssummasktable dst_negative_inversion_all_inputssummasktable dst_value_inversion_all_inputssummasktable. ((((exists ff_h_pvs_inversion_all_inputssummasktableentrypositive. ff_h_pvs_inversion_all_inputssummasktableentrypositive + S (dst_positive_inversion_all_inputssummasktable) = S ((S (dst_index_inversion_all_inputssummasktable)) * dst_positive_scale_inversion_all_inputssummasktable)) /\ exists ff_q_pvs_inversion_all_inputssummasktableentrypositive. dst_positive_code_inversion_all_inputssummasktable = ff_q_pvs_inversion_all_inputssummasktableentrypositive * S ((S (dst_index_inversion_all_inputssummasktable)) * dst_positive_scale_inversion_all_inputssummasktable) + (dst_positive_inversion_all_inputssummasktable))) /\ (((((exists ff_h_pvs_inversion_all_inputssummasktableentrynegative. ff_h_pvs_inversion_all_inputssummasktableentrynegative + S (dst_negative_inversion_all_inputssummasktable) = S ((S (dst_index_inversion_all_inputssummasktable)) * dst_negative_scale_inversion_all_inputssummasktable)) /\ exists ff_q_pvs_inversion_all_inputssummasktableentrynegative. dst_negative_code_inversion_all_inputssummasktable = ff_q_pvs_inversion_all_inputssummasktableentrynegative * S ((S (dst_index_inversion_all_inputssummasktable)) * dst_negative_scale_inversion_all_inputssummasktable) + (dst_negative_inversion_all_inputssummasktable))) /\ (exists ge_balance_positive_inversion_all_inputssummasktableentryvalue ge_balance_negative_inversion_all_inputssummasktableentryvalue. (((((dst_value_inversion_all_inputssummasktable) = 2 * (ge_balance_positive_inversion_all_inputssummasktableentryvalue) /\ (ge_balance_negative_inversion_all_inputssummasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_all_inputssummasktableentryvaluedecode. (((dst_value_inversion_all_inputssummasktable) = 2 * ge_signed_half_inversion_all_inputssummasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_all_inputssummasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_all_inputssummasktableentryvalue) = S ge_signed_half_inversion_all_inputssummasktableentryvaluedecode))) /\ ((dst_positive_inversion_all_inputssummasktable) + ge_balance_negative_inversion_all_inputssummasktableentryvalue = (dst_negative_inversion_all_inputssummasktable) + ge_balance_positive_inversion_all_inputssummasktableentryvalue))))))))) /\ (forall dm_index_inversion_all_inputssummask dm_value_inversion_all_inputssummask. (exists pvs_le_gap_inversion_all_inputssummaskdomain. pvs_le_gap_inversion_all_inputssummaskdomain + (dm_index_inversion_all_inputssummask) = (mi_index_inversion_all_inputs)) -> (exists dst_positive_code_inversion_all_inputssummasklookup dst_positive_scale_inversion_all_inputssummasklookup dst_negative_code_inversion_all_inputssummasklookup dst_negative_scale_inversion_all_inputssummasklookup dst_positive_inversion_all_inputssummasklookup dst_negative_inversion_all_inputssummasklookup. (((dm_mask_table_inversion_all_inputssum) = (((((dst_positive_code_inversion_all_inputssummasklookup) + (dst_positive_scale_inversion_all_inputssummasklookup)) * S ((dst_positive_code_inversion_all_inputssummasklookup) + (dst_positive_scale_inversion_all_inputssummasklookup)) + ((dst_positive_scale_inversion_all_inputssummasklookup) + (dst_positive_scale_inversion_all_inputssummasklookup))) + (((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) * S ((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) + ((dst_negative_scale_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)))) * S ((((dst_positive_code_inversion_all_inputssummasklookup) + (dst_positive_scale_inversion_all_inputssummasklookup)) * S ((dst_positive_code_inversion_all_inputssummasklookup) + (dst_positive_scale_inversion_all_inputssummasklookup)) + ((dst_positive_scale_inversion_all_inputssummasklookup) + (dst_positive_scale_inversion_all_inputssummasklookup))) + (((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) * S ((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) + ((dst_negative_scale_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)))) + ((((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) * S ((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) + ((dst_negative_scale_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup))) + (((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) * S ((dst_negative_code_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)) + ((dst_negative_scale_inversion_all_inputssummasklookup) + (dst_negative_scale_inversion_all_inputssummasklookup)))))) /\ (((((exists ff_h_pvs_inversion_all_inputssummasklookuppositive. ff_h_pvs_inversion_all_inputssummasklookuppositive + S (dst_positive_inversion_all_inputssummasklookup) = S ((S (dm_index_inversion_all_inputssummask)) * dst_positive_scale_inversion_all_inputssummasklookup)) /\ exists ff_q_pvs_inversion_all_inputssummasklookuppositive. dst_positive_code_inversion_all_inputssummasklookup = ff_q_pvs_inversion_all_inputssummasklookuppositive * S ((S (dm_index_inversion_all_inputssummask)) * dst_positive_scale_inversion_all_inputssummasklookup) + (dst_positive_inversion_all_inputssummasklookup))) /\ (((((exists ff_h_pvs_inversion_all_inputssummasklookupnegative. ff_h_pvs_inversion_all_inputssummasklookupnegative + S (dst_negative_inversion_all_inputssummasklookup) = S ((S (dm_index_inversion_all_inputssummask)) * dst_negative_scale_inversion_all_inputssummasklookup)) /\ exists ff_q_pvs_inversion_all_inputssummasklookupnegative. dst_negative_code_inversion_all_inputssummasklookup = ff_q_pvs_inversion_all_inputssummasklookupnegative * S ((S (dm_index_inversion_all_inputssummask)) * dst_negative_scale_inversion_all_inputssummasklookup) + (dst_negative_inversion_all_inputssummasklookup))) /\ (exists ge_balance_positive_inversion_all_inputssummasklookupvalue ge_balance_negative_inversion_all_inputssummasklookupvalue. (((((dm_value_inversion_all_inputssummask) = 2 * (ge_balance_positive_inversion_all_inputssummasklookupvalue) /\ (ge_balance_negative_inversion_all_inputssummasklookupvalue) = 0) \/ exists ge_signed_half_inversion_all_inputssummasklookupvaluedecode. (((dm_value_inversion_all_inputssummask) = 2 * ge_signed_half_inversion_all_inputssummasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_all_inputssummasklookupvalue) = 0) /\ (ge_balance_negative_inversion_all_inputssummasklookupvalue) = S ge_signed_half_inversion_all_inputssummasklookupvaluedecode))) /\ ((dst_positive_inversion_all_inputssummasklookup) + ge_balance_negative_inversion_all_inputssummasklookupvalue = (dst_negative_inversion_all_inputssummasklookup) + ge_balance_positive_inversion_all_inputssummasklookupvalue))))))))) -> ((((~((dm_index_inversion_all_inputssummask)=0)) /\ (exists dm_quotient_inversion_all_inputssummaskentry. (((mi_index_inversion_all_inputs)=(dm_index_inversion_all_inputssummask)*dm_quotient_inversion_all_inputssummaskentry) /\ (exists dst_positive_code_inversion_all_inputssummaskentryinput dst_positive_scale_inversion_all_inputssummaskentryinput dst_negative_code_inversion_all_inputssummaskentryinput dst_negative_scale_inversion_all_inputssummaskentryinput dst_positive_inversion_all_inputssummaskentryinput dst_negative_inversion_all_inputssummaskentryinput. (((F) = (((((dst_positive_code_inversion_all_inputssummaskentryinput) + (dst_positive_scale_inversion_all_inputssummaskentryinput)) * S ((dst_positive_code_inversion_all_inputssummaskentryinput) + (dst_positive_scale_inversion_all_inputssummaskentryinput)) + ((dst_positive_scale_inversion_all_inputssummaskentryinput) + (dst_positive_scale_inversion_all_inputssummaskentryinput))) + (((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) * S ((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) + ((dst_negative_scale_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)))) * S ((((dst_positive_code_inversion_all_inputssummaskentryinput) + (dst_positive_scale_inversion_all_inputssummaskentryinput)) * S ((dst_positive_code_inversion_all_inputssummaskentryinput) + (dst_positive_scale_inversion_all_inputssummaskentryinput)) + ((dst_positive_scale_inversion_all_inputssummaskentryinput) + (dst_positive_scale_inversion_all_inputssummaskentryinput))) + (((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) * S ((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) + ((dst_negative_scale_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)))) + ((((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) * S ((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) + ((dst_negative_scale_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput))) + (((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) * S ((dst_negative_code_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)) + ((dst_negative_scale_inversion_all_inputssummaskentryinput) + (dst_negative_scale_inversion_all_inputssummaskentryinput)))))) /\ (((((exists ff_h_pvs_inversion_all_inputssummaskentryinputpositive. ff_h_pvs_inversion_all_inputssummaskentryinputpositive + S (dst_positive_inversion_all_inputssummaskentryinput) = S ((S (dm_index_inversion_all_inputssummask)) * dst_positive_scale_inversion_all_inputssummaskentryinput)) /\ exists ff_q_pvs_inversion_all_inputssummaskentryinputpositive. dst_positive_code_inversion_all_inputssummaskentryinput = ff_q_pvs_inversion_all_inputssummaskentryinputpositive * S ((S (dm_index_inversion_all_inputssummask)) * dst_positive_scale_inversion_all_inputssummaskentryinput) + (dst_positive_inversion_all_inputssummaskentryinput))) /\ (((((exists ff_h_pvs_inversion_all_inputssummaskentryinputnegative. ff_h_pvs_inversion_all_inputssummaskentryinputnegative + S (dst_negative_inversion_all_inputssummaskentryinput) = S ((S (dm_index_inversion_all_inputssummask)) * dst_negative_scale_inversion_all_inputssummaskentryinput)) /\ exists ff_q_pvs_inversion_all_inputssummaskentryinputnegative. dst_negative_code_inversion_all_inputssummaskentryinput = ff_q_pvs_inversion_all_inputssummaskentryinputnegative * S ((S (dm_index_inversion_all_inputssummask)) * dst_negative_scale_inversion_all_inputssummaskentryinput) + (dst_negative_inversion_all_inputssummaskentryinput))) /\ (exists ge_balance_positive_inversion_all_inputssummaskentryinputvalue ge_balance_negative_inversion_all_inputssummaskentryinputvalue. (((((dm_value_inversion_all_inputssummask) = 2 * (ge_balance_positive_inversion_all_inputssummaskentryinputvalue) /\ (ge_balance_negative_inversion_all_inputssummaskentryinputvalue) = 0) \/ exists ge_signed_half_inversion_all_inputssummaskentryinputvaluedecode. (((dm_value_inversion_all_inputssummask) = 2 * ge_signed_half_inversion_all_inputssummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_inversion_all_inputssummaskentryinputvalue) = 0) /\ (ge_balance_negative_inversion_all_inputssummaskentryinputvalue) = S ge_signed_half_inversion_all_inputssummaskentryinputvaluedecode))) /\ ((dst_positive_inversion_all_inputssummaskentryinput) + ge_balance_negative_inversion_all_inputssummaskentryinputvalue = (dst_negative_inversion_all_inputssummaskentryinput) + ge_balance_positive_inversion_all_inputssummaskentryinputvalue))))))))))))) \/ ((((dm_index_inversion_all_inputssummask)=0 \/ ~(exists pvs_factor_inversion_all_inputssummaskentrynondivisor. (mi_index_inversion_all_inputs) = (dm_index_inversion_all_inputssummask) * pvs_factor_inversion_all_inputssummaskentrynondivisor)) /\ ((dm_value_inversion_all_inputssummask)=0))))))) /\ (exists dst_positive_code_inversion_all_inputssumfold dst_positive_scale_inversion_all_inputssumfold dst_negative_code_inversion_all_inputssumfold dst_negative_scale_inversion_all_inputssumfold dst_positive_sum_inversion_all_inputssumfold dst_negative_sum_inversion_all_inputssumfold. (((dm_mask_table_inversion_all_inputssum) = (((((dst_positive_code_inversion_all_inputssumfold) + (dst_positive_scale_inversion_all_inputssumfold)) * S ((dst_positive_code_inversion_all_inputssumfold) + (dst_positive_scale_inversion_all_inputssumfold)) + ((dst_positive_scale_inversion_all_inputssumfold) + (dst_positive_scale_inversion_all_inputssumfold))) + (((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) * S ((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) + ((dst_negative_scale_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)))) * S ((((dst_positive_code_inversion_all_inputssumfold) + (dst_positive_scale_inversion_all_inputssumfold)) * S ((dst_positive_code_inversion_all_inputssumfold) + (dst_positive_scale_inversion_all_inputssumfold)) + ((dst_positive_scale_inversion_all_inputssumfold) + (dst_positive_scale_inversion_all_inputssumfold))) + (((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) * S ((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) + ((dst_negative_scale_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)))) + ((((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) * S ((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) + ((dst_negative_scale_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold))) + (((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) * S ((dst_negative_code_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)) + ((dst_negative_scale_inversion_all_inputssumfold) + (dst_negative_scale_inversion_all_inputssumfold)))))) /\ (((exists fs_u_dst_inversion_all_inputssumfoldpositive fs_v_dst_inversion_all_inputssumfoldpositive. ((((exists fs_h_dst_inversion_all_inputssumfoldpositive_body_start. fs_h_dst_inversion_all_inputssumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_all_inputssumfoldpositive)) /\ exists fs_q_dst_inversion_all_inputssumfoldpositive_body_start. fs_u_dst_inversion_all_inputssumfoldpositive = fs_q_dst_inversion_all_inputssumfoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_all_inputssumfoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_all_inputssumfoldpositive_body_terminal. fs_h_dst_inversion_all_inputssumfoldpositive_body_terminal + S (dst_positive_sum_inversion_all_inputssumfold) = S ((S (S (mi_index_inversion_all_inputs))) * fs_v_dst_inversion_all_inputssumfoldpositive)) /\ exists fs_q_dst_inversion_all_inputssumfoldpositive_body_terminal. fs_u_dst_inversion_all_inputssumfoldpositive = fs_q_dst_inversion_all_inputssumfoldpositive_body_terminal * S ((S (S (mi_index_inversion_all_inputs))) * fs_v_dst_inversion_all_inputssumfoldpositive) + (dst_positive_sum_inversion_all_inputssumfold))) /\ forall fs_i_dst_inversion_all_inputssumfoldpositive_body_steps. (exists fs_lt_dst_inversion_all_inputssumfoldpositive_body_steps_bound. fs_lt_dst_inversion_all_inputssumfoldpositive_body_steps_bound + S fs_i_dst_inversion_all_inputssumfoldpositive_body_steps = S (mi_index_inversion_all_inputs)) -> exists fs_a_dst_inversion_all_inputssumfoldpositive_body_steps fs_r_dst_inversion_all_inputssumfoldpositive_body_steps fs_s_dst_inversion_all_inputssumfoldpositive_body_steps. ((((exists fs_h_dst_inversion_all_inputssumfoldpositive_body_steps_summand. fs_h_dst_inversion_all_inputssumfoldpositive_body_steps_summand + S (fs_a_dst_inversion_all_inputssumfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_all_inputssumfoldpositive_body_steps)) * dst_positive_scale_inversion_all_inputssumfold)) /\ exists fs_q_dst_inversion_all_inputssumfoldpositive_body_steps_summand. dst_positive_code_inversion_all_inputssumfold = fs_q_dst_inversion_all_inputssumfoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_all_inputssumfoldpositive_body_steps)) * dst_positive_scale_inversion_all_inputssumfold) + (fs_a_dst_inversion_all_inputssumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_all_inputssumfoldpositive_body_steps_partial. fs_h_dst_inversion_all_inputssumfoldpositive_body_steps_partial + S (fs_r_dst_inversion_all_inputssumfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_all_inputssumfoldpositive_body_steps)) * fs_v_dst_inversion_all_inputssumfoldpositive)) /\ exists fs_q_dst_inversion_all_inputssumfoldpositive_body_steps_partial. fs_u_dst_inversion_all_inputssumfoldpositive = fs_q_dst_inversion_all_inputssumfoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_all_inputssumfoldpositive_body_steps)) * fs_v_dst_inversion_all_inputssumfoldpositive) + (fs_r_dst_inversion_all_inputssumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_all_inputssumfoldpositive_body_steps_successor. fs_h_dst_inversion_all_inputssumfoldpositive_body_steps_successor + S (fs_s_dst_inversion_all_inputssumfoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_all_inputssumfoldpositive_body_steps)) * fs_v_dst_inversion_all_inputssumfoldpositive)) /\ exists fs_q_dst_inversion_all_inputssumfoldpositive_body_steps_successor. fs_u_dst_inversion_all_inputssumfoldpositive = fs_q_dst_inversion_all_inputssumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_all_inputssumfoldpositive_body_steps)) * fs_v_dst_inversion_all_inputssumfoldpositive) + (fs_s_dst_inversion_all_inputssumfoldpositive_body_steps))) /\ fs_s_dst_inversion_all_inputssumfoldpositive_body_steps = fs_r_dst_inversion_all_inputssumfoldpositive_body_steps + fs_a_dst_inversion_all_inputssumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_all_inputssumfoldnegative fs_v_dst_inversion_all_inputssumfoldnegative. ((((exists fs_h_dst_inversion_all_inputssumfoldnegative_body_start. fs_h_dst_inversion_all_inputssumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_all_inputssumfoldnegative)) /\ exists fs_q_dst_inversion_all_inputssumfoldnegative_body_start. fs_u_dst_inversion_all_inputssumfoldnegative = fs_q_dst_inversion_all_inputssumfoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_all_inputssumfoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_all_inputssumfoldnegative_body_terminal. fs_h_dst_inversion_all_inputssumfoldnegative_body_terminal + S (dst_negative_sum_inversion_all_inputssumfold) = S ((S (S (mi_index_inversion_all_inputs))) * fs_v_dst_inversion_all_inputssumfoldnegative)) /\ exists fs_q_dst_inversion_all_inputssumfoldnegative_body_terminal. fs_u_dst_inversion_all_inputssumfoldnegative = fs_q_dst_inversion_all_inputssumfoldnegative_body_terminal * S ((S (S (mi_index_inversion_all_inputs))) * fs_v_dst_inversion_all_inputssumfoldnegative) + (dst_negative_sum_inversion_all_inputssumfold))) /\ forall fs_i_dst_inversion_all_inputssumfoldnegative_body_steps. (exists fs_lt_dst_inversion_all_inputssumfoldnegative_body_steps_bound. fs_lt_dst_inversion_all_inputssumfoldnegative_body_steps_bound + S fs_i_dst_inversion_all_inputssumfoldnegative_body_steps = S (mi_index_inversion_all_inputs)) -> exists fs_a_dst_inversion_all_inputssumfoldnegative_body_steps fs_r_dst_inversion_all_inputssumfoldnegative_body_steps fs_s_dst_inversion_all_inputssumfoldnegative_body_steps. ((((exists fs_h_dst_inversion_all_inputssumfoldnegative_body_steps_summand. fs_h_dst_inversion_all_inputssumfoldnegative_body_steps_summand + S (fs_a_dst_inversion_all_inputssumfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_all_inputssumfoldnegative_body_steps)) * dst_negative_scale_inversion_all_inputssumfold)) /\ exists fs_q_dst_inversion_all_inputssumfoldnegative_body_steps_summand. dst_negative_code_inversion_all_inputssumfold = fs_q_dst_inversion_all_inputssumfoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_all_inputssumfoldnegative_body_steps)) * dst_negative_scale_inversion_all_inputssumfold) + (fs_a_dst_inversion_all_inputssumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_all_inputssumfoldnegative_body_steps_partial. fs_h_dst_inversion_all_inputssumfoldnegative_body_steps_partial + S (fs_r_dst_inversion_all_inputssumfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_all_inputssumfoldnegative_body_steps)) * fs_v_dst_inversion_all_inputssumfoldnegative)) /\ exists fs_q_dst_inversion_all_inputssumfoldnegative_body_steps_partial. fs_u_dst_inversion_all_inputssumfoldnegative = fs_q_dst_inversion_all_inputssumfoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_all_inputssumfoldnegative_body_steps)) * fs_v_dst_inversion_all_inputssumfoldnegative) + (fs_r_dst_inversion_all_inputssumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_all_inputssumfoldnegative_body_steps_successor. fs_h_dst_inversion_all_inputssumfoldnegative_body_steps_successor + S (fs_s_dst_inversion_all_inputssumfoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_all_inputssumfoldnegative_body_steps)) * fs_v_dst_inversion_all_inputssumfoldnegative)) /\ exists fs_q_dst_inversion_all_inputssumfoldnegative_body_steps_successor. fs_u_dst_inversion_all_inputssumfoldnegative = fs_q_dst_inversion_all_inputssumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_all_inputssumfoldnegative_body_steps)) * fs_v_dst_inversion_all_inputssumfoldnegative) + (fs_s_dst_inversion_all_inputssumfoldnegative_body_steps))) /\ fs_s_dst_inversion_all_inputssumfoldnegative_body_steps = fs_r_dst_inversion_all_inputssumfoldnegative_body_steps + fs_a_dst_inversion_all_inputssumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_all_inputssumfoldresult ge_balance_negative_inversion_all_inputssumfoldresult. (((((mi_value_inversion_all_inputs) = 2 * (ge_balance_positive_inversion_all_inputssumfoldresult) /\ (ge_balance_negative_inversion_all_inputssumfoldresult) = 0) \/ exists ge_signed_half_inversion_all_inputssumfoldresultdecode. (((mi_value_inversion_all_inputs) = 2 * ge_signed_half_inversion_all_inputssumfoldresultdecode + 1 /\ (ge_balance_positive_inversion_all_inputssumfoldresult) = 0) /\ (ge_balance_negative_inversion_all_inputssumfoldresult) = S ge_signed_half_inversion_all_inputssumfoldresultdecode))) /\ ((dst_positive_sum_inversion_all_inputssumfold) + ge_balance_negative_inversion_all_inputssumfoldresult = (dst_negative_sum_inversion_all_inputssumfold) + ge_balance_positive_inversion_all_inputssumfoldresult)))))))))))))) -> (((exists dst_positive_code_inversion_resultleft dst_positive_scale_inversion_resultleft dst_negative_code_inversion_resultleft dst_negative_scale_inversion_resultleft. (((M) = (((((dst_positive_code_inversion_resultleft) + (dst_positive_scale_inversion_resultleft)) * S ((dst_positive_code_inversion_resultleft) + (dst_positive_scale_inversion_resultleft)) + ((dst_positive_scale_inversion_resultleft) + (dst_positive_scale_inversion_resultleft))) + (((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) * S ((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) + ((dst_negative_scale_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)))) * S ((((dst_positive_code_inversion_resultleft) + (dst_positive_scale_inversion_resultleft)) * S ((dst_positive_code_inversion_resultleft) + (dst_positive_scale_inversion_resultleft)) + ((dst_positive_scale_inversion_resultleft) + (dst_positive_scale_inversion_resultleft))) + (((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) * S ((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) + ((dst_negative_scale_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)))) + ((((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) * S ((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) + ((dst_negative_scale_inversion_resultleft) + (dst_negative_scale_inversion_resultleft))) + (((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) * S ((dst_negative_code_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)) + ((dst_negative_scale_inversion_resultleft) + (dst_negative_scale_inversion_resultleft)))))) /\ (forall dst_index_inversion_resultleft. (exists pvs_le_gap_inversion_resultleftdomain. pvs_le_gap_inversion_resultleftdomain + (dst_index_inversion_resultleft) = (N)) -> exists dst_positive_inversion_resultleft dst_negative_inversion_resultleft dst_value_inversion_resultleft. ((((exists ff_h_pvs_inversion_resultleftentrypositive. ff_h_pvs_inversion_resultleftentrypositive + S (dst_positive_inversion_resultleft) = S ((S (dst_index_inversion_resultleft)) * dst_positive_scale_inversion_resultleft)) /\ exists ff_q_pvs_inversion_resultleftentrypositive. dst_positive_code_inversion_resultleft = ff_q_pvs_inversion_resultleftentrypositive * S ((S (dst_index_inversion_resultleft)) * dst_positive_scale_inversion_resultleft) + (dst_positive_inversion_resultleft))) /\ (((((exists ff_h_pvs_inversion_resultleftentrynegative. ff_h_pvs_inversion_resultleftentrynegative + S (dst_negative_inversion_resultleft) = S ((S (dst_index_inversion_resultleft)) * dst_negative_scale_inversion_resultleft)) /\ exists ff_q_pvs_inversion_resultleftentrynegative. dst_negative_code_inversion_resultleft = ff_q_pvs_inversion_resultleftentrynegative * S ((S (dst_index_inversion_resultleft)) * dst_negative_scale_inversion_resultleft) + (dst_negative_inversion_resultleft))) /\ (exists ge_balance_positive_inversion_resultleftentryvalue ge_balance_negative_inversion_resultleftentryvalue. (((((dst_value_inversion_resultleft) = 2 * (ge_balance_positive_inversion_resultleftentryvalue) /\ (ge_balance_negative_inversion_resultleftentryvalue) = 0) \/ exists ge_signed_half_inversion_resultleftentryvaluedecode. (((dst_value_inversion_resultleft) = 2 * ge_signed_half_inversion_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_inversion_resultleftentryvalue) = 0) /\ (ge_balance_negative_inversion_resultleftentryvalue) = S ge_signed_half_inversion_resultleftentryvaluedecode))) /\ ((dst_positive_inversion_resultleft) + ge_balance_negative_inversion_resultleftentryvalue = (dst_negative_inversion_resultleft) + ge_balance_positive_inversion_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_inversion_resultright dst_positive_scale_inversion_resultright dst_negative_code_inversion_resultright dst_negative_scale_inversion_resultright. (((G) = (((((dst_positive_code_inversion_resultright) + (dst_positive_scale_inversion_resultright)) * S ((dst_positive_code_inversion_resultright) + (dst_positive_scale_inversion_resultright)) + ((dst_positive_scale_inversion_resultright) + (dst_positive_scale_inversion_resultright))) + (((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) * S ((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) + ((dst_negative_scale_inversion_resultright) + (dst_negative_scale_inversion_resultright)))) * S ((((dst_positive_code_inversion_resultright) + (dst_positive_scale_inversion_resultright)) * S ((dst_positive_code_inversion_resultright) + (dst_positive_scale_inversion_resultright)) + ((dst_positive_scale_inversion_resultright) + (dst_positive_scale_inversion_resultright))) + (((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) * S ((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) + ((dst_negative_scale_inversion_resultright) + (dst_negative_scale_inversion_resultright)))) + ((((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) * S ((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) + ((dst_negative_scale_inversion_resultright) + (dst_negative_scale_inversion_resultright))) + (((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) * S ((dst_negative_code_inversion_resultright) + (dst_negative_scale_inversion_resultright)) + ((dst_negative_scale_inversion_resultright) + (dst_negative_scale_inversion_resultright)))))) /\ (forall dst_index_inversion_resultright. (exists pvs_le_gap_inversion_resultrightdomain. pvs_le_gap_inversion_resultrightdomain + (dst_index_inversion_resultright) = (N)) -> exists dst_positive_inversion_resultright dst_negative_inversion_resultright dst_value_inversion_resultright. ((((exists ff_h_pvs_inversion_resultrightentrypositive. ff_h_pvs_inversion_resultrightentrypositive + S (dst_positive_inversion_resultright) = S ((S (dst_index_inversion_resultright)) * dst_positive_scale_inversion_resultright)) /\ exists ff_q_pvs_inversion_resultrightentrypositive. dst_positive_code_inversion_resultright = ff_q_pvs_inversion_resultrightentrypositive * S ((S (dst_index_inversion_resultright)) * dst_positive_scale_inversion_resultright) + (dst_positive_inversion_resultright))) /\ (((((exists ff_h_pvs_inversion_resultrightentrynegative. ff_h_pvs_inversion_resultrightentrynegative + S (dst_negative_inversion_resultright) = S ((S (dst_index_inversion_resultright)) * dst_negative_scale_inversion_resultright)) /\ exists ff_q_pvs_inversion_resultrightentrynegative. dst_negative_code_inversion_resultright = ff_q_pvs_inversion_resultrightentrynegative * S ((S (dst_index_inversion_resultright)) * dst_negative_scale_inversion_resultright) + (dst_negative_inversion_resultright))) /\ (exists ge_balance_positive_inversion_resultrightentryvalue ge_balance_negative_inversion_resultrightentryvalue. (((((dst_value_inversion_resultright) = 2 * (ge_balance_positive_inversion_resultrightentryvalue) /\ (ge_balance_negative_inversion_resultrightentryvalue) = 0) \/ exists ge_signed_half_inversion_resultrightentryvaluedecode. (((dst_value_inversion_resultright) = 2 * ge_signed_half_inversion_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_inversion_resultrightentryvalue) = 0) /\ (ge_balance_negative_inversion_resultrightentryvalue) = S ge_signed_half_inversion_resultrightentryvaluedecode))) /\ ((dst_positive_inversion_resultright) + ge_balance_negative_inversion_resultrightentryvalue = (dst_negative_inversion_resultright) + ge_balance_positive_inversion_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_inversion_resulttable dst_positive_scale_inversion_resulttable dst_negative_code_inversion_resulttable dst_negative_scale_inversion_resulttable. (((F) = (((((dst_positive_code_inversion_resulttable) + (dst_positive_scale_inversion_resulttable)) * S ((dst_positive_code_inversion_resulttable) + (dst_positive_scale_inversion_resulttable)) + ((dst_positive_scale_inversion_resulttable) + (dst_positive_scale_inversion_resulttable))) + (((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) * S ((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) + ((dst_negative_scale_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)))) * S ((((dst_positive_code_inversion_resulttable) + (dst_positive_scale_inversion_resulttable)) * S ((dst_positive_code_inversion_resulttable) + (dst_positive_scale_inversion_resulttable)) + ((dst_positive_scale_inversion_resulttable) + (dst_positive_scale_inversion_resulttable))) + (((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) * S ((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) + ((dst_negative_scale_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)))) + ((((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) * S ((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) + ((dst_negative_scale_inversion_resulttable) + (dst_negative_scale_inversion_resulttable))) + (((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) * S ((dst_negative_code_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)) + ((dst_negative_scale_inversion_resulttable) + (dst_negative_scale_inversion_resulttable)))))) /\ (forall dst_index_inversion_resulttable. (exists pvs_le_gap_inversion_resulttabledomain. pvs_le_gap_inversion_resulttabledomain + (dst_index_inversion_resulttable) = (N)) -> exists dst_positive_inversion_resulttable dst_negative_inversion_resulttable dst_value_inversion_resulttable. ((((exists ff_h_pvs_inversion_resulttableentrypositive. ff_h_pvs_inversion_resulttableentrypositive + S (dst_positive_inversion_resulttable) = S ((S (dst_index_inversion_resulttable)) * dst_positive_scale_inversion_resulttable)) /\ exists ff_q_pvs_inversion_resulttableentrypositive. dst_positive_code_inversion_resulttable = ff_q_pvs_inversion_resulttableentrypositive * S ((S (dst_index_inversion_resulttable)) * dst_positive_scale_inversion_resulttable) + (dst_positive_inversion_resulttable))) /\ (((((exists ff_h_pvs_inversion_resulttableentrynegative. ff_h_pvs_inversion_resulttableentrynegative + S (dst_negative_inversion_resulttable) = S ((S (dst_index_inversion_resulttable)) * dst_negative_scale_inversion_resulttable)) /\ exists ff_q_pvs_inversion_resulttableentrynegative. dst_negative_code_inversion_resulttable = ff_q_pvs_inversion_resulttableentrynegative * S ((S (dst_index_inversion_resulttable)) * dst_negative_scale_inversion_resulttable) + (dst_negative_inversion_resulttable))) /\ (exists ge_balance_positive_inversion_resulttableentryvalue ge_balance_negative_inversion_resulttableentryvalue. (((((dst_value_inversion_resulttable) = 2 * (ge_balance_positive_inversion_resulttableentryvalue) /\ (ge_balance_negative_inversion_resulttableentryvalue) = 0) \/ exists ge_signed_half_inversion_resulttableentryvaluedecode. (((dst_value_inversion_resulttable) = 2 * ge_signed_half_inversion_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_resulttableentryvalue) = 0) /\ (ge_balance_negative_inversion_resulttableentryvalue) = S ge_signed_half_inversion_resulttableentryvaluedecode))) /\ ((dst_positive_inversion_resulttable) + ge_balance_negative_inversion_resulttableentryvalue = (dst_negative_inversion_resulttable) + ge_balance_positive_inversion_resulttableentryvalue))))))))) /\ (forall dc_input_inversion_result dc_output_inversion_result. ~(dc_input_inversion_result=0) -> (exists pvs_le_gap_inversion_resultdomain. pvs_le_gap_inversion_resultdomain + (dc_input_inversion_result) = (N)) -> (exists dst_positive_code_inversion_resultlookup dst_positive_scale_inversion_resultlookup dst_negative_code_inversion_resultlookup dst_negative_scale_inversion_resultlookup dst_positive_inversion_resultlookup dst_negative_inversion_resultlookup. (((F) = (((((dst_positive_code_inversion_resultlookup) + (dst_positive_scale_inversion_resultlookup)) * S ((dst_positive_code_inversion_resultlookup) + (dst_positive_scale_inversion_resultlookup)) + ((dst_positive_scale_inversion_resultlookup) + (dst_positive_scale_inversion_resultlookup))) + (((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) * S ((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) + ((dst_negative_scale_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)))) * S ((((dst_positive_code_inversion_resultlookup) + (dst_positive_scale_inversion_resultlookup)) * S ((dst_positive_code_inversion_resultlookup) + (dst_positive_scale_inversion_resultlookup)) + ((dst_positive_scale_inversion_resultlookup) + (dst_positive_scale_inversion_resultlookup))) + (((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) * S ((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) + ((dst_negative_scale_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)))) + ((((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) * S ((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) + ((dst_negative_scale_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup))) + (((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) * S ((dst_negative_code_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)) + ((dst_negative_scale_inversion_resultlookup) + (dst_negative_scale_inversion_resultlookup)))))) /\ (((((exists ff_h_pvs_inversion_resultlookuppositive. ff_h_pvs_inversion_resultlookuppositive + S (dst_positive_inversion_resultlookup) = S ((S (dc_input_inversion_result)) * dst_positive_scale_inversion_resultlookup)) /\ exists ff_q_pvs_inversion_resultlookuppositive. dst_positive_code_inversion_resultlookup = ff_q_pvs_inversion_resultlookuppositive * S ((S (dc_input_inversion_result)) * dst_positive_scale_inversion_resultlookup) + (dst_positive_inversion_resultlookup))) /\ (((((exists ff_h_pvs_inversion_resultlookupnegative. ff_h_pvs_inversion_resultlookupnegative + S (dst_negative_inversion_resultlookup) = S ((S (dc_input_inversion_result)) * dst_negative_scale_inversion_resultlookup)) /\ exists ff_q_pvs_inversion_resultlookupnegative. dst_negative_code_inversion_resultlookup = ff_q_pvs_inversion_resultlookupnegative * S ((S (dc_input_inversion_result)) * dst_negative_scale_inversion_resultlookup) + (dst_negative_inversion_resultlookup))) /\ (exists ge_balance_positive_inversion_resultlookupvalue ge_balance_negative_inversion_resultlookupvalue. (((((dc_output_inversion_result) = 2 * (ge_balance_positive_inversion_resultlookupvalue) /\ (ge_balance_negative_inversion_resultlookupvalue) = 0) \/ exists ge_signed_half_inversion_resultlookupvaluedecode. (((dc_output_inversion_result) = 2 * ge_signed_half_inversion_resultlookupvaluedecode + 1 /\ (ge_balance_positive_inversion_resultlookupvalue) = 0) /\ (ge_balance_negative_inversion_resultlookupvalue) = S ge_signed_half_inversion_resultlookupvaluedecode))) /\ ((dst_positive_inversion_resultlookup) + ge_balance_negative_inversion_resultlookupvalue = (dst_negative_inversion_resultlookup) + ge_balance_positive_inversion_resultlookupvalue))))))))) -> (((~((dc_input_inversion_result)=0)) /\ (exists dc_mask_inversion_resultvalue. ((((exists dst_positive_code_inversion_resultvaluemasktable dst_positive_scale_inversion_resultvaluemasktable dst_negative_code_inversion_resultvaluemasktable dst_negative_scale_inversion_resultvaluemasktable. (((dc_mask_inversion_resultvalue) = (((((dst_positive_code_inversion_resultvaluemasktable) + (dst_positive_scale_inversion_resultvaluemasktable)) * S ((dst_positive_code_inversion_resultvaluemasktable) + (dst_positive_scale_inversion_resultvaluemasktable)) + ((dst_positive_scale_inversion_resultvaluemasktable) + (dst_positive_scale_inversion_resultvaluemasktable))) + (((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) * S ((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) + ((dst_negative_scale_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)))) * S ((((dst_positive_code_inversion_resultvaluemasktable) + (dst_positive_scale_inversion_resultvaluemasktable)) * S ((dst_positive_code_inversion_resultvaluemasktable) + (dst_positive_scale_inversion_resultvaluemasktable)) + ((dst_positive_scale_inversion_resultvaluemasktable) + (dst_positive_scale_inversion_resultvaluemasktable))) + (((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) * S ((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) + ((dst_negative_scale_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)))) + ((((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) * S ((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) + ((dst_negative_scale_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable))) + (((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) * S ((dst_negative_code_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)) + ((dst_negative_scale_inversion_resultvaluemasktable) + (dst_negative_scale_inversion_resultvaluemasktable)))))) /\ (forall dst_index_inversion_resultvaluemasktable. (exists pvs_le_gap_inversion_resultvaluemasktabledomain. pvs_le_gap_inversion_resultvaluemasktabledomain + (dst_index_inversion_resultvaluemasktable) = (dc_input_inversion_result)) -> exists dst_positive_inversion_resultvaluemasktable dst_negative_inversion_resultvaluemasktable dst_value_inversion_resultvaluemasktable. ((((exists ff_h_pvs_inversion_resultvaluemasktableentrypositive. ff_h_pvs_inversion_resultvaluemasktableentrypositive + S (dst_positive_inversion_resultvaluemasktable) = S ((S (dst_index_inversion_resultvaluemasktable)) * dst_positive_scale_inversion_resultvaluemasktable)) /\ exists ff_q_pvs_inversion_resultvaluemasktableentrypositive. dst_positive_code_inversion_resultvaluemasktable = ff_q_pvs_inversion_resultvaluemasktableentrypositive * S ((S (dst_index_inversion_resultvaluemasktable)) * dst_positive_scale_inversion_resultvaluemasktable) + (dst_positive_inversion_resultvaluemasktable))) /\ (((((exists ff_h_pvs_inversion_resultvaluemasktableentrynegative. ff_h_pvs_inversion_resultvaluemasktableentrynegative + S (dst_negative_inversion_resultvaluemasktable) = S ((S (dst_index_inversion_resultvaluemasktable)) * dst_negative_scale_inversion_resultvaluemasktable)) /\ exists ff_q_pvs_inversion_resultvaluemasktableentrynegative. dst_negative_code_inversion_resultvaluemasktable = ff_q_pvs_inversion_resultvaluemasktableentrynegative * S ((S (dst_index_inversion_resultvaluemasktable)) * dst_negative_scale_inversion_resultvaluemasktable) + (dst_negative_inversion_resultvaluemasktable))) /\ (exists ge_balance_positive_inversion_resultvaluemasktableentryvalue ge_balance_negative_inversion_resultvaluemasktableentryvalue. (((((dst_value_inversion_resultvaluemasktable) = 2 * (ge_balance_positive_inversion_resultvaluemasktableentryvalue) /\ (ge_balance_negative_inversion_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_resultvaluemasktableentryvaluedecode. (((dst_value_inversion_resultvaluemasktable) = 2 * ge_signed_half_inversion_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_resultvaluemasktableentryvalue) = S ge_signed_half_inversion_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_inversion_resultvaluemasktable) + ge_balance_negative_inversion_resultvaluemasktableentryvalue = (dst_negative_inversion_resultvaluemasktable) + ge_balance_positive_inversion_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_inversion_resultvaluemask dc_value_inversion_resultvaluemask. (exists pvs_le_gap_inversion_resultvaluemaskdomain. pvs_le_gap_inversion_resultvaluemaskdomain + (dc_index_inversion_resultvaluemask) = (dc_input_inversion_result)) -> (exists dst_positive_code_inversion_resultvaluemasklookup dst_positive_scale_inversion_resultvaluemasklookup dst_negative_code_inversion_resultvaluemasklookup dst_negative_scale_inversion_resultvaluemasklookup dst_positive_inversion_resultvaluemasklookup dst_negative_inversion_resultvaluemasklookup. (((dc_mask_inversion_resultvalue) = (((((dst_positive_code_inversion_resultvaluemasklookup) + (dst_positive_scale_inversion_resultvaluemasklookup)) * S ((dst_positive_code_inversion_resultvaluemasklookup) + (dst_positive_scale_inversion_resultvaluemasklookup)) + ((dst_positive_scale_inversion_resultvaluemasklookup) + (dst_positive_scale_inversion_resultvaluemasklookup))) + (((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) * S ((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) + ((dst_negative_scale_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)))) * S ((((dst_positive_code_inversion_resultvaluemasklookup) + (dst_positive_scale_inversion_resultvaluemasklookup)) * S ((dst_positive_code_inversion_resultvaluemasklookup) + (dst_positive_scale_inversion_resultvaluemasklookup)) + ((dst_positive_scale_inversion_resultvaluemasklookup) + (dst_positive_scale_inversion_resultvaluemasklookup))) + (((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) * S ((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) + ((dst_negative_scale_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)))) + ((((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) * S ((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) + ((dst_negative_scale_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup))) + (((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) * S ((dst_negative_code_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)) + ((dst_negative_scale_inversion_resultvaluemasklookup) + (dst_negative_scale_inversion_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inversion_resultvaluemasklookuppositive. ff_h_pvs_inversion_resultvaluemasklookuppositive + S (dst_positive_inversion_resultvaluemasklookup) = S ((S (dc_index_inversion_resultvaluemask)) * dst_positive_scale_inversion_resultvaluemasklookup)) /\ exists ff_q_pvs_inversion_resultvaluemasklookuppositive. dst_positive_code_inversion_resultvaluemasklookup = ff_q_pvs_inversion_resultvaluemasklookuppositive * S ((S (dc_index_inversion_resultvaluemask)) * dst_positive_scale_inversion_resultvaluemasklookup) + (dst_positive_inversion_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_inversion_resultvaluemasklookupnegative. ff_h_pvs_inversion_resultvaluemasklookupnegative + S (dst_negative_inversion_resultvaluemasklookup) = S ((S (dc_index_inversion_resultvaluemask)) * dst_negative_scale_inversion_resultvaluemasklookup)) /\ exists ff_q_pvs_inversion_resultvaluemasklookupnegative. dst_negative_code_inversion_resultvaluemasklookup = ff_q_pvs_inversion_resultvaluemasklookupnegative * S ((S (dc_index_inversion_resultvaluemask)) * dst_negative_scale_inversion_resultvaluemasklookup) + (dst_negative_inversion_resultvaluemasklookup))) /\ (exists ge_balance_positive_inversion_resultvaluemasklookupvalue ge_balance_negative_inversion_resultvaluemasklookupvalue. (((((dc_value_inversion_resultvaluemask) = 2 * (ge_balance_positive_inversion_resultvaluemasklookupvalue) /\ (ge_balance_negative_inversion_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inversion_resultvaluemasklookupvaluedecode. (((dc_value_inversion_resultvaluemask) = 2 * ge_signed_half_inversion_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inversion_resultvaluemasklookupvalue) = S ge_signed_half_inversion_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_inversion_resultvaluemasklookup) + ge_balance_negative_inversion_resultvaluemasklookupvalue = (dst_negative_inversion_resultvaluemasklookup) + ge_balance_positive_inversion_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_inversion_resultvaluemask)=0)) /\ (exists dc_quotient_inversion_resultvaluemaskentry dc_left_inversion_resultvaluemaskentry dc_right_inversion_resultvaluemaskentry. (((dc_input_inversion_result)=(dc_index_inversion_resultvaluemask)*dc_quotient_inversion_resultvaluemaskentry) /\ (((exists dst_positive_code_inversion_resultvaluemaskentryleft dst_positive_scale_inversion_resultvaluemaskentryleft dst_negative_code_inversion_resultvaluemaskentryleft dst_negative_scale_inversion_resultvaluemaskentryleft dst_positive_inversion_resultvaluemaskentryleft dst_negative_inversion_resultvaluemaskentryleft. (((M) = (((((dst_positive_code_inversion_resultvaluemaskentryleft) + (dst_positive_scale_inversion_resultvaluemaskentryleft)) * S ((dst_positive_code_inversion_resultvaluemaskentryleft) + (dst_positive_scale_inversion_resultvaluemaskentryleft)) + ((dst_positive_scale_inversion_resultvaluemaskentryleft) + (dst_positive_scale_inversion_resultvaluemaskentryleft))) + (((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) * S ((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) + ((dst_negative_scale_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)))) * S ((((dst_positive_code_inversion_resultvaluemaskentryleft) + (dst_positive_scale_inversion_resultvaluemaskentryleft)) * S ((dst_positive_code_inversion_resultvaluemaskentryleft) + (dst_positive_scale_inversion_resultvaluemaskentryleft)) + ((dst_positive_scale_inversion_resultvaluemaskentryleft) + (dst_positive_scale_inversion_resultvaluemaskentryleft))) + (((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) * S ((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) + ((dst_negative_scale_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)))) + ((((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) * S ((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) + ((dst_negative_scale_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft))) + (((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) * S ((dst_negative_code_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)) + ((dst_negative_scale_inversion_resultvaluemaskentryleft) + (dst_negative_scale_inversion_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inversion_resultvaluemaskentryleftpositive. ff_h_pvs_inversion_resultvaluemaskentryleftpositive + S (dst_positive_inversion_resultvaluemaskentryleft) = S ((S (dc_index_inversion_resultvaluemask)) * dst_positive_scale_inversion_resultvaluemaskentryleft)) /\ exists ff_q_pvs_inversion_resultvaluemaskentryleftpositive. dst_positive_code_inversion_resultvaluemaskentryleft = ff_q_pvs_inversion_resultvaluemaskentryleftpositive * S ((S (dc_index_inversion_resultvaluemask)) * dst_positive_scale_inversion_resultvaluemaskentryleft) + (dst_positive_inversion_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inversion_resultvaluemaskentryleftnegative. ff_h_pvs_inversion_resultvaluemaskentryleftnegative + S (dst_negative_inversion_resultvaluemaskentryleft) = S ((S (dc_index_inversion_resultvaluemask)) * dst_negative_scale_inversion_resultvaluemaskentryleft)) /\ exists ff_q_pvs_inversion_resultvaluemaskentryleftnegative. dst_negative_code_inversion_resultvaluemaskentryleft = ff_q_pvs_inversion_resultvaluemaskentryleftnegative * S ((S (dc_index_inversion_resultvaluemask)) * dst_negative_scale_inversion_resultvaluemaskentryleft) + (dst_negative_inversion_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_inversion_resultvaluemaskentryleftvalue ge_balance_negative_inversion_resultvaluemaskentryleftvalue. (((((dc_left_inversion_resultvaluemaskentry) = 2 * (ge_balance_positive_inversion_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_inversion_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inversion_resultvaluemaskentryleftvaluedecode. (((dc_left_inversion_resultvaluemaskentry) = 2 * ge_signed_half_inversion_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inversion_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inversion_resultvaluemaskentryleftvalue) = S ge_signed_half_inversion_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inversion_resultvaluemaskentryleft) + ge_balance_negative_inversion_resultvaluemaskentryleftvalue = (dst_negative_inversion_resultvaluemaskentryleft) + ge_balance_positive_inversion_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inversion_resultvaluemaskentryright dst_positive_scale_inversion_resultvaluemaskentryright dst_negative_code_inversion_resultvaluemaskentryright dst_negative_scale_inversion_resultvaluemaskentryright dst_positive_inversion_resultvaluemaskentryright dst_negative_inversion_resultvaluemaskentryright. (((G) = (((((dst_positive_code_inversion_resultvaluemaskentryright) + (dst_positive_scale_inversion_resultvaluemaskentryright)) * S ((dst_positive_code_inversion_resultvaluemaskentryright) + (dst_positive_scale_inversion_resultvaluemaskentryright)) + ((dst_positive_scale_inversion_resultvaluemaskentryright) + (dst_positive_scale_inversion_resultvaluemaskentryright))) + (((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) * S ((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) + ((dst_negative_scale_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)))) * S ((((dst_positive_code_inversion_resultvaluemaskentryright) + (dst_positive_scale_inversion_resultvaluemaskentryright)) * S ((dst_positive_code_inversion_resultvaluemaskentryright) + (dst_positive_scale_inversion_resultvaluemaskentryright)) + ((dst_positive_scale_inversion_resultvaluemaskentryright) + (dst_positive_scale_inversion_resultvaluemaskentryright))) + (((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) * S ((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) + ((dst_negative_scale_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)))) + ((((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) * S ((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) + ((dst_negative_scale_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright))) + (((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) * S ((dst_negative_code_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)) + ((dst_negative_scale_inversion_resultvaluemaskentryright) + (dst_negative_scale_inversion_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inversion_resultvaluemaskentryrightpositive. ff_h_pvs_inversion_resultvaluemaskentryrightpositive + S (dst_positive_inversion_resultvaluemaskentryright) = S ((S (dc_quotient_inversion_resultvaluemaskentry)) * dst_positive_scale_inversion_resultvaluemaskentryright)) /\ exists ff_q_pvs_inversion_resultvaluemaskentryrightpositive. dst_positive_code_inversion_resultvaluemaskentryright = ff_q_pvs_inversion_resultvaluemaskentryrightpositive * S ((S (dc_quotient_inversion_resultvaluemaskentry)) * dst_positive_scale_inversion_resultvaluemaskentryright) + (dst_positive_inversion_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_inversion_resultvaluemaskentryrightnegative. ff_h_pvs_inversion_resultvaluemaskentryrightnegative + S (dst_negative_inversion_resultvaluemaskentryright) = S ((S (dc_quotient_inversion_resultvaluemaskentry)) * dst_negative_scale_inversion_resultvaluemaskentryright)) /\ exists ff_q_pvs_inversion_resultvaluemaskentryrightnegative. dst_negative_code_inversion_resultvaluemaskentryright = ff_q_pvs_inversion_resultvaluemaskentryrightnegative * S ((S (dc_quotient_inversion_resultvaluemaskentry)) * dst_negative_scale_inversion_resultvaluemaskentryright) + (dst_negative_inversion_resultvaluemaskentryright))) /\ (exists ge_balance_positive_inversion_resultvaluemaskentryrightvalue ge_balance_negative_inversion_resultvaluemaskentryrightvalue. (((((dc_right_inversion_resultvaluemaskentry) = 2 * (ge_balance_positive_inversion_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_inversion_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inversion_resultvaluemaskentryrightvaluedecode. (((dc_right_inversion_resultvaluemaskentry) = 2 * ge_signed_half_inversion_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inversion_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inversion_resultvaluemaskentryrightvalue) = S ge_signed_half_inversion_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inversion_resultvaluemaskentryright) + ge_balance_negative_inversion_resultvaluemaskentryrightvalue = (dst_negative_inversion_resultvaluemaskentryright) + ge_balance_positive_inversion_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inversion_resultvaluemaskentryproduct sto_an_inversion_resultvaluemaskentryproduct sto_bp_inversion_resultvaluemaskentryproduct sto_bn_inversion_resultvaluemaskentryproduct sto_cp_inversion_resultvaluemaskentryproduct sto_cn_inversion_resultvaluemaskentryproduct. (((((dc_left_inversion_resultvaluemaskentry) = 2 * (sto_ap_inversion_resultvaluemaskentryproduct) /\ (sto_an_inversion_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_resultvaluemaskentryproductleft. (((dc_left_inversion_resultvaluemaskentry) = 2 * ge_signed_half_inversion_resultvaluemaskentryproductleft + 1 /\ (sto_ap_inversion_resultvaluemaskentryproduct) = 0) /\ (sto_an_inversion_resultvaluemaskentryproduct) = S ge_signed_half_inversion_resultvaluemaskentryproductleft))) /\ ((((((dc_right_inversion_resultvaluemaskentry) = 2 * (sto_bp_inversion_resultvaluemaskentryproduct) /\ (sto_bn_inversion_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_resultvaluemaskentryproductright. (((dc_right_inversion_resultvaluemaskentry) = 2 * ge_signed_half_inversion_resultvaluemaskentryproductright + 1 /\ (sto_bp_inversion_resultvaluemaskentryproduct) = 0) /\ (sto_bn_inversion_resultvaluemaskentryproduct) = S ge_signed_half_inversion_resultvaluemaskentryproductright))) /\ ((((((dc_value_inversion_resultvaluemask) = 2 * (sto_cp_inversion_resultvaluemaskentryproduct) /\ (sto_cn_inversion_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_resultvaluemaskentryproductoutput. (((dc_value_inversion_resultvaluemask) = 2 * ge_signed_half_inversion_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_inversion_resultvaluemaskentryproduct) = 0) /\ (sto_cn_inversion_resultvaluemaskentryproduct) = S ge_signed_half_inversion_resultvaluemaskentryproductoutput))) /\ ((sto_ap_inversion_resultvaluemaskentryproduct * sto_bp_inversion_resultvaluemaskentryproduct + sto_an_inversion_resultvaluemaskentryproduct * sto_bn_inversion_resultvaluemaskentryproduct) + sto_cn_inversion_resultvaluemaskentryproduct = (sto_ap_inversion_resultvaluemaskentryproduct * sto_bn_inversion_resultvaluemaskentryproduct + sto_an_inversion_resultvaluemaskentryproduct * sto_bp_inversion_resultvaluemaskentryproduct) + sto_cp_inversion_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inversion_resultvaluemask)=0 \/ ~(exists pvs_factor_inversion_resultvaluemaskentrynondivisor. (dc_input_inversion_result) = (dc_index_inversion_resultvaluemask) * pvs_factor_inversion_resultvaluemaskentrynondivisor)) /\ ((dc_value_inversion_resultvaluemask)=0))))))) /\ (exists dst_positive_code_inversion_resultvaluefold dst_positive_scale_inversion_resultvaluefold dst_negative_code_inversion_resultvaluefold dst_negative_scale_inversion_resultvaluefold dst_positive_sum_inversion_resultvaluefold dst_negative_sum_inversion_resultvaluefold. (((dc_mask_inversion_resultvalue) = (((((dst_positive_code_inversion_resultvaluefold) + (dst_positive_scale_inversion_resultvaluefold)) * S ((dst_positive_code_inversion_resultvaluefold) + (dst_positive_scale_inversion_resultvaluefold)) + ((dst_positive_scale_inversion_resultvaluefold) + (dst_positive_scale_inversion_resultvaluefold))) + (((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) * S ((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) + ((dst_negative_scale_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)))) * S ((((dst_positive_code_inversion_resultvaluefold) + (dst_positive_scale_inversion_resultvaluefold)) * S ((dst_positive_code_inversion_resultvaluefold) + (dst_positive_scale_inversion_resultvaluefold)) + ((dst_positive_scale_inversion_resultvaluefold) + (dst_positive_scale_inversion_resultvaluefold))) + (((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) * S ((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) + ((dst_negative_scale_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)))) + ((((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) * S ((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) + ((dst_negative_scale_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold))) + (((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) * S ((dst_negative_code_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)) + ((dst_negative_scale_inversion_resultvaluefold) + (dst_negative_scale_inversion_resultvaluefold)))))) /\ (((exists fs_u_dst_inversion_resultvaluefoldpositive fs_v_dst_inversion_resultvaluefoldpositive. ((((exists fs_h_dst_inversion_resultvaluefoldpositive_body_start. fs_h_dst_inversion_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_resultvaluefoldpositive)) /\ exists fs_q_dst_inversion_resultvaluefoldpositive_body_start. fs_u_dst_inversion_resultvaluefoldpositive = fs_q_dst_inversion_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_resultvaluefoldpositive_body_terminal. fs_h_dst_inversion_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_inversion_resultvaluefold) = S ((S (S (dc_input_inversion_result))) * fs_v_dst_inversion_resultvaluefoldpositive)) /\ exists fs_q_dst_inversion_resultvaluefoldpositive_body_terminal. fs_u_dst_inversion_resultvaluefoldpositive = fs_q_dst_inversion_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_inversion_result))) * fs_v_dst_inversion_resultvaluefoldpositive) + (dst_positive_sum_inversion_resultvaluefold))) /\ forall fs_i_dst_inversion_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_inversion_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_inversion_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_inversion_resultvaluefoldpositive_body_steps = S (dc_input_inversion_result)) -> exists fs_a_dst_inversion_resultvaluefoldpositive_body_steps fs_r_dst_inversion_resultvaluefoldpositive_body_steps fs_s_dst_inversion_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_inversion_resultvaluefoldpositive_body_steps_summand. fs_h_dst_inversion_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_inversion_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inversion_resultvaluefoldpositive_body_steps)) * dst_positive_scale_inversion_resultvaluefold)) /\ exists fs_q_dst_inversion_resultvaluefoldpositive_body_steps_summand. dst_positive_code_inversion_resultvaluefold = fs_q_dst_inversion_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_resultvaluefoldpositive_body_steps)) * dst_positive_scale_inversion_resultvaluefold) + (fs_a_dst_inversion_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_resultvaluefoldpositive_body_steps_partial. fs_h_dst_inversion_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_inversion_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inversion_resultvaluefoldpositive_body_steps)) * fs_v_dst_inversion_resultvaluefoldpositive)) /\ exists fs_q_dst_inversion_resultvaluefoldpositive_body_steps_partial. fs_u_dst_inversion_resultvaluefoldpositive = fs_q_dst_inversion_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_resultvaluefoldpositive_body_steps)) * fs_v_dst_inversion_resultvaluefoldpositive) + (fs_r_dst_inversion_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_resultvaluefoldpositive_body_steps_successor. fs_h_dst_inversion_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_inversion_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_resultvaluefoldpositive_body_steps)) * fs_v_dst_inversion_resultvaluefoldpositive)) /\ exists fs_q_dst_inversion_resultvaluefoldpositive_body_steps_successor. fs_u_dst_inversion_resultvaluefoldpositive = fs_q_dst_inversion_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_resultvaluefoldpositive_body_steps)) * fs_v_dst_inversion_resultvaluefoldpositive) + (fs_s_dst_inversion_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_inversion_resultvaluefoldpositive_body_steps = fs_r_dst_inversion_resultvaluefoldpositive_body_steps + fs_a_dst_inversion_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_resultvaluefoldnegative fs_v_dst_inversion_resultvaluefoldnegative. ((((exists fs_h_dst_inversion_resultvaluefoldnegative_body_start. fs_h_dst_inversion_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_resultvaluefoldnegative)) /\ exists fs_q_dst_inversion_resultvaluefoldnegative_body_start. fs_u_dst_inversion_resultvaluefoldnegative = fs_q_dst_inversion_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_resultvaluefoldnegative_body_terminal. fs_h_dst_inversion_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_inversion_resultvaluefold) = S ((S (S (dc_input_inversion_result))) * fs_v_dst_inversion_resultvaluefoldnegative)) /\ exists fs_q_dst_inversion_resultvaluefoldnegative_body_terminal. fs_u_dst_inversion_resultvaluefoldnegative = fs_q_dst_inversion_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_inversion_result))) * fs_v_dst_inversion_resultvaluefoldnegative) + (dst_negative_sum_inversion_resultvaluefold))) /\ forall fs_i_dst_inversion_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_inversion_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_inversion_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_inversion_resultvaluefoldnegative_body_steps = S (dc_input_inversion_result)) -> exists fs_a_dst_inversion_resultvaluefoldnegative_body_steps fs_r_dst_inversion_resultvaluefoldnegative_body_steps fs_s_dst_inversion_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_inversion_resultvaluefoldnegative_body_steps_summand. fs_h_dst_inversion_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_inversion_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inversion_resultvaluefoldnegative_body_steps)) * dst_negative_scale_inversion_resultvaluefold)) /\ exists fs_q_dst_inversion_resultvaluefoldnegative_body_steps_summand. dst_negative_code_inversion_resultvaluefold = fs_q_dst_inversion_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_resultvaluefoldnegative_body_steps)) * dst_negative_scale_inversion_resultvaluefold) + (fs_a_dst_inversion_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_resultvaluefoldnegative_body_steps_partial. fs_h_dst_inversion_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_inversion_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inversion_resultvaluefoldnegative_body_steps)) * fs_v_dst_inversion_resultvaluefoldnegative)) /\ exists fs_q_dst_inversion_resultvaluefoldnegative_body_steps_partial. fs_u_dst_inversion_resultvaluefoldnegative = fs_q_dst_inversion_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_resultvaluefoldnegative_body_steps)) * fs_v_dst_inversion_resultvaluefoldnegative) + (fs_r_dst_inversion_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_resultvaluefoldnegative_body_steps_successor. fs_h_dst_inversion_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_inversion_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_resultvaluefoldnegative_body_steps)) * fs_v_dst_inversion_resultvaluefoldnegative)) /\ exists fs_q_dst_inversion_resultvaluefoldnegative_body_steps_successor. fs_u_dst_inversion_resultvaluefoldnegative = fs_q_dst_inversion_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_resultvaluefoldnegative_body_steps)) * fs_v_dst_inversion_resultvaluefoldnegative) + (fs_s_dst_inversion_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_inversion_resultvaluefoldnegative_body_steps = fs_r_dst_inversion_resultvaluefoldnegative_body_steps + fs_a_dst_inversion_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_resultvaluefoldresult ge_balance_negative_inversion_resultvaluefoldresult. (((((dc_output_inversion_result) = 2 * (ge_balance_positive_inversion_resultvaluefoldresult) /\ (ge_balance_negative_inversion_resultvaluefoldresult) = 0) \/ exists ge_signed_half_inversion_resultvaluefoldresultdecode. (((dc_output_inversion_result) = 2 * ge_signed_half_inversion_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_inversion_resultvaluefoldresult) = 0) /\ (ge_balance_negative_inversion_resultvaluefoldresult) = S ge_signed_half_inversion_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_inversion_resultvaluefold) + ge_balance_negative_inversion_resultvaluefoldresult = (dst_negative_sum_inversion_resultvaluefold) + ge_balance_positive_inversion_resultvaluefoldresult))))))))))))))))))))Constructive proof overview
Generated structural guide
Construct one and delta tables and every genuine weighted fold before proving that the actual original table is the full positive-window Möbius inverse.
The unchanged tactic script uses 4 declared prerequisites and contains 68 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
dirichlet_constant_one_table_exists Alpha theorem; checked-use authorized dirichlet_kronecker_delta_table_exists Alpha theorem; checked-use authorized dirichlet_convolution_sum_exists Alpha theorem; checked-use authorized MI0004 mobius_dirichlet_inversion_valueDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (1)
01Fix variables and assumptionsL1–8
02Separate the logical casesL9–10
03Establish hUL11–14
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet constant one table exists.
04Separate the logical casesL15–16
05Establish hEL17–20
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table exists.
06Separate the logical casesL21–23
07Use earlier factsL24–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L24
exact hM_left
08Separate the logical casesL25–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
split
09Use earlier factsL26–26
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
exact hG
10Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
split
11Use earlier factsL28–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L28
exact hF
12Fix variables and assumptionsL29–33
13Establish hsL34–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution sum exists.
- L34
have hs : ∃ a. DirichletSum(M,G,n,a)Definitions: DirichletSum - L35
specialize dirichlet_convolution_sum_exists (N) - L36
specialize dirichlet_convolution_sum_exists (M) - L37
specialize dirichlet_convolution_sum_exists (G) - L38
specialize dirichlet_convolution_sum_exists (n) - L39
apply dirichlet_convolution_sum_exists - L40
exact hM_left - L41
exact hG - L42
exact hn - L43
exact hbound
14Separate the logical casesL44–44
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
cases hs
15Establish heL45–54
Establish this local claim before using it. It is not an additional assumption.
- L45
have he : z=x2 - L46
specialize mobius_dirichlet_inversion_value (N) - L47
specialize mobius_dirichlet_inversion_value (F) - L48
specialize mobius_dirichlet_inversion_value (G) - L49
specialize mobius_dirichlet_inversion_value (M) - L50
specialize mobius_dirichlet_inversion_value (x) - L51
specialize mobius_dirichlet_inversion_value (x1) - L52
specialize mobius_dirichlet_inversion_value (n) - L53
specialize mobius_dirichlet_inversion_value (z) - L54
specialize mobius_dirichlet_inversion_value (x2)
16Use earlier factsL55–64
17Use earlier factsL65–65
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L65
exact hs_witness
18Calculate and transport equalitiesL66–67
19Use earlier factsL68–68
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L68
exact hs_witness
Original exact command ledger · 68 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro M - 0005
intro hF - 0006
intro hG - 0007
intro hM - 0008
intro ht - 0009
cases hM - 0010
cases hM_right - 0011
have hU : exists U. (((exists dst_positive_code_inversion_actual_onetable dst_positive_scale_inversion_actual_onetable dst_negative_code_inversion_actual_onetable dst_negative_scale_inversion_actual_onetable. (((U) = (((((dst_positive_code_inversion_actual_onetable) + (dst_positive_scale_inversion_actual_onetable)) * S ((dst_positive_code_inversion_actual_onetable) + (dst_positive_scale_inversion_actual_onetable)) + ((dst_positive_scale_inversion_actual_onetable) + (dst_positive_scale_inversion_actual_onetable))) + (((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) * S ((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) + ((dst_negative_scale_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)))) * S ((((dst_positive_code_inversion_actual_onetable) + (dst_positive_scale_inversion_actual_onetable)) * S ((dst_positive_code_inversion_actual_onetable) + (dst_positive_scale_inversion_actual_onetable)) + ((dst_positive_scale_inversion_actual_onetable) + (dst_positive_scale_inversion_actual_onetable))) + (((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) * S ((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) + ((dst_negative_scale_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)))) + ((((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) * S ((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) + ((dst_negative_scale_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable))) + (((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) * S ((dst_negative_code_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)) + ((dst_negative_scale_inversion_actual_onetable) + (dst_negative_scale_inversion_actual_onetable)))))) /\ (forall dst_index_inversion_actual_onetable. (exists pvs_le_gap_inversion_actual_onetabledomain. pvs_le_gap_inversion_actual_onetabledomain + (dst_index_inversion_actual_onetable) = (N)) -> exists dst_positive_inversion_actual_onetable dst_negative_inversion_actual_onetable dst_value_inversion_actual_onetable. ((((exists ff_h_pvs_inversion_actual_onetableentrypositive. ff_h_pvs_inversion_actual_onetableentrypositive + S (dst_positive_inversion_actual_onetable) = S ((S (dst_index_inversion_actual_onetable)) * dst_positive_scale_inversion_actual_onetable)) /\ exists ff_q_pvs_inversion_actual_onetableentrypositive. dst_positive_code_inversion_actual_onetable = ff_q_pvs_inversion_actual_onetableentrypositive * S ((S (dst_index_inversion_actual_onetable)) * dst_positive_scale_inversion_actual_onetable) + (dst_positive_inversion_actual_onetable))) /\ (((((exists ff_h_pvs_inversion_actual_onetableentrynegative. ff_h_pvs_inversion_actual_onetableentrynegative + S (dst_negative_inversion_actual_onetable) = S ((S (dst_index_inversion_actual_onetable)) * dst_negative_scale_inversion_actual_onetable)) /\ exists ff_q_pvs_inversion_actual_onetableentrynegative. dst_negative_code_inversion_actual_onetable = ff_q_pvs_inversion_actual_onetableentrynegative * S ((S (dst_index_inversion_actual_onetable)) * dst_negative_scale_inversion_actual_onetable) + (dst_negative_inversion_actual_onetable))) /\ (exists ge_balance_positive_inversion_actual_onetableentryvalue ge_balance_negative_inversion_actual_onetableentryvalue. (((((dst_value_inversion_actual_onetable) = 2 * (ge_balance_positive_inversion_actual_onetableentryvalue) /\ (ge_balance_negative_inversion_actual_onetableentryvalue) = 0) \/ exists ge_signed_half_inversion_actual_onetableentryvaluedecode. (((dst_value_inversion_actual_onetable) = 2 * ge_signed_half_inversion_actual_onetableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_actual_onetableentryvalue) = 0) /\ (ge_balance_negative_inversion_actual_onetableentryvalue) = S ge_signed_half_inversion_actual_onetableentryvaluedecode))) /\ ((dst_positive_inversion_actual_onetable) + ge_balance_negative_inversion_actual_onetableentryvalue = (dst_negative_inversion_actual_onetable) + ge_balance_positive_inversion_actual_onetableentryvalue))))))))) /\ (forall du_index_inversion_actual_one du_value_inversion_actual_one. ~(du_index_inversion_actual_one=0) -> (exists pvs_le_gap_inversion_actual_onebound. pvs_le_gap_inversion_actual_onebound + (du_index_inversion_actual_one) = (N)) -> (exists dst_positive_code_inversion_actual_oneentry dst_positive_scale_inversion_actual_oneentry dst_negative_code_inversion_actual_oneentry dst_negative_scale_inversion_actual_oneentry dst_positive_inversion_actual_oneentry dst_negative_inversion_actual_oneentry. (((U) = (((((dst_positive_code_inversion_actual_oneentry) + (dst_positive_scale_inversion_actual_oneentry)) * S ((dst_positive_code_inversion_actual_oneentry) + (dst_positive_scale_inversion_actual_oneentry)) + ((dst_positive_scale_inversion_actual_oneentry) + (dst_positive_scale_inversion_actual_oneentry))) + (((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) * S ((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) + ((dst_negative_scale_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)))) * S ((((dst_positive_code_inversion_actual_oneentry) + (dst_positive_scale_inversion_actual_oneentry)) * S ((dst_positive_code_inversion_actual_oneentry) + (dst_positive_scale_inversion_actual_oneentry)) + ((dst_positive_scale_inversion_actual_oneentry) + (dst_positive_scale_inversion_actual_oneentry))) + (((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) * S ((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) + ((dst_negative_scale_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)))) + ((((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) * S ((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) + ((dst_negative_scale_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry))) + (((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) * S ((dst_negative_code_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)) + ((dst_negative_scale_inversion_actual_oneentry) + (dst_negative_scale_inversion_actual_oneentry)))))) /\ (((((exists ff_h_pvs_inversion_actual_oneentrypositive. ff_h_pvs_inversion_actual_oneentrypositive + S (dst_positive_inversion_actual_oneentry) = S ((S (du_index_inversion_actual_one)) * dst_positive_scale_inversion_actual_oneentry)) /\ exists ff_q_pvs_inversion_actual_oneentrypositive. dst_positive_code_inversion_actual_oneentry = ff_q_pvs_inversion_actual_oneentrypositive * S ((S (du_index_inversion_actual_one)) * dst_positive_scale_inversion_actual_oneentry) + (dst_positive_inversion_actual_oneentry))) /\ (((((exists ff_h_pvs_inversion_actual_oneentrynegative. ff_h_pvs_inversion_actual_oneentrynegative + S (dst_negative_inversion_actual_oneentry) = S ((S (du_index_inversion_actual_one)) * dst_negative_scale_inversion_actual_oneentry)) /\ exists ff_q_pvs_inversion_actual_oneentrynegative. dst_negative_code_inversion_actual_oneentry = ff_q_pvs_inversion_actual_oneentrynegative * S ((S (du_index_inversion_actual_one)) * dst_negative_scale_inversion_actual_oneentry) + (dst_negative_inversion_actual_oneentry))) /\ (exists ge_balance_positive_inversion_actual_oneentryvalue ge_balance_negative_inversion_actual_oneentryvalue. (((((du_value_inversion_actual_one) = 2 * (ge_balance_positive_inversion_actual_oneentryvalue) /\ (ge_balance_negative_inversion_actual_oneentryvalue) = 0) \/ exists ge_signed_half_inversion_actual_oneentryvaluedecode. (((du_value_inversion_actual_one) = 2 * ge_signed_half_inversion_actual_oneentryvaluedecode + 1 /\ (ge_balance_positive_inversion_actual_oneentryvalue) = 0) /\ (ge_balance_negative_inversion_actual_oneentryvalue) = S ge_signed_half_inversion_actual_oneentryvaluedecode))) /\ ((dst_positive_inversion_actual_oneentry) + ge_balance_negative_inversion_actual_oneentryvalue = (dst_negative_inversion_actual_oneentry) + ge_balance_positive_inversion_actual_oneentryvalue))))))))) -> du_value_inversion_actual_one=2))) /\ (exists dst_positive_code_inversion_one_zero dst_positive_scale_inversion_one_zero dst_negative_code_inversion_one_zero dst_negative_scale_inversion_one_zero dst_positive_inversion_one_zero dst_negative_inversion_one_zero. (((U) = (((((dst_positive_code_inversion_one_zero) + (dst_positive_scale_inversion_one_zero)) * S ((dst_positive_code_inversion_one_zero) + (dst_positive_scale_inversion_one_zero)) + ((dst_positive_scale_inversion_one_zero) + (dst_positive_scale_inversion_one_zero))) + (((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) * S ((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) + ((dst_negative_scale_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)))) * S ((((dst_positive_code_inversion_one_zero) + (dst_positive_scale_inversion_one_zero)) * S ((dst_positive_code_inversion_one_zero) + (dst_positive_scale_inversion_one_zero)) + ((dst_positive_scale_inversion_one_zero) + (dst_positive_scale_inversion_one_zero))) + (((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) * S ((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) + ((dst_negative_scale_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)))) + ((((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) * S ((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) + ((dst_negative_scale_inversion_one_zero) + (dst_negative_scale_inversion_one_zero))) + (((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) * S ((dst_negative_code_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)) + ((dst_negative_scale_inversion_one_zero) + (dst_negative_scale_inversion_one_zero)))))) /\ (((((exists ff_h_pvs_inversion_one_zeropositive. ff_h_pvs_inversion_one_zeropositive + S (dst_positive_inversion_one_zero) = S ((S (0)) * dst_positive_scale_inversion_one_zero)) /\ exists ff_q_pvs_inversion_one_zeropositive. dst_positive_code_inversion_one_zero = ff_q_pvs_inversion_one_zeropositive * S ((S (0)) * dst_positive_scale_inversion_one_zero) + (dst_positive_inversion_one_zero))) /\ (((((exists ff_h_pvs_inversion_one_zeronegative. ff_h_pvs_inversion_one_zeronegative + S (dst_negative_inversion_one_zero) = S ((S (0)) * dst_negative_scale_inversion_one_zero)) /\ exists ff_q_pvs_inversion_one_zeronegative. dst_negative_code_inversion_one_zero = ff_q_pvs_inversion_one_zeronegative * S ((S (0)) * dst_negative_scale_inversion_one_zero) + (dst_negative_inversion_one_zero))) /\ (exists ge_balance_positive_inversion_one_zerovalue ge_balance_negative_inversion_one_zerovalue. (((((0) = 2 * (ge_balance_positive_inversion_one_zerovalue) /\ (ge_balance_negative_inversion_one_zerovalue) = 0) \/ exists ge_signed_half_inversion_one_zerovaluedecode. (((0) = 2 * ge_signed_half_inversion_one_zerovaluedecode + 1 /\ (ge_balance_positive_inversion_one_zerovalue) = 0) /\ (ge_balance_negative_inversion_one_zerovalue) = S ge_signed_half_inversion_one_zerovaluedecode))) /\ ((dst_positive_inversion_one_zero) + ge_balance_negative_inversion_one_zerovalue = (dst_negative_inversion_one_zero) + ge_balance_positive_inversion_one_zerovalue))))))))) - 0012
specialize dirichlet_constant_one_table_exists (N) - 0013
specialize dirichlet_constant_one_table_exists (0) - 0014
apply dirichlet_constant_one_table_exists - 0015
cases hU - 0016
cases hU_witness - 0017
have hE : exists E. (((exists dst_positive_code_inversion_actual_deltatable dst_positive_scale_inversion_actual_deltatable dst_negative_code_inversion_actual_deltatable dst_negative_scale_inversion_actual_deltatable. (((E) = (((((dst_positive_code_inversion_actual_deltatable) + (dst_positive_scale_inversion_actual_deltatable)) * S ((dst_positive_code_inversion_actual_deltatable) + (dst_positive_scale_inversion_actual_deltatable)) + ((dst_positive_scale_inversion_actual_deltatable) + (dst_positive_scale_inversion_actual_deltatable))) + (((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) * S ((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) + ((dst_negative_scale_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)))) * S ((((dst_positive_code_inversion_actual_deltatable) + (dst_positive_scale_inversion_actual_deltatable)) * S ((dst_positive_code_inversion_actual_deltatable) + (dst_positive_scale_inversion_actual_deltatable)) + ((dst_positive_scale_inversion_actual_deltatable) + (dst_positive_scale_inversion_actual_deltatable))) + (((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) * S ((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) + ((dst_negative_scale_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)))) + ((((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) * S ((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) + ((dst_negative_scale_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable))) + (((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) * S ((dst_negative_code_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)) + ((dst_negative_scale_inversion_actual_deltatable) + (dst_negative_scale_inversion_actual_deltatable)))))) /\ (forall dst_index_inversion_actual_deltatable. (exists pvs_le_gap_inversion_actual_deltatabledomain. pvs_le_gap_inversion_actual_deltatabledomain + (dst_index_inversion_actual_deltatable) = (N)) -> exists dst_positive_inversion_actual_deltatable dst_negative_inversion_actual_deltatable dst_value_inversion_actual_deltatable. ((((exists ff_h_pvs_inversion_actual_deltatableentrypositive. ff_h_pvs_inversion_actual_deltatableentrypositive + S (dst_positive_inversion_actual_deltatable) = S ((S (dst_index_inversion_actual_deltatable)) * dst_positive_scale_inversion_actual_deltatable)) /\ exists ff_q_pvs_inversion_actual_deltatableentrypositive. dst_positive_code_inversion_actual_deltatable = ff_q_pvs_inversion_actual_deltatableentrypositive * S ((S (dst_index_inversion_actual_deltatable)) * dst_positive_scale_inversion_actual_deltatable) + (dst_positive_inversion_actual_deltatable))) /\ (((((exists ff_h_pvs_inversion_actual_deltatableentrynegative. ff_h_pvs_inversion_actual_deltatableentrynegative + S (dst_negative_inversion_actual_deltatable) = S ((S (dst_index_inversion_actual_deltatable)) * dst_negative_scale_inversion_actual_deltatable)) /\ exists ff_q_pvs_inversion_actual_deltatableentrynegative. dst_negative_code_inversion_actual_deltatable = ff_q_pvs_inversion_actual_deltatableentrynegative * S ((S (dst_index_inversion_actual_deltatable)) * dst_negative_scale_inversion_actual_deltatable) + (dst_negative_inversion_actual_deltatable))) /\ (exists ge_balance_positive_inversion_actual_deltatableentryvalue ge_balance_negative_inversion_actual_deltatableentryvalue. (((((dst_value_inversion_actual_deltatable) = 2 * (ge_balance_positive_inversion_actual_deltatableentryvalue) /\ (ge_balance_negative_inversion_actual_deltatableentryvalue) = 0) \/ exists ge_signed_half_inversion_actual_deltatableentryvaluedecode. (((dst_value_inversion_actual_deltatable) = 2 * ge_signed_half_inversion_actual_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_actual_deltatableentryvalue) = 0) /\ (ge_balance_negative_inversion_actual_deltatableentryvalue) = S ge_signed_half_inversion_actual_deltatableentryvaluedecode))) /\ ((dst_positive_inversion_actual_deltatable) + ge_balance_negative_inversion_actual_deltatableentryvalue = (dst_negative_inversion_actual_deltatable) + ge_balance_positive_inversion_actual_deltatableentryvalue))))))))) /\ (forall du_index_inversion_actual_delta du_value_inversion_actual_delta. ~(du_index_inversion_actual_delta=0) -> (exists pvs_le_gap_inversion_actual_deltabound. pvs_le_gap_inversion_actual_deltabound + (du_index_inversion_actual_delta) = (N)) -> (exists dst_positive_code_inversion_actual_deltaentry dst_positive_scale_inversion_actual_deltaentry dst_negative_code_inversion_actual_deltaentry dst_negative_scale_inversion_actual_deltaentry dst_positive_inversion_actual_deltaentry dst_negative_inversion_actual_deltaentry. (((E) = (((((dst_positive_code_inversion_actual_deltaentry) + (dst_positive_scale_inversion_actual_deltaentry)) * S ((dst_positive_code_inversion_actual_deltaentry) + (dst_positive_scale_inversion_actual_deltaentry)) + ((dst_positive_scale_inversion_actual_deltaentry) + (dst_positive_scale_inversion_actual_deltaentry))) + (((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) * S ((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) + ((dst_negative_scale_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)))) * S ((((dst_positive_code_inversion_actual_deltaentry) + (dst_positive_scale_inversion_actual_deltaentry)) * S ((dst_positive_code_inversion_actual_deltaentry) + (dst_positive_scale_inversion_actual_deltaentry)) + ((dst_positive_scale_inversion_actual_deltaentry) + (dst_positive_scale_inversion_actual_deltaentry))) + (((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) * S ((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) + ((dst_negative_scale_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)))) + ((((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) * S ((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) + ((dst_negative_scale_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry))) + (((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) * S ((dst_negative_code_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)) + ((dst_negative_scale_inversion_actual_deltaentry) + (dst_negative_scale_inversion_actual_deltaentry)))))) /\ (((((exists ff_h_pvs_inversion_actual_deltaentrypositive. ff_h_pvs_inversion_actual_deltaentrypositive + S (dst_positive_inversion_actual_deltaentry) = S ((S (du_index_inversion_actual_delta)) * dst_positive_scale_inversion_actual_deltaentry)) /\ exists ff_q_pvs_inversion_actual_deltaentrypositive. dst_positive_code_inversion_actual_deltaentry = ff_q_pvs_inversion_actual_deltaentrypositive * S ((S (du_index_inversion_actual_delta)) * dst_positive_scale_inversion_actual_deltaentry) + (dst_positive_inversion_actual_deltaentry))) /\ (((((exists ff_h_pvs_inversion_actual_deltaentrynegative. ff_h_pvs_inversion_actual_deltaentrynegative + S (dst_negative_inversion_actual_deltaentry) = S ((S (du_index_inversion_actual_delta)) * dst_negative_scale_inversion_actual_deltaentry)) /\ exists ff_q_pvs_inversion_actual_deltaentrynegative. dst_negative_code_inversion_actual_deltaentry = ff_q_pvs_inversion_actual_deltaentrynegative * S ((S (du_index_inversion_actual_delta)) * dst_negative_scale_inversion_actual_deltaentry) + (dst_negative_inversion_actual_deltaentry))) /\ (exists ge_balance_positive_inversion_actual_deltaentryvalue ge_balance_negative_inversion_actual_deltaentryvalue. (((((du_value_inversion_actual_delta) = 2 * (ge_balance_positive_inversion_actual_deltaentryvalue) /\ (ge_balance_negative_inversion_actual_deltaentryvalue) = 0) \/ exists ge_signed_half_inversion_actual_deltaentryvaluedecode. (((du_value_inversion_actual_delta) = 2 * ge_signed_half_inversion_actual_deltaentryvaluedecode + 1 /\ (ge_balance_positive_inversion_actual_deltaentryvalue) = 0) /\ (ge_balance_negative_inversion_actual_deltaentryvalue) = S ge_signed_half_inversion_actual_deltaentryvaluedecode))) /\ ((dst_positive_inversion_actual_deltaentry) + ge_balance_negative_inversion_actual_deltaentryvalue = (dst_negative_inversion_actual_deltaentry) + ge_balance_positive_inversion_actual_deltaentryvalue))))))))) -> ((((du_index_inversion_actual_delta)=1 -> (du_value_inversion_actual_delta)=2) /\ (~((du_index_inversion_actual_delta)=1) -> (du_value_inversion_actual_delta)=0)))))) /\ (exists dst_positive_code_inversion_delta_zero dst_positive_scale_inversion_delta_zero dst_negative_code_inversion_delta_zero dst_negative_scale_inversion_delta_zero dst_positive_inversion_delta_zero dst_negative_inversion_delta_zero. (((E) = (((((dst_positive_code_inversion_delta_zero) + (dst_positive_scale_inversion_delta_zero)) * S ((dst_positive_code_inversion_delta_zero) + (dst_positive_scale_inversion_delta_zero)) + ((dst_positive_scale_inversion_delta_zero) + (dst_positive_scale_inversion_delta_zero))) + (((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) * S ((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) + ((dst_negative_scale_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)))) * S ((((dst_positive_code_inversion_delta_zero) + (dst_positive_scale_inversion_delta_zero)) * S ((dst_positive_code_inversion_delta_zero) + (dst_positive_scale_inversion_delta_zero)) + ((dst_positive_scale_inversion_delta_zero) + (dst_positive_scale_inversion_delta_zero))) + (((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) * S ((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) + ((dst_negative_scale_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)))) + ((((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) * S ((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) + ((dst_negative_scale_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero))) + (((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) * S ((dst_negative_code_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)) + ((dst_negative_scale_inversion_delta_zero) + (dst_negative_scale_inversion_delta_zero)))))) /\ (((((exists ff_h_pvs_inversion_delta_zeropositive. ff_h_pvs_inversion_delta_zeropositive + S (dst_positive_inversion_delta_zero) = S ((S (0)) * dst_positive_scale_inversion_delta_zero)) /\ exists ff_q_pvs_inversion_delta_zeropositive. dst_positive_code_inversion_delta_zero = ff_q_pvs_inversion_delta_zeropositive * S ((S (0)) * dst_positive_scale_inversion_delta_zero) + (dst_positive_inversion_delta_zero))) /\ (((((exists ff_h_pvs_inversion_delta_zeronegative. ff_h_pvs_inversion_delta_zeronegative + S (dst_negative_inversion_delta_zero) = S ((S (0)) * dst_negative_scale_inversion_delta_zero)) /\ exists ff_q_pvs_inversion_delta_zeronegative. dst_negative_code_inversion_delta_zero = ff_q_pvs_inversion_delta_zeronegative * S ((S (0)) * dst_negative_scale_inversion_delta_zero) + (dst_negative_inversion_delta_zero))) /\ (exists ge_balance_positive_inversion_delta_zerovalue ge_balance_negative_inversion_delta_zerovalue. (((((0) = 2 * (ge_balance_positive_inversion_delta_zerovalue) /\ (ge_balance_negative_inversion_delta_zerovalue) = 0) \/ exists ge_signed_half_inversion_delta_zerovaluedecode. (((0) = 2 * ge_signed_half_inversion_delta_zerovaluedecode + 1 /\ (ge_balance_positive_inversion_delta_zerovalue) = 0) /\ (ge_balance_negative_inversion_delta_zerovalue) = S ge_signed_half_inversion_delta_zerovaluedecode))) /\ ((dst_positive_inversion_delta_zero) + ge_balance_negative_inversion_delta_zerovalue = (dst_negative_inversion_delta_zero) + ge_balance_positive_inversion_delta_zerovalue))))))))) - 0018
specialize dirichlet_kronecker_delta_table_exists (N) - 0019
specialize dirichlet_kronecker_delta_table_exists (0) - 0020
apply dirichlet_kronecker_delta_table_exists - 0021
cases hE - 0022
cases hE_witness - 0023
split - 0024
exact hM_left - 0025
split - 0026
exact hG - 0027
split - 0028
exact hF - 0029
intro n - 0030
intro z - 0031
intro hn - 0032
intro hbound - 0033
intro hz - 0034
have hs : exists a. (((~((n)=0)) /\ (exists dc_mask_inversion_construct_fold. ((((exists dst_positive_code_inversion_construct_foldmasktable dst_positive_scale_inversion_construct_foldmasktable dst_negative_code_inversion_construct_foldmasktable dst_negative_scale_inversion_construct_foldmasktable. (((dc_mask_inversion_construct_fold) = (((((dst_positive_code_inversion_construct_foldmasktable) + (dst_positive_scale_inversion_construct_foldmasktable)) * S ((dst_positive_code_inversion_construct_foldmasktable) + (dst_positive_scale_inversion_construct_foldmasktable)) + ((dst_positive_scale_inversion_construct_foldmasktable) + (dst_positive_scale_inversion_construct_foldmasktable))) + (((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) * S ((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) + ((dst_negative_scale_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)))) * S ((((dst_positive_code_inversion_construct_foldmasktable) + (dst_positive_scale_inversion_construct_foldmasktable)) * S ((dst_positive_code_inversion_construct_foldmasktable) + (dst_positive_scale_inversion_construct_foldmasktable)) + ((dst_positive_scale_inversion_construct_foldmasktable) + (dst_positive_scale_inversion_construct_foldmasktable))) + (((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) * S ((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) + ((dst_negative_scale_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)))) + ((((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) * S ((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) + ((dst_negative_scale_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable))) + (((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) * S ((dst_negative_code_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)) + ((dst_negative_scale_inversion_construct_foldmasktable) + (dst_negative_scale_inversion_construct_foldmasktable)))))) /\ (forall dst_index_inversion_construct_foldmasktable. (exists pvs_le_gap_inversion_construct_foldmasktabledomain. pvs_le_gap_inversion_construct_foldmasktabledomain + (dst_index_inversion_construct_foldmasktable) = (n)) -> exists dst_positive_inversion_construct_foldmasktable dst_negative_inversion_construct_foldmasktable dst_value_inversion_construct_foldmasktable. ((((exists ff_h_pvs_inversion_construct_foldmasktableentrypositive. ff_h_pvs_inversion_construct_foldmasktableentrypositive + S (dst_positive_inversion_construct_foldmasktable) = S ((S (dst_index_inversion_construct_foldmasktable)) * dst_positive_scale_inversion_construct_foldmasktable)) /\ exists ff_q_pvs_inversion_construct_foldmasktableentrypositive. dst_positive_code_inversion_construct_foldmasktable = ff_q_pvs_inversion_construct_foldmasktableentrypositive * S ((S (dst_index_inversion_construct_foldmasktable)) * dst_positive_scale_inversion_construct_foldmasktable) + (dst_positive_inversion_construct_foldmasktable))) /\ (((((exists ff_h_pvs_inversion_construct_foldmasktableentrynegative. ff_h_pvs_inversion_construct_foldmasktableentrynegative + S (dst_negative_inversion_construct_foldmasktable) = S ((S (dst_index_inversion_construct_foldmasktable)) * dst_negative_scale_inversion_construct_foldmasktable)) /\ exists ff_q_pvs_inversion_construct_foldmasktableentrynegative. dst_negative_code_inversion_construct_foldmasktable = ff_q_pvs_inversion_construct_foldmasktableentrynegative * S ((S (dst_index_inversion_construct_foldmasktable)) * dst_negative_scale_inversion_construct_foldmasktable) + (dst_negative_inversion_construct_foldmasktable))) /\ (exists ge_balance_positive_inversion_construct_foldmasktableentryvalue ge_balance_negative_inversion_construct_foldmasktableentryvalue. (((((dst_value_inversion_construct_foldmasktable) = 2 * (ge_balance_positive_inversion_construct_foldmasktableentryvalue) /\ (ge_balance_negative_inversion_construct_foldmasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_construct_foldmasktableentryvaluedecode. (((dst_value_inversion_construct_foldmasktable) = 2 * ge_signed_half_inversion_construct_foldmasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_construct_foldmasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_construct_foldmasktableentryvalue) = S ge_signed_half_inversion_construct_foldmasktableentryvaluedecode))) /\ ((dst_positive_inversion_construct_foldmasktable) + ge_balance_negative_inversion_construct_foldmasktableentryvalue = (dst_negative_inversion_construct_foldmasktable) + ge_balance_positive_inversion_construct_foldmasktableentryvalue))))))))) /\ (forall dc_index_inversion_construct_foldmask dc_value_inversion_construct_foldmask. (exists pvs_le_gap_inversion_construct_foldmaskdomain. pvs_le_gap_inversion_construct_foldmaskdomain + (dc_index_inversion_construct_foldmask) = (n)) -> (exists dst_positive_code_inversion_construct_foldmasklookup dst_positive_scale_inversion_construct_foldmasklookup dst_negative_code_inversion_construct_foldmasklookup dst_negative_scale_inversion_construct_foldmasklookup dst_positive_inversion_construct_foldmasklookup dst_negative_inversion_construct_foldmasklookup. (((dc_mask_inversion_construct_fold) = (((((dst_positive_code_inversion_construct_foldmasklookup) + (dst_positive_scale_inversion_construct_foldmasklookup)) * S ((dst_positive_code_inversion_construct_foldmasklookup) + (dst_positive_scale_inversion_construct_foldmasklookup)) + ((dst_positive_scale_inversion_construct_foldmasklookup) + (dst_positive_scale_inversion_construct_foldmasklookup))) + (((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) * S ((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) + ((dst_negative_scale_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)))) * S ((((dst_positive_code_inversion_construct_foldmasklookup) + (dst_positive_scale_inversion_construct_foldmasklookup)) * S ((dst_positive_code_inversion_construct_foldmasklookup) + (dst_positive_scale_inversion_construct_foldmasklookup)) + ((dst_positive_scale_inversion_construct_foldmasklookup) + (dst_positive_scale_inversion_construct_foldmasklookup))) + (((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) * S ((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) + ((dst_negative_scale_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)))) + ((((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) * S ((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) + ((dst_negative_scale_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup))) + (((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) * S ((dst_negative_code_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)) + ((dst_negative_scale_inversion_construct_foldmasklookup) + (dst_negative_scale_inversion_construct_foldmasklookup)))))) /\ (((((exists ff_h_pvs_inversion_construct_foldmasklookuppositive. ff_h_pvs_inversion_construct_foldmasklookuppositive + S (dst_positive_inversion_construct_foldmasklookup) = S ((S (dc_index_inversion_construct_foldmask)) * dst_positive_scale_inversion_construct_foldmasklookup)) /\ exists ff_q_pvs_inversion_construct_foldmasklookuppositive. dst_positive_code_inversion_construct_foldmasklookup = ff_q_pvs_inversion_construct_foldmasklookuppositive * S ((S (dc_index_inversion_construct_foldmask)) * dst_positive_scale_inversion_construct_foldmasklookup) + (dst_positive_inversion_construct_foldmasklookup))) /\ (((((exists ff_h_pvs_inversion_construct_foldmasklookupnegative. ff_h_pvs_inversion_construct_foldmasklookupnegative + S (dst_negative_inversion_construct_foldmasklookup) = S ((S (dc_index_inversion_construct_foldmask)) * dst_negative_scale_inversion_construct_foldmasklookup)) /\ exists ff_q_pvs_inversion_construct_foldmasklookupnegative. dst_negative_code_inversion_construct_foldmasklookup = ff_q_pvs_inversion_construct_foldmasklookupnegative * S ((S (dc_index_inversion_construct_foldmask)) * dst_negative_scale_inversion_construct_foldmasklookup) + (dst_negative_inversion_construct_foldmasklookup))) /\ (exists ge_balance_positive_inversion_construct_foldmasklookupvalue ge_balance_negative_inversion_construct_foldmasklookupvalue. (((((dc_value_inversion_construct_foldmask) = 2 * (ge_balance_positive_inversion_construct_foldmasklookupvalue) /\ (ge_balance_negative_inversion_construct_foldmasklookupvalue) = 0) \/ exists ge_signed_half_inversion_construct_foldmasklookupvaluedecode. (((dc_value_inversion_construct_foldmask) = 2 * ge_signed_half_inversion_construct_foldmasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_construct_foldmasklookupvalue) = 0) /\ (ge_balance_negative_inversion_construct_foldmasklookupvalue) = S ge_signed_half_inversion_construct_foldmasklookupvaluedecode))) /\ ((dst_positive_inversion_construct_foldmasklookup) + ge_balance_negative_inversion_construct_foldmasklookupvalue = (dst_negative_inversion_construct_foldmasklookup) + ge_balance_positive_inversion_construct_foldmasklookupvalue))))))))) -> ((((~((dc_index_inversion_construct_foldmask)=0)) /\ (exists dc_quotient_inversion_construct_foldmaskentry dc_left_inversion_construct_foldmaskentry dc_right_inversion_construct_foldmaskentry. (((n)=(dc_index_inversion_construct_foldmask)*dc_quotient_inversion_construct_foldmaskentry) /\ (((exists dst_positive_code_inversion_construct_foldmaskentryleft dst_positive_scale_inversion_construct_foldmaskentryleft dst_negative_code_inversion_construct_foldmaskentryleft dst_negative_scale_inversion_construct_foldmaskentryleft dst_positive_inversion_construct_foldmaskentryleft dst_negative_inversion_construct_foldmaskentryleft. (((M) = (((((dst_positive_code_inversion_construct_foldmaskentryleft) + (dst_positive_scale_inversion_construct_foldmaskentryleft)) * S ((dst_positive_code_inversion_construct_foldmaskentryleft) + (dst_positive_scale_inversion_construct_foldmaskentryleft)) + ((dst_positive_scale_inversion_construct_foldmaskentryleft) + (dst_positive_scale_inversion_construct_foldmaskentryleft))) + (((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) * S ((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) + ((dst_negative_scale_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)))) * S ((((dst_positive_code_inversion_construct_foldmaskentryleft) + (dst_positive_scale_inversion_construct_foldmaskentryleft)) * S ((dst_positive_code_inversion_construct_foldmaskentryleft) + (dst_positive_scale_inversion_construct_foldmaskentryleft)) + ((dst_positive_scale_inversion_construct_foldmaskentryleft) + (dst_positive_scale_inversion_construct_foldmaskentryleft))) + (((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) * S ((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) + ((dst_negative_scale_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)))) + ((((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) * S ((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) + ((dst_negative_scale_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft))) + (((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) * S ((dst_negative_code_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)) + ((dst_negative_scale_inversion_construct_foldmaskentryleft) + (dst_negative_scale_inversion_construct_foldmaskentryleft)))))) /\ (((((exists ff_h_pvs_inversion_construct_foldmaskentryleftpositive. ff_h_pvs_inversion_construct_foldmaskentryleftpositive + S (dst_positive_inversion_construct_foldmaskentryleft) = S ((S (dc_index_inversion_construct_foldmask)) * dst_positive_scale_inversion_construct_foldmaskentryleft)) /\ exists ff_q_pvs_inversion_construct_foldmaskentryleftpositive. dst_positive_code_inversion_construct_foldmaskentryleft = ff_q_pvs_inversion_construct_foldmaskentryleftpositive * S ((S (dc_index_inversion_construct_foldmask)) * dst_positive_scale_inversion_construct_foldmaskentryleft) + (dst_positive_inversion_construct_foldmaskentryleft))) /\ (((((exists ff_h_pvs_inversion_construct_foldmaskentryleftnegative. ff_h_pvs_inversion_construct_foldmaskentryleftnegative + S (dst_negative_inversion_construct_foldmaskentryleft) = S ((S (dc_index_inversion_construct_foldmask)) * dst_negative_scale_inversion_construct_foldmaskentryleft)) /\ exists ff_q_pvs_inversion_construct_foldmaskentryleftnegative. dst_negative_code_inversion_construct_foldmaskentryleft = ff_q_pvs_inversion_construct_foldmaskentryleftnegative * S ((S (dc_index_inversion_construct_foldmask)) * dst_negative_scale_inversion_construct_foldmaskentryleft) + (dst_negative_inversion_construct_foldmaskentryleft))) /\ (exists ge_balance_positive_inversion_construct_foldmaskentryleftvalue ge_balance_negative_inversion_construct_foldmaskentryleftvalue. (((((dc_left_inversion_construct_foldmaskentry) = 2 * (ge_balance_positive_inversion_construct_foldmaskentryleftvalue) /\ (ge_balance_negative_inversion_construct_foldmaskentryleftvalue) = 0) \/ exists ge_signed_half_inversion_construct_foldmaskentryleftvaluedecode. (((dc_left_inversion_construct_foldmaskentry) = 2 * ge_signed_half_inversion_construct_foldmaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inversion_construct_foldmaskentryleftvalue) = 0) /\ (ge_balance_negative_inversion_construct_foldmaskentryleftvalue) = S ge_signed_half_inversion_construct_foldmaskentryleftvaluedecode))) /\ ((dst_positive_inversion_construct_foldmaskentryleft) + ge_balance_negative_inversion_construct_foldmaskentryleftvalue = (dst_negative_inversion_construct_foldmaskentryleft) + ge_balance_positive_inversion_construct_foldmaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inversion_construct_foldmaskentryright dst_positive_scale_inversion_construct_foldmaskentryright dst_negative_code_inversion_construct_foldmaskentryright dst_negative_scale_inversion_construct_foldmaskentryright dst_positive_inversion_construct_foldmaskentryright dst_negative_inversion_construct_foldmaskentryright. (((G) = (((((dst_positive_code_inversion_construct_foldmaskentryright) + (dst_positive_scale_inversion_construct_foldmaskentryright)) * S ((dst_positive_code_inversion_construct_foldmaskentryright) + (dst_positive_scale_inversion_construct_foldmaskentryright)) + ((dst_positive_scale_inversion_construct_foldmaskentryright) + (dst_positive_scale_inversion_construct_foldmaskentryright))) + (((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) * S ((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) + ((dst_negative_scale_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)))) * S ((((dst_positive_code_inversion_construct_foldmaskentryright) + (dst_positive_scale_inversion_construct_foldmaskentryright)) * S ((dst_positive_code_inversion_construct_foldmaskentryright) + (dst_positive_scale_inversion_construct_foldmaskentryright)) + ((dst_positive_scale_inversion_construct_foldmaskentryright) + (dst_positive_scale_inversion_construct_foldmaskentryright))) + (((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) * S ((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) + ((dst_negative_scale_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)))) + ((((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) * S ((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) + ((dst_negative_scale_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright))) + (((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) * S ((dst_negative_code_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)) + ((dst_negative_scale_inversion_construct_foldmaskentryright) + (dst_negative_scale_inversion_construct_foldmaskentryright)))))) /\ (((((exists ff_h_pvs_inversion_construct_foldmaskentryrightpositive. ff_h_pvs_inversion_construct_foldmaskentryrightpositive + S (dst_positive_inversion_construct_foldmaskentryright) = S ((S (dc_quotient_inversion_construct_foldmaskentry)) * dst_positive_scale_inversion_construct_foldmaskentryright)) /\ exists ff_q_pvs_inversion_construct_foldmaskentryrightpositive. dst_positive_code_inversion_construct_foldmaskentryright = ff_q_pvs_inversion_construct_foldmaskentryrightpositive * S ((S (dc_quotient_inversion_construct_foldmaskentry)) * dst_positive_scale_inversion_construct_foldmaskentryright) + (dst_positive_inversion_construct_foldmaskentryright))) /\ (((((exists ff_h_pvs_inversion_construct_foldmaskentryrightnegative. ff_h_pvs_inversion_construct_foldmaskentryrightnegative + S (dst_negative_inversion_construct_foldmaskentryright) = S ((S (dc_quotient_inversion_construct_foldmaskentry)) * dst_negative_scale_inversion_construct_foldmaskentryright)) /\ exists ff_q_pvs_inversion_construct_foldmaskentryrightnegative. dst_negative_code_inversion_construct_foldmaskentryright = ff_q_pvs_inversion_construct_foldmaskentryrightnegative * S ((S (dc_quotient_inversion_construct_foldmaskentry)) * dst_negative_scale_inversion_construct_foldmaskentryright) + (dst_negative_inversion_construct_foldmaskentryright))) /\ (exists ge_balance_positive_inversion_construct_foldmaskentryrightvalue ge_balance_negative_inversion_construct_foldmaskentryrightvalue. (((((dc_right_inversion_construct_foldmaskentry) = 2 * (ge_balance_positive_inversion_construct_foldmaskentryrightvalue) /\ (ge_balance_negative_inversion_construct_foldmaskentryrightvalue) = 0) \/ exists ge_signed_half_inversion_construct_foldmaskentryrightvaluedecode. (((dc_right_inversion_construct_foldmaskentry) = 2 * ge_signed_half_inversion_construct_foldmaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inversion_construct_foldmaskentryrightvalue) = 0) /\ (ge_balance_negative_inversion_construct_foldmaskentryrightvalue) = S ge_signed_half_inversion_construct_foldmaskentryrightvaluedecode))) /\ ((dst_positive_inversion_construct_foldmaskentryright) + ge_balance_negative_inversion_construct_foldmaskentryrightvalue = (dst_negative_inversion_construct_foldmaskentryright) + ge_balance_positive_inversion_construct_foldmaskentryrightvalue))))))))) /\ (exists sto_ap_inversion_construct_foldmaskentryproduct sto_an_inversion_construct_foldmaskentryproduct sto_bp_inversion_construct_foldmaskentryproduct sto_bn_inversion_construct_foldmaskentryproduct sto_cp_inversion_construct_foldmaskentryproduct sto_cn_inversion_construct_foldmaskentryproduct. (((((dc_left_inversion_construct_foldmaskentry) = 2 * (sto_ap_inversion_construct_foldmaskentryproduct) /\ (sto_an_inversion_construct_foldmaskentryproduct) = 0) \/ exists ge_signed_half_inversion_construct_foldmaskentryproductleft. (((dc_left_inversion_construct_foldmaskentry) = 2 * ge_signed_half_inversion_construct_foldmaskentryproductleft + 1 /\ (sto_ap_inversion_construct_foldmaskentryproduct) = 0) /\ (sto_an_inversion_construct_foldmaskentryproduct) = S ge_signed_half_inversion_construct_foldmaskentryproductleft))) /\ ((((((dc_right_inversion_construct_foldmaskentry) = 2 * (sto_bp_inversion_construct_foldmaskentryproduct) /\ (sto_bn_inversion_construct_foldmaskentryproduct) = 0) \/ exists ge_signed_half_inversion_construct_foldmaskentryproductright. (((dc_right_inversion_construct_foldmaskentry) = 2 * ge_signed_half_inversion_construct_foldmaskentryproductright + 1 /\ (sto_bp_inversion_construct_foldmaskentryproduct) = 0) /\ (sto_bn_inversion_construct_foldmaskentryproduct) = S ge_signed_half_inversion_construct_foldmaskentryproductright))) /\ ((((((dc_value_inversion_construct_foldmask) = 2 * (sto_cp_inversion_construct_foldmaskentryproduct) /\ (sto_cn_inversion_construct_foldmaskentryproduct) = 0) \/ exists ge_signed_half_inversion_construct_foldmaskentryproductoutput. (((dc_value_inversion_construct_foldmask) = 2 * ge_signed_half_inversion_construct_foldmaskentryproductoutput + 1 /\ (sto_cp_inversion_construct_foldmaskentryproduct) = 0) /\ (sto_cn_inversion_construct_foldmaskentryproduct) = S ge_signed_half_inversion_construct_foldmaskentryproductoutput))) /\ ((sto_ap_inversion_construct_foldmaskentryproduct * sto_bp_inversion_construct_foldmaskentryproduct + sto_an_inversion_construct_foldmaskentryproduct * sto_bn_inversion_construct_foldmaskentryproduct) + sto_cn_inversion_construct_foldmaskentryproduct = (sto_ap_inversion_construct_foldmaskentryproduct * sto_bn_inversion_construct_foldmaskentryproduct + sto_an_inversion_construct_foldmaskentryproduct * sto_bp_inversion_construct_foldmaskentryproduct) + sto_cp_inversion_construct_foldmaskentryproduct))))))))))))))) \/ ((((dc_index_inversion_construct_foldmask)=0 \/ ~(exists pvs_factor_inversion_construct_foldmaskentrynondivisor. (n) = (dc_index_inversion_construct_foldmask) * pvs_factor_inversion_construct_foldmaskentrynondivisor)) /\ ((dc_value_inversion_construct_foldmask)=0))))))) /\ (exists dst_positive_code_inversion_construct_foldfold dst_positive_scale_inversion_construct_foldfold dst_negative_code_inversion_construct_foldfold dst_negative_scale_inversion_construct_foldfold dst_positive_sum_inversion_construct_foldfold dst_negative_sum_inversion_construct_foldfold. (((dc_mask_inversion_construct_fold) = (((((dst_positive_code_inversion_construct_foldfold) + (dst_positive_scale_inversion_construct_foldfold)) * S ((dst_positive_code_inversion_construct_foldfold) + (dst_positive_scale_inversion_construct_foldfold)) + ((dst_positive_scale_inversion_construct_foldfold) + (dst_positive_scale_inversion_construct_foldfold))) + (((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) * S ((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) + ((dst_negative_scale_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)))) * S ((((dst_positive_code_inversion_construct_foldfold) + (dst_positive_scale_inversion_construct_foldfold)) * S ((dst_positive_code_inversion_construct_foldfold) + (dst_positive_scale_inversion_construct_foldfold)) + ((dst_positive_scale_inversion_construct_foldfold) + (dst_positive_scale_inversion_construct_foldfold))) + (((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) * S ((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) + ((dst_negative_scale_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)))) + ((((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) * S ((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) + ((dst_negative_scale_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold))) + (((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) * S ((dst_negative_code_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)) + ((dst_negative_scale_inversion_construct_foldfold) + (dst_negative_scale_inversion_construct_foldfold)))))) /\ (((exists fs_u_dst_inversion_construct_foldfoldpositive fs_v_dst_inversion_construct_foldfoldpositive. ((((exists fs_h_dst_inversion_construct_foldfoldpositive_body_start. fs_h_dst_inversion_construct_foldfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_construct_foldfoldpositive)) /\ exists fs_q_dst_inversion_construct_foldfoldpositive_body_start. fs_u_dst_inversion_construct_foldfoldpositive = fs_q_dst_inversion_construct_foldfoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_construct_foldfoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_construct_foldfoldpositive_body_terminal. fs_h_dst_inversion_construct_foldfoldpositive_body_terminal + S (dst_positive_sum_inversion_construct_foldfold) = S ((S (S (n))) * fs_v_dst_inversion_construct_foldfoldpositive)) /\ exists fs_q_dst_inversion_construct_foldfoldpositive_body_terminal. fs_u_dst_inversion_construct_foldfoldpositive = fs_q_dst_inversion_construct_foldfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_inversion_construct_foldfoldpositive) + (dst_positive_sum_inversion_construct_foldfold))) /\ forall fs_i_dst_inversion_construct_foldfoldpositive_body_steps. (exists fs_lt_dst_inversion_construct_foldfoldpositive_body_steps_bound. fs_lt_dst_inversion_construct_foldfoldpositive_body_steps_bound + S fs_i_dst_inversion_construct_foldfoldpositive_body_steps = S (n)) -> exists fs_a_dst_inversion_construct_foldfoldpositive_body_steps fs_r_dst_inversion_construct_foldfoldpositive_body_steps fs_s_dst_inversion_construct_foldfoldpositive_body_steps. ((((exists fs_h_dst_inversion_construct_foldfoldpositive_body_steps_summand. fs_h_dst_inversion_construct_foldfoldpositive_body_steps_summand + S (fs_a_dst_inversion_construct_foldfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_construct_foldfoldpositive_body_steps)) * dst_positive_scale_inversion_construct_foldfold)) /\ exists fs_q_dst_inversion_construct_foldfoldpositive_body_steps_summand. dst_positive_code_inversion_construct_foldfold = fs_q_dst_inversion_construct_foldfoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_construct_foldfoldpositive_body_steps)) * dst_positive_scale_inversion_construct_foldfold) + (fs_a_dst_inversion_construct_foldfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_construct_foldfoldpositive_body_steps_partial. fs_h_dst_inversion_construct_foldfoldpositive_body_steps_partial + S (fs_r_dst_inversion_construct_foldfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_construct_foldfoldpositive_body_steps)) * fs_v_dst_inversion_construct_foldfoldpositive)) /\ exists fs_q_dst_inversion_construct_foldfoldpositive_body_steps_partial. fs_u_dst_inversion_construct_foldfoldpositive = fs_q_dst_inversion_construct_foldfoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_construct_foldfoldpositive_body_steps)) * fs_v_dst_inversion_construct_foldfoldpositive) + (fs_r_dst_inversion_construct_foldfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_construct_foldfoldpositive_body_steps_successor. fs_h_dst_inversion_construct_foldfoldpositive_body_steps_successor + S (fs_s_dst_inversion_construct_foldfoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_construct_foldfoldpositive_body_steps)) * fs_v_dst_inversion_construct_foldfoldpositive)) /\ exists fs_q_dst_inversion_construct_foldfoldpositive_body_steps_successor. fs_u_dst_inversion_construct_foldfoldpositive = fs_q_dst_inversion_construct_foldfoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_construct_foldfoldpositive_body_steps)) * fs_v_dst_inversion_construct_foldfoldpositive) + (fs_s_dst_inversion_construct_foldfoldpositive_body_steps))) /\ fs_s_dst_inversion_construct_foldfoldpositive_body_steps = fs_r_dst_inversion_construct_foldfoldpositive_body_steps + fs_a_dst_inversion_construct_foldfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_construct_foldfoldnegative fs_v_dst_inversion_construct_foldfoldnegative. ((((exists fs_h_dst_inversion_construct_foldfoldnegative_body_start. fs_h_dst_inversion_construct_foldfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_construct_foldfoldnegative)) /\ exists fs_q_dst_inversion_construct_foldfoldnegative_body_start. fs_u_dst_inversion_construct_foldfoldnegative = fs_q_dst_inversion_construct_foldfoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_construct_foldfoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_construct_foldfoldnegative_body_terminal. fs_h_dst_inversion_construct_foldfoldnegative_body_terminal + S (dst_negative_sum_inversion_construct_foldfold) = S ((S (S (n))) * fs_v_dst_inversion_construct_foldfoldnegative)) /\ exists fs_q_dst_inversion_construct_foldfoldnegative_body_terminal. fs_u_dst_inversion_construct_foldfoldnegative = fs_q_dst_inversion_construct_foldfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_inversion_construct_foldfoldnegative) + (dst_negative_sum_inversion_construct_foldfold))) /\ forall fs_i_dst_inversion_construct_foldfoldnegative_body_steps. (exists fs_lt_dst_inversion_construct_foldfoldnegative_body_steps_bound. fs_lt_dst_inversion_construct_foldfoldnegative_body_steps_bound + S fs_i_dst_inversion_construct_foldfoldnegative_body_steps = S (n)) -> exists fs_a_dst_inversion_construct_foldfoldnegative_body_steps fs_r_dst_inversion_construct_foldfoldnegative_body_steps fs_s_dst_inversion_construct_foldfoldnegative_body_steps. ((((exists fs_h_dst_inversion_construct_foldfoldnegative_body_steps_summand. fs_h_dst_inversion_construct_foldfoldnegative_body_steps_summand + S (fs_a_dst_inversion_construct_foldfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_construct_foldfoldnegative_body_steps)) * dst_negative_scale_inversion_construct_foldfold)) /\ exists fs_q_dst_inversion_construct_foldfoldnegative_body_steps_summand. dst_negative_code_inversion_construct_foldfold = fs_q_dst_inversion_construct_foldfoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_construct_foldfoldnegative_body_steps)) * dst_negative_scale_inversion_construct_foldfold) + (fs_a_dst_inversion_construct_foldfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_construct_foldfoldnegative_body_steps_partial. fs_h_dst_inversion_construct_foldfoldnegative_body_steps_partial + S (fs_r_dst_inversion_construct_foldfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_construct_foldfoldnegative_body_steps)) * fs_v_dst_inversion_construct_foldfoldnegative)) /\ exists fs_q_dst_inversion_construct_foldfoldnegative_body_steps_partial. fs_u_dst_inversion_construct_foldfoldnegative = fs_q_dst_inversion_construct_foldfoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_construct_foldfoldnegative_body_steps)) * fs_v_dst_inversion_construct_foldfoldnegative) + (fs_r_dst_inversion_construct_foldfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_construct_foldfoldnegative_body_steps_successor. fs_h_dst_inversion_construct_foldfoldnegative_body_steps_successor + S (fs_s_dst_inversion_construct_foldfoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_construct_foldfoldnegative_body_steps)) * fs_v_dst_inversion_construct_foldfoldnegative)) /\ exists fs_q_dst_inversion_construct_foldfoldnegative_body_steps_successor. fs_u_dst_inversion_construct_foldfoldnegative = fs_q_dst_inversion_construct_foldfoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_construct_foldfoldnegative_body_steps)) * fs_v_dst_inversion_construct_foldfoldnegative) + (fs_s_dst_inversion_construct_foldfoldnegative_body_steps))) /\ fs_s_dst_inversion_construct_foldfoldnegative_body_steps = fs_r_dst_inversion_construct_foldfoldnegative_body_steps + fs_a_dst_inversion_construct_foldfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_construct_foldfoldresult ge_balance_negative_inversion_construct_foldfoldresult. (((((a) = 2 * (ge_balance_positive_inversion_construct_foldfoldresult) /\ (ge_balance_negative_inversion_construct_foldfoldresult) = 0) \/ exists ge_signed_half_inversion_construct_foldfoldresultdecode. (((a) = 2 * ge_signed_half_inversion_construct_foldfoldresultdecode + 1 /\ (ge_balance_positive_inversion_construct_foldfoldresult) = 0) /\ (ge_balance_negative_inversion_construct_foldfoldresult) = S ge_signed_half_inversion_construct_foldfoldresultdecode))) /\ ((dst_positive_sum_inversion_construct_foldfold) + ge_balance_negative_inversion_construct_foldfoldresult = (dst_negative_sum_inversion_construct_foldfold) + ge_balance_positive_inversion_construct_foldfoldresult))))))))))))) - 0035
specialize dirichlet_convolution_sum_exists (N) - 0036
specialize dirichlet_convolution_sum_exists (M) - 0037
specialize dirichlet_convolution_sum_exists (G) - 0038
specialize dirichlet_convolution_sum_exists (n) - 0039
apply dirichlet_convolution_sum_exists - 0040
exact hM_left - 0041
exact hG - 0042
exact hn - 0043
exact hbound - 0044
cases hs - 0045
have he : z=x2 - 0046
specialize mobius_dirichlet_inversion_value (N) - 0047
specialize mobius_dirichlet_inversion_value (F) - 0048
specialize mobius_dirichlet_inversion_value (G) - 0049
specialize mobius_dirichlet_inversion_value (M) - 0050
specialize mobius_dirichlet_inversion_value (x) - 0051
specialize mobius_dirichlet_inversion_value (x1) - 0052
specialize mobius_dirichlet_inversion_value (n) - 0053
specialize mobius_dirichlet_inversion_value (z) - 0054
specialize mobius_dirichlet_inversion_value (x2) - 0055
apply mobius_dirichlet_inversion_value - 0056
exact hF - 0057
exact hG - 0058
exact hM - 0059
exact hU_witness_left - 0060
exact hE_witness_left - 0061
exact ht - 0062
exact hn - 0063
exact hbound - 0064
exact hz - 0065
exact hs_witness - 0066
rewrite he - 0067
rewrite he - 0068
exact hs_witness