mobius_table_zero_constructor

forall F. (exists dst_positive_code_base_table dst_positive_scale_base_table dst_negative_code_base_table dst_negative_scale_base_table. (((F) = (((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) * S ((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) + ((((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))))) /\ (forall dst_index_base_table. (exists pvs_le_gap_base_tabledomain. pvs_le_gap_base_tabledomain + (dst_index_base_table) = (0)) -> exists dst_positive_base_table dst_negative_base_table dst_value_base_table. ((((exists ff_h_pvs_base_tableentrypositive. ff_h_pvs_base_tableentrypositive + S (dst_positive_base_table) = S ((S (dst_index_base_table)) * dst_positive_scale_base_table)) /\ exists ff_q_pvs_base_tableentrypositive. dst_positive_code_base_table = ff_q_pvs_base_tableentrypositive * S ((S (dst_index_base_table)) * dst_positive_scale_base_table) + (dst_positive_base_table))) /\ (((((exists ff_h_pvs_base_tableentrynegative. ff_h_pvs_base_tableentrynegative + S (dst_negative_base_table) = S ((S (dst_index_base_table)) * dst_negative_scale_base_table)) /\ exists ff_q_pvs_base_tableentrynegative. dst_negative_code_base_table = ff_q_pvs_base_tableentrynegative * S ((S (dst_index_base_table)) * dst_negative_scale_base_table) + (dst_negative_base_table))) /\ (exists ge_balance_positive_base_tableentryvalue ge_balance_negative_base_tableentryvalue. (((((dst_value_base_table) = 2 * (ge_balance_positive_base_tableentryvalue) /\ (ge_balance_negative_base_tableentryvalue) = 0) \/ exists ge_signed_half_base_tableentryvaluedecode. (((dst_value_base_table) = 2 * ge_signed_half_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_base_tableentryvalue) = 0) /\ (ge_balance_negative_base_tableentryvalue) = S ge_signed_half_base_tableentryvaluedecode))) /\ ((dst_positive_base_table) + ge_balance_negative_base_tableentryvalue = (dst_negative_base_table) + ge_balance_positive_base_tableentryvalue))))))))) -> (exists dst_positive_code_base_zero dst_positive_scale_base_zero dst_negative_code_base_zero dst_negative_scale_base_zero dst_positive_base_zero dst_negative_base_zero. (((F) = (((((dst_positive_code_base_zero) + (dst_positive_scale_base_zero)) * S ((dst_positive_code_base_zero) + (dst_positive_scale_base_zero)) + ((dst_positive_scale_base_zero) + (dst_positive_scale_base_zero))) + (((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) * S ((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) + ((dst_negative_scale_base_zero) + (dst_negative_scale_base_zero)))) * S ((((dst_positive_code_base_zero) + (dst_positive_scale_base_zero)) * S ((dst_positive_code_base_zero) + (dst_positive_scale_base_zero)) + ((dst_positive_scale_base_zero) + (dst_positive_scale_base_zero))) + (((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) * S ((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) + ((dst_negative_scale_base_zero) + (dst_negative_scale_base_zero)))) + ((((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) * S ((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) + ((dst_negative_scale_base_zero) + (dst_negative_scale_base_zero))) + (((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) * S ((dst_negative_code_base_zero) + (dst_negative_scale_base_zero)) + ((dst_negative_scale_base_zero) + (dst_negative_scale_base_zero)))))) /\ (((((exists ff_h_pvs_base_zeropositive. ff_h_pvs_base_zeropositive + S (dst_positive_base_zero) = S ((S (0)) * dst_positive_scale_base_zero)) /\ exists ff_q_pvs_base_zeropositive. dst_positive_code_base_zero = ff_q_pvs_base_zeropositive * S ((S (0)) * dst_positive_scale_base_zero) + (dst_positive_base_zero))) /\ (((((exists ff_h_pvs_base_zeronegative. ff_h_pvs_base_zeronegative + S (dst_negative_base_zero) = S ((S (0)) * dst_negative_scale_base_zero)) /\ exists ff_q_pvs_base_zeronegative. dst_negative_code_base_zero = ff_q_pvs_base_zeronegative * S ((S (0)) * dst_negative_scale_base_zero) + (dst_negative_base_zero))) /\ (exists ge_balance_positive_base_zerovalue ge_balance_negative_base_zerovalue. (((((0) = 2 * (ge_balance_positive_base_zerovalue) /\ (ge_balance_negative_base_zerovalue) = 0) \/ exists ge_signed_half_base_zerovaluedecode. (((0) = 2 * ge_signed_half_base_zerovaluedecode + 1 /\ (ge_balance_positive_base_zerovalue) = 0) /\ (ge_balance_negative_base_zerovalue) = S ge_signed_half_base_zerovaluedecode))) /\ ((dst_positive_base_zero) + ge_balance_negative_base_zerovalue = (dst_negative_base_zero) + ge_balance_positive_base_zerovalue))))))))) -> (((exists dst_positive_code_base_resulttable dst_positive_scale_base_resulttable dst_negative_code_base_resulttable dst_negative_scale_base_resulttable. (((F) = (((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) * S ((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) + ((((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))))) /\ (forall dst_index_base_resulttable. (exists pvs_le_gap_base_resulttabledomain. pvs_le_gap_base_resulttabledomain + (dst_index_base_resulttable) = (0)) -> exists dst_positive_base_resulttable dst_negative_base_resulttable dst_value_base_resulttable. ((((exists ff_h_pvs_base_resulttableentrypositive. ff_h_pvs_base_resulttableentrypositive + S (dst_positive_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrypositive. dst_positive_code_base_resulttable = ff_q_pvs_base_resulttableentrypositive * S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable) + (dst_positive_base_resulttable))) /\ (((((exists ff_h_pvs_base_resulttableentrynegative. ff_h_pvs_base_resulttableentrynegative + S (dst_negative_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrynegative. dst_negative_code_base_resulttable = ff_q_pvs_base_resulttableentrynegative * S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable) + (dst_negative_base_resulttable))) /\ (exists ge_balance_positive_base_resulttableentryvalue ge_balance_negative_base_resulttableentryvalue. (((((dst_value_base_resulttable) = 2 * (ge_balance_positive_base_resulttableentryvalue) /\ (ge_balance_negative_base_resulttableentryvalue) = 0) \/ exists ge_signed_half_base_resulttableentryvaluedecode. (((dst_value_base_resulttable) = 2 * ge_signed_half_base_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_base_resulttableentryvalue) = 0) /\ (ge_balance_negative_base_resulttableentryvalue) = S ge_signed_half_base_resulttableentryvaluedecode))) /\ ((dst_positive_base_resulttable) + ge_balance_negative_base_resulttableentryvalue = (dst_negative_base_resulttable) + ge_balance_positive_base_resulttableentryvalue))))))))) /\ (((exists dst_positive_code_base_resultzero dst_positive_scale_base_resultzero dst_negative_code_base_resultzero dst_negative_scale_base_resultzero dst_positive_base_resultzero dst_negative_base_resultzero. (((F) = (((((dst_positive_code_base_resultzero) + (dst_positive_scale_base_resultzero)) * S ((dst_positive_code_base_resultzero) + (dst_positive_scale_base_resultzero)) + ((dst_positive_scale_base_resultzero) + (dst_positive_scale_base_resultzero))) + (((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) * S ((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) + ((dst_negative_scale_base_resultzero) + (dst_negative_scale_base_resultzero)))) * S ((((dst_positive_code_base_resultzero) + (dst_positive_scale_base_resultzero)) * S ((dst_positive_code_base_resultzero) + (dst_positive_scale_base_resultzero)) + ((dst_positive_scale_base_resultzero) + (dst_positive_scale_base_resultzero))) + (((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) * S ((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) + ((dst_negative_scale_base_resultzero) + (dst_negative_scale_base_resultzero)))) + ((((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) * S ((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) + ((dst_negative_scale_base_resultzero) + (dst_negative_scale_base_resultzero))) + (((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) * S ((dst_negative_code_base_resultzero) + (dst_negative_scale_base_resultzero)) + ((dst_negative_scale_base_resultzero) + (dst_negative_scale_base_resultzero)))))) /\ (((((exists ff_h_pvs_base_resultzeropositive. ff_h_pvs_base_resultzeropositive + S (dst_positive_base_resultzero) = S ((S (0)) * dst_positive_scale_base_resultzero)) /\ exists ff_q_pvs_base_resultzeropositive. dst_positive_code_base_resultzero = ff_q_pvs_base_resultzeropositive * S ((S (0)) * dst_positive_scale_base_resultzero) + (dst_positive_base_resultzero))) /\ (((((exists ff_h_pvs_base_resultzeronegative. ff_h_pvs_base_resultzeronegative + S (dst_negative_base_resultzero) = S ((S (0)) * dst_negative_scale_base_resultzero)) /\ exists ff_q_pvs_base_resultzeronegative. dst_negative_code_base_resultzero = ff_q_pvs_base_resultzeronegative * S ((S (0)) * dst_negative_scale_base_resultzero) + (dst_negative_base_resultzero))) /\ (exists ge_balance_positive_base_resultzerovalue ge_balance_negative_base_resultzerovalue. (((((0) = 2 * (ge_balance_positive_base_resultzerovalue) /\ (ge_balance_negative_base_resultzerovalue) = 0) \/ exists ge_signed_half_base_resultzerovaluedecode. (((0) = 2 * ge_signed_half_base_resultzerovaluedecode + 1 /\ (ge_balance_positive_base_resultzerovalue) = 0) /\ (ge_balance_negative_base_resultzerovalue) = S ge_signed_half_base_resultzerovaluedecode))) /\ ((dst_positive_base_resultzero) + ge_balance_negative_base_resultzerovalue = (dst_negative_base_resultzero) + ge_balance_positive_base_resultzerovalue))))))))) /\ (forall mt_index_base_result mt_value_base_result. ~(mt_index_base_result=0) -> (exists pvs_le_gap_base_resultdomain. pvs_le_gap_base_resultdomain + (mt_index_base_result) = (0)) -> (exists dst_positive_code_base_resultentry dst_positive_scale_base_resultentry dst_negative_code_base_resultentry dst_negative_scale_base_resultentry dst_positive_base_resultentry dst_negative_base_resultentry. (((F) = (((((dst_positive_code_base_resultentry) + (dst_positive_scale_base_resultentry)) * S ((dst_positive_code_base_resultentry) + (dst_positive_scale_base_resultentry)) + ((dst_positive_scale_base_resultentry) + (dst_positive_scale_base_resultentry))) + (((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) * S ((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) + ((dst_negative_scale_base_resultentry) + (dst_negative_scale_base_resultentry)))) * S ((((dst_positive_code_base_resultentry) + (dst_positive_scale_base_resultentry)) * S ((dst_positive_code_base_resultentry) + (dst_positive_scale_base_resultentry)) + ((dst_positive_scale_base_resultentry) + (dst_positive_scale_base_resultentry))) + (((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) * S ((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) + ((dst_negative_scale_base_resultentry) + (dst_negative_scale_base_resultentry)))) + ((((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) * S ((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) + ((dst_negative_scale_base_resultentry) + (dst_negative_scale_base_resultentry))) + (((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) * S ((dst_negative_code_base_resultentry) + (dst_negative_scale_base_resultentry)) + ((dst_negative_scale_base_resultentry) + (dst_negative_scale_base_resultentry)))))) /\ (((((exists ff_h_pvs_base_resultentrypositive. ff_h_pvs_base_resultentrypositive + S (dst_positive_base_resultentry) = S ((S (mt_index_base_result)) * dst_positive_scale_base_resultentry)) /\ exists ff_q_pvs_base_resultentrypositive. dst_positive_code_base_resultentry = ff_q_pvs_base_resultentrypositive * S ((S (mt_index_base_result)) * dst_positive_scale_base_resultentry) + (dst_positive_base_resultentry))) /\ (((((exists ff_h_pvs_base_resultentrynegative. ff_h_pvs_base_resultentrynegative + S (dst_negative_base_resultentry) = S ((S (mt_index_base_result)) * dst_negative_scale_base_resultentry)) /\ exists ff_q_pvs_base_resultentrynegative. dst_negative_code_base_resultentry = ff_q_pvs_base_resultentrynegative * S ((S (mt_index_base_result)) * dst_negative_scale_base_resultentry) + (dst_negative_base_resultentry))) /\ (exists ge_balance_positive_base_resultentryvalue ge_balance_negative_base_resultentryvalue. (((((mt_value_base_result) = 2 * (ge_balance_positive_base_resultentryvalue) /\ (ge_balance_negative_base_resultentryvalue) = 0) \/ exists ge_signed_half_base_resultentryvaluedecode. (((mt_value_base_result) = 2 * ge_signed_half_base_resultentryvaluedecode + 1 /\ (ge_balance_positive_base_resultentryvalue) = 0) /\ (ge_balance_negative_base_resultentryvalue) = S ge_signed_half_base_resultentryvaluedecode))) /\ ((dst_positive_base_resultentry) + ge_balance_negative_base_resultentryvalue = (dst_negative_base_resultentry) + ge_balance_positive_base_resultentryvalue))))))))) -> (((~((mt_index_base_result) = 0)) /\ ((((exists mv_square_prime_base_resultvaluesquare. ((~((mv_square_prime_base_resultvaluesquare) = 1) /\ forall pvs_left_base_resultvaluesquareprime pvs_right_base_resultvaluesquareprime. (mv_square_prime_base_resultvaluesquare) = pvs_left_base_resultvaluesquareprime * pvs_right_base_resultvaluesquareprime -> pvs_left_base_resultvaluesquareprime = 1 \/ pvs_right_base_resultvaluesquareprime = 1) /\ (exists pvs_factor_base_resultvaluesquaredivisor. (mt_index_base_result) = (mv_square_prime_base_resultvaluesquare * mv_square_prime_base_resultvaluesquare) * pvs_factor_base_resultvaluesquaredivisor))) /\ ((mt_value_base_result) = 0))) \/ (((((~((mt_index_base_result) = 0)) /\ (forall sfd_prime_base_resultvaluesquarefree. (~((sfd_prime_base_resultvaluesquarefree) = 1) /\ forall pvs_left_base_resultvaluesquarefreedomain pvs_right_base_resultvaluesquarefreedomain. (sfd_prime_base_resultvaluesquarefree) = pvs_left_base_resultvaluesquarefreedomain * pvs_right_base_resultvaluesquarefreedomain -> pvs_left_base_resultvaluesquarefreedomain = 1 \/ pvs_right_base_resultvaluesquarefreedomain = 1) -> (exists pvs_le_gap_base_resultvaluesquarefreebound. pvs_le_gap_base_resultvaluesquarefreebound + (sfd_prime_base_resultvaluesquarefree) = (mt_index_base_result)) -> ~(exists pvs_factor_base_resultvaluesquarefreesquare. (mt_index_base_result) = (sfd_prime_base_resultvaluesquarefree * sfd_prime_base_resultvaluesquarefree) * pvs_factor_base_resultvaluesquarefreesquare)))) /\ (exists mv_factor_code_base_resultvaluefactors mv_factor_scale_base_resultvaluefactors mv_factor_count_base_resultvaluefactors. (((~(mt_index_base_result = 0) /\ ((exists ff_u_fsat_base_resultvaluefactorsfactorization_product ff_v_fsat_base_resultvaluefactorsfactorization_product. ((((exists ff_h_fsat_base_resultvaluefactorsfactorization_product_start. ff_h_fsat_base_resultvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_base_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_base_resultvaluefactorsfactorization_product_start. ff_u_fsat_base_resultvaluefactorsfactorization_product = ff_q_fsat_base_resultvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_base_resultvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_base_resultvaluefactorsfactorization_product_terminal. ff_h_fsat_base_resultvaluefactorsfactorization_product_terminal + S (mt_index_base_result) = S ((S (mv_factor_count_base_resultvaluefactors)) * ff_v_fsat_base_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_base_resultvaluefactorsfactorization_product_terminal. ff_u_fsat_base_resultvaluefactorsfactorization_product = ff_q_fsat_base_resultvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_base_resultvaluefactors)) * ff_v_fsat_base_resultvaluefactorsfactorization_product) + (mt_index_base_result))) /\ forall ff_i_fsat_base_resultvaluefactorsfactorization_product. (exists ff_lt_fsat_base_resultvaluefactorsfactorization_product_bound. ff_lt_fsat_base_resultvaluefactorsfactorization_product_bound + S ff_i_fsat_base_resultvaluefactorsfactorization_product = mv_factor_count_base_resultvaluefactors) -> exists ff_p_fsat_base_resultvaluefactorsfactorization_product ff_r_fsat_base_resultvaluefactorsfactorization_product ff_s_fsat_base_resultvaluefactorsfactorization_product. ((((exists ff_h_fsat_base_resultvaluefactorsfactorization_product_factor. ff_h_fsat_base_resultvaluefactorsfactorization_product_factor + S (ff_p_fsat_base_resultvaluefactorsfactorization_product) = S ((S (ff_i_fsat_base_resultvaluefactorsfactorization_product)) * mv_factor_scale_base_resultvaluefactors)) /\ exists ff_q_fsat_base_resultvaluefactorsfactorization_product_factor. mv_factor_code_base_resultvaluefactors = ff_q_fsat_base_resultvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_base_resultvaluefactorsfactorization_product)) * mv_factor_scale_base_resultvaluefactors) + (ff_p_fsat_base_resultvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_base_resultvaluefactorsfactorization_product_partial. ff_h_fsat_base_resultvaluefactorsfactorization_product_partial + S (ff_r_fsat_base_resultvaluefactorsfactorization_product) = S ((S (ff_i_fsat_base_resultvaluefactorsfactorization_product)) * ff_v_fsat_base_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_base_resultvaluefactorsfactorization_product_partial. ff_u_fsat_base_resultvaluefactorsfactorization_product = ff_q_fsat_base_resultvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_base_resultvaluefactorsfactorization_product)) * ff_v_fsat_base_resultvaluefactorsfactorization_product) + (ff_r_fsat_base_resultvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_base_resultvaluefactorsfactorization_product_successor. ff_h_fsat_base_resultvaluefactorsfactorization_product_successor + S (ff_s_fsat_base_resultvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_base_resultvaluefactorsfactorization_product)) * ff_v_fsat_base_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_base_resultvaluefactorsfactorization_product_successor. ff_u_fsat_base_resultvaluefactorsfactorization_product = ff_q_fsat_base_resultvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_base_resultvaluefactorsfactorization_product)) * ff_v_fsat_base_resultvaluefactorsfactorization_product) + (ff_s_fsat_base_resultvaluefactorsfactorization_product))) /\ ff_s_fsat_base_resultvaluefactorsfactorization_product = ff_r_fsat_base_resultvaluefactorsfactorization_product * ff_p_fsat_base_resultvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_base_resultvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_base_resultvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_base_resultvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_base_resultvaluefactorsfactorization_primes = (mv_factor_count_base_resultvaluefactors)) -> exists ftsf_factor_fsat_base_resultvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_base_resultvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_base_resultvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_base_resultvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_base_resultvaluefactorsfactorization_primes)) * mv_factor_scale_base_resultvaluefactors)) /\ exists ff_q_ftsf_fsat_base_resultvaluefactorsfactorization_primes_entry. mv_factor_code_base_resultvaluefactors = ff_q_ftsf_fsat_base_resultvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_base_resultvaluefactorsfactorization_primes)) * mv_factor_scale_base_resultvaluefactors) + (ftsf_factor_fsat_base_resultvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_base_resultvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_base_resultvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_base_resultvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_base_resultvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_base_resultvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_base_resultvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_base_resultvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_base_resultvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_base_resultvaluefactorsparityeven. (mv_factor_count_base_resultvaluefactors) = 2 * mv_even_half_base_resultvaluefactorsparityeven) /\ ((mt_value_base_result) = 2))) \/ (((exists mv_odd_half_base_resultvaluefactorsparityodd. (mv_factor_count_base_resultvaluefactors) = 2 * mv_odd_half_base_resultvaluefactorsparityodd + 1) /\ ((mt_value_base_result) = 1))))))))))))))))