DV0009

mobius_table_append

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

An actual value of μ at the next positive index is appended by real beta recoding; every earlier signed value, including the zero convention, is preserved.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall N F 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)

Constructive proof overview

Generated structural guide

An actual value of μ at the next positive index is appended by real beta recoding; every earlier signed value, including the zero convention, is preserved.

The unchanged tactic script uses 8 declared prerequisites and contains 103 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

DV0004 arithmetic_signed_table_append DV0002 arithmetic_signed_table_equal_entry_transport zero_le Stable theorem; checked-use authorized succ_le_succ Stable theorem; checked-use authorized le_eq_or_lt Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized divisor_signed_table_at_functional Alpha theorem; checked-use authorized divisor_signed_table_lookup Alpha theorem; checked-use authorized

Direct dependents

DV000A mobius_table_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

103 script commands · 22 reading checkpoints · 6 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.

Named ingredients (2)
arithmetic signed table appendarithmetic signed table equal entry transport

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro z
  4. L4
    intro hmu
  5. L5
    intro hz
02Separate the logical casesL6–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases hmu
  2. L7
    cases hmu_right
03Establish hextL8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table append.

  1. L8
    have hext : ∃ G. ArithExtend(F,G,S N,z)Definitions: ArithExtend
  2. L9
    specialize arithmetic_signed_table_append (N)
  3. L10
    specialize arithmetic_signed_table_append (F)
  4. L11
    specialize arithmetic_signed_table_append (z)
  5. L12
    apply arithmetic_signed_table_append
  6. L13
    exact hmu_left
04Separate the logical casesL14–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hext
  2. L15
    cases hext_witness
  3. L16
    cases hext_witness_right
05Construct an explicit witnessL17–17

Supply the displayed value, then prove that it has the required property.

  1. L17
    exists x
06Separate the logical casesL18–19

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L18
    split
  2. L19
    split
07Use earlier factsL20–20

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    exact hext_witness_left
08Separate the logical casesL21–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    split
09Use earlier factsL22–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L22
    specialize arithmetic_signed_table_equal_entry_transport (S N)
  2. L23
    specialize arithmetic_signed_table_equal_entry_transport (F)
  3. L24
    specialize arithmetic_signed_table_equal_entry_transport (x)
  4. L25
    specialize arithmetic_signed_table_equal_entry_transport (S N)
  5. L26
    specialize arithmetic_signed_table_equal_entry_transport (0)
  6. L27
    specialize arithmetic_signed_table_equal_entry_transport (0)
  7. L28
    apply arithmetic_signed_table_equal_entry_transport
  8. L29
    exact hext_witness_left
  9. L30
    exact hext_witness_right_left
  10. L31
    specialize zero_le (S N)
10Use earlier factsL32–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    apply zero_le
  2. L33
    specialize succ_le_succ (0)
  3. L34
    specialize succ_le_succ (N)
  4. L35
    apply succ_le_succ
  5. L36
    specialize zero_le (N)
  6. L37
    apply zero_le
  7. L38
    exact hmu_right_left
11Fix variables and assumptionsL39–43

Work with arbitrary variables or the premises of the current implication.

  1. L39
    intro i
  2. L40
    intro y
  3. L41
    intro hi
  4. L42
    intro hib
  5. L43
    intro hv
12Establish hcaseL44–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L44
    have hcase : i = S N \/ (exists pvs_gap_append_cases. pvs_gap_append_cases + S (i) = (S N))
  2. L45
    specialize le_eq_or_lt (i)
  3. L46
    specialize le_eq_or_lt (S N)
  4. L47
    apply le_eq_or_lt
  5. L48
    exact hib
13Separate the logical casesL49–49

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L49
    cases hcase
14Calculate and transport equalitiesL50–53

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L50
    rewrite hcase_left at hv
  2. L51
    rewrite hcase_left at hv
  3. L52
    rewrite hcase_left at hv
  4. L53
    rewrite hcase_left at hv
15Establish heqL54–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L54
    have heq : z = y
  2. L55
    specialize divisor_signed_table_at_functional (x)
  3. L56
    specialize divisor_signed_table_at_functional (S N)
  4. L57
    specialize divisor_signed_table_at_functional (z)
  5. L58
    specialize divisor_signed_table_at_functional (y)
  6. L59
    apply divisor_signed_table_at_functional
  7. L60
    exact hext_witness_right_right
  8. L61
    exact hv
  9. L62
    rewrite heq at hz
  10. L63
    rewrite heq at hz
16Calculate and transport equalitiesL64–72

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L64
    rewrite heq at hz
  2. L65
    rewrite hcase_left
  3. L66
    rewrite hcase_left
  4. L67
    rewrite hcase_left
  5. L68
    rewrite hcase_left
  6. L69
    rewrite hcase_left
  7. L70
    rewrite hcase_left
  8. L71
    rewrite hcase_left
  9. L72
    rewrite hcase_left
17Use earlier factsL73–73

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L73
    exact hz
18Establish hboundL74–78

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L74
    have hbound : exists pvs_le_gap_append_old_bound. pvs_le_gap_append_old_bound + (i) = (N)
  2. L75
    specialize le_of_succ_le_succ (i)
  3. L76
    specialize le_of_succ_le_succ (N)
  4. L77
    apply le_of_succ_le_succ
  5. L78
    exact hcase_right
19Establish huL79–85

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.

  1. L79
    have hu : ∃ u. ArithAt(F,i,u)Definitions: ArithAt
  2. L80
    specialize divisor_signed_table_lookup (N)
  3. L81
    specialize divisor_signed_table_lookup (F)
  4. L82
    specialize divisor_signed_table_lookup (i)
  5. L83
    apply divisor_signed_table_lookup
  6. L84
    exact hmu_left
  7. L85
    exact hbound
20Separate the logical casesL86–86

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L86
    cases hu
21Establish heqL87–96

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hext witness right left.

  1. L87
    have heq : x1 = y
  2. L88
    specialize hext_witness_right_left (i)
  3. L89
    specialize hext_witness_right_left (x1)
  4. L90
    specialize hext_witness_right_left (y)
  5. L91
    apply hext_witness_right_left
  6. L92
    exact hcase_right
  7. L93
    exact hu_witness
  8. L94
    exact hv
  9. L95
    rewrite heq at hu_witness
  10. L96
    rewrite heq at hu_witness
22Use earlier factsL97–103

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L97
    specialize hmu_right_right (i)
  2. L98
    specialize hmu_right_right (y)
  3. L99
    apply hmu_right_right
  4. L100
    exact hi
  5. L101
    exact hbound
  6. L102
    exact hu_witness
  7. L103
    exact hext_witness_right_left

Library-wide reading audit

Original exact command ledger · 103 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro z
  4. 0004intro hmu
  5. 0005intro hz
  6. 0006cases hmu
  7. 0007cases hmu_right
  8. 0008have hext : exists G. (((exists dst_positive_code_append_realtable dst_positive_scale_append_realtable dst_negative_code_append_realtable dst_negative_scale_append_realtable. (((G) = (((((dst_positive_code_append_realtable) + (dst_positive_scale_append_realtable)) * S ((dst_positive_code_append_realtable) + (dst_positive_scale_append_realtable)) + ((dst_positive_scale_append_realtable) + (dst_positive_scale_append_realtable))) + (((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) * S ((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) + ((dst_negative_scale_append_realtable) + (dst_negative_scale_append_realtable)))) * S ((((dst_positive_code_append_realtable) + (dst_positive_scale_append_realtable)) * S ((dst_positive_code_append_realtable) + (dst_positive_scale_append_realtable)) + ((dst_positive_scale_append_realtable) + (dst_positive_scale_append_realtable))) + (((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) * S ((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) + ((dst_negative_scale_append_realtable) + (dst_negative_scale_append_realtable)))) + ((((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) * S ((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) + ((dst_negative_scale_append_realtable) + (dst_negative_scale_append_realtable))) + (((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) * S ((dst_negative_code_append_realtable) + (dst_negative_scale_append_realtable)) + ((dst_negative_scale_append_realtable) + (dst_negative_scale_append_realtable)))))) /\ (forall dst_index_append_realtable. (exists pvs_le_gap_append_realtabledomain. pvs_le_gap_append_realtabledomain + (dst_index_append_realtable) = (S N)) -> exists dst_positive_append_realtable dst_negative_append_realtable dst_value_append_realtable. ((((exists ff_h_pvs_append_realtableentrypositive. ff_h_pvs_append_realtableentrypositive + S (dst_positive_append_realtable) = S ((S (dst_index_append_realtable)) * dst_positive_scale_append_realtable)) /\ exists ff_q_pvs_append_realtableentrypositive. dst_positive_code_append_realtable = ff_q_pvs_append_realtableentrypositive * S ((S (dst_index_append_realtable)) * dst_positive_scale_append_realtable) + (dst_positive_append_realtable))) /\ (((((exists ff_h_pvs_append_realtableentrynegative. ff_h_pvs_append_realtableentrynegative + S (dst_negative_append_realtable) = S ((S (dst_index_append_realtable)) * dst_negative_scale_append_realtable)) /\ exists ff_q_pvs_append_realtableentrynegative. dst_negative_code_append_realtable = ff_q_pvs_append_realtableentrynegative * S ((S (dst_index_append_realtable)) * dst_negative_scale_append_realtable) + (dst_negative_append_realtable))) /\ (exists ge_balance_positive_append_realtableentryvalue ge_balance_negative_append_realtableentryvalue. (((((dst_value_append_realtable) = 2 * (ge_balance_positive_append_realtableentryvalue) /\ (ge_balance_negative_append_realtableentryvalue) = 0) \/ exists ge_signed_half_append_realtableentryvaluedecode. (((dst_value_append_realtable) = 2 * ge_signed_half_append_realtableentryvaluedecode + 1 /\ (ge_balance_positive_append_realtableentryvalue) = 0) /\ (ge_balance_negative_append_realtableentryvalue) = S ge_signed_half_append_realtableentryvaluedecode))) /\ ((dst_positive_append_realtable) + ge_balance_negative_append_realtableentryvalue = (dst_negative_append_realtable) + ge_balance_positive_append_realtableentryvalue))))))))) /\ (((forall dst_index_append_realprefix dst_first_append_realprefix dst_second_append_realprefix. (exists pvs_gap_append_realprefixbound. pvs_gap_append_realprefixbound + S (dst_index_append_realprefix) = (S N)) -> (exists dst_positive_code_append_realprefixfirst dst_positive_scale_append_realprefixfirst dst_negative_code_append_realprefixfirst dst_negative_scale_append_realprefixfirst dst_positive_append_realprefixfirst dst_negative_append_realprefixfirst. (((F) = (((((dst_positive_code_append_realprefixfirst) + (dst_positive_scale_append_realprefixfirst)) * S ((dst_positive_code_append_realprefixfirst) + (dst_positive_scale_append_realprefixfirst)) + ((dst_positive_scale_append_realprefixfirst) + (dst_positive_scale_append_realprefixfirst))) + (((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) * S ((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) + ((dst_negative_scale_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)))) * S ((((dst_positive_code_append_realprefixfirst) + (dst_positive_scale_append_realprefixfirst)) * S ((dst_positive_code_append_realprefixfirst) + (dst_positive_scale_append_realprefixfirst)) + ((dst_positive_scale_append_realprefixfirst) + (dst_positive_scale_append_realprefixfirst))) + (((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) * S ((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) + ((dst_negative_scale_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)))) + ((((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) * S ((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) + ((dst_negative_scale_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst))) + (((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) * S ((dst_negative_code_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)) + ((dst_negative_scale_append_realprefixfirst) + (dst_negative_scale_append_realprefixfirst)))))) /\ (((((exists ff_h_pvs_append_realprefixfirstpositive. ff_h_pvs_append_realprefixfirstpositive + S (dst_positive_append_realprefixfirst) = S ((S (dst_index_append_realprefix)) * dst_positive_scale_append_realprefixfirst)) /\ exists ff_q_pvs_append_realprefixfirstpositive. dst_positive_code_append_realprefixfirst = ff_q_pvs_append_realprefixfirstpositive * S ((S (dst_index_append_realprefix)) * dst_positive_scale_append_realprefixfirst) + (dst_positive_append_realprefixfirst))) /\ (((((exists ff_h_pvs_append_realprefixfirstnegative. ff_h_pvs_append_realprefixfirstnegative + S (dst_negative_append_realprefixfirst) = S ((S (dst_index_append_realprefix)) * dst_negative_scale_append_realprefixfirst)) /\ exists ff_q_pvs_append_realprefixfirstnegative. dst_negative_code_append_realprefixfirst = ff_q_pvs_append_realprefixfirstnegative * S ((S (dst_index_append_realprefix)) * dst_negative_scale_append_realprefixfirst) + (dst_negative_append_realprefixfirst))) /\ (exists ge_balance_positive_append_realprefixfirstvalue ge_balance_negative_append_realprefixfirstvalue. (((((dst_first_append_realprefix) = 2 * (ge_balance_positive_append_realprefixfirstvalue) /\ (ge_balance_negative_append_realprefixfirstvalue) = 0) \/ exists ge_signed_half_append_realprefixfirstvaluedecode. (((dst_first_append_realprefix) = 2 * ge_signed_half_append_realprefixfirstvaluedecode + 1 /\ (ge_balance_positive_append_realprefixfirstvalue) = 0) /\ (ge_balance_negative_append_realprefixfirstvalue) = S ge_signed_half_append_realprefixfirstvaluedecode))) /\ ((dst_positive_append_realprefixfirst) + ge_balance_negative_append_realprefixfirstvalue = (dst_negative_append_realprefixfirst) + ge_balance_positive_append_realprefixfirstvalue))))))))) -> (exists dst_positive_code_append_realprefixsecond dst_positive_scale_append_realprefixsecond dst_negative_code_append_realprefixsecond dst_negative_scale_append_realprefixsecond dst_positive_append_realprefixsecond dst_negative_append_realprefixsecond. (((G) = (((((dst_positive_code_append_realprefixsecond) + (dst_positive_scale_append_realprefixsecond)) * S ((dst_positive_code_append_realprefixsecond) + (dst_positive_scale_append_realprefixsecond)) + ((dst_positive_scale_append_realprefixsecond) + (dst_positive_scale_append_realprefixsecond))) + (((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) * S ((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) + ((dst_negative_scale_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)))) * S ((((dst_positive_code_append_realprefixsecond) + (dst_positive_scale_append_realprefixsecond)) * S ((dst_positive_code_append_realprefixsecond) + (dst_positive_scale_append_realprefixsecond)) + ((dst_positive_scale_append_realprefixsecond) + (dst_positive_scale_append_realprefixsecond))) + (((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) * S ((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) + ((dst_negative_scale_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)))) + ((((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) * S ((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) + ((dst_negative_scale_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond))) + (((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) * S ((dst_negative_code_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)) + ((dst_negative_scale_append_realprefixsecond) + (dst_negative_scale_append_realprefixsecond)))))) /\ (((((exists ff_h_pvs_append_realprefixsecondpositive. ff_h_pvs_append_realprefixsecondpositive + S (dst_positive_append_realprefixsecond) = S ((S (dst_index_append_realprefix)) * dst_positive_scale_append_realprefixsecond)) /\ exists ff_q_pvs_append_realprefixsecondpositive. dst_positive_code_append_realprefixsecond = ff_q_pvs_append_realprefixsecondpositive * S ((S (dst_index_append_realprefix)) * dst_positive_scale_append_realprefixsecond) + (dst_positive_append_realprefixsecond))) /\ (((((exists ff_h_pvs_append_realprefixsecondnegative. ff_h_pvs_append_realprefixsecondnegative + S (dst_negative_append_realprefixsecond) = S ((S (dst_index_append_realprefix)) * dst_negative_scale_append_realprefixsecond)) /\ exists ff_q_pvs_append_realprefixsecondnegative. dst_negative_code_append_realprefixsecond = ff_q_pvs_append_realprefixsecondnegative * S ((S (dst_index_append_realprefix)) * dst_negative_scale_append_realprefixsecond) + (dst_negative_append_realprefixsecond))) /\ (exists ge_balance_positive_append_realprefixsecondvalue ge_balance_negative_append_realprefixsecondvalue. (((((dst_second_append_realprefix) = 2 * (ge_balance_positive_append_realprefixsecondvalue) /\ (ge_balance_negative_append_realprefixsecondvalue) = 0) \/ exists ge_signed_half_append_realprefixsecondvaluedecode. (((dst_second_append_realprefix) = 2 * ge_signed_half_append_realprefixsecondvaluedecode + 1 /\ (ge_balance_positive_append_realprefixsecondvalue) = 0) /\ (ge_balance_negative_append_realprefixsecondvalue) = S ge_signed_half_append_realprefixsecondvaluedecode))) /\ ((dst_positive_append_realprefixsecond) + ge_balance_negative_append_realprefixsecondvalue = (dst_negative_append_realprefixsecond) + ge_balance_positive_append_realprefixsecondvalue))))))))) -> dst_first_append_realprefix = dst_second_append_realprefix) /\ (exists dst_positive_code_append_reallast dst_positive_scale_append_reallast dst_negative_code_append_reallast dst_negative_scale_append_reallast dst_positive_append_reallast dst_negative_append_reallast. (((G) = (((((dst_positive_code_append_reallast) + (dst_positive_scale_append_reallast)) * S ((dst_positive_code_append_reallast) + (dst_positive_scale_append_reallast)) + ((dst_positive_scale_append_reallast) + (dst_positive_scale_append_reallast))) + (((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) * S ((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) + ((dst_negative_scale_append_reallast) + (dst_negative_scale_append_reallast)))) * S ((((dst_positive_code_append_reallast) + (dst_positive_scale_append_reallast)) * S ((dst_positive_code_append_reallast) + (dst_positive_scale_append_reallast)) + ((dst_positive_scale_append_reallast) + (dst_positive_scale_append_reallast))) + (((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) * S ((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) + ((dst_negative_scale_append_reallast) + (dst_negative_scale_append_reallast)))) + ((((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) * S ((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) + ((dst_negative_scale_append_reallast) + (dst_negative_scale_append_reallast))) + (((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) * S ((dst_negative_code_append_reallast) + (dst_negative_scale_append_reallast)) + ((dst_negative_scale_append_reallast) + (dst_negative_scale_append_reallast)))))) /\ (((((exists ff_h_pvs_append_reallastpositive. ff_h_pvs_append_reallastpositive + S (dst_positive_append_reallast) = S ((S (S N)) * dst_positive_scale_append_reallast)) /\ exists ff_q_pvs_append_reallastpositive. dst_positive_code_append_reallast = ff_q_pvs_append_reallastpositive * S ((S (S N)) * dst_positive_scale_append_reallast) + (dst_positive_append_reallast))) /\ (((((exists ff_h_pvs_append_reallastnegative. ff_h_pvs_append_reallastnegative + S (dst_negative_append_reallast) = S ((S (S N)) * dst_negative_scale_append_reallast)) /\ exists ff_q_pvs_append_reallastnegative. dst_negative_code_append_reallast = ff_q_pvs_append_reallastnegative * S ((S (S N)) * dst_negative_scale_append_reallast) + (dst_negative_append_reallast))) /\ (exists ge_balance_positive_append_reallastvalue ge_balance_negative_append_reallastvalue. (((((z) = 2 * (ge_balance_positive_append_reallastvalue) /\ (ge_balance_negative_append_reallastvalue) = 0) \/ exists ge_signed_half_append_reallastvaluedecode. (((z) = 2 * ge_signed_half_append_reallastvaluedecode + 1 /\ (ge_balance_positive_append_reallastvalue) = 0) /\ (ge_balance_negative_append_reallastvalue) = S ge_signed_half_append_reallastvaluedecode))) /\ ((dst_positive_append_reallast) + ge_balance_negative_append_reallastvalue = (dst_negative_append_reallast) + ge_balance_positive_append_reallastvalue)))))))))))))
  9. 0009specialize arithmetic_signed_table_append (N)
  10. 0010specialize arithmetic_signed_table_append (F)
  11. 0011specialize arithmetic_signed_table_append (z)
  12. 0012apply arithmetic_signed_table_append
  13. 0013exact hmu_left
  14. 0014cases hext
  15. 0015cases hext_witness
  16. 0016cases hext_witness_right
  17. 0017exists x
  18. 0018split
  19. 0019split
  20. 0020exact hext_witness_left
  21. 0021split
  22. 0022specialize arithmetic_signed_table_equal_entry_transport (S N)
  23. 0023specialize arithmetic_signed_table_equal_entry_transport (F)
  24. 0024specialize arithmetic_signed_table_equal_entry_transport (x)
  25. 0025specialize arithmetic_signed_table_equal_entry_transport (S N)
  26. 0026specialize arithmetic_signed_table_equal_entry_transport (0)
  27. 0027specialize arithmetic_signed_table_equal_entry_transport (0)
  28. 0028apply arithmetic_signed_table_equal_entry_transport
  29. 0029exact hext_witness_left
  30. 0030exact hext_witness_right_left
  31. 0031specialize zero_le (S N)
  32. 0032apply zero_le
  33. 0033specialize succ_le_succ (0)
  34. 0034specialize succ_le_succ (N)
  35. 0035apply succ_le_succ
  36. 0036specialize zero_le (N)
  37. 0037apply zero_le
  38. 0038exact hmu_right_left
  39. 0039intro i
  40. 0040intro y
  41. 0041intro hi
  42. 0042intro hib
  43. 0043intro hv
  44. 0044have hcase : i = S N \/ (exists pvs_gap_append_cases. pvs_gap_append_cases + S (i) = (S N))
  45. 0045specialize le_eq_or_lt (i)
  46. 0046specialize le_eq_or_lt (S N)
  47. 0047apply le_eq_or_lt
  48. 0048exact hib
  49. 0049cases hcase
  50. 0050rewrite hcase_left at hv
  51. 0051rewrite hcase_left at hv
  52. 0052rewrite hcase_left at hv
  53. 0053rewrite hcase_left at hv
  54. 0054have heq : z = y
  55. 0055specialize divisor_signed_table_at_functional (x)
  56. 0056specialize divisor_signed_table_at_functional (S N)
  57. 0057specialize divisor_signed_table_at_functional (z)
  58. 0058specialize divisor_signed_table_at_functional (y)
  59. 0059apply divisor_signed_table_at_functional
  60. 0060exact hext_witness_right_right
  61. 0061exact hv
  62. 0062rewrite heq at hz
  63. 0063rewrite heq at hz
  64. 0064rewrite heq at hz
  65. 0065rewrite hcase_left
  66. 0066rewrite hcase_left
  67. 0067rewrite hcase_left
  68. 0068rewrite hcase_left
  69. 0069rewrite hcase_left
  70. 0070rewrite hcase_left
  71. 0071rewrite hcase_left
  72. 0072rewrite hcase_left
  73. 0073exact hz
  74. 0074have hbound : exists pvs_le_gap_append_old_bound. pvs_le_gap_append_old_bound + (i) = (N)
  75. 0075specialize le_of_succ_le_succ (i)
  76. 0076specialize le_of_succ_le_succ (N)
  77. 0077apply le_of_succ_le_succ
  78. 0078exact hcase_right
  79. 0079have hu : exists u. (exists dst_positive_code_append_old_lookup dst_positive_scale_append_old_lookup dst_negative_code_append_old_lookup dst_negative_scale_append_old_lookup dst_positive_append_old_lookup dst_negative_append_old_lookup. (((F) = (((((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) * S ((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) + ((dst_positive_scale_append_old_lookup) + (dst_positive_scale_append_old_lookup))) + (((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup)))) * S ((((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) * S ((dst_positive_code_append_old_lookup) + (dst_positive_scale_append_old_lookup)) + ((dst_positive_scale_append_old_lookup) + (dst_positive_scale_append_old_lookup))) + (((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup)))) + ((((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup))) + (((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) * S ((dst_negative_code_append_old_lookup) + (dst_negative_scale_append_old_lookup)) + ((dst_negative_scale_append_old_lookup) + (dst_negative_scale_append_old_lookup)))))) /\ (((((exists ff_h_pvs_append_old_lookuppositive. ff_h_pvs_append_old_lookuppositive + S (dst_positive_append_old_lookup) = S ((S (i)) * dst_positive_scale_append_old_lookup)) /\ exists ff_q_pvs_append_old_lookuppositive. dst_positive_code_append_old_lookup = ff_q_pvs_append_old_lookuppositive * S ((S (i)) * dst_positive_scale_append_old_lookup) + (dst_positive_append_old_lookup))) /\ (((((exists ff_h_pvs_append_old_lookupnegative. ff_h_pvs_append_old_lookupnegative + S (dst_negative_append_old_lookup) = S ((S (i)) * dst_negative_scale_append_old_lookup)) /\ exists ff_q_pvs_append_old_lookupnegative. dst_negative_code_append_old_lookup = ff_q_pvs_append_old_lookupnegative * S ((S (i)) * dst_negative_scale_append_old_lookup) + (dst_negative_append_old_lookup))) /\ (exists ge_balance_positive_append_old_lookupvalue ge_balance_negative_append_old_lookupvalue. (((((u) = 2 * (ge_balance_positive_append_old_lookupvalue) /\ (ge_balance_negative_append_old_lookupvalue) = 0) \/ exists ge_signed_half_append_old_lookupvaluedecode. (((u) = 2 * ge_signed_half_append_old_lookupvaluedecode + 1 /\ (ge_balance_positive_append_old_lookupvalue) = 0) /\ (ge_balance_negative_append_old_lookupvalue) = S ge_signed_half_append_old_lookupvaluedecode))) /\ ((dst_positive_append_old_lookup) + ge_balance_negative_append_old_lookupvalue = (dst_negative_append_old_lookup) + ge_balance_positive_append_old_lookupvalue)))))))))
  80. 0080specialize divisor_signed_table_lookup (N)
  81. 0081specialize divisor_signed_table_lookup (F)
  82. 0082specialize divisor_signed_table_lookup (i)
  83. 0083apply divisor_signed_table_lookup
  84. 0084exact hmu_left
  85. 0085exact hbound
  86. 0086cases hu
  87. 0087have heq : x1 = y
  88. 0088specialize hext_witness_right_left (i)
  89. 0089specialize hext_witness_right_left (x1)
  90. 0090specialize hext_witness_right_left (y)
  91. 0091apply hext_witness_right_left
  92. 0092exact hcase_right
  93. 0093exact hu_witness
  94. 0094exact hv
  95. 0095rewrite heq at hu_witness
  96. 0096rewrite heq at hu_witness
  97. 0097specialize hmu_right_right (i)
  98. 0098specialize hmu_right_right (y)
  99. 0099apply hmu_right_right
  100. 0100exact hi
  101. 0101exact hbound
  102. 0102exact hu_witness
  103. 0103exact hext_witness_right_left