Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
The full finite signed G007 theorem includes the reverse equivalence and actual witnesses at N=0. The divisor-transform premise covers every required positive quotient. F(0), G(0) and H(0) are unrestricted; only the historical Möbius witness retains its separate zero convention. Full G009 multiplicative closure is admitted in Alpha v32; G091 prime-power fields remain open.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ∀ M. ArithTable(N,F) → ArithTable(N,G) → MobiusTable(N,M) → DivisorTransform(N,F,G) → DirichletTable(N,M,G,F)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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))))))))))))))))))))Complete tactic proof in conservative notation
All 68 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
68 script commands · 19 reading checkpoints · 4 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
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.
- L11
have hU : ∃ U. ConstantOneTable(N,U) ∧ ArithAt(U,0,0)Definitions: ConstantOneTable(N,U)ArithAt(U,0,0)Original native command in the exact edition - L12
specialize dirichlet_constant_one_table_exists (N) - L13
specialize dirichlet_constant_one_table_exists (0) - L14
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.
- L17
have hE : ∃ E. KroneckerDeltaTable(N,E) ∧ ArithAt(E,0,0)Definitions: KroneckerDeltaTable(N,E)ArithAt(E,0,0)Original native command in the exact edition - L18
specialize dirichlet_kronecker_delta_table_exists (N) - L19
specialize dirichlet_kronecker_delta_table_exists (0) - L20
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(M,G,n,a)Original native command in the exact edition - 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 defined 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 : ∃ U. ConstantOneTable(N,U) ∧ ArithAt(U,0,0) - 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 : ∃ E. KroneckerDeltaTable(N,E) ∧ ArithAt(E,0,0) - 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 : ∃ a. DirichletSum(M,G,n,a) - 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