mobius_table_append

forall N F z. (((exists dst_positive_code_append_oldtable dst_positive_scale_append_oldtable dst_negative_code_append_oldtable dst_negative_scale_append_oldtable. (((F) = (((((dst_positive_code_append_oldtable) + (dst_positive_scale_append_oldtable)) * S ((dst_positive_code_append_oldtable) + (dst_positive_scale_append_oldtable)) + ((dst_positive_scale_append_oldtable) + (dst_positive_scale_append_oldtable))) + (((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) * S ((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) + ((dst_negative_scale_append_oldtable) + (dst_negative_scale_append_oldtable)))) * S ((((dst_positive_code_append_oldtable) + (dst_positive_scale_append_oldtable)) * S ((dst_positive_code_append_oldtable) + (dst_positive_scale_append_oldtable)) + ((dst_positive_scale_append_oldtable) + (dst_positive_scale_append_oldtable))) + (((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) * S ((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) + ((dst_negative_scale_append_oldtable) + (dst_negative_scale_append_oldtable)))) + ((((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) * S ((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) + ((dst_negative_scale_append_oldtable) + (dst_negative_scale_append_oldtable))) + (((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) * S ((dst_negative_code_append_oldtable) + (dst_negative_scale_append_oldtable)) + ((dst_negative_scale_append_oldtable) + (dst_negative_scale_append_oldtable)))))) /\ (forall dst_index_append_oldtable. (exists pvs_le_gap_append_oldtabledomain. pvs_le_gap_append_oldtabledomain + (dst_index_append_oldtable) = (N)) -> exists dst_positive_append_oldtable dst_negative_append_oldtable dst_value_append_oldtable. ((((exists ff_h_pvs_append_oldtableentrypositive. ff_h_pvs_append_oldtableentrypositive + S (dst_positive_append_oldtable) = S ((S (dst_index_append_oldtable)) * dst_positive_scale_append_oldtable)) /\ exists ff_q_pvs_append_oldtableentrypositive. dst_positive_code_append_oldtable = ff_q_pvs_append_oldtableentrypositive * S ((S (dst_index_append_oldtable)) * dst_positive_scale_append_oldtable) + (dst_positive_append_oldtable))) /\ (((((exists ff_h_pvs_append_oldtableentrynegative. ff_h_pvs_append_oldtableentrynegative + S (dst_negative_append_oldtable) = S ((S (dst_index_append_oldtable)) * dst_negative_scale_append_oldtable)) /\ exists ff_q_pvs_append_oldtableentrynegative. dst_negative_code_append_oldtable = ff_q_pvs_append_oldtableentrynegative * S ((S (dst_index_append_oldtable)) * dst_negative_scale_append_oldtable) + (dst_negative_append_oldtable))) /\ (exists ge_balance_positive_append_oldtableentryvalue ge_balance_negative_append_oldtableentryvalue. (((((dst_value_append_oldtable) = 2 * (ge_balance_positive_append_oldtableentryvalue) /\ (ge_balance_negative_append_oldtableentryvalue) = 0) \/ exists ge_signed_half_append_oldtableentryvaluedecode. (((dst_value_append_oldtable) = 2 * ge_signed_half_append_oldtableentryvaluedecode + 1 /\ (ge_balance_positive_append_oldtableentryvalue) = 0) /\ (ge_balance_negative_append_oldtableentryvalue) = S ge_signed_half_append_oldtableentryvaluedecode))) /\ ((dst_positive_append_oldtable) + ge_balance_negative_append_oldtableentryvalue = (dst_negative_append_oldtable) + ge_balance_positive_append_oldtableentryvalue))))))))) /\ (((exists dst_positive_code_append_oldzero dst_positive_scale_append_oldzero dst_negative_code_append_oldzero dst_negative_scale_append_oldzero dst_positive_append_oldzero dst_negative_append_oldzero. (((F) = (((((dst_positive_code_append_oldzero) + (dst_positive_scale_append_oldzero)) * S ((dst_positive_code_append_oldzero) + (dst_positive_scale_append_oldzero)) + ((dst_positive_scale_append_oldzero) + (dst_positive_scale_append_oldzero))) + (((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) * S ((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) + ((dst_negative_scale_append_oldzero) + (dst_negative_scale_append_oldzero)))) * S ((((dst_positive_code_append_oldzero) + (dst_positive_scale_append_oldzero)) * S ((dst_positive_code_append_oldzero) + (dst_positive_scale_append_oldzero)) + ((dst_positive_scale_append_oldzero) + (dst_positive_scale_append_oldzero))) + (((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) * S ((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) + ((dst_negative_scale_append_oldzero) + (dst_negative_scale_append_oldzero)))) + ((((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) * S ((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) + ((dst_negative_scale_append_oldzero) + (dst_negative_scale_append_oldzero))) + (((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) * S ((dst_negative_code_append_oldzero) + (dst_negative_scale_append_oldzero)) + ((dst_negative_scale_append_oldzero) + (dst_negative_scale_append_oldzero)))))) /\ (((((exists ff_h_pvs_append_oldzeropositive. ff_h_pvs_append_oldzeropositive + S (dst_positive_append_oldzero) = S ((S (0)) * dst_positive_scale_append_oldzero)) /\ exists ff_q_pvs_append_oldzeropositive. dst_positive_code_append_oldzero = ff_q_pvs_append_oldzeropositive * S ((S (0)) * dst_positive_scale_append_oldzero) + (dst_positive_append_oldzero))) /\ (((((exists ff_h_pvs_append_oldzeronegative. ff_h_pvs_append_oldzeronegative + S (dst_negative_append_oldzero) = S ((S (0)) * dst_negative_scale_append_oldzero)) /\ exists ff_q_pvs_append_oldzeronegative. dst_negative_code_append_oldzero = ff_q_pvs_append_oldzeronegative * S ((S (0)) * dst_negative_scale_append_oldzero) + (dst_negative_append_oldzero))) /\ (exists ge_balance_positive_append_oldzerovalue ge_balance_negative_append_oldzerovalue. (((((0) = 2 * (ge_balance_positive_append_oldzerovalue) /\ (ge_balance_negative_append_oldzerovalue) = 0) \/ exists ge_signed_half_append_oldzerovaluedecode. (((0) = 2 * ge_signed_half_append_oldzerovaluedecode + 1 /\ (ge_balance_positive_append_oldzerovalue) = 0) /\ (ge_balance_negative_append_oldzerovalue) = S ge_signed_half_append_oldzerovaluedecode))) /\ ((dst_positive_append_oldzero) + ge_balance_negative_append_oldzerovalue = (dst_negative_append_oldzero) + ge_balance_positive_append_oldzerovalue))))))))) /\ (forall mt_index_append_old mt_value_append_old. ~(mt_index_append_old=0) -> (exists pvs_le_gap_append_olddomain. pvs_le_gap_append_olddomain + (mt_index_append_old) = (N)) -> (exists dst_positive_code_append_oldentry dst_positive_scale_append_oldentry dst_negative_code_append_oldentry dst_negative_scale_append_oldentry dst_positive_append_oldentry dst_negative_append_oldentry. (((F) = (((((dst_positive_code_append_oldentry) + (dst_positive_scale_append_oldentry)) * S ((dst_positive_code_append_oldentry) + (dst_positive_scale_append_oldentry)) + ((dst_positive_scale_append_oldentry) + (dst_positive_scale_append_oldentry))) + (((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) * S ((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) + ((dst_negative_scale_append_oldentry) + (dst_negative_scale_append_oldentry)))) * S ((((dst_positive_code_append_oldentry) + (dst_positive_scale_append_oldentry)) * S ((dst_positive_code_append_oldentry) + (dst_positive_scale_append_oldentry)) + ((dst_positive_scale_append_oldentry) + (dst_positive_scale_append_oldentry))) + (((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) * S ((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) + ((dst_negative_scale_append_oldentry) + (dst_negative_scale_append_oldentry)))) + ((((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) * S ((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) + ((dst_negative_scale_append_oldentry) + (dst_negative_scale_append_oldentry))) + (((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) * S ((dst_negative_code_append_oldentry) + (dst_negative_scale_append_oldentry)) + ((dst_negative_scale_append_oldentry) + (dst_negative_scale_append_oldentry)))))) /\ (((((exists ff_h_pvs_append_oldentrypositive. ff_h_pvs_append_oldentrypositive + S (dst_positive_append_oldentry) = S ((S (mt_index_append_old)) * dst_positive_scale_append_oldentry)) /\ exists ff_q_pvs_append_oldentrypositive. dst_positive_code_append_oldentry = ff_q_pvs_append_oldentrypositive * S ((S (mt_index_append_old)) * dst_positive_scale_append_oldentry) + (dst_positive_append_oldentry))) /\ (((((exists ff_h_pvs_append_oldentrynegative. ff_h_pvs_append_oldentrynegative + S (dst_negative_append_oldentry) = S ((S (mt_index_append_old)) * dst_negative_scale_append_oldentry)) /\ exists ff_q_pvs_append_oldentrynegative. dst_negative_code_append_oldentry = ff_q_pvs_append_oldentrynegative * S ((S (mt_index_append_old)) * dst_negative_scale_append_oldentry) + (dst_negative_append_oldentry))) /\ (exists ge_balance_positive_append_oldentryvalue ge_balance_negative_append_oldentryvalue. (((((mt_value_append_old) = 2 * (ge_balance_positive_append_oldentryvalue) /\ (ge_balance_negative_append_oldentryvalue) = 0) \/ exists ge_signed_half_append_oldentryvaluedecode. (((mt_value_append_old) = 2 * ge_signed_half_append_oldentryvaluedecode + 1 /\ (ge_balance_positive_append_oldentryvalue) = 0) /\ (ge_balance_negative_append_oldentryvalue) = S ge_signed_half_append_oldentryvaluedecode))) /\ ((dst_positive_append_oldentry) + ge_balance_negative_append_oldentryvalue = (dst_negative_append_oldentry) + ge_balance_positive_append_oldentryvalue))))))))) -> (((~((mt_index_append_old) = 0)) /\ ((((exists mv_square_prime_append_oldvaluesquare. ((~((mv_square_prime_append_oldvaluesquare) = 1) /\ forall pvs_left_append_oldvaluesquareprime pvs_right_append_oldvaluesquareprime. (mv_square_prime_append_oldvaluesquare) = pvs_left_append_oldvaluesquareprime * pvs_right_append_oldvaluesquareprime -> pvs_left_append_oldvaluesquareprime = 1 \/ pvs_right_append_oldvaluesquareprime = 1) /\ (exists pvs_factor_append_oldvaluesquaredivisor. (mt_index_append_old) = (mv_square_prime_append_oldvaluesquare * mv_square_prime_append_oldvaluesquare) * pvs_factor_append_oldvaluesquaredivisor))) /\ ((mt_value_append_old) = 0))) \/ (((((~((mt_index_append_old) = 0)) /\ (forall sfd_prime_append_oldvaluesquarefree. (~((sfd_prime_append_oldvaluesquarefree) = 1) /\ forall pvs_left_append_oldvaluesquarefreedomain pvs_right_append_oldvaluesquarefreedomain. (sfd_prime_append_oldvaluesquarefree) = pvs_left_append_oldvaluesquarefreedomain * pvs_right_append_oldvaluesquarefreedomain -> pvs_left_append_oldvaluesquarefreedomain = 1 \/ pvs_right_append_oldvaluesquarefreedomain = 1) -> (exists pvs_le_gap_append_oldvaluesquarefreebound. pvs_le_gap_append_oldvaluesquarefreebound + (sfd_prime_append_oldvaluesquarefree) = (mt_index_append_old)) -> ~(exists pvs_factor_append_oldvaluesquarefreesquare. (mt_index_append_old) = (sfd_prime_append_oldvaluesquarefree * sfd_prime_append_oldvaluesquarefree) * pvs_factor_append_oldvaluesquarefreesquare)))) /\ (exists mv_factor_code_append_oldvaluefactors mv_factor_scale_append_oldvaluefactors mv_factor_count_append_oldvaluefactors. (((~(mt_index_append_old = 0) /\ ((exists ff_u_fsat_append_oldvaluefactorsfactorization_product ff_v_fsat_append_oldvaluefactorsfactorization_product. ((((exists ff_h_fsat_append_oldvaluefactorsfactorization_product_start. ff_h_fsat_append_oldvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_append_oldvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_oldvaluefactorsfactorization_product_start. ff_u_fsat_append_oldvaluefactorsfactorization_product = ff_q_fsat_append_oldvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_append_oldvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_append_oldvaluefactorsfactorization_product_terminal. ff_h_fsat_append_oldvaluefactorsfactorization_product_terminal + S (mt_index_append_old) = S ((S (mv_factor_count_append_oldvaluefactors)) * ff_v_fsat_append_oldvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_oldvaluefactorsfactorization_product_terminal. ff_u_fsat_append_oldvaluefactorsfactorization_product = ff_q_fsat_append_oldvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_append_oldvaluefactors)) * ff_v_fsat_append_oldvaluefactorsfactorization_product) + (mt_index_append_old))) /\ forall ff_i_fsat_append_oldvaluefactorsfactorization_product. (exists ff_lt_fsat_append_oldvaluefactorsfactorization_product_bound. ff_lt_fsat_append_oldvaluefactorsfactorization_product_bound + S ff_i_fsat_append_oldvaluefactorsfactorization_product = mv_factor_count_append_oldvaluefactors) -> exists ff_p_fsat_append_oldvaluefactorsfactorization_product ff_r_fsat_append_oldvaluefactorsfactorization_product ff_s_fsat_append_oldvaluefactorsfactorization_product. ((((exists ff_h_fsat_append_oldvaluefactorsfactorization_product_factor. ff_h_fsat_append_oldvaluefactorsfactorization_product_factor + S (ff_p_fsat_append_oldvaluefactorsfactorization_product) = S ((S (ff_i_fsat_append_oldvaluefactorsfactorization_product)) * mv_factor_scale_append_oldvaluefactors)) /\ exists ff_q_fsat_append_oldvaluefactorsfactorization_product_factor. mv_factor_code_append_oldvaluefactors = ff_q_fsat_append_oldvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_append_oldvaluefactorsfactorization_product)) * mv_factor_scale_append_oldvaluefactors) + (ff_p_fsat_append_oldvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_append_oldvaluefactorsfactorization_product_partial. ff_h_fsat_append_oldvaluefactorsfactorization_product_partial + S (ff_r_fsat_append_oldvaluefactorsfactorization_product) = S ((S (ff_i_fsat_append_oldvaluefactorsfactorization_product)) * ff_v_fsat_append_oldvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_oldvaluefactorsfactorization_product_partial. ff_u_fsat_append_oldvaluefactorsfactorization_product = ff_q_fsat_append_oldvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_append_oldvaluefactorsfactorization_product)) * ff_v_fsat_append_oldvaluefactorsfactorization_product) + (ff_r_fsat_append_oldvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_append_oldvaluefactorsfactorization_product_successor. ff_h_fsat_append_oldvaluefactorsfactorization_product_successor + S (ff_s_fsat_append_oldvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_append_oldvaluefactorsfactorization_product)) * ff_v_fsat_append_oldvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_oldvaluefactorsfactorization_product_successor. ff_u_fsat_append_oldvaluefactorsfactorization_product = ff_q_fsat_append_oldvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_append_oldvaluefactorsfactorization_product)) * ff_v_fsat_append_oldvaluefactorsfactorization_product) + (ff_s_fsat_append_oldvaluefactorsfactorization_product))) /\ ff_s_fsat_append_oldvaluefactorsfactorization_product = ff_r_fsat_append_oldvaluefactorsfactorization_product * ff_p_fsat_append_oldvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_append_oldvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_append_oldvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_append_oldvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_append_oldvaluefactorsfactorization_primes = (mv_factor_count_append_oldvaluefactors)) -> exists ftsf_factor_fsat_append_oldvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_append_oldvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_append_oldvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_append_oldvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_append_oldvaluefactorsfactorization_primes)) * mv_factor_scale_append_oldvaluefactors)) /\ exists ff_q_ftsf_fsat_append_oldvaluefactorsfactorization_primes_entry. mv_factor_code_append_oldvaluefactors = ff_q_ftsf_fsat_append_oldvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_append_oldvaluefactorsfactorization_primes)) * mv_factor_scale_append_oldvaluefactors) + (ftsf_factor_fsat_append_oldvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_append_oldvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_append_oldvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_append_oldvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_append_oldvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_append_oldvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_append_oldvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_append_oldvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_append_oldvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_append_oldvaluefactorsparityeven. (mv_factor_count_append_oldvaluefactors) = 2 * mv_even_half_append_oldvaluefactorsparityeven) /\ ((mt_value_append_old) = 2))) \/ (((exists mv_odd_half_append_oldvaluefactorsparityodd. (mv_factor_count_append_oldvaluefactors) = 2 * mv_odd_half_append_oldvaluefactorsparityodd + 1) /\ ((mt_value_append_old) = 1)))))))))))))))) -> (((~((S N) = 0)) /\ ((((exists mv_square_prime_append_valuesquare. ((~((mv_square_prime_append_valuesquare) = 1) /\ forall pvs_left_append_valuesquareprime pvs_right_append_valuesquareprime. (mv_square_prime_append_valuesquare) = pvs_left_append_valuesquareprime * pvs_right_append_valuesquareprime -> pvs_left_append_valuesquareprime = 1 \/ pvs_right_append_valuesquareprime = 1) /\ (exists pvs_factor_append_valuesquaredivisor. (S N) = (mv_square_prime_append_valuesquare * mv_square_prime_append_valuesquare) * pvs_factor_append_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((S N) = 0)) /\ (forall sfd_prime_append_valuesquarefree. (~((sfd_prime_append_valuesquarefree) = 1) /\ forall pvs_left_append_valuesquarefreedomain pvs_right_append_valuesquarefreedomain. (sfd_prime_append_valuesquarefree) = pvs_left_append_valuesquarefreedomain * pvs_right_append_valuesquarefreedomain -> pvs_left_append_valuesquarefreedomain = 1 \/ pvs_right_append_valuesquarefreedomain = 1) -> (exists pvs_le_gap_append_valuesquarefreebound. pvs_le_gap_append_valuesquarefreebound + (sfd_prime_append_valuesquarefree) = (S N)) -> ~(exists pvs_factor_append_valuesquarefreesquare. (S N) = (sfd_prime_append_valuesquarefree * sfd_prime_append_valuesquarefree) * pvs_factor_append_valuesquarefreesquare)))) /\ (exists mv_factor_code_append_valuefactors mv_factor_scale_append_valuefactors mv_factor_count_append_valuefactors. (((~(S N = 0) /\ ((exists ff_u_fsat_append_valuefactorsfactorization_product ff_v_fsat_append_valuefactorsfactorization_product. ((((exists ff_h_fsat_append_valuefactorsfactorization_product_start. ff_h_fsat_append_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_append_valuefactorsfactorization_product)) /\ exists ff_q_fsat_append_valuefactorsfactorization_product_start. ff_u_fsat_append_valuefactorsfactorization_product = ff_q_fsat_append_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_append_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_append_valuefactorsfactorization_product_terminal. ff_h_fsat_append_valuefactorsfactorization_product_terminal + S (S N) = S ((S (mv_factor_count_append_valuefactors)) * ff_v_fsat_append_valuefactorsfactorization_product)) /\ exists ff_q_fsat_append_valuefactorsfactorization_product_terminal. ff_u_fsat_append_valuefactorsfactorization_product = ff_q_fsat_append_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_append_valuefactors)) * ff_v_fsat_append_valuefactorsfactorization_product) + (S N))) /\ forall ff_i_fsat_append_valuefactorsfactorization_product. (exists ff_lt_fsat_append_valuefactorsfactorization_product_bound. ff_lt_fsat_append_valuefactorsfactorization_product_bound + S ff_i_fsat_append_valuefactorsfactorization_product = mv_factor_count_append_valuefactors) -> exists ff_p_fsat_append_valuefactorsfactorization_product ff_r_fsat_append_valuefactorsfactorization_product ff_s_fsat_append_valuefactorsfactorization_product. ((((exists ff_h_fsat_append_valuefactorsfactorization_product_factor. ff_h_fsat_append_valuefactorsfactorization_product_factor + S (ff_p_fsat_append_valuefactorsfactorization_product) = S ((S (ff_i_fsat_append_valuefactorsfactorization_product)) * mv_factor_scale_append_valuefactors)) /\ exists ff_q_fsat_append_valuefactorsfactorization_product_factor. mv_factor_code_append_valuefactors = ff_q_fsat_append_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_append_valuefactorsfactorization_product)) * mv_factor_scale_append_valuefactors) + (ff_p_fsat_append_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_append_valuefactorsfactorization_product_partial. ff_h_fsat_append_valuefactorsfactorization_product_partial + S (ff_r_fsat_append_valuefactorsfactorization_product) = S ((S (ff_i_fsat_append_valuefactorsfactorization_product)) * ff_v_fsat_append_valuefactorsfactorization_product)) /\ exists ff_q_fsat_append_valuefactorsfactorization_product_partial. ff_u_fsat_append_valuefactorsfactorization_product = ff_q_fsat_append_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_append_valuefactorsfactorization_product)) * ff_v_fsat_append_valuefactorsfactorization_product) + (ff_r_fsat_append_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_append_valuefactorsfactorization_product_successor. ff_h_fsat_append_valuefactorsfactorization_product_successor + S (ff_s_fsat_append_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_append_valuefactorsfactorization_product)) * ff_v_fsat_append_valuefactorsfactorization_product)) /\ exists ff_q_fsat_append_valuefactorsfactorization_product_successor. ff_u_fsat_append_valuefactorsfactorization_product = ff_q_fsat_append_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_append_valuefactorsfactorization_product)) * ff_v_fsat_append_valuefactorsfactorization_product) + (ff_s_fsat_append_valuefactorsfactorization_product))) /\ ff_s_fsat_append_valuefactorsfactorization_product = ff_r_fsat_append_valuefactorsfactorization_product * ff_p_fsat_append_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_append_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_append_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_append_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_append_valuefactorsfactorization_primes = (mv_factor_count_append_valuefactors)) -> exists ftsf_factor_fsat_append_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_append_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_append_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_append_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_append_valuefactorsfactorization_primes)) * mv_factor_scale_append_valuefactors)) /\ exists ff_q_ftsf_fsat_append_valuefactorsfactorization_primes_entry. mv_factor_code_append_valuefactors = ff_q_ftsf_fsat_append_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_append_valuefactorsfactorization_primes)) * mv_factor_scale_append_valuefactors) + (ftsf_factor_fsat_append_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_append_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_append_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_append_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_append_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_append_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_append_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_append_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_append_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_append_valuefactorsparityeven. (mv_factor_count_append_valuefactors) = 2 * mv_even_half_append_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_append_valuefactorsparityodd. (mv_factor_count_append_valuefactors) = 2 * mv_odd_half_append_valuefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> exists G. (((exists dst_positive_code_append_newtable dst_positive_scale_append_newtable dst_negative_code_append_newtable dst_negative_scale_append_newtable. (((G) = (((((dst_positive_code_append_newtable) + (dst_positive_scale_append_newtable)) * S ((dst_positive_code_append_newtable) + (dst_positive_scale_append_newtable)) + ((dst_positive_scale_append_newtable) + (dst_positive_scale_append_newtable))) + (((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) * S ((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) + ((dst_negative_scale_append_newtable) + (dst_negative_scale_append_newtable)))) * S ((((dst_positive_code_append_newtable) + (dst_positive_scale_append_newtable)) * S ((dst_positive_code_append_newtable) + (dst_positive_scale_append_newtable)) + ((dst_positive_scale_append_newtable) + (dst_positive_scale_append_newtable))) + (((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) * S ((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) + ((dst_negative_scale_append_newtable) + (dst_negative_scale_append_newtable)))) + ((((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) * S ((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) + ((dst_negative_scale_append_newtable) + (dst_negative_scale_append_newtable))) + (((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) * S ((dst_negative_code_append_newtable) + (dst_negative_scale_append_newtable)) + ((dst_negative_scale_append_newtable) + (dst_negative_scale_append_newtable)))))) /\ (forall dst_index_append_newtable. (exists pvs_le_gap_append_newtabledomain. pvs_le_gap_append_newtabledomain + (dst_index_append_newtable) = (S N)) -> exists dst_positive_append_newtable dst_negative_append_newtable dst_value_append_newtable. ((((exists ff_h_pvs_append_newtableentrypositive. ff_h_pvs_append_newtableentrypositive + S (dst_positive_append_newtable) = S ((S (dst_index_append_newtable)) * dst_positive_scale_append_newtable)) /\ exists ff_q_pvs_append_newtableentrypositive. dst_positive_code_append_newtable = ff_q_pvs_append_newtableentrypositive * S ((S (dst_index_append_newtable)) * dst_positive_scale_append_newtable) + (dst_positive_append_newtable))) /\ (((((exists ff_h_pvs_append_newtableentrynegative. ff_h_pvs_append_newtableentrynegative + S (dst_negative_append_newtable) = S ((S (dst_index_append_newtable)) * dst_negative_scale_append_newtable)) /\ exists ff_q_pvs_append_newtableentrynegative. dst_negative_code_append_newtable = ff_q_pvs_append_newtableentrynegative * S ((S (dst_index_append_newtable)) * dst_negative_scale_append_newtable) + (dst_negative_append_newtable))) /\ (exists ge_balance_positive_append_newtableentryvalue ge_balance_negative_append_newtableentryvalue. (((((dst_value_append_newtable) = 2 * (ge_balance_positive_append_newtableentryvalue) /\ (ge_balance_negative_append_newtableentryvalue) = 0) \/ exists ge_signed_half_append_newtableentryvaluedecode. (((dst_value_append_newtable) = 2 * ge_signed_half_append_newtableentryvaluedecode + 1 /\ (ge_balance_positive_append_newtableentryvalue) = 0) /\ (ge_balance_negative_append_newtableentryvalue) = S ge_signed_half_append_newtableentryvaluedecode))) /\ ((dst_positive_append_newtable) + ge_balance_negative_append_newtableentryvalue = (dst_negative_append_newtable) + ge_balance_positive_append_newtableentryvalue))))))))) /\ (((exists dst_positive_code_append_newzero dst_positive_scale_append_newzero dst_negative_code_append_newzero dst_negative_scale_append_newzero dst_positive_append_newzero dst_negative_append_newzero. (((G) = (((((dst_positive_code_append_newzero) + (dst_positive_scale_append_newzero)) * S ((dst_positive_code_append_newzero) + (dst_positive_scale_append_newzero)) + ((dst_positive_scale_append_newzero) + (dst_positive_scale_append_newzero))) + (((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) * S ((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) + ((dst_negative_scale_append_newzero) + (dst_negative_scale_append_newzero)))) * S ((((dst_positive_code_append_newzero) + (dst_positive_scale_append_newzero)) * S ((dst_positive_code_append_newzero) + (dst_positive_scale_append_newzero)) + ((dst_positive_scale_append_newzero) + (dst_positive_scale_append_newzero))) + (((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) * S ((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) + ((dst_negative_scale_append_newzero) + (dst_negative_scale_append_newzero)))) + ((((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) * S ((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) + ((dst_negative_scale_append_newzero) + (dst_negative_scale_append_newzero))) + (((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) * S ((dst_negative_code_append_newzero) + (dst_negative_scale_append_newzero)) + ((dst_negative_scale_append_newzero) + (dst_negative_scale_append_newzero)))))) /\ (((((exists ff_h_pvs_append_newzeropositive. ff_h_pvs_append_newzeropositive + S (dst_positive_append_newzero) = S ((S (0)) * dst_positive_scale_append_newzero)) /\ exists ff_q_pvs_append_newzeropositive. dst_positive_code_append_newzero = ff_q_pvs_append_newzeropositive * S ((S (0)) * dst_positive_scale_append_newzero) + (dst_positive_append_newzero))) /\ (((((exists ff_h_pvs_append_newzeronegative. ff_h_pvs_append_newzeronegative + S (dst_negative_append_newzero) = S ((S (0)) * dst_negative_scale_append_newzero)) /\ exists ff_q_pvs_append_newzeronegative. dst_negative_code_append_newzero = ff_q_pvs_append_newzeronegative * S ((S (0)) * dst_negative_scale_append_newzero) + (dst_negative_append_newzero))) /\ (exists ge_balance_positive_append_newzerovalue ge_balance_negative_append_newzerovalue. (((((0) = 2 * (ge_balance_positive_append_newzerovalue) /\ (ge_balance_negative_append_newzerovalue) = 0) \/ exists ge_signed_half_append_newzerovaluedecode. (((0) = 2 * ge_signed_half_append_newzerovaluedecode + 1 /\ (ge_balance_positive_append_newzerovalue) = 0) /\ (ge_balance_negative_append_newzerovalue) = S ge_signed_half_append_newzerovaluedecode))) /\ ((dst_positive_append_newzero) + ge_balance_negative_append_newzerovalue = (dst_negative_append_newzero) + ge_balance_positive_append_newzerovalue))))))))) /\ (forall mt_index_append_new mt_value_append_new. ~(mt_index_append_new=0) -> (exists pvs_le_gap_append_newdomain. pvs_le_gap_append_newdomain + (mt_index_append_new) = (S N)) -> (exists dst_positive_code_append_newentry dst_positive_scale_append_newentry dst_negative_code_append_newentry dst_negative_scale_append_newentry dst_positive_append_newentry dst_negative_append_newentry. (((G) = (((((dst_positive_code_append_newentry) + (dst_positive_scale_append_newentry)) * S ((dst_positive_code_append_newentry) + (dst_positive_scale_append_newentry)) + ((dst_positive_scale_append_newentry) + (dst_positive_scale_append_newentry))) + (((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) * S ((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) + ((dst_negative_scale_append_newentry) + (dst_negative_scale_append_newentry)))) * S ((((dst_positive_code_append_newentry) + (dst_positive_scale_append_newentry)) * S ((dst_positive_code_append_newentry) + (dst_positive_scale_append_newentry)) + ((dst_positive_scale_append_newentry) + (dst_positive_scale_append_newentry))) + (((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) * S ((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) + ((dst_negative_scale_append_newentry) + (dst_negative_scale_append_newentry)))) + ((((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) * S ((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) + ((dst_negative_scale_append_newentry) + (dst_negative_scale_append_newentry))) + (((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) * S ((dst_negative_code_append_newentry) + (dst_negative_scale_append_newentry)) + ((dst_negative_scale_append_newentry) + (dst_negative_scale_append_newentry)))))) /\ (((((exists ff_h_pvs_append_newentrypositive. ff_h_pvs_append_newentrypositive + S (dst_positive_append_newentry) = S ((S (mt_index_append_new)) * dst_positive_scale_append_newentry)) /\ exists ff_q_pvs_append_newentrypositive. dst_positive_code_append_newentry = ff_q_pvs_append_newentrypositive * S ((S (mt_index_append_new)) * dst_positive_scale_append_newentry) + (dst_positive_append_newentry))) /\ (((((exists ff_h_pvs_append_newentrynegative. ff_h_pvs_append_newentrynegative + S (dst_negative_append_newentry) = S ((S (mt_index_append_new)) * dst_negative_scale_append_newentry)) /\ exists ff_q_pvs_append_newentrynegative. dst_negative_code_append_newentry = ff_q_pvs_append_newentrynegative * S ((S (mt_index_append_new)) * dst_negative_scale_append_newentry) + (dst_negative_append_newentry))) /\ (exists ge_balance_positive_append_newentryvalue ge_balance_negative_append_newentryvalue. (((((mt_value_append_new) = 2 * (ge_balance_positive_append_newentryvalue) /\ (ge_balance_negative_append_newentryvalue) = 0) \/ exists ge_signed_half_append_newentryvaluedecode. (((mt_value_append_new) = 2 * ge_signed_half_append_newentryvaluedecode + 1 /\ (ge_balance_positive_append_newentryvalue) = 0) /\ (ge_balance_negative_append_newentryvalue) = S ge_signed_half_append_newentryvaluedecode))) /\ ((dst_positive_append_newentry) + ge_balance_negative_append_newentryvalue = (dst_negative_append_newentry) + ge_balance_positive_append_newentryvalue))))))))) -> (((~((mt_index_append_new) = 0)) /\ ((((exists mv_square_prime_append_newvaluesquare. ((~((mv_square_prime_append_newvaluesquare) = 1) /\ forall pvs_left_append_newvaluesquareprime pvs_right_append_newvaluesquareprime. (mv_square_prime_append_newvaluesquare) = pvs_left_append_newvaluesquareprime * pvs_right_append_newvaluesquareprime -> pvs_left_append_newvaluesquareprime = 1 \/ pvs_right_append_newvaluesquareprime = 1) /\ (exists pvs_factor_append_newvaluesquaredivisor. (mt_index_append_new) = (mv_square_prime_append_newvaluesquare * mv_square_prime_append_newvaluesquare) * pvs_factor_append_newvaluesquaredivisor))) /\ ((mt_value_append_new) = 0))) \/ (((((~((mt_index_append_new) = 0)) /\ (forall sfd_prime_append_newvaluesquarefree. (~((sfd_prime_append_newvaluesquarefree) = 1) /\ forall pvs_left_append_newvaluesquarefreedomain pvs_right_append_newvaluesquarefreedomain. (sfd_prime_append_newvaluesquarefree) = pvs_left_append_newvaluesquarefreedomain * pvs_right_append_newvaluesquarefreedomain -> pvs_left_append_newvaluesquarefreedomain = 1 \/ pvs_right_append_newvaluesquarefreedomain = 1) -> (exists pvs_le_gap_append_newvaluesquarefreebound. pvs_le_gap_append_newvaluesquarefreebound + (sfd_prime_append_newvaluesquarefree) = (mt_index_append_new)) -> ~(exists pvs_factor_append_newvaluesquarefreesquare. (mt_index_append_new) = (sfd_prime_append_newvaluesquarefree * sfd_prime_append_newvaluesquarefree) * pvs_factor_append_newvaluesquarefreesquare)))) /\ (exists mv_factor_code_append_newvaluefactors mv_factor_scale_append_newvaluefactors mv_factor_count_append_newvaluefactors. (((~(mt_index_append_new = 0) /\ ((exists ff_u_fsat_append_newvaluefactorsfactorization_product ff_v_fsat_append_newvaluefactorsfactorization_product. ((((exists ff_h_fsat_append_newvaluefactorsfactorization_product_start. ff_h_fsat_append_newvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_append_newvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_newvaluefactorsfactorization_product_start. ff_u_fsat_append_newvaluefactorsfactorization_product = ff_q_fsat_append_newvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_append_newvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_append_newvaluefactorsfactorization_product_terminal. ff_h_fsat_append_newvaluefactorsfactorization_product_terminal + S (mt_index_append_new) = S ((S (mv_factor_count_append_newvaluefactors)) * ff_v_fsat_append_newvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_newvaluefactorsfactorization_product_terminal. ff_u_fsat_append_newvaluefactorsfactorization_product = ff_q_fsat_append_newvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_append_newvaluefactors)) * ff_v_fsat_append_newvaluefactorsfactorization_product) + (mt_index_append_new))) /\ forall ff_i_fsat_append_newvaluefactorsfactorization_product. (exists ff_lt_fsat_append_newvaluefactorsfactorization_product_bound. ff_lt_fsat_append_newvaluefactorsfactorization_product_bound + S ff_i_fsat_append_newvaluefactorsfactorization_product = mv_factor_count_append_newvaluefactors) -> exists ff_p_fsat_append_newvaluefactorsfactorization_product ff_r_fsat_append_newvaluefactorsfactorization_product ff_s_fsat_append_newvaluefactorsfactorization_product. ((((exists ff_h_fsat_append_newvaluefactorsfactorization_product_factor. ff_h_fsat_append_newvaluefactorsfactorization_product_factor + S (ff_p_fsat_append_newvaluefactorsfactorization_product) = S ((S (ff_i_fsat_append_newvaluefactorsfactorization_product)) * mv_factor_scale_append_newvaluefactors)) /\ exists ff_q_fsat_append_newvaluefactorsfactorization_product_factor. mv_factor_code_append_newvaluefactors = ff_q_fsat_append_newvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_append_newvaluefactorsfactorization_product)) * mv_factor_scale_append_newvaluefactors) + (ff_p_fsat_append_newvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_append_newvaluefactorsfactorization_product_partial. ff_h_fsat_append_newvaluefactorsfactorization_product_partial + S (ff_r_fsat_append_newvaluefactorsfactorization_product) = S ((S (ff_i_fsat_append_newvaluefactorsfactorization_product)) * ff_v_fsat_append_newvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_newvaluefactorsfactorization_product_partial. ff_u_fsat_append_newvaluefactorsfactorization_product = ff_q_fsat_append_newvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_append_newvaluefactorsfactorization_product)) * ff_v_fsat_append_newvaluefactorsfactorization_product) + (ff_r_fsat_append_newvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_append_newvaluefactorsfactorization_product_successor. ff_h_fsat_append_newvaluefactorsfactorization_product_successor + S (ff_s_fsat_append_newvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_append_newvaluefactorsfactorization_product)) * ff_v_fsat_append_newvaluefactorsfactorization_product)) /\ exists ff_q_fsat_append_newvaluefactorsfactorization_product_successor. ff_u_fsat_append_newvaluefactorsfactorization_product = ff_q_fsat_append_newvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_append_newvaluefactorsfactorization_product)) * ff_v_fsat_append_newvaluefactorsfactorization_product) + (ff_s_fsat_append_newvaluefactorsfactorization_product))) /\ ff_s_fsat_append_newvaluefactorsfactorization_product = ff_r_fsat_append_newvaluefactorsfactorization_product * ff_p_fsat_append_newvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_append_newvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_append_newvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_append_newvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_append_newvaluefactorsfactorization_primes = (mv_factor_count_append_newvaluefactors)) -> exists ftsf_factor_fsat_append_newvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_append_newvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_append_newvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_append_newvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_append_newvaluefactorsfactorization_primes)) * mv_factor_scale_append_newvaluefactors)) /\ exists ff_q_ftsf_fsat_append_newvaluefactorsfactorization_primes_entry. mv_factor_code_append_newvaluefactors = ff_q_ftsf_fsat_append_newvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_append_newvaluefactorsfactorization_primes)) * mv_factor_scale_append_newvaluefactors) + (ftsf_factor_fsat_append_newvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_append_newvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_append_newvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_append_newvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_append_newvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_append_newvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_append_newvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_append_newvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_append_newvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_append_newvaluefactorsparityeven. (mv_factor_count_append_newvaluefactors) = 2 * mv_even_half_append_newvaluefactorsparityeven) /\ ((mt_value_append_new) = 2))) \/ (((exists mv_odd_half_append_newvaluefactorsparityodd. (mv_factor_count_append_newvaluefactors) = 2 * mv_odd_half_append_newvaluefactorsparityodd + 1) /\ ((mt_value_append_new) = 1)))))))))))))))) /\ (forall dst_index_append_preserved dst_first_append_preserved dst_second_append_preserved. (exists pvs_gap_append_preservedbound. pvs_gap_append_preservedbound + S (dst_index_append_preserved) = (S N)) -> (exists dst_positive_code_append_preservedfirst dst_positive_scale_append_preservedfirst dst_negative_code_append_preservedfirst dst_negative_scale_append_preservedfirst dst_positive_append_preservedfirst dst_negative_append_preservedfirst. (((F) = (((((dst_positive_code_append_preservedfirst) + (dst_positive_scale_append_preservedfirst)) * S ((dst_positive_code_append_preservedfirst) + (dst_positive_scale_append_preservedfirst)) + ((dst_positive_scale_append_preservedfirst) + (dst_positive_scale_append_preservedfirst))) + (((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) * S ((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) + ((dst_negative_scale_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)))) * S ((((dst_positive_code_append_preservedfirst) + (dst_positive_scale_append_preservedfirst)) * S ((dst_positive_code_append_preservedfirst) + (dst_positive_scale_append_preservedfirst)) + ((dst_positive_scale_append_preservedfirst) + (dst_positive_scale_append_preservedfirst))) + (((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) * S ((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) + ((dst_negative_scale_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)))) + ((((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) * S ((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) + ((dst_negative_scale_append_preservedfirst) + (dst_negative_scale_append_preservedfirst))) + (((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) * S ((dst_negative_code_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)) + ((dst_negative_scale_append_preservedfirst) + (dst_negative_scale_append_preservedfirst)))))) /\ (((((exists ff_h_pvs_append_preservedfirstpositive. ff_h_pvs_append_preservedfirstpositive + S (dst_positive_append_preservedfirst) = S ((S (dst_index_append_preserved)) * dst_positive_scale_append_preservedfirst)) /\ exists ff_q_pvs_append_preservedfirstpositive. dst_positive_code_append_preservedfirst = ff_q_pvs_append_preservedfirstpositive * S ((S (dst_index_append_preserved)) * dst_positive_scale_append_preservedfirst) + (dst_positive_append_preservedfirst))) /\ (((((exists ff_h_pvs_append_preservedfirstnegative. ff_h_pvs_append_preservedfirstnegative + S (dst_negative_append_preservedfirst) = S ((S (dst_index_append_preserved)) * dst_negative_scale_append_preservedfirst)) /\ exists ff_q_pvs_append_preservedfirstnegative. dst_negative_code_append_preservedfirst = ff_q_pvs_append_preservedfirstnegative * S ((S (dst_index_append_preserved)) * dst_negative_scale_append_preservedfirst) + (dst_negative_append_preservedfirst))) /\ (exists ge_balance_positive_append_preservedfirstvalue ge_balance_negative_append_preservedfirstvalue. (((((dst_first_append_preserved) = 2 * (ge_balance_positive_append_preservedfirstvalue) /\ (ge_balance_negative_append_preservedfirstvalue) = 0) \/ exists ge_signed_half_append_preservedfirstvaluedecode. (((dst_first_append_preserved) = 2 * ge_signed_half_append_preservedfirstvaluedecode + 1 /\ (ge_balance_positive_append_preservedfirstvalue) = 0) /\ (ge_balance_negative_append_preservedfirstvalue) = S ge_signed_half_append_preservedfirstvaluedecode))) /\ ((dst_positive_append_preservedfirst) + ge_balance_negative_append_preservedfirstvalue = (dst_negative_append_preservedfirst) + ge_balance_positive_append_preservedfirstvalue))))))))) -> (exists dst_positive_code_append_preservedsecond dst_positive_scale_append_preservedsecond dst_negative_code_append_preservedsecond dst_negative_scale_append_preservedsecond dst_positive_append_preservedsecond dst_negative_append_preservedsecond. (((G) = (((((dst_positive_code_append_preservedsecond) + (dst_positive_scale_append_preservedsecond)) * S ((dst_positive_code_append_preservedsecond) + (dst_positive_scale_append_preservedsecond)) + ((dst_positive_scale_append_preservedsecond) + (dst_positive_scale_append_preservedsecond))) + (((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) * S ((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) + ((dst_negative_scale_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)))) * S ((((dst_positive_code_append_preservedsecond) + (dst_positive_scale_append_preservedsecond)) * S ((dst_positive_code_append_preservedsecond) + (dst_positive_scale_append_preservedsecond)) + ((dst_positive_scale_append_preservedsecond) + (dst_positive_scale_append_preservedsecond))) + (((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) * S ((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) + ((dst_negative_scale_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)))) + ((((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) * S ((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) + ((dst_negative_scale_append_preservedsecond) + (dst_negative_scale_append_preservedsecond))) + (((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) * S ((dst_negative_code_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)) + ((dst_negative_scale_append_preservedsecond) + (dst_negative_scale_append_preservedsecond)))))) /\ (((((exists ff_h_pvs_append_preservedsecondpositive. ff_h_pvs_append_preservedsecondpositive + S (dst_positive_append_preservedsecond) = S ((S (dst_index_append_preserved)) * dst_positive_scale_append_preservedsecond)) /\ exists ff_q_pvs_append_preservedsecondpositive. dst_positive_code_append_preservedsecond = ff_q_pvs_append_preservedsecondpositive * S ((S (dst_index_append_preserved)) * dst_positive_scale_append_preservedsecond) + (dst_positive_append_preservedsecond))) /\ (((((exists ff_h_pvs_append_preservedsecondnegative. ff_h_pvs_append_preservedsecondnegative + S (dst_negative_append_preservedsecond) = S ((S (dst_index_append_preserved)) * dst_negative_scale_append_preservedsecond)) /\ exists ff_q_pvs_append_preservedsecondnegative. dst_negative_code_append_preservedsecond = ff_q_pvs_append_preservedsecondnegative * S ((S (dst_index_append_preserved)) * dst_negative_scale_append_preservedsecond) + (dst_negative_append_preservedsecond))) /\ (exists ge_balance_positive_append_preservedsecondvalue ge_balance_negative_append_preservedsecondvalue. (((((dst_second_append_preserved) = 2 * (ge_balance_positive_append_preservedsecondvalue) /\ (ge_balance_negative_append_preservedsecondvalue) = 0) \/ exists ge_signed_half_append_preservedsecondvaluedecode. (((dst_second_append_preserved) = 2 * ge_signed_half_append_preservedsecondvaluedecode + 1 /\ (ge_balance_positive_append_preservedsecondvalue) = 0) /\ (ge_balance_negative_append_preservedsecondvalue) = S ge_signed_half_append_preservedsecondvaluedecode))) /\ ((dst_positive_append_preservedsecond) + ge_balance_negative_append_preservedsecondvalue = (dst_negative_append_preservedsecond) + ge_balance_positive_append_preservedsecondvalue))))))))) -> dst_first_append_preserved = dst_second_append_preserved)