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)) ∧ (DirichletTable(N,M,G,F) → DivisorTransform(N,F,G))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_iff_source dst_positive_scale_iff_source dst_negative_code_iff_source dst_negative_scale_iff_source. (((F) = (((((dst_positive_code_iff_source) + (dst_positive_scale_iff_source)) * S ((dst_positive_code_iff_source) + (dst_positive_scale_iff_source)) + ((dst_positive_scale_iff_source) + (dst_positive_scale_iff_source))) + (((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) * S ((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) + ((dst_negative_scale_iff_source) + (dst_negative_scale_iff_source)))) * S ((((dst_positive_code_iff_source) + (dst_positive_scale_iff_source)) * S ((dst_positive_code_iff_source) + (dst_positive_scale_iff_source)) + ((dst_positive_scale_iff_source) + (dst_positive_scale_iff_source))) + (((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) * S ((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) + ((dst_negative_scale_iff_source) + (dst_negative_scale_iff_source)))) + ((((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) * S ((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) + ((dst_negative_scale_iff_source) + (dst_negative_scale_iff_source))) + (((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) * S ((dst_negative_code_iff_source) + (dst_negative_scale_iff_source)) + ((dst_negative_scale_iff_source) + (dst_negative_scale_iff_source)))))) /\ (forall dst_index_iff_source. (exists pvs_le_gap_iff_sourcedomain. pvs_le_gap_iff_sourcedomain + (dst_index_iff_source) = (N)) -> exists dst_positive_iff_source dst_negative_iff_source dst_value_iff_source. ((((exists ff_h_pvs_iff_sourceentrypositive. ff_h_pvs_iff_sourceentrypositive + S (dst_positive_iff_source) = S ((S (dst_index_iff_source)) * dst_positive_scale_iff_source)) /\ exists ff_q_pvs_iff_sourceentrypositive. dst_positive_code_iff_source = ff_q_pvs_iff_sourceentrypositive * S ((S (dst_index_iff_source)) * dst_positive_scale_iff_source) + (dst_positive_iff_source))) /\ (((((exists ff_h_pvs_iff_sourceentrynegative. ff_h_pvs_iff_sourceentrynegative + S (dst_negative_iff_source) = S ((S (dst_index_iff_source)) * dst_negative_scale_iff_source)) /\ exists ff_q_pvs_iff_sourceentrynegative. dst_negative_code_iff_source = ff_q_pvs_iff_sourceentrynegative * S ((S (dst_index_iff_source)) * dst_negative_scale_iff_source) + (dst_negative_iff_source))) /\ (exists ge_balance_positive_iff_sourceentryvalue ge_balance_negative_iff_sourceentryvalue. (((((dst_value_iff_source) = 2 * (ge_balance_positive_iff_sourceentryvalue) /\ (ge_balance_negative_iff_sourceentryvalue) = 0) \/ exists ge_signed_half_iff_sourceentryvaluedecode. (((dst_value_iff_source) = 2 * ge_signed_half_iff_sourceentryvaluedecode + 1 /\ (ge_balance_positive_iff_sourceentryvalue) = 0) /\ (ge_balance_negative_iff_sourceentryvalue) = S ge_signed_half_iff_sourceentryvaluedecode))) /\ ((dst_positive_iff_source) + ge_balance_negative_iff_sourceentryvalue = (dst_negative_iff_source) + ge_balance_positive_iff_sourceentryvalue))))))))) -> (exists dst_positive_code_iff_transform_table dst_positive_scale_iff_transform_table dst_negative_code_iff_transform_table dst_negative_scale_iff_transform_table. (((G) = (((((dst_positive_code_iff_transform_table) + (dst_positive_scale_iff_transform_table)) * S ((dst_positive_code_iff_transform_table) + (dst_positive_scale_iff_transform_table)) + ((dst_positive_scale_iff_transform_table) + (dst_positive_scale_iff_transform_table))) + (((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) * S ((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) + ((dst_negative_scale_iff_transform_table) + (dst_negative_scale_iff_transform_table)))) * S ((((dst_positive_code_iff_transform_table) + (dst_positive_scale_iff_transform_table)) * S ((dst_positive_code_iff_transform_table) + (dst_positive_scale_iff_transform_table)) + ((dst_positive_scale_iff_transform_table) + (dst_positive_scale_iff_transform_table))) + (((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) * S ((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) + ((dst_negative_scale_iff_transform_table) + (dst_negative_scale_iff_transform_table)))) + ((((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) * S ((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) + ((dst_negative_scale_iff_transform_table) + (dst_negative_scale_iff_transform_table))) + (((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) * S ((dst_negative_code_iff_transform_table) + (dst_negative_scale_iff_transform_table)) + ((dst_negative_scale_iff_transform_table) + (dst_negative_scale_iff_transform_table)))))) /\ (forall dst_index_iff_transform_table. (exists pvs_le_gap_iff_transform_tabledomain. pvs_le_gap_iff_transform_tabledomain + (dst_index_iff_transform_table) = (N)) -> exists dst_positive_iff_transform_table dst_negative_iff_transform_table dst_value_iff_transform_table. ((((exists ff_h_pvs_iff_transform_tableentrypositive. ff_h_pvs_iff_transform_tableentrypositive + S (dst_positive_iff_transform_table) = S ((S (dst_index_iff_transform_table)) * dst_positive_scale_iff_transform_table)) /\ exists ff_q_pvs_iff_transform_tableentrypositive. dst_positive_code_iff_transform_table = ff_q_pvs_iff_transform_tableentrypositive * S ((S (dst_index_iff_transform_table)) * dst_positive_scale_iff_transform_table) + (dst_positive_iff_transform_table))) /\ (((((exists ff_h_pvs_iff_transform_tableentrynegative. ff_h_pvs_iff_transform_tableentrynegative + S (dst_negative_iff_transform_table) = S ((S (dst_index_iff_transform_table)) * dst_negative_scale_iff_transform_table)) /\ exists ff_q_pvs_iff_transform_tableentrynegative. dst_negative_code_iff_transform_table = ff_q_pvs_iff_transform_tableentrynegative * S ((S (dst_index_iff_transform_table)) * dst_negative_scale_iff_transform_table) + (dst_negative_iff_transform_table))) /\ (exists ge_balance_positive_iff_transform_tableentryvalue ge_balance_negative_iff_transform_tableentryvalue. (((((dst_value_iff_transform_table) = 2 * (ge_balance_positive_iff_transform_tableentryvalue) /\ (ge_balance_negative_iff_transform_tableentryvalue) = 0) \/ exists ge_signed_half_iff_transform_tableentryvaluedecode. (((dst_value_iff_transform_table) = 2 * ge_signed_half_iff_transform_tableentryvaluedecode + 1 /\ (ge_balance_positive_iff_transform_tableentryvalue) = 0) /\ (ge_balance_negative_iff_transform_tableentryvalue) = S ge_signed_half_iff_transform_tableentryvaluedecode))) /\ ((dst_positive_iff_transform_table) + ge_balance_negative_iff_transform_tableentryvalue = (dst_negative_iff_transform_table) + ge_balance_positive_iff_transform_tableentryvalue))))))))) -> (((exists dst_positive_code_iff_mobiustable dst_positive_scale_iff_mobiustable dst_negative_code_iff_mobiustable dst_negative_scale_iff_mobiustable. (((M) = (((((dst_positive_code_iff_mobiustable) + (dst_positive_scale_iff_mobiustable)) * S ((dst_positive_code_iff_mobiustable) + (dst_positive_scale_iff_mobiustable)) + ((dst_positive_scale_iff_mobiustable) + (dst_positive_scale_iff_mobiustable))) + (((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) * S ((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) + ((dst_negative_scale_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)))) * S ((((dst_positive_code_iff_mobiustable) + (dst_positive_scale_iff_mobiustable)) * S ((dst_positive_code_iff_mobiustable) + (dst_positive_scale_iff_mobiustable)) + ((dst_positive_scale_iff_mobiustable) + (dst_positive_scale_iff_mobiustable))) + (((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) * S ((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) + ((dst_negative_scale_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)))) + ((((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) * S ((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) + ((dst_negative_scale_iff_mobiustable) + (dst_negative_scale_iff_mobiustable))) + (((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) * S ((dst_negative_code_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)) + ((dst_negative_scale_iff_mobiustable) + (dst_negative_scale_iff_mobiustable)))))) /\ (forall dst_index_iff_mobiustable. (exists pvs_le_gap_iff_mobiustabledomain. pvs_le_gap_iff_mobiustabledomain + (dst_index_iff_mobiustable) = (N)) -> exists dst_positive_iff_mobiustable dst_negative_iff_mobiustable dst_value_iff_mobiustable. ((((exists ff_h_pvs_iff_mobiustableentrypositive. ff_h_pvs_iff_mobiustableentrypositive + S (dst_positive_iff_mobiustable) = S ((S (dst_index_iff_mobiustable)) * dst_positive_scale_iff_mobiustable)) /\ exists ff_q_pvs_iff_mobiustableentrypositive. dst_positive_code_iff_mobiustable = ff_q_pvs_iff_mobiustableentrypositive * S ((S (dst_index_iff_mobiustable)) * dst_positive_scale_iff_mobiustable) + (dst_positive_iff_mobiustable))) /\ (((((exists ff_h_pvs_iff_mobiustableentrynegative. ff_h_pvs_iff_mobiustableentrynegative + S (dst_negative_iff_mobiustable) = S ((S (dst_index_iff_mobiustable)) * dst_negative_scale_iff_mobiustable)) /\ exists ff_q_pvs_iff_mobiustableentrynegative. dst_negative_code_iff_mobiustable = ff_q_pvs_iff_mobiustableentrynegative * S ((S (dst_index_iff_mobiustable)) * dst_negative_scale_iff_mobiustable) + (dst_negative_iff_mobiustable))) /\ (exists ge_balance_positive_iff_mobiustableentryvalue ge_balance_negative_iff_mobiustableentryvalue. (((((dst_value_iff_mobiustable) = 2 * (ge_balance_positive_iff_mobiustableentryvalue) /\ (ge_balance_negative_iff_mobiustableentryvalue) = 0) \/ exists ge_signed_half_iff_mobiustableentryvaluedecode. (((dst_value_iff_mobiustable) = 2 * ge_signed_half_iff_mobiustableentryvaluedecode + 1 /\ (ge_balance_positive_iff_mobiustableentryvalue) = 0) /\ (ge_balance_negative_iff_mobiustableentryvalue) = S ge_signed_half_iff_mobiustableentryvaluedecode))) /\ ((dst_positive_iff_mobiustable) + ge_balance_negative_iff_mobiustableentryvalue = (dst_negative_iff_mobiustable) + ge_balance_positive_iff_mobiustableentryvalue))))))))) /\ (((exists dst_positive_code_iff_mobiuszero dst_positive_scale_iff_mobiuszero dst_negative_code_iff_mobiuszero dst_negative_scale_iff_mobiuszero dst_positive_iff_mobiuszero dst_negative_iff_mobiuszero. (((M) = (((((dst_positive_code_iff_mobiuszero) + (dst_positive_scale_iff_mobiuszero)) * S ((dst_positive_code_iff_mobiuszero) + (dst_positive_scale_iff_mobiuszero)) + ((dst_positive_scale_iff_mobiuszero) + (dst_positive_scale_iff_mobiuszero))) + (((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) * S ((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) + ((dst_negative_scale_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)))) * S ((((dst_positive_code_iff_mobiuszero) + (dst_positive_scale_iff_mobiuszero)) * S ((dst_positive_code_iff_mobiuszero) + (dst_positive_scale_iff_mobiuszero)) + ((dst_positive_scale_iff_mobiuszero) + (dst_positive_scale_iff_mobiuszero))) + (((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) * S ((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) + ((dst_negative_scale_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)))) + ((((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) * S ((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) + ((dst_negative_scale_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero))) + (((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) * S ((dst_negative_code_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)) + ((dst_negative_scale_iff_mobiuszero) + (dst_negative_scale_iff_mobiuszero)))))) /\ (((((exists ff_h_pvs_iff_mobiuszeropositive. ff_h_pvs_iff_mobiuszeropositive + S (dst_positive_iff_mobiuszero) = S ((S (0)) * dst_positive_scale_iff_mobiuszero)) /\ exists ff_q_pvs_iff_mobiuszeropositive. dst_positive_code_iff_mobiuszero = ff_q_pvs_iff_mobiuszeropositive * S ((S (0)) * dst_positive_scale_iff_mobiuszero) + (dst_positive_iff_mobiuszero))) /\ (((((exists ff_h_pvs_iff_mobiuszeronegative. ff_h_pvs_iff_mobiuszeronegative + S (dst_negative_iff_mobiuszero) = S ((S (0)) * dst_negative_scale_iff_mobiuszero)) /\ exists ff_q_pvs_iff_mobiuszeronegative. dst_negative_code_iff_mobiuszero = ff_q_pvs_iff_mobiuszeronegative * S ((S (0)) * dst_negative_scale_iff_mobiuszero) + (dst_negative_iff_mobiuszero))) /\ (exists ge_balance_positive_iff_mobiuszerovalue ge_balance_negative_iff_mobiuszerovalue. (((((0) = 2 * (ge_balance_positive_iff_mobiuszerovalue) /\ (ge_balance_negative_iff_mobiuszerovalue) = 0) \/ exists ge_signed_half_iff_mobiuszerovaluedecode. (((0) = 2 * ge_signed_half_iff_mobiuszerovaluedecode + 1 /\ (ge_balance_positive_iff_mobiuszerovalue) = 0) /\ (ge_balance_negative_iff_mobiuszerovalue) = S ge_signed_half_iff_mobiuszerovaluedecode))) /\ ((dst_positive_iff_mobiuszero) + ge_balance_negative_iff_mobiuszerovalue = (dst_negative_iff_mobiuszero) + ge_balance_positive_iff_mobiuszerovalue))))))))) /\ (forall mt_index_iff_mobius mt_value_iff_mobius. ~(mt_index_iff_mobius=0) -> (exists pvs_le_gap_iff_mobiusdomain. pvs_le_gap_iff_mobiusdomain + (mt_index_iff_mobius) = (N)) -> (exists dst_positive_code_iff_mobiusentry dst_positive_scale_iff_mobiusentry dst_negative_code_iff_mobiusentry dst_negative_scale_iff_mobiusentry dst_positive_iff_mobiusentry dst_negative_iff_mobiusentry. (((M) = (((((dst_positive_code_iff_mobiusentry) + (dst_positive_scale_iff_mobiusentry)) * S ((dst_positive_code_iff_mobiusentry) + (dst_positive_scale_iff_mobiusentry)) + ((dst_positive_scale_iff_mobiusentry) + (dst_positive_scale_iff_mobiusentry))) + (((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) * S ((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) + ((dst_negative_scale_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)))) * S ((((dst_positive_code_iff_mobiusentry) + (dst_positive_scale_iff_mobiusentry)) * S ((dst_positive_code_iff_mobiusentry) + (dst_positive_scale_iff_mobiusentry)) + ((dst_positive_scale_iff_mobiusentry) + (dst_positive_scale_iff_mobiusentry))) + (((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) * S ((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) + ((dst_negative_scale_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)))) + ((((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) * S ((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) + ((dst_negative_scale_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry))) + (((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) * S ((dst_negative_code_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)) + ((dst_negative_scale_iff_mobiusentry) + (dst_negative_scale_iff_mobiusentry)))))) /\ (((((exists ff_h_pvs_iff_mobiusentrypositive. ff_h_pvs_iff_mobiusentrypositive + S (dst_positive_iff_mobiusentry) = S ((S (mt_index_iff_mobius)) * dst_positive_scale_iff_mobiusentry)) /\ exists ff_q_pvs_iff_mobiusentrypositive. dst_positive_code_iff_mobiusentry = ff_q_pvs_iff_mobiusentrypositive * S ((S (mt_index_iff_mobius)) * dst_positive_scale_iff_mobiusentry) + (dst_positive_iff_mobiusentry))) /\ (((((exists ff_h_pvs_iff_mobiusentrynegative. ff_h_pvs_iff_mobiusentrynegative + S (dst_negative_iff_mobiusentry) = S ((S (mt_index_iff_mobius)) * dst_negative_scale_iff_mobiusentry)) /\ exists ff_q_pvs_iff_mobiusentrynegative. dst_negative_code_iff_mobiusentry = ff_q_pvs_iff_mobiusentrynegative * S ((S (mt_index_iff_mobius)) * dst_negative_scale_iff_mobiusentry) + (dst_negative_iff_mobiusentry))) /\ (exists ge_balance_positive_iff_mobiusentryvalue ge_balance_negative_iff_mobiusentryvalue. (((((mt_value_iff_mobius) = 2 * (ge_balance_positive_iff_mobiusentryvalue) /\ (ge_balance_negative_iff_mobiusentryvalue) = 0) \/ exists ge_signed_half_iff_mobiusentryvaluedecode. (((mt_value_iff_mobius) = 2 * ge_signed_half_iff_mobiusentryvaluedecode + 1 /\ (ge_balance_positive_iff_mobiusentryvalue) = 0) /\ (ge_balance_negative_iff_mobiusentryvalue) = S ge_signed_half_iff_mobiusentryvaluedecode))) /\ ((dst_positive_iff_mobiusentry) + ge_balance_negative_iff_mobiusentryvalue = (dst_negative_iff_mobiusentry) + ge_balance_positive_iff_mobiusentryvalue))))))))) -> (((~((mt_index_iff_mobius) = 0)) /\ ((((exists mv_square_prime_iff_mobiusvaluesquare. ((~((mv_square_prime_iff_mobiusvaluesquare) = 1) /\ forall pvs_left_iff_mobiusvaluesquareprime pvs_right_iff_mobiusvaluesquareprime. (mv_square_prime_iff_mobiusvaluesquare) = pvs_left_iff_mobiusvaluesquareprime * pvs_right_iff_mobiusvaluesquareprime -> pvs_left_iff_mobiusvaluesquareprime = 1 \/ pvs_right_iff_mobiusvaluesquareprime = 1) /\ (exists pvs_factor_iff_mobiusvaluesquaredivisor. (mt_index_iff_mobius) = (mv_square_prime_iff_mobiusvaluesquare * mv_square_prime_iff_mobiusvaluesquare) * pvs_factor_iff_mobiusvaluesquaredivisor))) /\ ((mt_value_iff_mobius) = 0))) \/ (((((~((mt_index_iff_mobius) = 0)) /\ (forall sfd_prime_iff_mobiusvaluesquarefree. (~((sfd_prime_iff_mobiusvaluesquarefree) = 1) /\ forall pvs_left_iff_mobiusvaluesquarefreedomain pvs_right_iff_mobiusvaluesquarefreedomain. (sfd_prime_iff_mobiusvaluesquarefree) = pvs_left_iff_mobiusvaluesquarefreedomain * pvs_right_iff_mobiusvaluesquarefreedomain -> pvs_left_iff_mobiusvaluesquarefreedomain = 1 \/ pvs_right_iff_mobiusvaluesquarefreedomain = 1) -> (exists pvs_le_gap_iff_mobiusvaluesquarefreebound. pvs_le_gap_iff_mobiusvaluesquarefreebound + (sfd_prime_iff_mobiusvaluesquarefree) = (mt_index_iff_mobius)) -> ~(exists pvs_factor_iff_mobiusvaluesquarefreesquare. (mt_index_iff_mobius) = (sfd_prime_iff_mobiusvaluesquarefree * sfd_prime_iff_mobiusvaluesquarefree) * pvs_factor_iff_mobiusvaluesquarefreesquare)))) /\ (exists mv_factor_code_iff_mobiusvaluefactors mv_factor_scale_iff_mobiusvaluefactors mv_factor_count_iff_mobiusvaluefactors. (((~(mt_index_iff_mobius = 0) /\ ((exists ff_u_fsat_iff_mobiusvaluefactorsfactorization_product ff_v_fsat_iff_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_start. ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_start. ff_u_fsat_iff_mobiusvaluefactorsfactorization_product = ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_terminal. ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_terminal + S (mt_index_iff_mobius) = S ((S (mv_factor_count_iff_mobiusvaluefactors)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_terminal. ff_u_fsat_iff_mobiusvaluefactorsfactorization_product = ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_iff_mobiusvaluefactors)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product) + (mt_index_iff_mobius))) /\ forall ff_i_fsat_iff_mobiusvaluefactorsfactorization_product. (exists ff_lt_fsat_iff_mobiusvaluefactorsfactorization_product_bound. ff_lt_fsat_iff_mobiusvaluefactorsfactorization_product_bound + S ff_i_fsat_iff_mobiusvaluefactorsfactorization_product = mv_factor_count_iff_mobiusvaluefactors) -> exists ff_p_fsat_iff_mobiusvaluefactorsfactorization_product ff_r_fsat_iff_mobiusvaluefactorsfactorization_product ff_s_fsat_iff_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_factor. ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_factor + S (ff_p_fsat_iff_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_iff_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_iff_mobiusvaluefactors)) /\ exists ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_factor. mv_factor_code_iff_mobiusvaluefactors = ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_iff_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_iff_mobiusvaluefactors) + (ff_p_fsat_iff_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_partial. ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_partial + S (ff_r_fsat_iff_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_iff_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_partial. ff_u_fsat_iff_mobiusvaluefactorsfactorization_product = ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_iff_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product) + (ff_r_fsat_iff_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_successor. ff_h_fsat_iff_mobiusvaluefactorsfactorization_product_successor + S (ff_s_fsat_iff_mobiusvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_iff_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_successor. ff_u_fsat_iff_mobiusvaluefactorsfactorization_product = ff_q_fsat_iff_mobiusvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_iff_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_iff_mobiusvaluefactorsfactorization_product) + (ff_s_fsat_iff_mobiusvaluefactorsfactorization_product))) /\ ff_s_fsat_iff_mobiusvaluefactorsfactorization_product = ff_r_fsat_iff_mobiusvaluefactorsfactorization_product * ff_p_fsat_iff_mobiusvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_iff_mobiusvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_iff_mobiusvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_iff_mobiusvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_iff_mobiusvaluefactorsfactorization_primes = (mv_factor_count_iff_mobiusvaluefactors)) -> exists ftsf_factor_fsat_iff_mobiusvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_iff_mobiusvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_iff_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_iff_mobiusvaluefactors)) /\ exists ff_q_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_entry. mv_factor_code_iff_mobiusvaluefactors = ff_q_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_iff_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_iff_mobiusvaluefactors) + (ftsf_factor_fsat_iff_mobiusvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_iff_mobiusvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_iff_mobiusvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_iff_mobiusvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_iff_mobiusvaluefactorsparityeven. (mv_factor_count_iff_mobiusvaluefactors) = 2 * mv_even_half_iff_mobiusvaluefactorsparityeven) /\ ((mt_value_iff_mobius) = 2))) \/ (((exists mv_odd_half_iff_mobiusvaluefactorsparityodd. (mv_factor_count_iff_mobiusvaluefactors) = 2 * mv_odd_half_iff_mobiusvaluefactorsparityodd + 1) /\ ((mt_value_iff_mobius) = 1)))))))))))))))) -> (((forall mi_index_inversion_iff_transform mi_value_inversion_iff_transform. ~(mi_index_inversion_iff_transform=0) -> (exists pvs_le_gap_inversion_iff_transformbound. pvs_le_gap_inversion_iff_transformbound + (mi_index_inversion_iff_transform) = (N)) -> (exists dst_positive_code_inversion_iff_transformentry dst_positive_scale_inversion_iff_transformentry dst_negative_code_inversion_iff_transformentry dst_negative_scale_inversion_iff_transformentry dst_positive_inversion_iff_transformentry dst_negative_inversion_iff_transformentry. (((G) = (((((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) * S ((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) + ((dst_positive_scale_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry))) + (((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)))) * S ((((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) * S ((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) + ((dst_positive_scale_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry))) + (((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)))) + ((((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry))) + (((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)))))) /\ (((((exists ff_h_pvs_inversion_iff_transformentrypositive. ff_h_pvs_inversion_iff_transformentrypositive + S (dst_positive_inversion_iff_transformentry) = S ((S (mi_index_inversion_iff_transform)) * dst_positive_scale_inversion_iff_transformentry)) /\ exists ff_q_pvs_inversion_iff_transformentrypositive. dst_positive_code_inversion_iff_transformentry = ff_q_pvs_inversion_iff_transformentrypositive * S ((S (mi_index_inversion_iff_transform)) * dst_positive_scale_inversion_iff_transformentry) + (dst_positive_inversion_iff_transformentry))) /\ (((((exists ff_h_pvs_inversion_iff_transformentrynegative. ff_h_pvs_inversion_iff_transformentrynegative + S (dst_negative_inversion_iff_transformentry) = S ((S (mi_index_inversion_iff_transform)) * dst_negative_scale_inversion_iff_transformentry)) /\ exists ff_q_pvs_inversion_iff_transformentrynegative. dst_negative_code_inversion_iff_transformentry = ff_q_pvs_inversion_iff_transformentrynegative * S ((S (mi_index_inversion_iff_transform)) * dst_negative_scale_inversion_iff_transformentry) + (dst_negative_inversion_iff_transformentry))) /\ (exists ge_balance_positive_inversion_iff_transformentryvalue ge_balance_negative_inversion_iff_transformentryvalue. (((((mi_value_inversion_iff_transform) = 2 * (ge_balance_positive_inversion_iff_transformentryvalue) /\ (ge_balance_negative_inversion_iff_transformentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformentryvaluedecode. (((mi_value_inversion_iff_transform) = 2 * ge_signed_half_inversion_iff_transformentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformentryvalue) = S ge_signed_half_inversion_iff_transformentryvaluedecode))) /\ ((dst_positive_inversion_iff_transformentry) + ge_balance_negative_inversion_iff_transformentryvalue = (dst_negative_inversion_iff_transformentry) + ge_balance_positive_inversion_iff_transformentryvalue))))))))) -> (((~((mi_index_inversion_iff_transform)=0)) /\ (exists dm_mask_table_inversion_iff_transformsum. ((((exists dst_positive_code_inversion_iff_transformsummasktable dst_positive_scale_inversion_iff_transformsummasktable dst_negative_code_inversion_iff_transformsummasktable dst_negative_scale_inversion_iff_transformsummasktable. (((dm_mask_table_inversion_iff_transformsum) = (((((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) * S ((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) + ((dst_positive_scale_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable))) + (((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)))) * S ((((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) * S ((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) + ((dst_positive_scale_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable))) + (((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)))) + ((((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable))) + (((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)))))) /\ (forall dst_index_inversion_iff_transformsummasktable. (exists pvs_le_gap_inversion_iff_transformsummasktabledomain. pvs_le_gap_inversion_iff_transformsummasktabledomain + (dst_index_inversion_iff_transformsummasktable) = (mi_index_inversion_iff_transform)) -> exists dst_positive_inversion_iff_transformsummasktable dst_negative_inversion_iff_transformsummasktable dst_value_inversion_iff_transformsummasktable. ((((exists ff_h_pvs_inversion_iff_transformsummasktableentrypositive. ff_h_pvs_inversion_iff_transformsummasktableentrypositive + S (dst_positive_inversion_iff_transformsummasktable) = S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_positive_scale_inversion_iff_transformsummasktable)) /\ exists ff_q_pvs_inversion_iff_transformsummasktableentrypositive. dst_positive_code_inversion_iff_transformsummasktable = ff_q_pvs_inversion_iff_transformsummasktableentrypositive * S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_positive_scale_inversion_iff_transformsummasktable) + (dst_positive_inversion_iff_transformsummasktable))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummasktableentrynegative. ff_h_pvs_inversion_iff_transformsummasktableentrynegative + S (dst_negative_inversion_iff_transformsummasktable) = S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_negative_scale_inversion_iff_transformsummasktable)) /\ exists ff_q_pvs_inversion_iff_transformsummasktableentrynegative. dst_negative_code_inversion_iff_transformsummasktable = ff_q_pvs_inversion_iff_transformsummasktableentrynegative * S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_inversion_iff_transformsummasktable))) /\ (exists ge_balance_positive_inversion_iff_transformsummasktableentryvalue ge_balance_negative_inversion_iff_transformsummasktableentryvalue. (((((dst_value_inversion_iff_transformsummasktable) = 2 * (ge_balance_positive_inversion_iff_transformsummasktableentryvalue) /\ (ge_balance_negative_inversion_iff_transformsummasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformsummasktableentryvaluedecode. (((dst_value_inversion_iff_transformsummasktable) = 2 * ge_signed_half_inversion_iff_transformsummasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformsummasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformsummasktableentryvalue) = S ge_signed_half_inversion_iff_transformsummasktableentryvaluedecode))) /\ ((dst_positive_inversion_iff_transformsummasktable) + ge_balance_negative_inversion_iff_transformsummasktableentryvalue = (dst_negative_inversion_iff_transformsummasktable) + ge_balance_positive_inversion_iff_transformsummasktableentryvalue))))))))) /\ (forall dm_index_inversion_iff_transformsummask dm_value_inversion_iff_transformsummask. (exists pvs_le_gap_inversion_iff_transformsummaskdomain. pvs_le_gap_inversion_iff_transformsummaskdomain + (dm_index_inversion_iff_transformsummask) = (mi_index_inversion_iff_transform)) -> (exists dst_positive_code_inversion_iff_transformsummasklookup dst_positive_scale_inversion_iff_transformsummasklookup dst_negative_code_inversion_iff_transformsummasklookup dst_negative_scale_inversion_iff_transformsummasklookup dst_positive_inversion_iff_transformsummasklookup dst_negative_inversion_iff_transformsummasklookup. (((dm_mask_table_inversion_iff_transformsum) = (((((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) * S ((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) + ((dst_positive_scale_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup))) + (((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)))) * S ((((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) * S ((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) + ((dst_positive_scale_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup))) + (((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)))) + ((((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup))) + (((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)))))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummasklookuppositive. ff_h_pvs_inversion_iff_transformsummasklookuppositive + S (dst_positive_inversion_iff_transformsummasklookup) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummasklookup)) /\ exists ff_q_pvs_inversion_iff_transformsummasklookuppositive. dst_positive_code_inversion_iff_transformsummasklookup = ff_q_pvs_inversion_iff_transformsummasklookuppositive * S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummasklookup) + (dst_positive_inversion_iff_transformsummasklookup))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummasklookupnegative. ff_h_pvs_inversion_iff_transformsummasklookupnegative + S (dst_negative_inversion_iff_transformsummasklookup) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummasklookup)) /\ exists ff_q_pvs_inversion_iff_transformsummasklookupnegative. dst_negative_code_inversion_iff_transformsummasklookup = ff_q_pvs_inversion_iff_transformsummasklookupnegative * S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_inversion_iff_transformsummasklookup))) /\ (exists ge_balance_positive_inversion_iff_transformsummasklookupvalue ge_balance_negative_inversion_iff_transformsummasklookupvalue. (((((dm_value_inversion_iff_transformsummask) = 2 * (ge_balance_positive_inversion_iff_transformsummasklookupvalue) /\ (ge_balance_negative_inversion_iff_transformsummasklookupvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformsummasklookupvaluedecode. (((dm_value_inversion_iff_transformsummask) = 2 * ge_signed_half_inversion_iff_transformsummasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformsummasklookupvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformsummasklookupvalue) = S ge_signed_half_inversion_iff_transformsummasklookupvaluedecode))) /\ ((dst_positive_inversion_iff_transformsummasklookup) + ge_balance_negative_inversion_iff_transformsummasklookupvalue = (dst_negative_inversion_iff_transformsummasklookup) + ge_balance_positive_inversion_iff_transformsummasklookupvalue))))))))) -> ((((~((dm_index_inversion_iff_transformsummask)=0)) /\ (exists dm_quotient_inversion_iff_transformsummaskentry. (((mi_index_inversion_iff_transform)=(dm_index_inversion_iff_transformsummask)*dm_quotient_inversion_iff_transformsummaskentry) /\ (exists dst_positive_code_inversion_iff_transformsummaskentryinput dst_positive_scale_inversion_iff_transformsummaskentryinput dst_negative_code_inversion_iff_transformsummaskentryinput dst_negative_scale_inversion_iff_transformsummaskentryinput dst_positive_inversion_iff_transformsummaskentryinput dst_negative_inversion_iff_transformsummaskentryinput. (((F) = (((((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) + ((dst_positive_scale_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput))) + (((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)))) * S ((((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) + ((dst_positive_scale_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput))) + (((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)))) + ((((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput))) + (((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)))))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummaskentryinputpositive. ff_h_pvs_inversion_iff_transformsummaskentryinputpositive + S (dst_positive_inversion_iff_transformsummaskentryinput) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummaskentryinput)) /\ exists ff_q_pvs_inversion_iff_transformsummaskentryinputpositive. dst_positive_code_inversion_iff_transformsummaskentryinput = ff_q_pvs_inversion_iff_transformsummaskentryinputpositive * S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummaskentryinput) + (dst_positive_inversion_iff_transformsummaskentryinput))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummaskentryinputnegative. ff_h_pvs_inversion_iff_transformsummaskentryinputnegative + S (dst_negative_inversion_iff_transformsummaskentryinput) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummaskentryinput)) /\ exists ff_q_pvs_inversion_iff_transformsummaskentryinputnegative. dst_negative_code_inversion_iff_transformsummaskentryinput = ff_q_pvs_inversion_iff_transformsummaskentryinputnegative * S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_inversion_iff_transformsummaskentryinput))) /\ (exists ge_balance_positive_inversion_iff_transformsummaskentryinputvalue ge_balance_negative_inversion_iff_transformsummaskentryinputvalue. (((((dm_value_inversion_iff_transformsummask) = 2 * (ge_balance_positive_inversion_iff_transformsummaskentryinputvalue) /\ (ge_balance_negative_inversion_iff_transformsummaskentryinputvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformsummaskentryinputvaluedecode. (((dm_value_inversion_iff_transformsummask) = 2 * ge_signed_half_inversion_iff_transformsummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformsummaskentryinputvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformsummaskentryinputvalue) = S ge_signed_half_inversion_iff_transformsummaskentryinputvaluedecode))) /\ ((dst_positive_inversion_iff_transformsummaskentryinput) + ge_balance_negative_inversion_iff_transformsummaskentryinputvalue = (dst_negative_inversion_iff_transformsummaskentryinput) + ge_balance_positive_inversion_iff_transformsummaskentryinputvalue))))))))))))) \/ ((((dm_index_inversion_iff_transformsummask)=0 \/ ~(exists pvs_factor_inversion_iff_transformsummaskentrynondivisor. (mi_index_inversion_iff_transform) = (dm_index_inversion_iff_transformsummask) * pvs_factor_inversion_iff_transformsummaskentrynondivisor)) /\ ((dm_value_inversion_iff_transformsummask)=0))))))) /\ (exists dst_positive_code_inversion_iff_transformsumfold dst_positive_scale_inversion_iff_transformsumfold dst_negative_code_inversion_iff_transformsumfold dst_negative_scale_inversion_iff_transformsumfold dst_positive_sum_inversion_iff_transformsumfold dst_negative_sum_inversion_iff_transformsumfold. (((dm_mask_table_inversion_iff_transformsum) = (((((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) * S ((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) + ((dst_positive_scale_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold))) + (((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)))) * S ((((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) * S ((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) + ((dst_positive_scale_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold))) + (((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)))) + ((((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold))) + (((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)))))) /\ (((exists fs_u_dst_inversion_iff_transformsumfoldpositive fs_v_dst_inversion_iff_transformsumfoldpositive. ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_start. fs_h_dst_inversion_iff_transformsumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_start. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_terminal. fs_h_dst_inversion_iff_transformsumfoldpositive_body_terminal + S (dst_positive_sum_inversion_iff_transformsumfold) = S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_terminal. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_terminal * S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (dst_positive_sum_inversion_iff_transformsumfold))) /\ forall fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps. (exists fs_lt_dst_inversion_iff_transformsumfoldpositive_body_steps_bound. fs_lt_dst_inversion_iff_transformsumfoldpositive_body_steps_bound + S fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps = S (mi_index_inversion_iff_transform)) -> exists fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps. ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_summand. fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_summand + S (fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * dst_positive_scale_inversion_iff_transformsumfold)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_summand. dst_positive_code_inversion_iff_transformsumfold = fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * dst_positive_scale_inversion_iff_transformsumfold) + (fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_partial. fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_partial + S (fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_partial. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_successor. fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_successor + S (fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_successor. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps))) /\ fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps = fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps + fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_iff_transformsumfoldnegative fs_v_dst_inversion_iff_transformsumfoldnegative. ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_start. fs_h_dst_inversion_iff_transformsumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_start. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_terminal. fs_h_dst_inversion_iff_transformsumfoldnegative_body_terminal + S (dst_negative_sum_inversion_iff_transformsumfold) = S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_terminal. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_terminal * S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (dst_negative_sum_inversion_iff_transformsumfold))) /\ forall fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps. (exists fs_lt_dst_inversion_iff_transformsumfoldnegative_body_steps_bound. fs_lt_dst_inversion_iff_transformsumfoldnegative_body_steps_bound + S fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps = S (mi_index_inversion_iff_transform)) -> exists fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps. ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_summand. fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_summand + S (fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * dst_negative_scale_inversion_iff_transformsumfold)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_summand. dst_negative_code_inversion_iff_transformsumfold = fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * dst_negative_scale_inversion_iff_transformsumfold) + (fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_partial. fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_partial + S (fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_partial. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_successor. fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_successor + S (fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_successor. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps))) /\ fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps = fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps + fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_iff_transformsumfoldresult ge_balance_negative_inversion_iff_transformsumfoldresult. (((((mi_value_inversion_iff_transform) = 2 * (ge_balance_positive_inversion_iff_transformsumfoldresult) /\ (ge_balance_negative_inversion_iff_transformsumfoldresult) = 0) \/ exists ge_signed_half_inversion_iff_transformsumfoldresultdecode. (((mi_value_inversion_iff_transform) = 2 * ge_signed_half_inversion_iff_transformsumfoldresultdecode + 1 /\ (ge_balance_positive_inversion_iff_transformsumfoldresult) = 0) /\ (ge_balance_negative_inversion_iff_transformsumfoldresult) = S ge_signed_half_inversion_iff_transformsumfoldresultdecode))) /\ ((dst_positive_sum_inversion_iff_transformsumfold) + ge_balance_negative_inversion_iff_transformsumfoldresult = (dst_negative_sum_inversion_iff_transformsumfold) + ge_balance_positive_inversion_iff_transformsumfoldresult)))))))))))))) -> (((exists dst_positive_code_inversion_iff_convolutionleft dst_positive_scale_inversion_iff_convolutionleft dst_negative_code_inversion_iff_convolutionleft dst_negative_scale_inversion_iff_convolutionleft. (((M) = (((((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) * S ((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) + ((dst_positive_scale_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft))) + (((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)))) * S ((((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) * S ((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) + ((dst_positive_scale_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft))) + (((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)))) + ((((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft))) + (((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)))))) /\ (forall dst_index_inversion_iff_convolutionleft. (exists pvs_le_gap_inversion_iff_convolutionleftdomain. pvs_le_gap_inversion_iff_convolutionleftdomain + (dst_index_inversion_iff_convolutionleft) = (N)) -> exists dst_positive_inversion_iff_convolutionleft dst_negative_inversion_iff_convolutionleft dst_value_inversion_iff_convolutionleft. ((((exists ff_h_pvs_inversion_iff_convolutionleftentrypositive. ff_h_pvs_inversion_iff_convolutionleftentrypositive + S (dst_positive_inversion_iff_convolutionleft) = S ((S (dst_index_inversion_iff_convolutionleft)) * dst_positive_scale_inversion_iff_convolutionleft)) /\ exists ff_q_pvs_inversion_iff_convolutionleftentrypositive. dst_positive_code_inversion_iff_convolutionleft = ff_q_pvs_inversion_iff_convolutionleftentrypositive * S ((S (dst_index_inversion_iff_convolutionleft)) * dst_positive_scale_inversion_iff_convolutionleft) + (dst_positive_inversion_iff_convolutionleft))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionleftentrynegative. ff_h_pvs_inversion_iff_convolutionleftentrynegative + S (dst_negative_inversion_iff_convolutionleft) = S ((S (dst_index_inversion_iff_convolutionleft)) * dst_negative_scale_inversion_iff_convolutionleft)) /\ exists ff_q_pvs_inversion_iff_convolutionleftentrynegative. dst_negative_code_inversion_iff_convolutionleft = ff_q_pvs_inversion_iff_convolutionleftentrynegative * S ((S (dst_index_inversion_iff_convolutionleft)) * dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_inversion_iff_convolutionleft))) /\ (exists ge_balance_positive_inversion_iff_convolutionleftentryvalue ge_balance_negative_inversion_iff_convolutionleftentryvalue. (((((dst_value_inversion_iff_convolutionleft) = 2 * (ge_balance_positive_inversion_iff_convolutionleftentryvalue) /\ (ge_balance_negative_inversion_iff_convolutionleftentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionleftentryvaluedecode. (((dst_value_inversion_iff_convolutionleft) = 2 * ge_signed_half_inversion_iff_convolutionleftentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionleftentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionleftentryvalue) = S ge_signed_half_inversion_iff_convolutionleftentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionleft) + ge_balance_negative_inversion_iff_convolutionleftentryvalue = (dst_negative_inversion_iff_convolutionleft) + ge_balance_positive_inversion_iff_convolutionleftentryvalue))))))))) /\ (((exists dst_positive_code_inversion_iff_convolutionright dst_positive_scale_inversion_iff_convolutionright dst_negative_code_inversion_iff_convolutionright dst_negative_scale_inversion_iff_convolutionright. (((G) = (((((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) * S ((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) + ((dst_positive_scale_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright))) + (((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)))) * S ((((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) * S ((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) + ((dst_positive_scale_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright))) + (((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)))) + ((((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright))) + (((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)))))) /\ (forall dst_index_inversion_iff_convolutionright. (exists pvs_le_gap_inversion_iff_convolutionrightdomain. pvs_le_gap_inversion_iff_convolutionrightdomain + (dst_index_inversion_iff_convolutionright) = (N)) -> exists dst_positive_inversion_iff_convolutionright dst_negative_inversion_iff_convolutionright dst_value_inversion_iff_convolutionright. ((((exists ff_h_pvs_inversion_iff_convolutionrightentrypositive. ff_h_pvs_inversion_iff_convolutionrightentrypositive + S (dst_positive_inversion_iff_convolutionright) = S ((S (dst_index_inversion_iff_convolutionright)) * dst_positive_scale_inversion_iff_convolutionright)) /\ exists ff_q_pvs_inversion_iff_convolutionrightentrypositive. dst_positive_code_inversion_iff_convolutionright = ff_q_pvs_inversion_iff_convolutionrightentrypositive * S ((S (dst_index_inversion_iff_convolutionright)) * dst_positive_scale_inversion_iff_convolutionright) + (dst_positive_inversion_iff_convolutionright))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionrightentrynegative. ff_h_pvs_inversion_iff_convolutionrightentrynegative + S (dst_negative_inversion_iff_convolutionright) = S ((S (dst_index_inversion_iff_convolutionright)) * dst_negative_scale_inversion_iff_convolutionright)) /\ exists ff_q_pvs_inversion_iff_convolutionrightentrynegative. dst_negative_code_inversion_iff_convolutionright = ff_q_pvs_inversion_iff_convolutionrightentrynegative * S ((S (dst_index_inversion_iff_convolutionright)) * dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_inversion_iff_convolutionright))) /\ (exists ge_balance_positive_inversion_iff_convolutionrightentryvalue ge_balance_negative_inversion_iff_convolutionrightentryvalue. (((((dst_value_inversion_iff_convolutionright) = 2 * (ge_balance_positive_inversion_iff_convolutionrightentryvalue) /\ (ge_balance_negative_inversion_iff_convolutionrightentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionrightentryvaluedecode. (((dst_value_inversion_iff_convolutionright) = 2 * ge_signed_half_inversion_iff_convolutionrightentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionrightentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionrightentryvalue) = S ge_signed_half_inversion_iff_convolutionrightentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionright) + ge_balance_negative_inversion_iff_convolutionrightentryvalue = (dst_negative_inversion_iff_convolutionright) + ge_balance_positive_inversion_iff_convolutionrightentryvalue))))))))) /\ (((exists dst_positive_code_inversion_iff_convolutiontable dst_positive_scale_inversion_iff_convolutiontable dst_negative_code_inversion_iff_convolutiontable dst_negative_scale_inversion_iff_convolutiontable. (((F) = (((((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) * S ((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) + ((dst_positive_scale_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable))) + (((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)))) * S ((((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) * S ((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) + ((dst_positive_scale_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable))) + (((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)))) + ((((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable))) + (((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)))))) /\ (forall dst_index_inversion_iff_convolutiontable. (exists pvs_le_gap_inversion_iff_convolutiontabledomain. pvs_le_gap_inversion_iff_convolutiontabledomain + (dst_index_inversion_iff_convolutiontable) = (N)) -> exists dst_positive_inversion_iff_convolutiontable dst_negative_inversion_iff_convolutiontable dst_value_inversion_iff_convolutiontable. ((((exists ff_h_pvs_inversion_iff_convolutiontableentrypositive. ff_h_pvs_inversion_iff_convolutiontableentrypositive + S (dst_positive_inversion_iff_convolutiontable) = S ((S (dst_index_inversion_iff_convolutiontable)) * dst_positive_scale_inversion_iff_convolutiontable)) /\ exists ff_q_pvs_inversion_iff_convolutiontableentrypositive. dst_positive_code_inversion_iff_convolutiontable = ff_q_pvs_inversion_iff_convolutiontableentrypositive * S ((S (dst_index_inversion_iff_convolutiontable)) * dst_positive_scale_inversion_iff_convolutiontable) + (dst_positive_inversion_iff_convolutiontable))) /\ (((((exists ff_h_pvs_inversion_iff_convolutiontableentrynegative. ff_h_pvs_inversion_iff_convolutiontableentrynegative + S (dst_negative_inversion_iff_convolutiontable) = S ((S (dst_index_inversion_iff_convolutiontable)) * dst_negative_scale_inversion_iff_convolutiontable)) /\ exists ff_q_pvs_inversion_iff_convolutiontableentrynegative. dst_negative_code_inversion_iff_convolutiontable = ff_q_pvs_inversion_iff_convolutiontableentrynegative * S ((S (dst_index_inversion_iff_convolutiontable)) * dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_inversion_iff_convolutiontable))) /\ (exists ge_balance_positive_inversion_iff_convolutiontableentryvalue ge_balance_negative_inversion_iff_convolutiontableentryvalue. (((((dst_value_inversion_iff_convolutiontable) = 2 * (ge_balance_positive_inversion_iff_convolutiontableentryvalue) /\ (ge_balance_negative_inversion_iff_convolutiontableentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutiontableentryvaluedecode. (((dst_value_inversion_iff_convolutiontable) = 2 * ge_signed_half_inversion_iff_convolutiontableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutiontableentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutiontableentryvalue) = S ge_signed_half_inversion_iff_convolutiontableentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutiontable) + ge_balance_negative_inversion_iff_convolutiontableentryvalue = (dst_negative_inversion_iff_convolutiontable) + ge_balance_positive_inversion_iff_convolutiontableentryvalue))))))))) /\ (forall dc_input_inversion_iff_convolution dc_output_inversion_iff_convolution. ~(dc_input_inversion_iff_convolution=0) -> (exists pvs_le_gap_inversion_iff_convolutiondomain. pvs_le_gap_inversion_iff_convolutiondomain + (dc_input_inversion_iff_convolution) = (N)) -> (exists dst_positive_code_inversion_iff_convolutionlookup dst_positive_scale_inversion_iff_convolutionlookup dst_negative_code_inversion_iff_convolutionlookup dst_negative_scale_inversion_iff_convolutionlookup dst_positive_inversion_iff_convolutionlookup dst_negative_inversion_iff_convolutionlookup. (((F) = (((((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) * S ((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) + ((dst_positive_scale_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup))) + (((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)))) * S ((((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) * S ((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) + ((dst_positive_scale_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup))) + (((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)))) + ((((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup))) + (((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionlookuppositive. ff_h_pvs_inversion_iff_convolutionlookuppositive + S (dst_positive_inversion_iff_convolutionlookup) = S ((S (dc_input_inversion_iff_convolution)) * dst_positive_scale_inversion_iff_convolutionlookup)) /\ exists ff_q_pvs_inversion_iff_convolutionlookuppositive. dst_positive_code_inversion_iff_convolutionlookup = ff_q_pvs_inversion_iff_convolutionlookuppositive * S ((S (dc_input_inversion_iff_convolution)) * dst_positive_scale_inversion_iff_convolutionlookup) + (dst_positive_inversion_iff_convolutionlookup))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionlookupnegative. ff_h_pvs_inversion_iff_convolutionlookupnegative + S (dst_negative_inversion_iff_convolutionlookup) = S ((S (dc_input_inversion_iff_convolution)) * dst_negative_scale_inversion_iff_convolutionlookup)) /\ exists ff_q_pvs_inversion_iff_convolutionlookupnegative. dst_negative_code_inversion_iff_convolutionlookup = ff_q_pvs_inversion_iff_convolutionlookupnegative * S ((S (dc_input_inversion_iff_convolution)) * dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_inversion_iff_convolutionlookup))) /\ (exists ge_balance_positive_inversion_iff_convolutionlookupvalue ge_balance_negative_inversion_iff_convolutionlookupvalue. (((((dc_output_inversion_iff_convolution) = 2 * (ge_balance_positive_inversion_iff_convolutionlookupvalue) /\ (ge_balance_negative_inversion_iff_convolutionlookupvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionlookupvaluedecode. (((dc_output_inversion_iff_convolution) = 2 * ge_signed_half_inversion_iff_convolutionlookupvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionlookupvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionlookupvalue) = S ge_signed_half_inversion_iff_convolutionlookupvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionlookup) + ge_balance_negative_inversion_iff_convolutionlookupvalue = (dst_negative_inversion_iff_convolutionlookup) + ge_balance_positive_inversion_iff_convolutionlookupvalue))))))))) -> (((~((dc_input_inversion_iff_convolution)=0)) /\ (exists dc_mask_inversion_iff_convolutionvalue. ((((exists dst_positive_code_inversion_iff_convolutionvaluemasktable dst_positive_scale_inversion_iff_convolutionvaluemasktable dst_negative_code_inversion_iff_convolutionvaluemasktable dst_negative_scale_inversion_iff_convolutionvaluemasktable. (((dc_mask_inversion_iff_convolutionvalue) = (((((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable))) + (((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable))) + (((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable))) + (((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)))))) /\ (forall dst_index_inversion_iff_convolutionvaluemasktable. (exists pvs_le_gap_inversion_iff_convolutionvaluemasktabledomain. pvs_le_gap_inversion_iff_convolutionvaluemasktabledomain + (dst_index_inversion_iff_convolutionvaluemasktable) = (dc_input_inversion_iff_convolution)) -> exists dst_positive_inversion_iff_convolutionvaluemasktable dst_negative_inversion_iff_convolutionvaluemasktable dst_value_inversion_iff_convolutionvaluemasktable. ((((exists ff_h_pvs_inversion_iff_convolutionvaluemasktableentrypositive. ff_h_pvs_inversion_iff_convolutionvaluemasktableentrypositive + S (dst_positive_inversion_iff_convolutionvaluemasktable) = S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_positive_scale_inversion_iff_convolutionvaluemasktable)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasktableentrypositive. dst_positive_code_inversion_iff_convolutionvaluemasktable = ff_q_pvs_inversion_iff_convolutionvaluemasktableentrypositive * S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_positive_scale_inversion_iff_convolutionvaluemasktable) + (dst_positive_inversion_iff_convolutionvaluemasktable))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemasktableentrynegative. ff_h_pvs_inversion_iff_convolutionvaluemasktableentrynegative + S (dst_negative_inversion_iff_convolutionvaluemasktable) = S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_negative_scale_inversion_iff_convolutionvaluemasktable)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasktableentrynegative. dst_negative_code_inversion_iff_convolutionvaluemasktable = ff_q_pvs_inversion_iff_convolutionvaluemasktableentrynegative * S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_inversion_iff_convolutionvaluemasktable))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue. (((((dst_value_inversion_iff_convolutionvaluemasktable) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemasktableentryvaluedecode. (((dst_value_inversion_iff_convolutionvaluemasktable) = 2 * ge_signed_half_inversion_iff_convolutionvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue) = S ge_signed_half_inversion_iff_convolutionvaluemasktableentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemasktable) + ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue = (dst_negative_inversion_iff_convolutionvaluemasktable) + ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue))))))))) /\ (forall dc_index_inversion_iff_convolutionvaluemask dc_value_inversion_iff_convolutionvaluemask. (exists pvs_le_gap_inversion_iff_convolutionvaluemaskdomain. pvs_le_gap_inversion_iff_convolutionvaluemaskdomain + (dc_index_inversion_iff_convolutionvaluemask) = (dc_input_inversion_iff_convolution)) -> (exists dst_positive_code_inversion_iff_convolutionvaluemasklookup dst_positive_scale_inversion_iff_convolutionvaluemasklookup dst_negative_code_inversion_iff_convolutionvaluemasklookup dst_negative_scale_inversion_iff_convolutionvaluemasklookup dst_positive_inversion_iff_convolutionvaluemasklookup dst_negative_inversion_iff_convolutionvaluemasklookup. (((dc_mask_inversion_iff_convolutionvalue) = (((((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup))) + (((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup))) + (((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup))) + (((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemasklookuppositive. ff_h_pvs_inversion_iff_convolutionvaluemasklookuppositive + S (dst_positive_inversion_iff_convolutionvaluemasklookup) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasklookuppositive. dst_positive_code_inversion_iff_convolutionvaluemasklookup = ff_q_pvs_inversion_iff_convolutionvaluemasklookuppositive * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemasklookup) + (dst_positive_inversion_iff_convolutionvaluemasklookup))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemasklookupnegative. ff_h_pvs_inversion_iff_convolutionvaluemasklookupnegative + S (dst_negative_inversion_iff_convolutionvaluemasklookup) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasklookupnegative. dst_negative_code_inversion_iff_convolutionvaluemasklookup = ff_q_pvs_inversion_iff_convolutionvaluemasklookupnegative * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_inversion_iff_convolutionvaluemasklookup))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue. (((((dc_value_inversion_iff_convolutionvaluemask) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemasklookupvaluedecode. (((dc_value_inversion_iff_convolutionvaluemask) = 2 * ge_signed_half_inversion_iff_convolutionvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue) = S ge_signed_half_inversion_iff_convolutionvaluemasklookupvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemasklookup) + ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue = (dst_negative_inversion_iff_convolutionvaluemasklookup) + ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue))))))))) -> ((((~((dc_index_inversion_iff_convolutionvaluemask)=0)) /\ (exists dc_quotient_inversion_iff_convolutionvaluemaskentry dc_left_inversion_iff_convolutionvaluemaskentry dc_right_inversion_iff_convolutionvaluemaskentry. (((dc_input_inversion_iff_convolution)=(dc_index_inversion_iff_convolutionvaluemask)*dc_quotient_inversion_iff_convolutionvaluemaskentry) /\ (((exists dst_positive_code_inversion_iff_convolutionvaluemaskentryleft dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft dst_negative_code_inversion_iff_convolutionvaluemaskentryleft dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft dst_positive_inversion_iff_convolutionvaluemaskentryleft dst_negative_inversion_iff_convolutionvaluemaskentryleft. (((M) = (((((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftpositive. ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftpositive + S (dst_positive_inversion_iff_convolutionvaluemaskentryleft) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftpositive. dst_positive_code_inversion_iff_convolutionvaluemaskentryleft = ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftpositive * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_inversion_iff_convolutionvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftnegative. ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftnegative + S (dst_negative_inversion_iff_convolutionvaluemaskentryleft) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftnegative. dst_negative_code_inversion_iff_convolutionvaluemaskentryleft = ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftnegative * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_inversion_iff_convolutionvaluemaskentryleft))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue. (((((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryleftvaluedecode. (((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemaskentryleft) + ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue = (dst_negative_inversion_iff_convolutionvaluemaskentryleft) + ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inversion_iff_convolutionvaluemaskentryright dst_positive_scale_inversion_iff_convolutionvaluemaskentryright dst_negative_code_inversion_iff_convolutionvaluemaskentryright dst_negative_scale_inversion_iff_convolutionvaluemaskentryright dst_positive_inversion_iff_convolutionvaluemaskentryright dst_negative_inversion_iff_convolutionvaluemaskentryright. (((G) = (((((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightpositive. ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightpositive + S (dst_positive_inversion_iff_convolutionvaluemaskentryright) = S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightpositive. dst_positive_code_inversion_iff_convolutionvaluemaskentryright = ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightpositive * S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_inversion_iff_convolutionvaluemaskentryright))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightnegative. ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightnegative + S (dst_negative_inversion_iff_convolutionvaluemaskentryright) = S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightnegative. dst_negative_code_inversion_iff_convolutionvaluemaskentryright = ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightnegative * S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_inversion_iff_convolutionvaluemaskentryright))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue. (((((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryrightvaluedecode. (((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemaskentryright) + ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue = (dst_negative_inversion_iff_convolutionvaluemaskentryright) + ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inversion_iff_convolutionvaluemaskentryproduct sto_an_inversion_iff_convolutionvaluemaskentryproduct sto_bp_inversion_iff_convolutionvaluemaskentryproduct sto_bn_inversion_iff_convolutionvaluemaskentryproduct sto_cp_inversion_iff_convolutionvaluemaskentryproduct sto_cn_inversion_iff_convolutionvaluemaskentryproduct. (((((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * (sto_ap_inversion_iff_convolutionvaluemaskentryproduct) /\ (sto_an_inversion_iff_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryproductleft. (((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryproductleft + 1 /\ (sto_ap_inversion_iff_convolutionvaluemaskentryproduct) = 0) /\ (sto_an_inversion_iff_convolutionvaluemaskentryproduct) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryproductleft))) /\ ((((((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * (sto_bp_inversion_iff_convolutionvaluemaskentryproduct) /\ (sto_bn_inversion_iff_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryproductright. (((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryproductright + 1 /\ (sto_bp_inversion_iff_convolutionvaluemaskentryproduct) = 0) /\ (sto_bn_inversion_iff_convolutionvaluemaskentryproduct) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryproductright))) /\ ((((((dc_value_inversion_iff_convolutionvaluemask) = 2 * (sto_cp_inversion_iff_convolutionvaluemaskentryproduct) /\ (sto_cn_inversion_iff_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryproductoutput. (((dc_value_inversion_iff_convolutionvaluemask) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryproductoutput + 1 /\ (sto_cp_inversion_iff_convolutionvaluemaskentryproduct) = 0) /\ (sto_cn_inversion_iff_convolutionvaluemaskentryproduct) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryproductoutput))) /\ ((sto_ap_inversion_iff_convolutionvaluemaskentryproduct * sto_bp_inversion_iff_convolutionvaluemaskentryproduct + sto_an_inversion_iff_convolutionvaluemaskentryproduct * sto_bn_inversion_iff_convolutionvaluemaskentryproduct) + sto_cn_inversion_iff_convolutionvaluemaskentryproduct = (sto_ap_inversion_iff_convolutionvaluemaskentryproduct * sto_bn_inversion_iff_convolutionvaluemaskentryproduct + sto_an_inversion_iff_convolutionvaluemaskentryproduct * sto_bp_inversion_iff_convolutionvaluemaskentryproduct) + sto_cp_inversion_iff_convolutionvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inversion_iff_convolutionvaluemask)=0 \/ ~(exists pvs_factor_inversion_iff_convolutionvaluemaskentrynondivisor. (dc_input_inversion_iff_convolution) = (dc_index_inversion_iff_convolutionvaluemask) * pvs_factor_inversion_iff_convolutionvaluemaskentrynondivisor)) /\ ((dc_value_inversion_iff_convolutionvaluemask)=0))))))) /\ (exists dst_positive_code_inversion_iff_convolutionvaluefold dst_positive_scale_inversion_iff_convolutionvaluefold dst_negative_code_inversion_iff_convolutionvaluefold dst_negative_scale_inversion_iff_convolutionvaluefold dst_positive_sum_inversion_iff_convolutionvaluefold dst_negative_sum_inversion_iff_convolutionvaluefold. (((dc_mask_inversion_iff_convolutionvalue) = (((((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) * S ((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) + ((dst_positive_scale_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold))) + (((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) * S ((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) + ((dst_positive_scale_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold))) + (((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)))) + ((((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold))) + (((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)))))) /\ (((exists fs_u_dst_inversion_iff_convolutionvaluefoldpositive fs_v_dst_inversion_iff_convolutionvaluefoldpositive. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_start. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_start. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal + S (dst_positive_sum_inversion_iff_convolutionvaluefold) = S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal * S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (dst_positive_sum_inversion_iff_convolutionvaluefold))) /\ forall fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps. (exists fs_lt_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_bound. fs_lt_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_bound + S fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps = S (dc_input_inversion_iff_convolution)) -> exists fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand + S (fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * dst_positive_scale_inversion_iff_convolutionvaluefold)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand. dst_positive_code_inversion_iff_convolutionvaluefold = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * dst_positive_scale_inversion_iff_convolutionvaluefold) + (fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial + S (fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor + S (fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps))) /\ fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps = fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps + fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_iff_convolutionvaluefoldnegative fs_v_dst_inversion_iff_convolutionvaluefoldnegative. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_start. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_start. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal + S (dst_negative_sum_inversion_iff_convolutionvaluefold) = S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal * S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (dst_negative_sum_inversion_iff_convolutionvaluefold))) /\ forall fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps. (exists fs_lt_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_bound. fs_lt_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_bound + S fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps = S (dc_input_inversion_iff_convolution)) -> exists fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand + S (fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * dst_negative_scale_inversion_iff_convolutionvaluefold)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand. dst_negative_code_inversion_iff_convolutionvaluefold = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * dst_negative_scale_inversion_iff_convolutionvaluefold) + (fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial + S (fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor + S (fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps))) /\ fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps = fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps + fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluefoldresult ge_balance_negative_inversion_iff_convolutionvaluefoldresult. (((((dc_output_inversion_iff_convolution) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluefoldresult) /\ (ge_balance_negative_inversion_iff_convolutionvaluefoldresult) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluefoldresultdecode. (((dc_output_inversion_iff_convolution) = 2 * ge_signed_half_inversion_iff_convolutionvaluefoldresultdecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluefoldresult) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluefoldresult) = S ge_signed_half_inversion_iff_convolutionvaluefoldresultdecode))) /\ ((dst_positive_sum_inversion_iff_convolutionvaluefold) + ge_balance_negative_inversion_iff_convolutionvaluefoldresult = (dst_negative_sum_inversion_iff_convolutionvaluefold) + ge_balance_positive_inversion_iff_convolutionvaluefoldresult))))))))))))))))))))) /\ ((((exists dst_positive_code_inversion_iff_convolutionleft dst_positive_scale_inversion_iff_convolutionleft dst_negative_code_inversion_iff_convolutionleft dst_negative_scale_inversion_iff_convolutionleft. (((M) = (((((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) * S ((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) + ((dst_positive_scale_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft))) + (((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)))) * S ((((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) * S ((dst_positive_code_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft)) + ((dst_positive_scale_inversion_iff_convolutionleft) + (dst_positive_scale_inversion_iff_convolutionleft))) + (((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)))) + ((((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft))) + (((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) * S ((dst_negative_code_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)) + ((dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_scale_inversion_iff_convolutionleft)))))) /\ (forall dst_index_inversion_iff_convolutionleft. (exists pvs_le_gap_inversion_iff_convolutionleftdomain. pvs_le_gap_inversion_iff_convolutionleftdomain + (dst_index_inversion_iff_convolutionleft) = (N)) -> exists dst_positive_inversion_iff_convolutionleft dst_negative_inversion_iff_convolutionleft dst_value_inversion_iff_convolutionleft. ((((exists ff_h_pvs_inversion_iff_convolutionleftentrypositive. ff_h_pvs_inversion_iff_convolutionleftentrypositive + S (dst_positive_inversion_iff_convolutionleft) = S ((S (dst_index_inversion_iff_convolutionleft)) * dst_positive_scale_inversion_iff_convolutionleft)) /\ exists ff_q_pvs_inversion_iff_convolutionleftentrypositive. dst_positive_code_inversion_iff_convolutionleft = ff_q_pvs_inversion_iff_convolutionleftentrypositive * S ((S (dst_index_inversion_iff_convolutionleft)) * dst_positive_scale_inversion_iff_convolutionleft) + (dst_positive_inversion_iff_convolutionleft))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionleftentrynegative. ff_h_pvs_inversion_iff_convolutionleftentrynegative + S (dst_negative_inversion_iff_convolutionleft) = S ((S (dst_index_inversion_iff_convolutionleft)) * dst_negative_scale_inversion_iff_convolutionleft)) /\ exists ff_q_pvs_inversion_iff_convolutionleftentrynegative. dst_negative_code_inversion_iff_convolutionleft = ff_q_pvs_inversion_iff_convolutionleftentrynegative * S ((S (dst_index_inversion_iff_convolutionleft)) * dst_negative_scale_inversion_iff_convolutionleft) + (dst_negative_inversion_iff_convolutionleft))) /\ (exists ge_balance_positive_inversion_iff_convolutionleftentryvalue ge_balance_negative_inversion_iff_convolutionleftentryvalue. (((((dst_value_inversion_iff_convolutionleft) = 2 * (ge_balance_positive_inversion_iff_convolutionleftentryvalue) /\ (ge_balance_negative_inversion_iff_convolutionleftentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionleftentryvaluedecode. (((dst_value_inversion_iff_convolutionleft) = 2 * ge_signed_half_inversion_iff_convolutionleftentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionleftentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionleftentryvalue) = S ge_signed_half_inversion_iff_convolutionleftentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionleft) + ge_balance_negative_inversion_iff_convolutionleftentryvalue = (dst_negative_inversion_iff_convolutionleft) + ge_balance_positive_inversion_iff_convolutionleftentryvalue))))))))) /\ (((exists dst_positive_code_inversion_iff_convolutionright dst_positive_scale_inversion_iff_convolutionright dst_negative_code_inversion_iff_convolutionright dst_negative_scale_inversion_iff_convolutionright. (((G) = (((((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) * S ((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) + ((dst_positive_scale_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright))) + (((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)))) * S ((((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) * S ((dst_positive_code_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright)) + ((dst_positive_scale_inversion_iff_convolutionright) + (dst_positive_scale_inversion_iff_convolutionright))) + (((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)))) + ((((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright))) + (((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) * S ((dst_negative_code_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)) + ((dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_scale_inversion_iff_convolutionright)))))) /\ (forall dst_index_inversion_iff_convolutionright. (exists pvs_le_gap_inversion_iff_convolutionrightdomain. pvs_le_gap_inversion_iff_convolutionrightdomain + (dst_index_inversion_iff_convolutionright) = (N)) -> exists dst_positive_inversion_iff_convolutionright dst_negative_inversion_iff_convolutionright dst_value_inversion_iff_convolutionright. ((((exists ff_h_pvs_inversion_iff_convolutionrightentrypositive. ff_h_pvs_inversion_iff_convolutionrightentrypositive + S (dst_positive_inversion_iff_convolutionright) = S ((S (dst_index_inversion_iff_convolutionright)) * dst_positive_scale_inversion_iff_convolutionright)) /\ exists ff_q_pvs_inversion_iff_convolutionrightentrypositive. dst_positive_code_inversion_iff_convolutionright = ff_q_pvs_inversion_iff_convolutionrightentrypositive * S ((S (dst_index_inversion_iff_convolutionright)) * dst_positive_scale_inversion_iff_convolutionright) + (dst_positive_inversion_iff_convolutionright))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionrightentrynegative. ff_h_pvs_inversion_iff_convolutionrightentrynegative + S (dst_negative_inversion_iff_convolutionright) = S ((S (dst_index_inversion_iff_convolutionright)) * dst_negative_scale_inversion_iff_convolutionright)) /\ exists ff_q_pvs_inversion_iff_convolutionrightentrynegative. dst_negative_code_inversion_iff_convolutionright = ff_q_pvs_inversion_iff_convolutionrightentrynegative * S ((S (dst_index_inversion_iff_convolutionright)) * dst_negative_scale_inversion_iff_convolutionright) + (dst_negative_inversion_iff_convolutionright))) /\ (exists ge_balance_positive_inversion_iff_convolutionrightentryvalue ge_balance_negative_inversion_iff_convolutionrightentryvalue. (((((dst_value_inversion_iff_convolutionright) = 2 * (ge_balance_positive_inversion_iff_convolutionrightentryvalue) /\ (ge_balance_negative_inversion_iff_convolutionrightentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionrightentryvaluedecode. (((dst_value_inversion_iff_convolutionright) = 2 * ge_signed_half_inversion_iff_convolutionrightentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionrightentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionrightentryvalue) = S ge_signed_half_inversion_iff_convolutionrightentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionright) + ge_balance_negative_inversion_iff_convolutionrightentryvalue = (dst_negative_inversion_iff_convolutionright) + ge_balance_positive_inversion_iff_convolutionrightentryvalue))))))))) /\ (((exists dst_positive_code_inversion_iff_convolutiontable dst_positive_scale_inversion_iff_convolutiontable dst_negative_code_inversion_iff_convolutiontable dst_negative_scale_inversion_iff_convolutiontable. (((F) = (((((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) * S ((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) + ((dst_positive_scale_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable))) + (((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)))) * S ((((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) * S ((dst_positive_code_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable)) + ((dst_positive_scale_inversion_iff_convolutiontable) + (dst_positive_scale_inversion_iff_convolutiontable))) + (((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)))) + ((((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable))) + (((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) * S ((dst_negative_code_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)) + ((dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_scale_inversion_iff_convolutiontable)))))) /\ (forall dst_index_inversion_iff_convolutiontable. (exists pvs_le_gap_inversion_iff_convolutiontabledomain. pvs_le_gap_inversion_iff_convolutiontabledomain + (dst_index_inversion_iff_convolutiontable) = (N)) -> exists dst_positive_inversion_iff_convolutiontable dst_negative_inversion_iff_convolutiontable dst_value_inversion_iff_convolutiontable. ((((exists ff_h_pvs_inversion_iff_convolutiontableentrypositive. ff_h_pvs_inversion_iff_convolutiontableentrypositive + S (dst_positive_inversion_iff_convolutiontable) = S ((S (dst_index_inversion_iff_convolutiontable)) * dst_positive_scale_inversion_iff_convolutiontable)) /\ exists ff_q_pvs_inversion_iff_convolutiontableentrypositive. dst_positive_code_inversion_iff_convolutiontable = ff_q_pvs_inversion_iff_convolutiontableentrypositive * S ((S (dst_index_inversion_iff_convolutiontable)) * dst_positive_scale_inversion_iff_convolutiontable) + (dst_positive_inversion_iff_convolutiontable))) /\ (((((exists ff_h_pvs_inversion_iff_convolutiontableentrynegative. ff_h_pvs_inversion_iff_convolutiontableentrynegative + S (dst_negative_inversion_iff_convolutiontable) = S ((S (dst_index_inversion_iff_convolutiontable)) * dst_negative_scale_inversion_iff_convolutiontable)) /\ exists ff_q_pvs_inversion_iff_convolutiontableentrynegative. dst_negative_code_inversion_iff_convolutiontable = ff_q_pvs_inversion_iff_convolutiontableentrynegative * S ((S (dst_index_inversion_iff_convolutiontable)) * dst_negative_scale_inversion_iff_convolutiontable) + (dst_negative_inversion_iff_convolutiontable))) /\ (exists ge_balance_positive_inversion_iff_convolutiontableentryvalue ge_balance_negative_inversion_iff_convolutiontableentryvalue. (((((dst_value_inversion_iff_convolutiontable) = 2 * (ge_balance_positive_inversion_iff_convolutiontableentryvalue) /\ (ge_balance_negative_inversion_iff_convolutiontableentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutiontableentryvaluedecode. (((dst_value_inversion_iff_convolutiontable) = 2 * ge_signed_half_inversion_iff_convolutiontableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutiontableentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutiontableentryvalue) = S ge_signed_half_inversion_iff_convolutiontableentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutiontable) + ge_balance_negative_inversion_iff_convolutiontableentryvalue = (dst_negative_inversion_iff_convolutiontable) + ge_balance_positive_inversion_iff_convolutiontableentryvalue))))))))) /\ (forall dc_input_inversion_iff_convolution dc_output_inversion_iff_convolution. ~(dc_input_inversion_iff_convolution=0) -> (exists pvs_le_gap_inversion_iff_convolutiondomain. pvs_le_gap_inversion_iff_convolutiondomain + (dc_input_inversion_iff_convolution) = (N)) -> (exists dst_positive_code_inversion_iff_convolutionlookup dst_positive_scale_inversion_iff_convolutionlookup dst_negative_code_inversion_iff_convolutionlookup dst_negative_scale_inversion_iff_convolutionlookup dst_positive_inversion_iff_convolutionlookup dst_negative_inversion_iff_convolutionlookup. (((F) = (((((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) * S ((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) + ((dst_positive_scale_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup))) + (((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)))) * S ((((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) * S ((dst_positive_code_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup)) + ((dst_positive_scale_inversion_iff_convolutionlookup) + (dst_positive_scale_inversion_iff_convolutionlookup))) + (((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)))) + ((((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup))) + (((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) * S ((dst_negative_code_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)) + ((dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_scale_inversion_iff_convolutionlookup)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionlookuppositive. ff_h_pvs_inversion_iff_convolutionlookuppositive + S (dst_positive_inversion_iff_convolutionlookup) = S ((S (dc_input_inversion_iff_convolution)) * dst_positive_scale_inversion_iff_convolutionlookup)) /\ exists ff_q_pvs_inversion_iff_convolutionlookuppositive. dst_positive_code_inversion_iff_convolutionlookup = ff_q_pvs_inversion_iff_convolutionlookuppositive * S ((S (dc_input_inversion_iff_convolution)) * dst_positive_scale_inversion_iff_convolutionlookup) + (dst_positive_inversion_iff_convolutionlookup))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionlookupnegative. ff_h_pvs_inversion_iff_convolutionlookupnegative + S (dst_negative_inversion_iff_convolutionlookup) = S ((S (dc_input_inversion_iff_convolution)) * dst_negative_scale_inversion_iff_convolutionlookup)) /\ exists ff_q_pvs_inversion_iff_convolutionlookupnegative. dst_negative_code_inversion_iff_convolutionlookup = ff_q_pvs_inversion_iff_convolutionlookupnegative * S ((S (dc_input_inversion_iff_convolution)) * dst_negative_scale_inversion_iff_convolutionlookup) + (dst_negative_inversion_iff_convolutionlookup))) /\ (exists ge_balance_positive_inversion_iff_convolutionlookupvalue ge_balance_negative_inversion_iff_convolutionlookupvalue. (((((dc_output_inversion_iff_convolution) = 2 * (ge_balance_positive_inversion_iff_convolutionlookupvalue) /\ (ge_balance_negative_inversion_iff_convolutionlookupvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionlookupvaluedecode. (((dc_output_inversion_iff_convolution) = 2 * ge_signed_half_inversion_iff_convolutionlookupvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionlookupvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionlookupvalue) = S ge_signed_half_inversion_iff_convolutionlookupvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionlookup) + ge_balance_negative_inversion_iff_convolutionlookupvalue = (dst_negative_inversion_iff_convolutionlookup) + ge_balance_positive_inversion_iff_convolutionlookupvalue))))))))) -> (((~((dc_input_inversion_iff_convolution)=0)) /\ (exists dc_mask_inversion_iff_convolutionvalue. ((((exists dst_positive_code_inversion_iff_convolutionvaluemasktable dst_positive_scale_inversion_iff_convolutionvaluemasktable dst_negative_code_inversion_iff_convolutionvaluemasktable dst_negative_scale_inversion_iff_convolutionvaluemasktable. (((dc_mask_inversion_iff_convolutionvalue) = (((((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable))) + (((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasktable) + (dst_positive_scale_inversion_iff_convolutionvaluemasktable))) + (((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable))) + (((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_scale_inversion_iff_convolutionvaluemasktable)))))) /\ (forall dst_index_inversion_iff_convolutionvaluemasktable. (exists pvs_le_gap_inversion_iff_convolutionvaluemasktabledomain. pvs_le_gap_inversion_iff_convolutionvaluemasktabledomain + (dst_index_inversion_iff_convolutionvaluemasktable) = (dc_input_inversion_iff_convolution)) -> exists dst_positive_inversion_iff_convolutionvaluemasktable dst_negative_inversion_iff_convolutionvaluemasktable dst_value_inversion_iff_convolutionvaluemasktable. ((((exists ff_h_pvs_inversion_iff_convolutionvaluemasktableentrypositive. ff_h_pvs_inversion_iff_convolutionvaluemasktableentrypositive + S (dst_positive_inversion_iff_convolutionvaluemasktable) = S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_positive_scale_inversion_iff_convolutionvaluemasktable)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasktableentrypositive. dst_positive_code_inversion_iff_convolutionvaluemasktable = ff_q_pvs_inversion_iff_convolutionvaluemasktableentrypositive * S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_positive_scale_inversion_iff_convolutionvaluemasktable) + (dst_positive_inversion_iff_convolutionvaluemasktable))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemasktableentrynegative. ff_h_pvs_inversion_iff_convolutionvaluemasktableentrynegative + S (dst_negative_inversion_iff_convolutionvaluemasktable) = S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_negative_scale_inversion_iff_convolutionvaluemasktable)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasktableentrynegative. dst_negative_code_inversion_iff_convolutionvaluemasktable = ff_q_pvs_inversion_iff_convolutionvaluemasktableentrynegative * S ((S (dst_index_inversion_iff_convolutionvaluemasktable)) * dst_negative_scale_inversion_iff_convolutionvaluemasktable) + (dst_negative_inversion_iff_convolutionvaluemasktable))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue. (((((dst_value_inversion_iff_convolutionvaluemasktable) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemasktableentryvaluedecode. (((dst_value_inversion_iff_convolutionvaluemasktable) = 2 * ge_signed_half_inversion_iff_convolutionvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue) = S ge_signed_half_inversion_iff_convolutionvaluemasktableentryvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemasktable) + ge_balance_negative_inversion_iff_convolutionvaluemasktableentryvalue = (dst_negative_inversion_iff_convolutionvaluemasktable) + ge_balance_positive_inversion_iff_convolutionvaluemasktableentryvalue))))))))) /\ (forall dc_index_inversion_iff_convolutionvaluemask dc_value_inversion_iff_convolutionvaluemask. (exists pvs_le_gap_inversion_iff_convolutionvaluemaskdomain. pvs_le_gap_inversion_iff_convolutionvaluemaskdomain + (dc_index_inversion_iff_convolutionvaluemask) = (dc_input_inversion_iff_convolution)) -> (exists dst_positive_code_inversion_iff_convolutionvaluemasklookup dst_positive_scale_inversion_iff_convolutionvaluemasklookup dst_negative_code_inversion_iff_convolutionvaluemasklookup dst_negative_scale_inversion_iff_convolutionvaluemasklookup dst_positive_inversion_iff_convolutionvaluemasklookup dst_negative_inversion_iff_convolutionvaluemasklookup. (((dc_mask_inversion_iff_convolutionvalue) = (((((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup))) + (((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_positive_code_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_positive_scale_inversion_iff_convolutionvaluemasklookup) + (dst_positive_scale_inversion_iff_convolutionvaluemasklookup))) + (((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup))) + (((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) * S ((dst_negative_code_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) + ((dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_scale_inversion_iff_convolutionvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemasklookuppositive. ff_h_pvs_inversion_iff_convolutionvaluemasklookuppositive + S (dst_positive_inversion_iff_convolutionvaluemasklookup) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemasklookup)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasklookuppositive. dst_positive_code_inversion_iff_convolutionvaluemasklookup = ff_q_pvs_inversion_iff_convolutionvaluemasklookuppositive * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemasklookup) + (dst_positive_inversion_iff_convolutionvaluemasklookup))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemasklookupnegative. ff_h_pvs_inversion_iff_convolutionvaluemasklookupnegative + S (dst_negative_inversion_iff_convolutionvaluemasklookup) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemasklookup)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemasklookupnegative. dst_negative_code_inversion_iff_convolutionvaluemasklookup = ff_q_pvs_inversion_iff_convolutionvaluemasklookupnegative * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemasklookup) + (dst_negative_inversion_iff_convolutionvaluemasklookup))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue. (((((dc_value_inversion_iff_convolutionvaluemask) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemasklookupvaluedecode. (((dc_value_inversion_iff_convolutionvaluemask) = 2 * ge_signed_half_inversion_iff_convolutionvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue) = S ge_signed_half_inversion_iff_convolutionvaluemasklookupvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemasklookup) + ge_balance_negative_inversion_iff_convolutionvaluemasklookupvalue = (dst_negative_inversion_iff_convolutionvaluemasklookup) + ge_balance_positive_inversion_iff_convolutionvaluemasklookupvalue))))))))) -> ((((~((dc_index_inversion_iff_convolutionvaluemask)=0)) /\ (exists dc_quotient_inversion_iff_convolutionvaluemaskentry dc_left_inversion_iff_convolutionvaluemaskentry dc_right_inversion_iff_convolutionvaluemaskentry. (((dc_input_inversion_iff_convolution)=(dc_index_inversion_iff_convolutionvaluemask)*dc_quotient_inversion_iff_convolutionvaluemaskentry) /\ (((exists dst_positive_code_inversion_iff_convolutionvaluemaskentryleft dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft dst_negative_code_inversion_iff_convolutionvaluemaskentryleft dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft dst_positive_inversion_iff_convolutionvaluemaskentryleft dst_negative_inversion_iff_convolutionvaluemaskentryleft. (((M) = (((((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftpositive. ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftpositive + S (dst_positive_inversion_iff_convolutionvaluemaskentryleft) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftpositive. dst_positive_code_inversion_iff_convolutionvaluemaskentryleft = ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftpositive * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_positive_inversion_iff_convolutionvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftnegative. ff_h_pvs_inversion_iff_convolutionvaluemaskentryleftnegative + S (dst_negative_inversion_iff_convolutionvaluemaskentryleft) = S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftnegative. dst_negative_code_inversion_iff_convolutionvaluemaskentryleft = ff_q_pvs_inversion_iff_convolutionvaluemaskentryleftnegative * S ((S (dc_index_inversion_iff_convolutionvaluemask)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryleft) + (dst_negative_inversion_iff_convolutionvaluemaskentryleft))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue. (((((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryleftvaluedecode. (((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemaskentryleft) + ge_balance_negative_inversion_iff_convolutionvaluemaskentryleftvalue = (dst_negative_inversion_iff_convolutionvaluemaskentryleft) + ge_balance_positive_inversion_iff_convolutionvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inversion_iff_convolutionvaluemaskentryright dst_positive_scale_inversion_iff_convolutionvaluemaskentryright dst_negative_code_inversion_iff_convolutionvaluemaskentryright dst_negative_scale_inversion_iff_convolutionvaluemaskentryright dst_positive_inversion_iff_convolutionvaluemaskentryright dst_negative_inversion_iff_convolutionvaluemaskentryright. (((G) = (((((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_positive_code_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_positive_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_scale_inversion_iff_convolutionvaluemaskentryright))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)))) + ((((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright))) + (((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) * S ((dst_negative_code_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) + ((dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightpositive. ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightpositive + S (dst_positive_inversion_iff_convolutionvaluemaskentryright) = S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryright)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightpositive. dst_positive_code_inversion_iff_convolutionvaluemaskentryright = ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightpositive * S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_positive_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_positive_inversion_iff_convolutionvaluemaskentryright))) /\ (((((exists ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightnegative. ff_h_pvs_inversion_iff_convolutionvaluemaskentryrightnegative + S (dst_negative_inversion_iff_convolutionvaluemaskentryright) = S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryright)) /\ exists ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightnegative. dst_negative_code_inversion_iff_convolutionvaluemaskentryright = ff_q_pvs_inversion_iff_convolutionvaluemaskentryrightnegative * S ((S (dc_quotient_inversion_iff_convolutionvaluemaskentry)) * dst_negative_scale_inversion_iff_convolutionvaluemaskentryright) + (dst_negative_inversion_iff_convolutionvaluemaskentryright))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue. (((((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryrightvaluedecode. (((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inversion_iff_convolutionvaluemaskentryright) + ge_balance_negative_inversion_iff_convolutionvaluemaskentryrightvalue = (dst_negative_inversion_iff_convolutionvaluemaskentryright) + ge_balance_positive_inversion_iff_convolutionvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inversion_iff_convolutionvaluemaskentryproduct sto_an_inversion_iff_convolutionvaluemaskentryproduct sto_bp_inversion_iff_convolutionvaluemaskentryproduct sto_bn_inversion_iff_convolutionvaluemaskentryproduct sto_cp_inversion_iff_convolutionvaluemaskentryproduct sto_cn_inversion_iff_convolutionvaluemaskentryproduct. (((((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * (sto_ap_inversion_iff_convolutionvaluemaskentryproduct) /\ (sto_an_inversion_iff_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryproductleft. (((dc_left_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryproductleft + 1 /\ (sto_ap_inversion_iff_convolutionvaluemaskentryproduct) = 0) /\ (sto_an_inversion_iff_convolutionvaluemaskentryproduct) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryproductleft))) /\ ((((((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * (sto_bp_inversion_iff_convolutionvaluemaskentryproduct) /\ (sto_bn_inversion_iff_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryproductright. (((dc_right_inversion_iff_convolutionvaluemaskentry) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryproductright + 1 /\ (sto_bp_inversion_iff_convolutionvaluemaskentryproduct) = 0) /\ (sto_bn_inversion_iff_convolutionvaluemaskentryproduct) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryproductright))) /\ ((((((dc_value_inversion_iff_convolutionvaluemask) = 2 * (sto_cp_inversion_iff_convolutionvaluemaskentryproduct) /\ (sto_cn_inversion_iff_convolutionvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluemaskentryproductoutput. (((dc_value_inversion_iff_convolutionvaluemask) = 2 * ge_signed_half_inversion_iff_convolutionvaluemaskentryproductoutput + 1 /\ (sto_cp_inversion_iff_convolutionvaluemaskentryproduct) = 0) /\ (sto_cn_inversion_iff_convolutionvaluemaskentryproduct) = S ge_signed_half_inversion_iff_convolutionvaluemaskentryproductoutput))) /\ ((sto_ap_inversion_iff_convolutionvaluemaskentryproduct * sto_bp_inversion_iff_convolutionvaluemaskentryproduct + sto_an_inversion_iff_convolutionvaluemaskentryproduct * sto_bn_inversion_iff_convolutionvaluemaskentryproduct) + sto_cn_inversion_iff_convolutionvaluemaskentryproduct = (sto_ap_inversion_iff_convolutionvaluemaskentryproduct * sto_bn_inversion_iff_convolutionvaluemaskentryproduct + sto_an_inversion_iff_convolutionvaluemaskentryproduct * sto_bp_inversion_iff_convolutionvaluemaskentryproduct) + sto_cp_inversion_iff_convolutionvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inversion_iff_convolutionvaluemask)=0 \/ ~(exists pvs_factor_inversion_iff_convolutionvaluemaskentrynondivisor. (dc_input_inversion_iff_convolution) = (dc_index_inversion_iff_convolutionvaluemask) * pvs_factor_inversion_iff_convolutionvaluemaskentrynondivisor)) /\ ((dc_value_inversion_iff_convolutionvaluemask)=0))))))) /\ (exists dst_positive_code_inversion_iff_convolutionvaluefold dst_positive_scale_inversion_iff_convolutionvaluefold dst_negative_code_inversion_iff_convolutionvaluefold dst_negative_scale_inversion_iff_convolutionvaluefold dst_positive_sum_inversion_iff_convolutionvaluefold dst_negative_sum_inversion_iff_convolutionvaluefold. (((dc_mask_inversion_iff_convolutionvalue) = (((((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) * S ((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) + ((dst_positive_scale_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold))) + (((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)))) * S ((((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) * S ((dst_positive_code_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold)) + ((dst_positive_scale_inversion_iff_convolutionvaluefold) + (dst_positive_scale_inversion_iff_convolutionvaluefold))) + (((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)))) + ((((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold))) + (((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) * S ((dst_negative_code_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)) + ((dst_negative_scale_inversion_iff_convolutionvaluefold) + (dst_negative_scale_inversion_iff_convolutionvaluefold)))))) /\ (((exists fs_u_dst_inversion_iff_convolutionvaluefoldpositive fs_v_dst_inversion_iff_convolutionvaluefoldpositive. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_start. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_start. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal + S (dst_positive_sum_inversion_iff_convolutionvaluefold) = S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_terminal * S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (dst_positive_sum_inversion_iff_convolutionvaluefold))) /\ forall fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps. (exists fs_lt_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_bound. fs_lt_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_bound + S fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps = S (dc_input_inversion_iff_convolution)) -> exists fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand + S (fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * dst_positive_scale_inversion_iff_convolutionvaluefold)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand. dst_positive_code_inversion_iff_convolutionvaluefold = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * dst_positive_scale_inversion_iff_convolutionvaluefold) + (fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial + S (fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor. fs_h_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor + S (fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor. fs_u_dst_inversion_iff_convolutionvaluefoldpositive = fs_q_dst_inversion_iff_convolutionvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldpositive) + (fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps))) /\ fs_s_dst_inversion_iff_convolutionvaluefoldpositive_body_steps = fs_r_dst_inversion_iff_convolutionvaluefoldpositive_body_steps + fs_a_dst_inversion_iff_convolutionvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_iff_convolutionvaluefoldnegative fs_v_dst_inversion_iff_convolutionvaluefoldnegative. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_start. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_start. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal + S (dst_negative_sum_inversion_iff_convolutionvaluefold) = S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_terminal * S ((S (S (dc_input_inversion_iff_convolution))) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (dst_negative_sum_inversion_iff_convolutionvaluefold))) /\ forall fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps. (exists fs_lt_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_bound. fs_lt_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_bound + S fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps = S (dc_input_inversion_iff_convolution)) -> exists fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps. ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand + S (fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * dst_negative_scale_inversion_iff_convolutionvaluefold)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand. dst_negative_code_inversion_iff_convolutionvaluefold = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * dst_negative_scale_inversion_iff_convolutionvaluefold) + (fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial + S (fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor. fs_h_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor + S (fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative)) /\ exists fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor. fs_u_dst_inversion_iff_convolutionvaluefoldnegative = fs_q_dst_inversion_iff_convolutionvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)) * fs_v_dst_inversion_iff_convolutionvaluefoldnegative) + (fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps))) /\ fs_s_dst_inversion_iff_convolutionvaluefoldnegative_body_steps = fs_r_dst_inversion_iff_convolutionvaluefoldnegative_body_steps + fs_a_dst_inversion_iff_convolutionvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_iff_convolutionvaluefoldresult ge_balance_negative_inversion_iff_convolutionvaluefoldresult. (((((dc_output_inversion_iff_convolution) = 2 * (ge_balance_positive_inversion_iff_convolutionvaluefoldresult) /\ (ge_balance_negative_inversion_iff_convolutionvaluefoldresult) = 0) \/ exists ge_signed_half_inversion_iff_convolutionvaluefoldresultdecode. (((dc_output_inversion_iff_convolution) = 2 * ge_signed_half_inversion_iff_convolutionvaluefoldresultdecode + 1 /\ (ge_balance_positive_inversion_iff_convolutionvaluefoldresult) = 0) /\ (ge_balance_negative_inversion_iff_convolutionvaluefoldresult) = S ge_signed_half_inversion_iff_convolutionvaluefoldresultdecode))) /\ ((dst_positive_sum_inversion_iff_convolutionvaluefold) + ge_balance_negative_inversion_iff_convolutionvaluefoldresult = (dst_negative_sum_inversion_iff_convolutionvaluefold) + ge_balance_positive_inversion_iff_convolutionvaluefoldresult)))))))))))))))))))) -> (forall mi_index_inversion_iff_transform mi_value_inversion_iff_transform. ~(mi_index_inversion_iff_transform=0) -> (exists pvs_le_gap_inversion_iff_transformbound. pvs_le_gap_inversion_iff_transformbound + (mi_index_inversion_iff_transform) = (N)) -> (exists dst_positive_code_inversion_iff_transformentry dst_positive_scale_inversion_iff_transformentry dst_negative_code_inversion_iff_transformentry dst_negative_scale_inversion_iff_transformentry dst_positive_inversion_iff_transformentry dst_negative_inversion_iff_transformentry. (((G) = (((((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) * S ((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) + ((dst_positive_scale_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry))) + (((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)))) * S ((((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) * S ((dst_positive_code_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry)) + ((dst_positive_scale_inversion_iff_transformentry) + (dst_positive_scale_inversion_iff_transformentry))) + (((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)))) + ((((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry))) + (((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) * S ((dst_negative_code_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)) + ((dst_negative_scale_inversion_iff_transformentry) + (dst_negative_scale_inversion_iff_transformentry)))))) /\ (((((exists ff_h_pvs_inversion_iff_transformentrypositive. ff_h_pvs_inversion_iff_transformentrypositive + S (dst_positive_inversion_iff_transformentry) = S ((S (mi_index_inversion_iff_transform)) * dst_positive_scale_inversion_iff_transformentry)) /\ exists ff_q_pvs_inversion_iff_transformentrypositive. dst_positive_code_inversion_iff_transformentry = ff_q_pvs_inversion_iff_transformentrypositive * S ((S (mi_index_inversion_iff_transform)) * dst_positive_scale_inversion_iff_transformentry) + (dst_positive_inversion_iff_transformentry))) /\ (((((exists ff_h_pvs_inversion_iff_transformentrynegative. ff_h_pvs_inversion_iff_transformentrynegative + S (dst_negative_inversion_iff_transformentry) = S ((S (mi_index_inversion_iff_transform)) * dst_negative_scale_inversion_iff_transformentry)) /\ exists ff_q_pvs_inversion_iff_transformentrynegative. dst_negative_code_inversion_iff_transformentry = ff_q_pvs_inversion_iff_transformentrynegative * S ((S (mi_index_inversion_iff_transform)) * dst_negative_scale_inversion_iff_transformentry) + (dst_negative_inversion_iff_transformentry))) /\ (exists ge_balance_positive_inversion_iff_transformentryvalue ge_balance_negative_inversion_iff_transformentryvalue. (((((mi_value_inversion_iff_transform) = 2 * (ge_balance_positive_inversion_iff_transformentryvalue) /\ (ge_balance_negative_inversion_iff_transformentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformentryvaluedecode. (((mi_value_inversion_iff_transform) = 2 * ge_signed_half_inversion_iff_transformentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformentryvalue) = S ge_signed_half_inversion_iff_transformentryvaluedecode))) /\ ((dst_positive_inversion_iff_transformentry) + ge_balance_negative_inversion_iff_transformentryvalue = (dst_negative_inversion_iff_transformentry) + ge_balance_positive_inversion_iff_transformentryvalue))))))))) -> (((~((mi_index_inversion_iff_transform)=0)) /\ (exists dm_mask_table_inversion_iff_transformsum. ((((exists dst_positive_code_inversion_iff_transformsummasktable dst_positive_scale_inversion_iff_transformsummasktable dst_negative_code_inversion_iff_transformsummasktable dst_negative_scale_inversion_iff_transformsummasktable. (((dm_mask_table_inversion_iff_transformsum) = (((((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) * S ((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) + ((dst_positive_scale_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable))) + (((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)))) * S ((((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) * S ((dst_positive_code_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable)) + ((dst_positive_scale_inversion_iff_transformsummasktable) + (dst_positive_scale_inversion_iff_transformsummasktable))) + (((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)))) + ((((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable))) + (((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) * S ((dst_negative_code_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)) + ((dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_scale_inversion_iff_transformsummasktable)))))) /\ (forall dst_index_inversion_iff_transformsummasktable. (exists pvs_le_gap_inversion_iff_transformsummasktabledomain. pvs_le_gap_inversion_iff_transformsummasktabledomain + (dst_index_inversion_iff_transformsummasktable) = (mi_index_inversion_iff_transform)) -> exists dst_positive_inversion_iff_transformsummasktable dst_negative_inversion_iff_transformsummasktable dst_value_inversion_iff_transformsummasktable. ((((exists ff_h_pvs_inversion_iff_transformsummasktableentrypositive. ff_h_pvs_inversion_iff_transformsummasktableentrypositive + S (dst_positive_inversion_iff_transformsummasktable) = S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_positive_scale_inversion_iff_transformsummasktable)) /\ exists ff_q_pvs_inversion_iff_transformsummasktableentrypositive. dst_positive_code_inversion_iff_transformsummasktable = ff_q_pvs_inversion_iff_transformsummasktableentrypositive * S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_positive_scale_inversion_iff_transformsummasktable) + (dst_positive_inversion_iff_transformsummasktable))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummasktableentrynegative. ff_h_pvs_inversion_iff_transformsummasktableentrynegative + S (dst_negative_inversion_iff_transformsummasktable) = S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_negative_scale_inversion_iff_transformsummasktable)) /\ exists ff_q_pvs_inversion_iff_transformsummasktableentrynegative. dst_negative_code_inversion_iff_transformsummasktable = ff_q_pvs_inversion_iff_transformsummasktableentrynegative * S ((S (dst_index_inversion_iff_transformsummasktable)) * dst_negative_scale_inversion_iff_transformsummasktable) + (dst_negative_inversion_iff_transformsummasktable))) /\ (exists ge_balance_positive_inversion_iff_transformsummasktableentryvalue ge_balance_negative_inversion_iff_transformsummasktableentryvalue. (((((dst_value_inversion_iff_transformsummasktable) = 2 * (ge_balance_positive_inversion_iff_transformsummasktableentryvalue) /\ (ge_balance_negative_inversion_iff_transformsummasktableentryvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformsummasktableentryvaluedecode. (((dst_value_inversion_iff_transformsummasktable) = 2 * ge_signed_half_inversion_iff_transformsummasktableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformsummasktableentryvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformsummasktableentryvalue) = S ge_signed_half_inversion_iff_transformsummasktableentryvaluedecode))) /\ ((dst_positive_inversion_iff_transformsummasktable) + ge_balance_negative_inversion_iff_transformsummasktableentryvalue = (dst_negative_inversion_iff_transformsummasktable) + ge_balance_positive_inversion_iff_transformsummasktableentryvalue))))))))) /\ (forall dm_index_inversion_iff_transformsummask dm_value_inversion_iff_transformsummask. (exists pvs_le_gap_inversion_iff_transformsummaskdomain. pvs_le_gap_inversion_iff_transformsummaskdomain + (dm_index_inversion_iff_transformsummask) = (mi_index_inversion_iff_transform)) -> (exists dst_positive_code_inversion_iff_transformsummasklookup dst_positive_scale_inversion_iff_transformsummasklookup dst_negative_code_inversion_iff_transformsummasklookup dst_negative_scale_inversion_iff_transformsummasklookup dst_positive_inversion_iff_transformsummasklookup dst_negative_inversion_iff_transformsummasklookup. (((dm_mask_table_inversion_iff_transformsum) = (((((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) * S ((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) + ((dst_positive_scale_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup))) + (((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)))) * S ((((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) * S ((dst_positive_code_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup)) + ((dst_positive_scale_inversion_iff_transformsummasklookup) + (dst_positive_scale_inversion_iff_transformsummasklookup))) + (((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)))) + ((((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup))) + (((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) * S ((dst_negative_code_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)) + ((dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_scale_inversion_iff_transformsummasklookup)))))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummasklookuppositive. ff_h_pvs_inversion_iff_transformsummasklookuppositive + S (dst_positive_inversion_iff_transformsummasklookup) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummasklookup)) /\ exists ff_q_pvs_inversion_iff_transformsummasklookuppositive. dst_positive_code_inversion_iff_transformsummasklookup = ff_q_pvs_inversion_iff_transformsummasklookuppositive * S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummasklookup) + (dst_positive_inversion_iff_transformsummasklookup))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummasklookupnegative. ff_h_pvs_inversion_iff_transformsummasklookupnegative + S (dst_negative_inversion_iff_transformsummasklookup) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummasklookup)) /\ exists ff_q_pvs_inversion_iff_transformsummasklookupnegative. dst_negative_code_inversion_iff_transformsummasklookup = ff_q_pvs_inversion_iff_transformsummasklookupnegative * S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummasklookup) + (dst_negative_inversion_iff_transformsummasklookup))) /\ (exists ge_balance_positive_inversion_iff_transformsummasklookupvalue ge_balance_negative_inversion_iff_transformsummasklookupvalue. (((((dm_value_inversion_iff_transformsummask) = 2 * (ge_balance_positive_inversion_iff_transformsummasklookupvalue) /\ (ge_balance_negative_inversion_iff_transformsummasklookupvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformsummasklookupvaluedecode. (((dm_value_inversion_iff_transformsummask) = 2 * ge_signed_half_inversion_iff_transformsummasklookupvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformsummasklookupvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformsummasklookupvalue) = S ge_signed_half_inversion_iff_transformsummasklookupvaluedecode))) /\ ((dst_positive_inversion_iff_transformsummasklookup) + ge_balance_negative_inversion_iff_transformsummasklookupvalue = (dst_negative_inversion_iff_transformsummasklookup) + ge_balance_positive_inversion_iff_transformsummasklookupvalue))))))))) -> ((((~((dm_index_inversion_iff_transformsummask)=0)) /\ (exists dm_quotient_inversion_iff_transformsummaskentry. (((mi_index_inversion_iff_transform)=(dm_index_inversion_iff_transformsummask)*dm_quotient_inversion_iff_transformsummaskentry) /\ (exists dst_positive_code_inversion_iff_transformsummaskentryinput dst_positive_scale_inversion_iff_transformsummaskentryinput dst_negative_code_inversion_iff_transformsummaskentryinput dst_negative_scale_inversion_iff_transformsummaskentryinput dst_positive_inversion_iff_transformsummaskentryinput dst_negative_inversion_iff_transformsummaskentryinput. (((F) = (((((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) + ((dst_positive_scale_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput))) + (((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)))) * S ((((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_positive_code_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput)) + ((dst_positive_scale_inversion_iff_transformsummaskentryinput) + (dst_positive_scale_inversion_iff_transformsummaskentryinput))) + (((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)))) + ((((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput))) + (((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) * S ((dst_negative_code_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)) + ((dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_scale_inversion_iff_transformsummaskentryinput)))))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummaskentryinputpositive. ff_h_pvs_inversion_iff_transformsummaskentryinputpositive + S (dst_positive_inversion_iff_transformsummaskentryinput) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummaskentryinput)) /\ exists ff_q_pvs_inversion_iff_transformsummaskentryinputpositive. dst_positive_code_inversion_iff_transformsummaskentryinput = ff_q_pvs_inversion_iff_transformsummaskentryinputpositive * S ((S (dm_index_inversion_iff_transformsummask)) * dst_positive_scale_inversion_iff_transformsummaskentryinput) + (dst_positive_inversion_iff_transformsummaskentryinput))) /\ (((((exists ff_h_pvs_inversion_iff_transformsummaskentryinputnegative. ff_h_pvs_inversion_iff_transformsummaskentryinputnegative + S (dst_negative_inversion_iff_transformsummaskentryinput) = S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummaskentryinput)) /\ exists ff_q_pvs_inversion_iff_transformsummaskentryinputnegative. dst_negative_code_inversion_iff_transformsummaskentryinput = ff_q_pvs_inversion_iff_transformsummaskentryinputnegative * S ((S (dm_index_inversion_iff_transformsummask)) * dst_negative_scale_inversion_iff_transformsummaskentryinput) + (dst_negative_inversion_iff_transformsummaskentryinput))) /\ (exists ge_balance_positive_inversion_iff_transformsummaskentryinputvalue ge_balance_negative_inversion_iff_transformsummaskentryinputvalue. (((((dm_value_inversion_iff_transformsummask) = 2 * (ge_balance_positive_inversion_iff_transformsummaskentryinputvalue) /\ (ge_balance_negative_inversion_iff_transformsummaskentryinputvalue) = 0) \/ exists ge_signed_half_inversion_iff_transformsummaskentryinputvaluedecode. (((dm_value_inversion_iff_transformsummask) = 2 * ge_signed_half_inversion_iff_transformsummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_inversion_iff_transformsummaskentryinputvalue) = 0) /\ (ge_balance_negative_inversion_iff_transformsummaskentryinputvalue) = S ge_signed_half_inversion_iff_transformsummaskentryinputvaluedecode))) /\ ((dst_positive_inversion_iff_transformsummaskentryinput) + ge_balance_negative_inversion_iff_transformsummaskentryinputvalue = (dst_negative_inversion_iff_transformsummaskentryinput) + ge_balance_positive_inversion_iff_transformsummaskentryinputvalue))))))))))))) \/ ((((dm_index_inversion_iff_transformsummask)=0 \/ ~(exists pvs_factor_inversion_iff_transformsummaskentrynondivisor. (mi_index_inversion_iff_transform) = (dm_index_inversion_iff_transformsummask) * pvs_factor_inversion_iff_transformsummaskentrynondivisor)) /\ ((dm_value_inversion_iff_transformsummask)=0))))))) /\ (exists dst_positive_code_inversion_iff_transformsumfold dst_positive_scale_inversion_iff_transformsumfold dst_negative_code_inversion_iff_transformsumfold dst_negative_scale_inversion_iff_transformsumfold dst_positive_sum_inversion_iff_transformsumfold dst_negative_sum_inversion_iff_transformsumfold. (((dm_mask_table_inversion_iff_transformsum) = (((((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) * S ((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) + ((dst_positive_scale_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold))) + (((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)))) * S ((((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) * S ((dst_positive_code_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold)) + ((dst_positive_scale_inversion_iff_transformsumfold) + (dst_positive_scale_inversion_iff_transformsumfold))) + (((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)))) + ((((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold))) + (((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) * S ((dst_negative_code_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)) + ((dst_negative_scale_inversion_iff_transformsumfold) + (dst_negative_scale_inversion_iff_transformsumfold)))))) /\ (((exists fs_u_dst_inversion_iff_transformsumfoldpositive fs_v_dst_inversion_iff_transformsumfoldpositive. ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_start. fs_h_dst_inversion_iff_transformsumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_start. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_start * S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (0))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_terminal. fs_h_dst_inversion_iff_transformsumfoldpositive_body_terminal + S (dst_positive_sum_inversion_iff_transformsumfold) = S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_terminal. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_terminal * S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (dst_positive_sum_inversion_iff_transformsumfold))) /\ forall fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps. (exists fs_lt_dst_inversion_iff_transformsumfoldpositive_body_steps_bound. fs_lt_dst_inversion_iff_transformsumfoldpositive_body_steps_bound + S fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps = S (mi_index_inversion_iff_transform)) -> exists fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps. ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_summand. fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_summand + S (fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * dst_positive_scale_inversion_iff_transformsumfold)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_summand. dst_positive_code_inversion_iff_transformsumfold = fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_summand * S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * dst_positive_scale_inversion_iff_transformsumfold) + (fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_partial. fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_partial + S (fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_partial. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_partial * S ((S (fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_successor. fs_h_dst_inversion_iff_transformsumfoldpositive_body_steps_successor + S (fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps) = S ((S (S fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive)) /\ exists fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_successor. fs_u_dst_inversion_iff_transformsumfoldpositive = fs_q_dst_inversion_iff_transformsumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_transformsumfoldpositive_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldpositive) + (fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps))) /\ fs_s_dst_inversion_iff_transformsumfoldpositive_body_steps = fs_r_dst_inversion_iff_transformsumfoldpositive_body_steps + fs_a_dst_inversion_iff_transformsumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inversion_iff_transformsumfoldnegative fs_v_dst_inversion_iff_transformsumfoldnegative. ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_start. fs_h_dst_inversion_iff_transformsumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_start. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_start * S ((S (0)) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (0))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_terminal. fs_h_dst_inversion_iff_transformsumfoldnegative_body_terminal + S (dst_negative_sum_inversion_iff_transformsumfold) = S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_terminal. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_terminal * S ((S (S (mi_index_inversion_iff_transform))) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (dst_negative_sum_inversion_iff_transformsumfold))) /\ forall fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps. (exists fs_lt_dst_inversion_iff_transformsumfoldnegative_body_steps_bound. fs_lt_dst_inversion_iff_transformsumfoldnegative_body_steps_bound + S fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps = S (mi_index_inversion_iff_transform)) -> exists fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps. ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_summand. fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_summand + S (fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * dst_negative_scale_inversion_iff_transformsumfold)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_summand. dst_negative_code_inversion_iff_transformsumfold = fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_summand * S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * dst_negative_scale_inversion_iff_transformsumfold) + (fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_partial. fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_partial + S (fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps) = S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_partial. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_partial * S ((S (fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_successor. fs_h_dst_inversion_iff_transformsumfoldnegative_body_steps_successor + S (fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps) = S ((S (S fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative)) /\ exists fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_successor. fs_u_dst_inversion_iff_transformsumfoldnegative = fs_q_dst_inversion_iff_transformsumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_inversion_iff_transformsumfoldnegative_body_steps)) * fs_v_dst_inversion_iff_transformsumfoldnegative) + (fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps))) /\ fs_s_dst_inversion_iff_transformsumfoldnegative_body_steps = fs_r_dst_inversion_iff_transformsumfoldnegative_body_steps + fs_a_dst_inversion_iff_transformsumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inversion_iff_transformsumfoldresult ge_balance_negative_inversion_iff_transformsumfoldresult. (((((mi_value_inversion_iff_transform) = 2 * (ge_balance_positive_inversion_iff_transformsumfoldresult) /\ (ge_balance_negative_inversion_iff_transformsumfoldresult) = 0) \/ exists ge_signed_half_inversion_iff_transformsumfoldresultdecode. (((mi_value_inversion_iff_transform) = 2 * ge_signed_half_inversion_iff_transformsumfoldresultdecode + 1 /\ (ge_balance_positive_inversion_iff_transformsumfoldresult) = 0) /\ (ge_balance_negative_inversion_iff_transformsumfoldresult) = S ge_signed_half_inversion_iff_transformsumfoldresultdecode))) /\ ((dst_positive_sum_inversion_iff_transformsumfold) + ge_balance_negative_inversion_iff_transformsumfoldresult = (dst_negative_sum_inversion_iff_transformsumfold) + ge_balance_positive_inversion_iff_transformsumfoldresult))))))))))))))))Complete tactic proof in conservative notation
All 28 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
28 script commands · 6 reading checkpoints · 0 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 (2)
01Fix variables and assumptionsL1–7
02Separate the logical casesL8–8
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L8
split
03Fix variables and assumptionsL9–9
Work with arbitrary variables or the premises of the current implication.
- L9
intro ht
04Use earlier factsL10–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
specialize mobius_inversion_for_actual_mobius_table (N) - L11
specialize mobius_inversion_for_actual_mobius_table (F) - L12
specialize mobius_inversion_for_actual_mobius_table (G) - L13
specialize mobius_inversion_for_actual_mobius_table (M) - L14
apply mobius_inversion_for_actual_mobius_table - L15
exact hF - L16
exact hG - L17
exact hM - L18
exact ht
05Fix variables and assumptionsL19–19
Work with arbitrary variables or the premises of the current implication.
- L19
intro hc
06Use earlier factsL20–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
specialize mobius_inversion_reconstructs_divisor_transform (N) - L21
specialize mobius_inversion_reconstructs_divisor_transform (F) - L22
specialize mobius_inversion_reconstructs_divisor_transform (G) - L23
specialize mobius_inversion_reconstructs_divisor_transform (M) - L24
apply mobius_inversion_reconstructs_divisor_transform - L25
exact hF - L26
exact hG - L27
exact hM - L28
exact hc
Original defined command ledger · 28 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro M - 0005
intro hF - 0006
intro hG - 0007
intro hM - 0008
split - 0009
intro ht - 0010
specialize mobius_inversion_for_actual_mobius_table (N) - 0011
specialize mobius_inversion_for_actual_mobius_table (F) - 0012
specialize mobius_inversion_for_actual_mobius_table (G) - 0013
specialize mobius_inversion_for_actual_mobius_table (M) - 0014
apply mobius_inversion_for_actual_mobius_table - 0015
exact hF - 0016
exact hG - 0017
exact hM - 0018
exact ht - 0019
intro hc - 0020
specialize mobius_inversion_reconstructs_divisor_transform (N) - 0021
specialize mobius_inversion_reconstructs_divisor_transform (F) - 0022
specialize mobius_inversion_reconstructs_divisor_transform (G) - 0023
specialize mobius_inversion_reconstructs_divisor_transform (M) - 0024
apply mobius_inversion_reconstructs_divisor_transform - 0025
exact hF - 0026
exact hG - 0027
exact hM - 0028
exact hc