MC0016

mobius_divisor_mask_prime_factor_sum_zero

A genuinely constructed prime-toggle permutation makes the actual zero-masked Möbius sum anti-invariant, hence zero; no cancellation formula is an input.

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

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

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ N. ∀ M. ∀ n. ∀ K. ∀ p. ∀ z. MobiusTable(N,M) → ¬n = 0 → Le(n,N) → Prime(p) → Dvd(p,n) → DivisorMask(M,n,n,K) → SignedPrefixSum(K,S n,z) → z = 0

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedNegate(a,b) · 1PermutationPrefix(b,c,l) · 1ArithTable(N,F) · 1ArithAt(F,i,z) · 1SignedPrefixSum(F,l,z) · 2ArithReindex(F,G,r,s,l) · 1MobiusTable(N,M) · 1DivisorMask(F,n,l,M) · 1DivisorPrimeToggle(n,p,d,e) · 1DivisorPrimeTogglePrefix(n,p,b,c,l) · 1ArithNegate(F,G,l) · 1Le(a,b) · 2Dvd(d,n) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

divisor_prime_toggle_permutation_existsdivisor_signed_table_reindex_exists · checked external prerequisitearithmetic_signed_sum_exists · checked external prerequisitedivisor_prime_toggle_boundedle_of_succ_le_succ · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisitemobius_divisor_mask_prime_toggle_negatesanti_invariant_signed_permutation_sum_zero
Original expanded first-order statement 
forall N M n K p z. (((exists dst_positive_code_cancel_mask_mutable dst_positive_scale_cancel_mask_mutable dst_negative_code_cancel_mask_mutable dst_negative_scale_cancel_mask_mutable. (((M) = (((((dst_positive_code_cancel_mask_mutable) + (dst_positive_scale_cancel_mask_mutable)) * S ((dst_positive_code_cancel_mask_mutable) + (dst_positive_scale_cancel_mask_mutable)) + ((dst_positive_scale_cancel_mask_mutable) + (dst_positive_scale_cancel_mask_mutable))) + (((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) * S ((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) + ((dst_negative_scale_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)))) * S ((((dst_positive_code_cancel_mask_mutable) + (dst_positive_scale_cancel_mask_mutable)) * S ((dst_positive_code_cancel_mask_mutable) + (dst_positive_scale_cancel_mask_mutable)) + ((dst_positive_scale_cancel_mask_mutable) + (dst_positive_scale_cancel_mask_mutable))) + (((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) * S ((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) + ((dst_negative_scale_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)))) + ((((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) * S ((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) + ((dst_negative_scale_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable))) + (((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) * S ((dst_negative_code_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)) + ((dst_negative_scale_cancel_mask_mutable) + (dst_negative_scale_cancel_mask_mutable)))))) /\ (forall dst_index_cancel_mask_mutable. (exists pvs_le_gap_cancel_mask_mutabledomain. pvs_le_gap_cancel_mask_mutabledomain + (dst_index_cancel_mask_mutable) = (N)) -> exists dst_positive_cancel_mask_mutable dst_negative_cancel_mask_mutable dst_value_cancel_mask_mutable. ((((exists ff_h_pvs_cancel_mask_mutableentrypositive. ff_h_pvs_cancel_mask_mutableentrypositive + S (dst_positive_cancel_mask_mutable) = S ((S (dst_index_cancel_mask_mutable)) * dst_positive_scale_cancel_mask_mutable)) /\ exists ff_q_pvs_cancel_mask_mutableentrypositive. dst_positive_code_cancel_mask_mutable = ff_q_pvs_cancel_mask_mutableentrypositive * S ((S (dst_index_cancel_mask_mutable)) * dst_positive_scale_cancel_mask_mutable) + (dst_positive_cancel_mask_mutable))) /\ (((((exists ff_h_pvs_cancel_mask_mutableentrynegative. ff_h_pvs_cancel_mask_mutableentrynegative + S (dst_negative_cancel_mask_mutable) = S ((S (dst_index_cancel_mask_mutable)) * dst_negative_scale_cancel_mask_mutable)) /\ exists ff_q_pvs_cancel_mask_mutableentrynegative. dst_negative_code_cancel_mask_mutable = ff_q_pvs_cancel_mask_mutableentrynegative * S ((S (dst_index_cancel_mask_mutable)) * dst_negative_scale_cancel_mask_mutable) + (dst_negative_cancel_mask_mutable))) /\ (exists ge_balance_positive_cancel_mask_mutableentryvalue ge_balance_negative_cancel_mask_mutableentryvalue. (((((dst_value_cancel_mask_mutable) = 2 * (ge_balance_positive_cancel_mask_mutableentryvalue) /\ (ge_balance_negative_cancel_mask_mutableentryvalue) = 0) \/ exists ge_signed_half_cancel_mask_mutableentryvaluedecode. (((dst_value_cancel_mask_mutable) = 2 * ge_signed_half_cancel_mask_mutableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_mask_mutableentryvalue) = 0) /\ (ge_balance_negative_cancel_mask_mutableentryvalue) = S ge_signed_half_cancel_mask_mutableentryvaluedecode))) /\ ((dst_positive_cancel_mask_mutable) + ge_balance_negative_cancel_mask_mutableentryvalue = (dst_negative_cancel_mask_mutable) + ge_balance_positive_cancel_mask_mutableentryvalue))))))))) /\ (((exists dst_positive_code_cancel_mask_muzero dst_positive_scale_cancel_mask_muzero dst_negative_code_cancel_mask_muzero dst_negative_scale_cancel_mask_muzero dst_positive_cancel_mask_muzero dst_negative_cancel_mask_muzero. (((M) = (((((dst_positive_code_cancel_mask_muzero) + (dst_positive_scale_cancel_mask_muzero)) * S ((dst_positive_code_cancel_mask_muzero) + (dst_positive_scale_cancel_mask_muzero)) + ((dst_positive_scale_cancel_mask_muzero) + (dst_positive_scale_cancel_mask_muzero))) + (((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) * S ((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) + ((dst_negative_scale_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)))) * S ((((dst_positive_code_cancel_mask_muzero) + (dst_positive_scale_cancel_mask_muzero)) * S ((dst_positive_code_cancel_mask_muzero) + (dst_positive_scale_cancel_mask_muzero)) + ((dst_positive_scale_cancel_mask_muzero) + (dst_positive_scale_cancel_mask_muzero))) + (((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) * S ((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) + ((dst_negative_scale_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)))) + ((((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) * S ((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) + ((dst_negative_scale_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero))) + (((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) * S ((dst_negative_code_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)) + ((dst_negative_scale_cancel_mask_muzero) + (dst_negative_scale_cancel_mask_muzero)))))) /\ (((((exists ff_h_pvs_cancel_mask_muzeropositive. ff_h_pvs_cancel_mask_muzeropositive + S (dst_positive_cancel_mask_muzero) = S ((S (0)) * dst_positive_scale_cancel_mask_muzero)) /\ exists ff_q_pvs_cancel_mask_muzeropositive. dst_positive_code_cancel_mask_muzero = ff_q_pvs_cancel_mask_muzeropositive * S ((S (0)) * dst_positive_scale_cancel_mask_muzero) + (dst_positive_cancel_mask_muzero))) /\ (((((exists ff_h_pvs_cancel_mask_muzeronegative. ff_h_pvs_cancel_mask_muzeronegative + S (dst_negative_cancel_mask_muzero) = S ((S (0)) * dst_negative_scale_cancel_mask_muzero)) /\ exists ff_q_pvs_cancel_mask_muzeronegative. dst_negative_code_cancel_mask_muzero = ff_q_pvs_cancel_mask_muzeronegative * S ((S (0)) * dst_negative_scale_cancel_mask_muzero) + (dst_negative_cancel_mask_muzero))) /\ (exists ge_balance_positive_cancel_mask_muzerovalue ge_balance_negative_cancel_mask_muzerovalue. (((((0) = 2 * (ge_balance_positive_cancel_mask_muzerovalue) /\ (ge_balance_negative_cancel_mask_muzerovalue) = 0) \/ exists ge_signed_half_cancel_mask_muzerovaluedecode. (((0) = 2 * ge_signed_half_cancel_mask_muzerovaluedecode + 1 /\ (ge_balance_positive_cancel_mask_muzerovalue) = 0) /\ (ge_balance_negative_cancel_mask_muzerovalue) = S ge_signed_half_cancel_mask_muzerovaluedecode))) /\ ((dst_positive_cancel_mask_muzero) + ge_balance_negative_cancel_mask_muzerovalue = (dst_negative_cancel_mask_muzero) + ge_balance_positive_cancel_mask_muzerovalue))))))))) /\ (forall mt_index_cancel_mask_mu mt_value_cancel_mask_mu. ~(mt_index_cancel_mask_mu=0) -> (exists pvs_le_gap_cancel_mask_mudomain. pvs_le_gap_cancel_mask_mudomain + (mt_index_cancel_mask_mu) = (N)) -> (exists dst_positive_code_cancel_mask_muentry dst_positive_scale_cancel_mask_muentry dst_negative_code_cancel_mask_muentry dst_negative_scale_cancel_mask_muentry dst_positive_cancel_mask_muentry dst_negative_cancel_mask_muentry. (((M) = (((((dst_positive_code_cancel_mask_muentry) + (dst_positive_scale_cancel_mask_muentry)) * S ((dst_positive_code_cancel_mask_muentry) + (dst_positive_scale_cancel_mask_muentry)) + ((dst_positive_scale_cancel_mask_muentry) + (dst_positive_scale_cancel_mask_muentry))) + (((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) * S ((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) + ((dst_negative_scale_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)))) * S ((((dst_positive_code_cancel_mask_muentry) + (dst_positive_scale_cancel_mask_muentry)) * S ((dst_positive_code_cancel_mask_muentry) + (dst_positive_scale_cancel_mask_muentry)) + ((dst_positive_scale_cancel_mask_muentry) + (dst_positive_scale_cancel_mask_muentry))) + (((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) * S ((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) + ((dst_negative_scale_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)))) + ((((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) * S ((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) + ((dst_negative_scale_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry))) + (((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) * S ((dst_negative_code_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)) + ((dst_negative_scale_cancel_mask_muentry) + (dst_negative_scale_cancel_mask_muentry)))))) /\ (((((exists ff_h_pvs_cancel_mask_muentrypositive. ff_h_pvs_cancel_mask_muentrypositive + S (dst_positive_cancel_mask_muentry) = S ((S (mt_index_cancel_mask_mu)) * dst_positive_scale_cancel_mask_muentry)) /\ exists ff_q_pvs_cancel_mask_muentrypositive. dst_positive_code_cancel_mask_muentry = ff_q_pvs_cancel_mask_muentrypositive * S ((S (mt_index_cancel_mask_mu)) * dst_positive_scale_cancel_mask_muentry) + (dst_positive_cancel_mask_muentry))) /\ (((((exists ff_h_pvs_cancel_mask_muentrynegative. ff_h_pvs_cancel_mask_muentrynegative + S (dst_negative_cancel_mask_muentry) = S ((S (mt_index_cancel_mask_mu)) * dst_negative_scale_cancel_mask_muentry)) /\ exists ff_q_pvs_cancel_mask_muentrynegative. dst_negative_code_cancel_mask_muentry = ff_q_pvs_cancel_mask_muentrynegative * S ((S (mt_index_cancel_mask_mu)) * dst_negative_scale_cancel_mask_muentry) + (dst_negative_cancel_mask_muentry))) /\ (exists ge_balance_positive_cancel_mask_muentryvalue ge_balance_negative_cancel_mask_muentryvalue. (((((mt_value_cancel_mask_mu) = 2 * (ge_balance_positive_cancel_mask_muentryvalue) /\ (ge_balance_negative_cancel_mask_muentryvalue) = 0) \/ exists ge_signed_half_cancel_mask_muentryvaluedecode. (((mt_value_cancel_mask_mu) = 2 * ge_signed_half_cancel_mask_muentryvaluedecode + 1 /\ (ge_balance_positive_cancel_mask_muentryvalue) = 0) /\ (ge_balance_negative_cancel_mask_muentryvalue) = S ge_signed_half_cancel_mask_muentryvaluedecode))) /\ ((dst_positive_cancel_mask_muentry) + ge_balance_negative_cancel_mask_muentryvalue = (dst_negative_cancel_mask_muentry) + ge_balance_positive_cancel_mask_muentryvalue))))))))) -> (((~((mt_index_cancel_mask_mu) = 0)) /\ ((((exists mv_square_prime_cancel_mask_muvaluesquare. ((~((mv_square_prime_cancel_mask_muvaluesquare) = 1) /\ forall pvs_left_cancel_mask_muvaluesquareprime pvs_right_cancel_mask_muvaluesquareprime. (mv_square_prime_cancel_mask_muvaluesquare) = pvs_left_cancel_mask_muvaluesquareprime * pvs_right_cancel_mask_muvaluesquareprime -> pvs_left_cancel_mask_muvaluesquareprime = 1 \/ pvs_right_cancel_mask_muvaluesquareprime = 1) /\ (exists pvs_factor_cancel_mask_muvaluesquaredivisor. (mt_index_cancel_mask_mu) = (mv_square_prime_cancel_mask_muvaluesquare * mv_square_prime_cancel_mask_muvaluesquare) * pvs_factor_cancel_mask_muvaluesquaredivisor))) /\ ((mt_value_cancel_mask_mu) = 0))) \/ (((((~((mt_index_cancel_mask_mu) = 0)) /\ (forall sfd_prime_cancel_mask_muvaluesquarefree. (~((sfd_prime_cancel_mask_muvaluesquarefree) = 1) /\ forall pvs_left_cancel_mask_muvaluesquarefreedomain pvs_right_cancel_mask_muvaluesquarefreedomain. (sfd_prime_cancel_mask_muvaluesquarefree) = pvs_left_cancel_mask_muvaluesquarefreedomain * pvs_right_cancel_mask_muvaluesquarefreedomain -> pvs_left_cancel_mask_muvaluesquarefreedomain = 1 \/ pvs_right_cancel_mask_muvaluesquarefreedomain = 1) -> (exists pvs_le_gap_cancel_mask_muvaluesquarefreebound. pvs_le_gap_cancel_mask_muvaluesquarefreebound + (sfd_prime_cancel_mask_muvaluesquarefree) = (mt_index_cancel_mask_mu)) -> ~(exists pvs_factor_cancel_mask_muvaluesquarefreesquare. (mt_index_cancel_mask_mu) = (sfd_prime_cancel_mask_muvaluesquarefree * sfd_prime_cancel_mask_muvaluesquarefree) * pvs_factor_cancel_mask_muvaluesquarefreesquare)))) /\ (exists mv_factor_code_cancel_mask_muvaluefactors mv_factor_scale_cancel_mask_muvaluefactors mv_factor_count_cancel_mask_muvaluefactors. (((~(mt_index_cancel_mask_mu = 0) /\ ((exists ff_u_fsat_cancel_mask_muvaluefactorsfactorization_product ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_start. ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_start. ff_u_fsat_cancel_mask_muvaluefactorsfactorization_product = ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_terminal. ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_terminal + S (mt_index_cancel_mask_mu) = S ((S (mv_factor_count_cancel_mask_muvaluefactors)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_terminal. ff_u_fsat_cancel_mask_muvaluefactorsfactorization_product = ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_cancel_mask_muvaluefactors)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product) + (mt_index_cancel_mask_mu))) /\ forall ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product. (exists ff_lt_fsat_cancel_mask_muvaluefactorsfactorization_product_bound. ff_lt_fsat_cancel_mask_muvaluefactorsfactorization_product_bound + S ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product = mv_factor_count_cancel_mask_muvaluefactors) -> exists ff_p_fsat_cancel_mask_muvaluefactorsfactorization_product ff_r_fsat_cancel_mask_muvaluefactorsfactorization_product ff_s_fsat_cancel_mask_muvaluefactorsfactorization_product. ((((exists ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_factor. ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_factor + S (ff_p_fsat_cancel_mask_muvaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product)) * mv_factor_scale_cancel_mask_muvaluefactors)) /\ exists ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_factor. mv_factor_code_cancel_mask_muvaluefactors = ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product)) * mv_factor_scale_cancel_mask_muvaluefactors) + (ff_p_fsat_cancel_mask_muvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_partial. ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_partial + S (ff_r_fsat_cancel_mask_muvaluefactorsfactorization_product) = S ((S (ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_partial. ff_u_fsat_cancel_mask_muvaluefactorsfactorization_product = ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product) + (ff_r_fsat_cancel_mask_muvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_successor. ff_h_fsat_cancel_mask_muvaluefactorsfactorization_product_successor + S (ff_s_fsat_cancel_mask_muvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_successor. ff_u_fsat_cancel_mask_muvaluefactorsfactorization_product = ff_q_fsat_cancel_mask_muvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_cancel_mask_muvaluefactorsfactorization_product)) * ff_v_fsat_cancel_mask_muvaluefactorsfactorization_product) + (ff_s_fsat_cancel_mask_muvaluefactorsfactorization_product))) /\ ff_s_fsat_cancel_mask_muvaluefactorsfactorization_product = ff_r_fsat_cancel_mask_muvaluefactorsfactorization_product * ff_p_fsat_cancel_mask_muvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_cancel_mask_muvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_cancel_mask_muvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_cancel_mask_muvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_cancel_mask_muvaluefactorsfactorization_primes = (mv_factor_count_cancel_mask_muvaluefactors)) -> exists ftsf_factor_fsat_cancel_mask_muvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_cancel_mask_muvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_cancel_mask_muvaluefactorsfactorization_primes)) * mv_factor_scale_cancel_mask_muvaluefactors)) /\ exists ff_q_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_entry. mv_factor_code_cancel_mask_muvaluefactors = ff_q_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_cancel_mask_muvaluefactorsfactorization_primes)) * mv_factor_scale_cancel_mask_muvaluefactors) + (ftsf_factor_fsat_cancel_mask_muvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_cancel_mask_muvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_cancel_mask_muvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_cancel_mask_muvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_cancel_mask_muvaluefactorsparityeven. (mv_factor_count_cancel_mask_muvaluefactors) = 2 * mv_even_half_cancel_mask_muvaluefactorsparityeven) /\ ((mt_value_cancel_mask_mu) = 2))) \/ (((exists mv_odd_half_cancel_mask_muvaluefactorsparityodd. (mv_factor_count_cancel_mask_muvaluefactors) = 2 * mv_odd_half_cancel_mask_muvaluefactorsparityodd + 1) /\ ((mt_value_cancel_mask_mu) = 1)))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_cancel_mask_N. pvs_le_gap_cancel_mask_N + (n) = (N)) -> (~((p) = 1) /\ forall pvs_left_cancel_mask_prime pvs_right_cancel_mask_prime. (p) = pvs_left_cancel_mask_prime * pvs_right_cancel_mask_prime -> pvs_left_cancel_mask_prime = 1 \/ pvs_right_cancel_mask_prime = 1) -> (exists pvs_factor_cancel_mask_p_divisor. (n) = (p) * pvs_factor_cancel_mask_p_divisor) -> (((exists dst_positive_code_cancel_masktable dst_positive_scale_cancel_masktable dst_negative_code_cancel_masktable dst_negative_scale_cancel_masktable. (((K) = (((((dst_positive_code_cancel_masktable) + (dst_positive_scale_cancel_masktable)) * S ((dst_positive_code_cancel_masktable) + (dst_positive_scale_cancel_masktable)) + ((dst_positive_scale_cancel_masktable) + (dst_positive_scale_cancel_masktable))) + (((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) * S ((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) + ((dst_negative_scale_cancel_masktable) + (dst_negative_scale_cancel_masktable)))) * S ((((dst_positive_code_cancel_masktable) + (dst_positive_scale_cancel_masktable)) * S ((dst_positive_code_cancel_masktable) + (dst_positive_scale_cancel_masktable)) + ((dst_positive_scale_cancel_masktable) + (dst_positive_scale_cancel_masktable))) + (((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) * S ((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) + ((dst_negative_scale_cancel_masktable) + (dst_negative_scale_cancel_masktable)))) + ((((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) * S ((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) + ((dst_negative_scale_cancel_masktable) + (dst_negative_scale_cancel_masktable))) + (((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) * S ((dst_negative_code_cancel_masktable) + (dst_negative_scale_cancel_masktable)) + ((dst_negative_scale_cancel_masktable) + (dst_negative_scale_cancel_masktable)))))) /\ (forall dst_index_cancel_masktable. (exists pvs_le_gap_cancel_masktabledomain. pvs_le_gap_cancel_masktabledomain + (dst_index_cancel_masktable) = (n)) -> exists dst_positive_cancel_masktable dst_negative_cancel_masktable dst_value_cancel_masktable. ((((exists ff_h_pvs_cancel_masktableentrypositive. ff_h_pvs_cancel_masktableentrypositive + S (dst_positive_cancel_masktable) = S ((S (dst_index_cancel_masktable)) * dst_positive_scale_cancel_masktable)) /\ exists ff_q_pvs_cancel_masktableentrypositive. dst_positive_code_cancel_masktable = ff_q_pvs_cancel_masktableentrypositive * S ((S (dst_index_cancel_masktable)) * dst_positive_scale_cancel_masktable) + (dst_positive_cancel_masktable))) /\ (((((exists ff_h_pvs_cancel_masktableentrynegative. ff_h_pvs_cancel_masktableentrynegative + S (dst_negative_cancel_masktable) = S ((S (dst_index_cancel_masktable)) * dst_negative_scale_cancel_masktable)) /\ exists ff_q_pvs_cancel_masktableentrynegative. dst_negative_code_cancel_masktable = ff_q_pvs_cancel_masktableentrynegative * S ((S (dst_index_cancel_masktable)) * dst_negative_scale_cancel_masktable) + (dst_negative_cancel_masktable))) /\ (exists ge_balance_positive_cancel_masktableentryvalue ge_balance_negative_cancel_masktableentryvalue. (((((dst_value_cancel_masktable) = 2 * (ge_balance_positive_cancel_masktableentryvalue) /\ (ge_balance_negative_cancel_masktableentryvalue) = 0) \/ exists ge_signed_half_cancel_masktableentryvaluedecode. (((dst_value_cancel_masktable) = 2 * ge_signed_half_cancel_masktableentryvaluedecode + 1 /\ (ge_balance_positive_cancel_masktableentryvalue) = 0) /\ (ge_balance_negative_cancel_masktableentryvalue) = S ge_signed_half_cancel_masktableentryvaluedecode))) /\ ((dst_positive_cancel_masktable) + ge_balance_negative_cancel_masktableentryvalue = (dst_negative_cancel_masktable) + ge_balance_positive_cancel_masktableentryvalue))))))))) /\ (forall dm_index_cancel_mask dm_value_cancel_mask. (exists pvs_le_gap_cancel_maskdomain. pvs_le_gap_cancel_maskdomain + (dm_index_cancel_mask) = (n)) -> (exists dst_positive_code_cancel_masklookup dst_positive_scale_cancel_masklookup dst_negative_code_cancel_masklookup dst_negative_scale_cancel_masklookup dst_positive_cancel_masklookup dst_negative_cancel_masklookup. (((K) = (((((dst_positive_code_cancel_masklookup) + (dst_positive_scale_cancel_masklookup)) * S ((dst_positive_code_cancel_masklookup) + (dst_positive_scale_cancel_masklookup)) + ((dst_positive_scale_cancel_masklookup) + (dst_positive_scale_cancel_masklookup))) + (((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) * S ((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) + ((dst_negative_scale_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)))) * S ((((dst_positive_code_cancel_masklookup) + (dst_positive_scale_cancel_masklookup)) * S ((dst_positive_code_cancel_masklookup) + (dst_positive_scale_cancel_masklookup)) + ((dst_positive_scale_cancel_masklookup) + (dst_positive_scale_cancel_masklookup))) + (((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) * S ((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) + ((dst_negative_scale_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)))) + ((((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) * S ((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) + ((dst_negative_scale_cancel_masklookup) + (dst_negative_scale_cancel_masklookup))) + (((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) * S ((dst_negative_code_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)) + ((dst_negative_scale_cancel_masklookup) + (dst_negative_scale_cancel_masklookup)))))) /\ (((((exists ff_h_pvs_cancel_masklookuppositive. ff_h_pvs_cancel_masklookuppositive + S (dst_positive_cancel_masklookup) = S ((S (dm_index_cancel_mask)) * dst_positive_scale_cancel_masklookup)) /\ exists ff_q_pvs_cancel_masklookuppositive. dst_positive_code_cancel_masklookup = ff_q_pvs_cancel_masklookuppositive * S ((S (dm_index_cancel_mask)) * dst_positive_scale_cancel_masklookup) + (dst_positive_cancel_masklookup))) /\ (((((exists ff_h_pvs_cancel_masklookupnegative. ff_h_pvs_cancel_masklookupnegative + S (dst_negative_cancel_masklookup) = S ((S (dm_index_cancel_mask)) * dst_negative_scale_cancel_masklookup)) /\ exists ff_q_pvs_cancel_masklookupnegative. dst_negative_code_cancel_masklookup = ff_q_pvs_cancel_masklookupnegative * S ((S (dm_index_cancel_mask)) * dst_negative_scale_cancel_masklookup) + (dst_negative_cancel_masklookup))) /\ (exists ge_balance_positive_cancel_masklookupvalue ge_balance_negative_cancel_masklookupvalue. (((((dm_value_cancel_mask) = 2 * (ge_balance_positive_cancel_masklookupvalue) /\ (ge_balance_negative_cancel_masklookupvalue) = 0) \/ exists ge_signed_half_cancel_masklookupvaluedecode. (((dm_value_cancel_mask) = 2 * ge_signed_half_cancel_masklookupvaluedecode + 1 /\ (ge_balance_positive_cancel_masklookupvalue) = 0) /\ (ge_balance_negative_cancel_masklookupvalue) = S ge_signed_half_cancel_masklookupvaluedecode))) /\ ((dst_positive_cancel_masklookup) + ge_balance_negative_cancel_masklookupvalue = (dst_negative_cancel_masklookup) + ge_balance_positive_cancel_masklookupvalue))))))))) -> ((((~((dm_index_cancel_mask)=0)) /\ (exists dm_quotient_cancel_maskentry. (((n)=(dm_index_cancel_mask)*dm_quotient_cancel_maskentry) /\ (exists dst_positive_code_cancel_maskentryinput dst_positive_scale_cancel_maskentryinput dst_negative_code_cancel_maskentryinput dst_negative_scale_cancel_maskentryinput dst_positive_cancel_maskentryinput dst_negative_cancel_maskentryinput. (((M) = (((((dst_positive_code_cancel_maskentryinput) + (dst_positive_scale_cancel_maskentryinput)) * S ((dst_positive_code_cancel_maskentryinput) + (dst_positive_scale_cancel_maskentryinput)) + ((dst_positive_scale_cancel_maskentryinput) + (dst_positive_scale_cancel_maskentryinput))) + (((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) * S ((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) + ((dst_negative_scale_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)))) * S ((((dst_positive_code_cancel_maskentryinput) + (dst_positive_scale_cancel_maskentryinput)) * S ((dst_positive_code_cancel_maskentryinput) + (dst_positive_scale_cancel_maskentryinput)) + ((dst_positive_scale_cancel_maskentryinput) + (dst_positive_scale_cancel_maskentryinput))) + (((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) * S ((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) + ((dst_negative_scale_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)))) + ((((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) * S ((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) + ((dst_negative_scale_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput))) + (((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) * S ((dst_negative_code_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)) + ((dst_negative_scale_cancel_maskentryinput) + (dst_negative_scale_cancel_maskentryinput)))))) /\ (((((exists ff_h_pvs_cancel_maskentryinputpositive. ff_h_pvs_cancel_maskentryinputpositive + S (dst_positive_cancel_maskentryinput) = S ((S (dm_index_cancel_mask)) * dst_positive_scale_cancel_maskentryinput)) /\ exists ff_q_pvs_cancel_maskentryinputpositive. dst_positive_code_cancel_maskentryinput = ff_q_pvs_cancel_maskentryinputpositive * S ((S (dm_index_cancel_mask)) * dst_positive_scale_cancel_maskentryinput) + (dst_positive_cancel_maskentryinput))) /\ (((((exists ff_h_pvs_cancel_maskentryinputnegative. ff_h_pvs_cancel_maskentryinputnegative + S (dst_negative_cancel_maskentryinput) = S ((S (dm_index_cancel_mask)) * dst_negative_scale_cancel_maskentryinput)) /\ exists ff_q_pvs_cancel_maskentryinputnegative. dst_negative_code_cancel_maskentryinput = ff_q_pvs_cancel_maskentryinputnegative * S ((S (dm_index_cancel_mask)) * dst_negative_scale_cancel_maskentryinput) + (dst_negative_cancel_maskentryinput))) /\ (exists ge_balance_positive_cancel_maskentryinputvalue ge_balance_negative_cancel_maskentryinputvalue. (((((dm_value_cancel_mask) = 2 * (ge_balance_positive_cancel_maskentryinputvalue) /\ (ge_balance_negative_cancel_maskentryinputvalue) = 0) \/ exists ge_signed_half_cancel_maskentryinputvaluedecode. (((dm_value_cancel_mask) = 2 * ge_signed_half_cancel_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_cancel_maskentryinputvalue) = 0) /\ (ge_balance_negative_cancel_maskentryinputvalue) = S ge_signed_half_cancel_maskentryinputvaluedecode))) /\ ((dst_positive_cancel_maskentryinput) + ge_balance_negative_cancel_maskentryinputvalue = (dst_negative_cancel_maskentryinput) + ge_balance_positive_cancel_maskentryinputvalue))))))))))))) \/ ((((dm_index_cancel_mask)=0 \/ ~(exists pvs_factor_cancel_maskentrynondivisor. (n) = (dm_index_cancel_mask) * pvs_factor_cancel_maskentrynondivisor)) /\ ((dm_value_cancel_mask)=0))))))) -> (exists dst_positive_code_cancel_mask_sum dst_positive_scale_cancel_mask_sum dst_negative_code_cancel_mask_sum dst_negative_scale_cancel_mask_sum dst_positive_sum_cancel_mask_sum dst_negative_sum_cancel_mask_sum. (((K) = (((((dst_positive_code_cancel_mask_sum) + (dst_positive_scale_cancel_mask_sum)) * S ((dst_positive_code_cancel_mask_sum) + (dst_positive_scale_cancel_mask_sum)) + ((dst_positive_scale_cancel_mask_sum) + (dst_positive_scale_cancel_mask_sum))) + (((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) * S ((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) + ((dst_negative_scale_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)))) * S ((((dst_positive_code_cancel_mask_sum) + (dst_positive_scale_cancel_mask_sum)) * S ((dst_positive_code_cancel_mask_sum) + (dst_positive_scale_cancel_mask_sum)) + ((dst_positive_scale_cancel_mask_sum) + (dst_positive_scale_cancel_mask_sum))) + (((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) * S ((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) + ((dst_negative_scale_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)))) + ((((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) * S ((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) + ((dst_negative_scale_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum))) + (((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) * S ((dst_negative_code_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)) + ((dst_negative_scale_cancel_mask_sum) + (dst_negative_scale_cancel_mask_sum)))))) /\ (((exists fs_u_dst_cancel_mask_sumpositive fs_v_dst_cancel_mask_sumpositive. ((((exists fs_h_dst_cancel_mask_sumpositive_body_start. fs_h_dst_cancel_mask_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_mask_sumpositive)) /\ exists fs_q_dst_cancel_mask_sumpositive_body_start. fs_u_dst_cancel_mask_sumpositive = fs_q_dst_cancel_mask_sumpositive_body_start * S ((S (0)) * fs_v_dst_cancel_mask_sumpositive) + (0))) /\ ((((exists fs_h_dst_cancel_mask_sumpositive_body_terminal. fs_h_dst_cancel_mask_sumpositive_body_terminal + S (dst_positive_sum_cancel_mask_sum) = S ((S (S n)) * fs_v_dst_cancel_mask_sumpositive)) /\ exists fs_q_dst_cancel_mask_sumpositive_body_terminal. fs_u_dst_cancel_mask_sumpositive = fs_q_dst_cancel_mask_sumpositive_body_terminal * S ((S (S n)) * fs_v_dst_cancel_mask_sumpositive) + (dst_positive_sum_cancel_mask_sum))) /\ forall fs_i_dst_cancel_mask_sumpositive_body_steps. (exists fs_lt_dst_cancel_mask_sumpositive_body_steps_bound. fs_lt_dst_cancel_mask_sumpositive_body_steps_bound + S fs_i_dst_cancel_mask_sumpositive_body_steps = S n) -> exists fs_a_dst_cancel_mask_sumpositive_body_steps fs_r_dst_cancel_mask_sumpositive_body_steps fs_s_dst_cancel_mask_sumpositive_body_steps. ((((exists fs_h_dst_cancel_mask_sumpositive_body_steps_summand. fs_h_dst_cancel_mask_sumpositive_body_steps_summand + S (fs_a_dst_cancel_mask_sumpositive_body_steps) = S ((S (fs_i_dst_cancel_mask_sumpositive_body_steps)) * dst_positive_scale_cancel_mask_sum)) /\ exists fs_q_dst_cancel_mask_sumpositive_body_steps_summand. dst_positive_code_cancel_mask_sum = fs_q_dst_cancel_mask_sumpositive_body_steps_summand * S ((S (fs_i_dst_cancel_mask_sumpositive_body_steps)) * dst_positive_scale_cancel_mask_sum) + (fs_a_dst_cancel_mask_sumpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_mask_sumpositive_body_steps_partial. fs_h_dst_cancel_mask_sumpositive_body_steps_partial + S (fs_r_dst_cancel_mask_sumpositive_body_steps) = S ((S (fs_i_dst_cancel_mask_sumpositive_body_steps)) * fs_v_dst_cancel_mask_sumpositive)) /\ exists fs_q_dst_cancel_mask_sumpositive_body_steps_partial. fs_u_dst_cancel_mask_sumpositive = fs_q_dst_cancel_mask_sumpositive_body_steps_partial * S ((S (fs_i_dst_cancel_mask_sumpositive_body_steps)) * fs_v_dst_cancel_mask_sumpositive) + (fs_r_dst_cancel_mask_sumpositive_body_steps))) /\ ((((exists fs_h_dst_cancel_mask_sumpositive_body_steps_successor. fs_h_dst_cancel_mask_sumpositive_body_steps_successor + S (fs_s_dst_cancel_mask_sumpositive_body_steps) = S ((S (S fs_i_dst_cancel_mask_sumpositive_body_steps)) * fs_v_dst_cancel_mask_sumpositive)) /\ exists fs_q_dst_cancel_mask_sumpositive_body_steps_successor. fs_u_dst_cancel_mask_sumpositive = fs_q_dst_cancel_mask_sumpositive_body_steps_successor * S ((S (S fs_i_dst_cancel_mask_sumpositive_body_steps)) * fs_v_dst_cancel_mask_sumpositive) + (fs_s_dst_cancel_mask_sumpositive_body_steps))) /\ fs_s_dst_cancel_mask_sumpositive_body_steps = fs_r_dst_cancel_mask_sumpositive_body_steps + fs_a_dst_cancel_mask_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_cancel_mask_sumnegative fs_v_dst_cancel_mask_sumnegative. ((((exists fs_h_dst_cancel_mask_sumnegative_body_start. fs_h_dst_cancel_mask_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_cancel_mask_sumnegative)) /\ exists fs_q_dst_cancel_mask_sumnegative_body_start. fs_u_dst_cancel_mask_sumnegative = fs_q_dst_cancel_mask_sumnegative_body_start * S ((S (0)) * fs_v_dst_cancel_mask_sumnegative) + (0))) /\ ((((exists fs_h_dst_cancel_mask_sumnegative_body_terminal. fs_h_dst_cancel_mask_sumnegative_body_terminal + S (dst_negative_sum_cancel_mask_sum) = S ((S (S n)) * fs_v_dst_cancel_mask_sumnegative)) /\ exists fs_q_dst_cancel_mask_sumnegative_body_terminal. fs_u_dst_cancel_mask_sumnegative = fs_q_dst_cancel_mask_sumnegative_body_terminal * S ((S (S n)) * fs_v_dst_cancel_mask_sumnegative) + (dst_negative_sum_cancel_mask_sum))) /\ forall fs_i_dst_cancel_mask_sumnegative_body_steps. (exists fs_lt_dst_cancel_mask_sumnegative_body_steps_bound. fs_lt_dst_cancel_mask_sumnegative_body_steps_bound + S fs_i_dst_cancel_mask_sumnegative_body_steps = S n) -> exists fs_a_dst_cancel_mask_sumnegative_body_steps fs_r_dst_cancel_mask_sumnegative_body_steps fs_s_dst_cancel_mask_sumnegative_body_steps. ((((exists fs_h_dst_cancel_mask_sumnegative_body_steps_summand. fs_h_dst_cancel_mask_sumnegative_body_steps_summand + S (fs_a_dst_cancel_mask_sumnegative_body_steps) = S ((S (fs_i_dst_cancel_mask_sumnegative_body_steps)) * dst_negative_scale_cancel_mask_sum)) /\ exists fs_q_dst_cancel_mask_sumnegative_body_steps_summand. dst_negative_code_cancel_mask_sum = fs_q_dst_cancel_mask_sumnegative_body_steps_summand * S ((S (fs_i_dst_cancel_mask_sumnegative_body_steps)) * dst_negative_scale_cancel_mask_sum) + (fs_a_dst_cancel_mask_sumnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_mask_sumnegative_body_steps_partial. fs_h_dst_cancel_mask_sumnegative_body_steps_partial + S (fs_r_dst_cancel_mask_sumnegative_body_steps) = S ((S (fs_i_dst_cancel_mask_sumnegative_body_steps)) * fs_v_dst_cancel_mask_sumnegative)) /\ exists fs_q_dst_cancel_mask_sumnegative_body_steps_partial. fs_u_dst_cancel_mask_sumnegative = fs_q_dst_cancel_mask_sumnegative_body_steps_partial * S ((S (fs_i_dst_cancel_mask_sumnegative_body_steps)) * fs_v_dst_cancel_mask_sumnegative) + (fs_r_dst_cancel_mask_sumnegative_body_steps))) /\ ((((exists fs_h_dst_cancel_mask_sumnegative_body_steps_successor. fs_h_dst_cancel_mask_sumnegative_body_steps_successor + S (fs_s_dst_cancel_mask_sumnegative_body_steps) = S ((S (S fs_i_dst_cancel_mask_sumnegative_body_steps)) * fs_v_dst_cancel_mask_sumnegative)) /\ exists fs_q_dst_cancel_mask_sumnegative_body_steps_successor. fs_u_dst_cancel_mask_sumnegative = fs_q_dst_cancel_mask_sumnegative_body_steps_successor * S ((S (S fs_i_dst_cancel_mask_sumnegative_body_steps)) * fs_v_dst_cancel_mask_sumnegative) + (fs_s_dst_cancel_mask_sumnegative_body_steps))) /\ fs_s_dst_cancel_mask_sumnegative_body_steps = fs_r_dst_cancel_mask_sumnegative_body_steps + fs_a_dst_cancel_mask_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_cancel_mask_sumresult ge_balance_negative_cancel_mask_sumresult. (((((z) = 2 * (ge_balance_positive_cancel_mask_sumresult) /\ (ge_balance_negative_cancel_mask_sumresult) = 0) \/ exists ge_signed_half_cancel_mask_sumresultdecode. (((z) = 2 * ge_signed_half_cancel_mask_sumresultdecode + 1 /\ (ge_balance_positive_cancel_mask_sumresult) = 0) /\ (ge_balance_negative_cancel_mask_sumresult) = S ge_signed_half_cancel_mask_sumresultdecode))) /\ ((dst_positive_sum_cancel_mask_sum) + ge_balance_negative_cancel_mask_sumresult = (dst_negative_sum_cancel_mask_sum) + ge_balance_positive_cancel_mask_sumresult))))))))) -> z=0

Complete tactic proof in conservative notation

All 133 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

133 script commands · 23 reading checkpoints · 9 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)
divisor prime toggle permutation existsdivisor prime toggle boundedmobius divisor mask prime toggle negatesanti invariant signed permutation sum zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro M
  3. L3
    intro n
  4. L4
    intro K
  5. L5
    intro p
  6. L6
    intro z
  7. L7
    intro hmu
  8. L8
    intro hn
  9. L9
    intro hN
  10. L10
    intro hp
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hpn
  2. L12
    intro hmask
  3. L13
    intro hz
03Establish hmapL14–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor prime toggle permutation exists.

  1. L14
    have hmap : ∃ r. ∃ s. DivisorPrimeTogglePrefix(n,p,r,s,S n) ∧ PermutationPrefix(r,s,S n)Definitions: DivisorPrimeTogglePrefix(n,p,r,s,S n)PermutationPrefix(r,s,S n)Original native command in the exact edition
  2. L15
    specialize divisor_prime_toggle_permutation_exists (n)
  3. L16
    specialize divisor_prime_toggle_permutation_exists (p)
  4. L17
    apply divisor_prime_toggle_permutation_exists
  5. L18
    exact hn
  6. L19
    exact hp
  7. L20
    exact hpn
04Separate the logical casesL21–26

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

  1. L21
    cases hmap
  2. L22
    cases hmap_witness
  3. L23
    cases hmap_witness_witness
  4. L24
    cases hmap_witness_witness_right
  5. L25
    cases hmap_witness_witness_right_right
  6. L26
    cases hmask
05Establish hGL27–34

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

  1. L27
    have hG : ∃ G. ArithTable(S n,G) ∧ ArithReindex(K,G,x,x1,S n)Definitions: ArithTable(S n,G)ArithReindex(K,G,x,x1,S n)Original native command in the exact edition
  2. L28
    specialize divisor_signed_table_reindex_exists (n)
  3. L29
    specialize divisor_signed_table_reindex_exists (K)
  4. L30
    specialize divisor_signed_table_reindex_exists (x)
  5. L31
    specialize divisor_signed_table_reindex_exists (x1)
  6. L32
    specialize divisor_signed_table_reindex_exists (S n)
  7. L33
    apply divisor_signed_table_reindex_exists
  8. L34
    exact hmask_left
06Separate the logical casesL35–36

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

  1. L35
    cases hG
  2. L36
    cases hG_witness
07Establish hsumL37–42

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

  1. L37
    have hsum : ∃ w. SignedPrefixSum(x2,S n,w)Definitions: SignedPrefixSum(x2,S n,w)Original native command in the exact edition
  2. L38
    specialize arithmetic_signed_sum_exists (S n)
  3. L39
    specialize arithmetic_signed_sum_exists (x2)
  4. L40
    specialize arithmetic_signed_sum_exists (S n)
  5. L41
    apply arithmetic_signed_sum_exists
  6. L42
    exact hG_witness_left
08Separate the logical casesL43–43

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

  1. L43
    cases hsum
09Establish hpointL44–50

Establish this local claim before using it. It is not an additional assumption.

  1. L44
    have hpoint : ArithNegate(K,x2,S n)Definitions: ArithNegate(K,x2,S n)Original native command in the exact edition
  2. L45
    intro i
  3. L46
    intro a
  4. L47
    intro b
  5. L48
    intro hi
  6. L49
    intro ha
  7. L50
    intro hb
10Establish hiimageL51–54

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

  1. L51
    have hiimage : ∃ q. BetaAt(x,x1,i,q) ∧ DivisorPrimeToggle(n,p,i,q)Definitions: BetaAt(x,x1,i,q)DivisorPrimeToggle(n,p,i,q)Original native command in the exact edition
  2. L52
    specialize hmap_witness_witness_left (i)
  3. L53
    apply hmap_witness_witness_left
  4. L54
    exact hi
11Separate the logical casesL55–56

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

  1. L55
    cases hiimage
  2. L56
    cases hiimage_witness
12Establish hqboundL57–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor prime toggle bounded.

  1. L57
    have hqbound : Le(x4,n)Definitions: Le(x4,n)Original native command in the exact edition
  2. L58
    specialize divisor_prime_toggle_bounded (n)
  3. L59
    specialize divisor_prime_toggle_bounded (p)
  4. L60
    specialize divisor_prime_toggle_bounded (i)
  5. L61
    specialize divisor_prime_toggle_bounded (x4)
  6. L62
    apply divisor_prime_toggle_bounded
  7. L63
    exact hn
  8. L64
    exact hp
  9. L65
    exact hpn
  10. L66
    specialize le_of_succ_le_succ (i)
13Use earlier factsL67–70

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

  1. L67
    specialize le_of_succ_le_succ (n)
  2. L68
    apply le_of_succ_le_succ
  3. L69
    exact hi
  4. L70
    exact hiimage_witness_right
14Establish hvalueL71–77

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

  1. L71
    have hvalue : ∃ v. ArithAt(K,x4,v)Definitions: ArithAt(K,x4,v)Original native command in the exact edition
  2. L72
    specialize divisor_signed_table_lookup (n)
  3. L73
    specialize divisor_signed_table_lookup (K)
  4. L74
    specialize divisor_signed_table_lookup (x4)
  5. L75
    apply divisor_signed_table_lookup
  6. L76
    exact hmask_left
  7. L77
    exact hqbound
15Separate the logical casesL78–78

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

  1. L78
    cases hvalue
16Establish heqL79–88

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

  1. L79
    have heq : x5=b
  2. L80
    specialize divisor_signed_table_at_functional (x2)
  3. L81
    specialize divisor_signed_table_at_functional (i)
  4. L82
    specialize divisor_signed_table_at_functional (x5)
  5. L83
    specialize divisor_signed_table_at_functional (b)
  6. L84
    apply divisor_signed_table_at_functional
  7. L85
    specialize hG_witness_right (i)
  8. L86
    specialize hG_witness_right (x4)
  9. L87
    specialize hG_witness_right (x5)
  10. L88
    apply hG_witness_right
17Use earlier factsL89–92

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

  1. L89
    exact hi
  2. L90
    exact hiimage_witness_left
  3. L91
    exact hvalue_witness
  4. L92
    exact hb
18Establish hnegL93–102

Establish this local claim before using it. It is not an additional assumption.

  1. L93
    have hneg : SignedNegate(a,x5)Definitions: SignedNegate(a,x5)Original native command in the exact edition
  2. L94
    specialize mobius_divisor_mask_prime_toggle_negates (N)
  3. L95
    specialize mobius_divisor_mask_prime_toggle_negates (M)
  4. L96
    specialize mobius_divisor_mask_prime_toggle_negates (n)
  5. L97
    specialize mobius_divisor_mask_prime_toggle_negates (K)
  6. L98
    specialize mobius_divisor_mask_prime_toggle_negates (p)
  7. L99
    specialize mobius_divisor_mask_prime_toggle_negates (i)
  8. L100
    specialize mobius_divisor_mask_prime_toggle_negates (x4)
  9. L101
    specialize mobius_divisor_mask_prime_toggle_negates (a)
  10. L102
    specialize mobius_divisor_mask_prime_toggle_negates (x5)
19Use earlier factsL103–112

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

  1. L103
    apply mobius_divisor_mask_prime_toggle_negates
  2. L104
    exact hmu
  3. L105
    exact hn
  4. L106
    exact hN
  5. L107
    exact hp
  6. L108
    exact hpn
  7. L109
    exact hmask
  8. L110
    specialize le_of_succ_le_succ (i)
  9. L111
    specialize le_of_succ_le_succ (n)
  10. L112
    apply le_of_succ_le_succ
20Use earlier factsL113–116

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

  1. L113
    exact hi
  2. L114
    exact hiimage_witness_right
  3. L115
    exact ha
  4. L116
    exact hvalue_witness
21Calculate and transport equalitiesL117–118

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

  1. L117
    rewrite heq at hneg
  2. L118
    rewrite heq at hneg
22Use earlier factsL119–128

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

  1. L119
    exact hneg
  2. L120
    specialize anti_invariant_signed_permutation_sum_zero (K)
  3. L121
    specialize anti_invariant_signed_permutation_sum_zero (x2)
  4. L122
    specialize anti_invariant_signed_permutation_sum_zero (x)
  5. L123
    specialize anti_invariant_signed_permutation_sum_zero (x1)
  6. L124
    specialize anti_invariant_signed_permutation_sum_zero (S n)
  7. L125
    specialize anti_invariant_signed_permutation_sum_zero (z)
  8. L126
    specialize anti_invariant_signed_permutation_sum_zero (x3)
  9. L127
    apply anti_invariant_signed_permutation_sum_zero
  10. L128
    exact hmap_witness_witness_right_left
23Use earlier factsL129–133

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

  1. L129
    exact hmap_witness_witness_right_right_left
  2. L130
    exact hG_witness_right
  3. L131
    exact hpoint
  4. L132
    exact hz
  5. L133
    exact hsum_witness

Library-wide reading audit

Original defined command ledger · 133 lines
  1. 0001intro N
  2. 0002intro M
  3. 0003intro n
  4. 0004intro K
  5. 0005intro p
  6. 0006intro z
  7. 0007intro hmu
  8. 0008intro hn
  9. 0009intro hN
  10. 0010intro hp
  11. 0011intro hpn
  12. 0012intro hmask
  13. 0013intro hz
  14. 0014have hmap : ∃ r. ∃ s. DivisorPrimeTogglePrefix(n,p,r,s,S n) ∧ PermutationPrefix(r,s,S n)
  15. 0015specialize divisor_prime_toggle_permutation_exists (n)
  16. 0016specialize divisor_prime_toggle_permutation_exists (p)
  17. 0017apply divisor_prime_toggle_permutation_exists
  18. 0018exact hn
  19. 0019exact hp
  20. 0020exact hpn
  21. 0021cases hmap
  22. 0022cases hmap_witness
  23. 0023cases hmap_witness_witness
  24. 0024cases hmap_witness_witness_right
  25. 0025cases hmap_witness_witness_right_right
  26. 0026cases hmask
  27. 0027have hG : ∃ G. ArithTable(S n,G) ∧ ArithReindex(K,G,x,x1,S n)
  28. 0028specialize divisor_signed_table_reindex_exists (n)
  29. 0029specialize divisor_signed_table_reindex_exists (K)
  30. 0030specialize divisor_signed_table_reindex_exists (x)
  31. 0031specialize divisor_signed_table_reindex_exists (x1)
  32. 0032specialize divisor_signed_table_reindex_exists (S n)
  33. 0033apply divisor_signed_table_reindex_exists
  34. 0034exact hmask_left
  35. 0035cases hG
  36. 0036cases hG_witness
  37. 0037have hsum : ∃ w. SignedPrefixSum(x2,S n,w)
  38. 0038specialize arithmetic_signed_sum_exists (S n)
  39. 0039specialize arithmetic_signed_sum_exists (x2)
  40. 0040specialize arithmetic_signed_sum_exists (S n)
  41. 0041apply arithmetic_signed_sum_exists
  42. 0042exact hG_witness_left
  43. 0043cases hsum
  44. 0044have hpoint : ArithNegate(K,x2,S n)
  45. 0045intro i
  46. 0046intro a
  47. 0047intro b
  48. 0048intro hi
  49. 0049intro ha
  50. 0050intro hb
  51. 0051have hiimage : ∃ q. BetaAt(x,x1,i,q) ∧ DivisorPrimeToggle(n,p,i,q)
  52. 0052specialize hmap_witness_witness_left (i)
  53. 0053apply hmap_witness_witness_left
  54. 0054exact hi
  55. 0055cases hiimage
  56. 0056cases hiimage_witness
  57. 0057have hqbound : Le(x4,n)
  58. 0058specialize divisor_prime_toggle_bounded (n)
  59. 0059specialize divisor_prime_toggle_bounded (p)
  60. 0060specialize divisor_prime_toggle_bounded (i)
  61. 0061specialize divisor_prime_toggle_bounded (x4)
  62. 0062apply divisor_prime_toggle_bounded
  63. 0063exact hn
  64. 0064exact hp
  65. 0065exact hpn
  66. 0066specialize le_of_succ_le_succ (i)
  67. 0067specialize le_of_succ_le_succ (n)
  68. 0068apply le_of_succ_le_succ
  69. 0069exact hi
  70. 0070exact hiimage_witness_right
  71. 0071have hvalue : ∃ v. ArithAt(K,x4,v)
  72. 0072specialize divisor_signed_table_lookup (n)
  73. 0073specialize divisor_signed_table_lookup (K)
  74. 0074specialize divisor_signed_table_lookup (x4)
  75. 0075apply divisor_signed_table_lookup
  76. 0076exact hmask_left
  77. 0077exact hqbound
  78. 0078cases hvalue
  79. 0079have heq : x5=b
  80. 0080specialize divisor_signed_table_at_functional (x2)
  81. 0081specialize divisor_signed_table_at_functional (i)
  82. 0082specialize divisor_signed_table_at_functional (x5)
  83. 0083specialize divisor_signed_table_at_functional (b)
  84. 0084apply divisor_signed_table_at_functional
  85. 0085specialize hG_witness_right (i)
  86. 0086specialize hG_witness_right (x4)
  87. 0087specialize hG_witness_right (x5)
  88. 0088apply hG_witness_right
  89. 0089exact hi
  90. 0090exact hiimage_witness_left
  91. 0091exact hvalue_witness
  92. 0092exact hb
  93. 0093have hneg : SignedNegate(a,x5)
  94. 0094specialize mobius_divisor_mask_prime_toggle_negates (N)
  95. 0095specialize mobius_divisor_mask_prime_toggle_negates (M)
  96. 0096specialize mobius_divisor_mask_prime_toggle_negates (n)
  97. 0097specialize mobius_divisor_mask_prime_toggle_negates (K)
  98. 0098specialize mobius_divisor_mask_prime_toggle_negates (p)
  99. 0099specialize mobius_divisor_mask_prime_toggle_negates (i)
  100. 0100specialize mobius_divisor_mask_prime_toggle_negates (x4)
  101. 0101specialize mobius_divisor_mask_prime_toggle_negates (a)
  102. 0102specialize mobius_divisor_mask_prime_toggle_negates (x5)
  103. 0103apply mobius_divisor_mask_prime_toggle_negates
  104. 0104exact hmu
  105. 0105exact hn
  106. 0106exact hN
  107. 0107exact hp
  108. 0108exact hpn
  109. 0109exact hmask
  110. 0110specialize le_of_succ_le_succ (i)
  111. 0111specialize le_of_succ_le_succ (n)
  112. 0112apply le_of_succ_le_succ
  113. 0113exact hi
  114. 0114exact hiimage_witness_right
  115. 0115exact ha
  116. 0116exact hvalue_witness
  117. 0117rewrite heq at hneg
  118. 0118rewrite heq at hneg
  119. 0119exact hneg
  120. 0120specialize anti_invariant_signed_permutation_sum_zero (K)
  121. 0121specialize anti_invariant_signed_permutation_sum_zero (x2)
  122. 0122specialize anti_invariant_signed_permutation_sum_zero (x)
  123. 0123specialize anti_invariant_signed_permutation_sum_zero (x1)
  124. 0124specialize anti_invariant_signed_permutation_sum_zero (S n)
  125. 0125specialize anti_invariant_signed_permutation_sum_zero (z)
  126. 0126specialize anti_invariant_signed_permutation_sum_zero (x3)
  127. 0127apply anti_invariant_signed_permutation_sum_zero
  128. 0128exact hmap_witness_witness_right_left
  129. 0129exact hmap_witness_witness_right_right_left
  130. 0130exact hG_witness_right
  131. 0131exact hpoint
  132. 0132exact hz
  133. 0133exact hsum_witness