MC0012

mobius_divisor_mask_prime_toggle_negates

Every pair of actual Möbius-mask values along the finite prime toggle are signed opposites, including zero, nondivisors and squared-prime multiples.

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. ∀ d. ∀ e. ∀ a. ∀ b. MobiusTable(N,M) → ¬n = 0 → Le(n,N) → Prime(p) → Dvd(p,n) → DivisorMask(M,n,n,K) → Le(d,n) → DivisorPrimeToggle(n,p,d,e) → ArithAt(K,d,a) → ArithAt(K,e,b) → SignedNegate(a,b)

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

Definition DAG

SignedNegate(a,b) · 1ArithAt(F,i,z) · 2MobiusTable(N,M) · 1DivisorMask(F,n,l,M) · 1DivisorPrimeToggle(n,p,d,e) · 1Le(a,b) · 3Dvd(d,n) · 1Prime(p) · 1

Actual proof prerequisites

divisor_prime_toggle_boundedmobius_prime_factor_toggle_negatesmobius_divisor_mask_actual_valueprime_factor_toggle_positiveprime_nonzero · checked external prerequisiteprime_factor_toggle_preserves_divisordivisor_mask_entry_omitted_value · checked external prerequisitesigned_negate_zero · checked external prerequisite
Original expanded first-order statement 
forall N M n K p d e a b. (((exists dst_positive_code_mask_toggle_mutable dst_positive_scale_mask_toggle_mutable dst_negative_code_mask_toggle_mutable dst_negative_scale_mask_toggle_mutable. (((M) = (((((dst_positive_code_mask_toggle_mutable) + (dst_positive_scale_mask_toggle_mutable)) * S ((dst_positive_code_mask_toggle_mutable) + (dst_positive_scale_mask_toggle_mutable)) + ((dst_positive_scale_mask_toggle_mutable) + (dst_positive_scale_mask_toggle_mutable))) + (((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) * S ((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) + ((dst_negative_scale_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)))) * S ((((dst_positive_code_mask_toggle_mutable) + (dst_positive_scale_mask_toggle_mutable)) * S ((dst_positive_code_mask_toggle_mutable) + (dst_positive_scale_mask_toggle_mutable)) + ((dst_positive_scale_mask_toggle_mutable) + (dst_positive_scale_mask_toggle_mutable))) + (((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) * S ((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) + ((dst_negative_scale_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)))) + ((((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) * S ((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) + ((dst_negative_scale_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable))) + (((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) * S ((dst_negative_code_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)) + ((dst_negative_scale_mask_toggle_mutable) + (dst_negative_scale_mask_toggle_mutable)))))) /\ (forall dst_index_mask_toggle_mutable. (exists pvs_le_gap_mask_toggle_mutabledomain. pvs_le_gap_mask_toggle_mutabledomain + (dst_index_mask_toggle_mutable) = (N)) -> exists dst_positive_mask_toggle_mutable dst_negative_mask_toggle_mutable dst_value_mask_toggle_mutable. ((((exists ff_h_pvs_mask_toggle_mutableentrypositive. ff_h_pvs_mask_toggle_mutableentrypositive + S (dst_positive_mask_toggle_mutable) = S ((S (dst_index_mask_toggle_mutable)) * dst_positive_scale_mask_toggle_mutable)) /\ exists ff_q_pvs_mask_toggle_mutableentrypositive. dst_positive_code_mask_toggle_mutable = ff_q_pvs_mask_toggle_mutableentrypositive * S ((S (dst_index_mask_toggle_mutable)) * dst_positive_scale_mask_toggle_mutable) + (dst_positive_mask_toggle_mutable))) /\ (((((exists ff_h_pvs_mask_toggle_mutableentrynegative. ff_h_pvs_mask_toggle_mutableentrynegative + S (dst_negative_mask_toggle_mutable) = S ((S (dst_index_mask_toggle_mutable)) * dst_negative_scale_mask_toggle_mutable)) /\ exists ff_q_pvs_mask_toggle_mutableentrynegative. dst_negative_code_mask_toggle_mutable = ff_q_pvs_mask_toggle_mutableentrynegative * S ((S (dst_index_mask_toggle_mutable)) * dst_negative_scale_mask_toggle_mutable) + (dst_negative_mask_toggle_mutable))) /\ (exists ge_balance_positive_mask_toggle_mutableentryvalue ge_balance_negative_mask_toggle_mutableentryvalue. (((((dst_value_mask_toggle_mutable) = 2 * (ge_balance_positive_mask_toggle_mutableentryvalue) /\ (ge_balance_negative_mask_toggle_mutableentryvalue) = 0) \/ exists ge_signed_half_mask_toggle_mutableentryvaluedecode. (((dst_value_mask_toggle_mutable) = 2 * ge_signed_half_mask_toggle_mutableentryvaluedecode + 1 /\ (ge_balance_positive_mask_toggle_mutableentryvalue) = 0) /\ (ge_balance_negative_mask_toggle_mutableentryvalue) = S ge_signed_half_mask_toggle_mutableentryvaluedecode))) /\ ((dst_positive_mask_toggle_mutable) + ge_balance_negative_mask_toggle_mutableentryvalue = (dst_negative_mask_toggle_mutable) + ge_balance_positive_mask_toggle_mutableentryvalue))))))))) /\ (((exists dst_positive_code_mask_toggle_muzero dst_positive_scale_mask_toggle_muzero dst_negative_code_mask_toggle_muzero dst_negative_scale_mask_toggle_muzero dst_positive_mask_toggle_muzero dst_negative_mask_toggle_muzero. (((M) = (((((dst_positive_code_mask_toggle_muzero) + (dst_positive_scale_mask_toggle_muzero)) * S ((dst_positive_code_mask_toggle_muzero) + (dst_positive_scale_mask_toggle_muzero)) + ((dst_positive_scale_mask_toggle_muzero) + (dst_positive_scale_mask_toggle_muzero))) + (((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) * S ((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) + ((dst_negative_scale_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)))) * S ((((dst_positive_code_mask_toggle_muzero) + (dst_positive_scale_mask_toggle_muzero)) * S ((dst_positive_code_mask_toggle_muzero) + (dst_positive_scale_mask_toggle_muzero)) + ((dst_positive_scale_mask_toggle_muzero) + (dst_positive_scale_mask_toggle_muzero))) + (((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) * S ((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) + ((dst_negative_scale_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)))) + ((((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) * S ((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) + ((dst_negative_scale_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero))) + (((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) * S ((dst_negative_code_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)) + ((dst_negative_scale_mask_toggle_muzero) + (dst_negative_scale_mask_toggle_muzero)))))) /\ (((((exists ff_h_pvs_mask_toggle_muzeropositive. ff_h_pvs_mask_toggle_muzeropositive + S (dst_positive_mask_toggle_muzero) = S ((S (0)) * dst_positive_scale_mask_toggle_muzero)) /\ exists ff_q_pvs_mask_toggle_muzeropositive. dst_positive_code_mask_toggle_muzero = ff_q_pvs_mask_toggle_muzeropositive * S ((S (0)) * dst_positive_scale_mask_toggle_muzero) + (dst_positive_mask_toggle_muzero))) /\ (((((exists ff_h_pvs_mask_toggle_muzeronegative. ff_h_pvs_mask_toggle_muzeronegative + S (dst_negative_mask_toggle_muzero) = S ((S (0)) * dst_negative_scale_mask_toggle_muzero)) /\ exists ff_q_pvs_mask_toggle_muzeronegative. dst_negative_code_mask_toggle_muzero = ff_q_pvs_mask_toggle_muzeronegative * S ((S (0)) * dst_negative_scale_mask_toggle_muzero) + (dst_negative_mask_toggle_muzero))) /\ (exists ge_balance_positive_mask_toggle_muzerovalue ge_balance_negative_mask_toggle_muzerovalue. (((((0) = 2 * (ge_balance_positive_mask_toggle_muzerovalue) /\ (ge_balance_negative_mask_toggle_muzerovalue) = 0) \/ exists ge_signed_half_mask_toggle_muzerovaluedecode. (((0) = 2 * ge_signed_half_mask_toggle_muzerovaluedecode + 1 /\ (ge_balance_positive_mask_toggle_muzerovalue) = 0) /\ (ge_balance_negative_mask_toggle_muzerovalue) = S ge_signed_half_mask_toggle_muzerovaluedecode))) /\ ((dst_positive_mask_toggle_muzero) + ge_balance_negative_mask_toggle_muzerovalue = (dst_negative_mask_toggle_muzero) + ge_balance_positive_mask_toggle_muzerovalue))))))))) /\ (forall mt_index_mask_toggle_mu mt_value_mask_toggle_mu. ~(mt_index_mask_toggle_mu=0) -> (exists pvs_le_gap_mask_toggle_mudomain. pvs_le_gap_mask_toggle_mudomain + (mt_index_mask_toggle_mu) = (N)) -> (exists dst_positive_code_mask_toggle_muentry dst_positive_scale_mask_toggle_muentry dst_negative_code_mask_toggle_muentry dst_negative_scale_mask_toggle_muentry dst_positive_mask_toggle_muentry dst_negative_mask_toggle_muentry. (((M) = (((((dst_positive_code_mask_toggle_muentry) + (dst_positive_scale_mask_toggle_muentry)) * S ((dst_positive_code_mask_toggle_muentry) + (dst_positive_scale_mask_toggle_muentry)) + ((dst_positive_scale_mask_toggle_muentry) + (dst_positive_scale_mask_toggle_muentry))) + (((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) * S ((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) + ((dst_negative_scale_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)))) * S ((((dst_positive_code_mask_toggle_muentry) + (dst_positive_scale_mask_toggle_muentry)) * S ((dst_positive_code_mask_toggle_muentry) + (dst_positive_scale_mask_toggle_muentry)) + ((dst_positive_scale_mask_toggle_muentry) + (dst_positive_scale_mask_toggle_muentry))) + (((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) * S ((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) + ((dst_negative_scale_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)))) + ((((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) * S ((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) + ((dst_negative_scale_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry))) + (((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) * S ((dst_negative_code_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)) + ((dst_negative_scale_mask_toggle_muentry) + (dst_negative_scale_mask_toggle_muentry)))))) /\ (((((exists ff_h_pvs_mask_toggle_muentrypositive. ff_h_pvs_mask_toggle_muentrypositive + S (dst_positive_mask_toggle_muentry) = S ((S (mt_index_mask_toggle_mu)) * dst_positive_scale_mask_toggle_muentry)) /\ exists ff_q_pvs_mask_toggle_muentrypositive. dst_positive_code_mask_toggle_muentry = ff_q_pvs_mask_toggle_muentrypositive * S ((S (mt_index_mask_toggle_mu)) * dst_positive_scale_mask_toggle_muentry) + (dst_positive_mask_toggle_muentry))) /\ (((((exists ff_h_pvs_mask_toggle_muentrynegative. ff_h_pvs_mask_toggle_muentrynegative + S (dst_negative_mask_toggle_muentry) = S ((S (mt_index_mask_toggle_mu)) * dst_negative_scale_mask_toggle_muentry)) /\ exists ff_q_pvs_mask_toggle_muentrynegative. dst_negative_code_mask_toggle_muentry = ff_q_pvs_mask_toggle_muentrynegative * S ((S (mt_index_mask_toggle_mu)) * dst_negative_scale_mask_toggle_muentry) + (dst_negative_mask_toggle_muentry))) /\ (exists ge_balance_positive_mask_toggle_muentryvalue ge_balance_negative_mask_toggle_muentryvalue. (((((mt_value_mask_toggle_mu) = 2 * (ge_balance_positive_mask_toggle_muentryvalue) /\ (ge_balance_negative_mask_toggle_muentryvalue) = 0) \/ exists ge_signed_half_mask_toggle_muentryvaluedecode. (((mt_value_mask_toggle_mu) = 2 * ge_signed_half_mask_toggle_muentryvaluedecode + 1 /\ (ge_balance_positive_mask_toggle_muentryvalue) = 0) /\ (ge_balance_negative_mask_toggle_muentryvalue) = S ge_signed_half_mask_toggle_muentryvaluedecode))) /\ ((dst_positive_mask_toggle_muentry) + ge_balance_negative_mask_toggle_muentryvalue = (dst_negative_mask_toggle_muentry) + ge_balance_positive_mask_toggle_muentryvalue))))))))) -> (((~((mt_index_mask_toggle_mu) = 0)) /\ ((((exists mv_square_prime_mask_toggle_muvaluesquare. ((~((mv_square_prime_mask_toggle_muvaluesquare) = 1) /\ forall pvs_left_mask_toggle_muvaluesquareprime pvs_right_mask_toggle_muvaluesquareprime. (mv_square_prime_mask_toggle_muvaluesquare) = pvs_left_mask_toggle_muvaluesquareprime * pvs_right_mask_toggle_muvaluesquareprime -> pvs_left_mask_toggle_muvaluesquareprime = 1 \/ pvs_right_mask_toggle_muvaluesquareprime = 1) /\ (exists pvs_factor_mask_toggle_muvaluesquaredivisor. (mt_index_mask_toggle_mu) = (mv_square_prime_mask_toggle_muvaluesquare * mv_square_prime_mask_toggle_muvaluesquare) * pvs_factor_mask_toggle_muvaluesquaredivisor))) /\ ((mt_value_mask_toggle_mu) = 0))) \/ (((((~((mt_index_mask_toggle_mu) = 0)) /\ (forall sfd_prime_mask_toggle_muvaluesquarefree. (~((sfd_prime_mask_toggle_muvaluesquarefree) = 1) /\ forall pvs_left_mask_toggle_muvaluesquarefreedomain pvs_right_mask_toggle_muvaluesquarefreedomain. (sfd_prime_mask_toggle_muvaluesquarefree) = pvs_left_mask_toggle_muvaluesquarefreedomain * pvs_right_mask_toggle_muvaluesquarefreedomain -> pvs_left_mask_toggle_muvaluesquarefreedomain = 1 \/ pvs_right_mask_toggle_muvaluesquarefreedomain = 1) -> (exists pvs_le_gap_mask_toggle_muvaluesquarefreebound. pvs_le_gap_mask_toggle_muvaluesquarefreebound + (sfd_prime_mask_toggle_muvaluesquarefree) = (mt_index_mask_toggle_mu)) -> ~(exists pvs_factor_mask_toggle_muvaluesquarefreesquare. (mt_index_mask_toggle_mu) = (sfd_prime_mask_toggle_muvaluesquarefree * sfd_prime_mask_toggle_muvaluesquarefree) * pvs_factor_mask_toggle_muvaluesquarefreesquare)))) /\ (exists mv_factor_code_mask_toggle_muvaluefactors mv_factor_scale_mask_toggle_muvaluefactors mv_factor_count_mask_toggle_muvaluefactors. (((~(mt_index_mask_toggle_mu = 0) /\ ((exists ff_u_fsat_mask_toggle_muvaluefactorsfactorization_product ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product. ((((exists ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_start. ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_start. ff_u_fsat_mask_toggle_muvaluefactorsfactorization_product = ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_terminal. ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_terminal + S (mt_index_mask_toggle_mu) = S ((S (mv_factor_count_mask_toggle_muvaluefactors)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_terminal. ff_u_fsat_mask_toggle_muvaluefactorsfactorization_product = ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_mask_toggle_muvaluefactors)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product) + (mt_index_mask_toggle_mu))) /\ forall ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product. (exists ff_lt_fsat_mask_toggle_muvaluefactorsfactorization_product_bound. ff_lt_fsat_mask_toggle_muvaluefactorsfactorization_product_bound + S ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product = mv_factor_count_mask_toggle_muvaluefactors) -> exists ff_p_fsat_mask_toggle_muvaluefactorsfactorization_product ff_r_fsat_mask_toggle_muvaluefactorsfactorization_product ff_s_fsat_mask_toggle_muvaluefactorsfactorization_product. ((((exists ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_factor. ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_factor + S (ff_p_fsat_mask_toggle_muvaluefactorsfactorization_product) = S ((S (ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product)) * mv_factor_scale_mask_toggle_muvaluefactors)) /\ exists ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_factor. mv_factor_code_mask_toggle_muvaluefactors = ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product)) * mv_factor_scale_mask_toggle_muvaluefactors) + (ff_p_fsat_mask_toggle_muvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_partial. ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_partial + S (ff_r_fsat_mask_toggle_muvaluefactorsfactorization_product) = S ((S (ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_partial. ff_u_fsat_mask_toggle_muvaluefactorsfactorization_product = ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product) + (ff_r_fsat_mask_toggle_muvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_successor. ff_h_fsat_mask_toggle_muvaluefactorsfactorization_product_successor + S (ff_s_fsat_mask_toggle_muvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product)) /\ exists ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_successor. ff_u_fsat_mask_toggle_muvaluefactorsfactorization_product = ff_q_fsat_mask_toggle_muvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_mask_toggle_muvaluefactorsfactorization_product)) * ff_v_fsat_mask_toggle_muvaluefactorsfactorization_product) + (ff_s_fsat_mask_toggle_muvaluefactorsfactorization_product))) /\ ff_s_fsat_mask_toggle_muvaluefactorsfactorization_product = ff_r_fsat_mask_toggle_muvaluefactorsfactorization_product * ff_p_fsat_mask_toggle_muvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_mask_toggle_muvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_mask_toggle_muvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_mask_toggle_muvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_mask_toggle_muvaluefactorsfactorization_primes = (mv_factor_count_mask_toggle_muvaluefactors)) -> exists ftsf_factor_fsat_mask_toggle_muvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_mask_toggle_muvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_mask_toggle_muvaluefactorsfactorization_primes)) * mv_factor_scale_mask_toggle_muvaluefactors)) /\ exists ff_q_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_entry. mv_factor_code_mask_toggle_muvaluefactors = ff_q_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_mask_toggle_muvaluefactorsfactorization_primes)) * mv_factor_scale_mask_toggle_muvaluefactors) + (ftsf_factor_fsat_mask_toggle_muvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_mask_toggle_muvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_mask_toggle_muvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mask_toggle_muvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_mask_toggle_muvaluefactorsparityeven. (mv_factor_count_mask_toggle_muvaluefactors) = 2 * mv_even_half_mask_toggle_muvaluefactorsparityeven) /\ ((mt_value_mask_toggle_mu) = 2))) \/ (((exists mv_odd_half_mask_toggle_muvaluefactorsparityodd. (mv_factor_count_mask_toggle_muvaluefactors) = 2 * mv_odd_half_mask_toggle_muvaluefactorsparityodd + 1) /\ ((mt_value_mask_toggle_mu) = 1)))))))))))))))) -> ~(n=0) -> (exists pvs_le_gap_mask_toggle_N. pvs_le_gap_mask_toggle_N + (n) = (N)) -> (~((p) = 1) /\ forall pvs_left_mask_toggle_prime pvs_right_mask_toggle_prime. (p) = pvs_left_mask_toggle_prime * pvs_right_mask_toggle_prime -> pvs_left_mask_toggle_prime = 1 \/ pvs_right_mask_toggle_prime = 1) -> (exists pvs_factor_mask_toggle_prime_divisor. (n) = (p) * pvs_factor_mask_toggle_prime_divisor) -> (((exists dst_positive_code_mask_toggle_masktable dst_positive_scale_mask_toggle_masktable dst_negative_code_mask_toggle_masktable dst_negative_scale_mask_toggle_masktable. (((K) = (((((dst_positive_code_mask_toggle_masktable) + (dst_positive_scale_mask_toggle_masktable)) * S ((dst_positive_code_mask_toggle_masktable) + (dst_positive_scale_mask_toggle_masktable)) + ((dst_positive_scale_mask_toggle_masktable) + (dst_positive_scale_mask_toggle_masktable))) + (((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) * S ((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) + ((dst_negative_scale_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)))) * S ((((dst_positive_code_mask_toggle_masktable) + (dst_positive_scale_mask_toggle_masktable)) * S ((dst_positive_code_mask_toggle_masktable) + (dst_positive_scale_mask_toggle_masktable)) + ((dst_positive_scale_mask_toggle_masktable) + (dst_positive_scale_mask_toggle_masktable))) + (((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) * S ((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) + ((dst_negative_scale_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)))) + ((((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) * S ((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) + ((dst_negative_scale_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable))) + (((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) * S ((dst_negative_code_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)) + ((dst_negative_scale_mask_toggle_masktable) + (dst_negative_scale_mask_toggle_masktable)))))) /\ (forall dst_index_mask_toggle_masktable. (exists pvs_le_gap_mask_toggle_masktabledomain. pvs_le_gap_mask_toggle_masktabledomain + (dst_index_mask_toggle_masktable) = (n)) -> exists dst_positive_mask_toggle_masktable dst_negative_mask_toggle_masktable dst_value_mask_toggle_masktable. ((((exists ff_h_pvs_mask_toggle_masktableentrypositive. ff_h_pvs_mask_toggle_masktableentrypositive + S (dst_positive_mask_toggle_masktable) = S ((S (dst_index_mask_toggle_masktable)) * dst_positive_scale_mask_toggle_masktable)) /\ exists ff_q_pvs_mask_toggle_masktableentrypositive. dst_positive_code_mask_toggle_masktable = ff_q_pvs_mask_toggle_masktableentrypositive * S ((S (dst_index_mask_toggle_masktable)) * dst_positive_scale_mask_toggle_masktable) + (dst_positive_mask_toggle_masktable))) /\ (((((exists ff_h_pvs_mask_toggle_masktableentrynegative. ff_h_pvs_mask_toggle_masktableentrynegative + S (dst_negative_mask_toggle_masktable) = S ((S (dst_index_mask_toggle_masktable)) * dst_negative_scale_mask_toggle_masktable)) /\ exists ff_q_pvs_mask_toggle_masktableentrynegative. dst_negative_code_mask_toggle_masktable = ff_q_pvs_mask_toggle_masktableentrynegative * S ((S (dst_index_mask_toggle_masktable)) * dst_negative_scale_mask_toggle_masktable) + (dst_negative_mask_toggle_masktable))) /\ (exists ge_balance_positive_mask_toggle_masktableentryvalue ge_balance_negative_mask_toggle_masktableentryvalue. (((((dst_value_mask_toggle_masktable) = 2 * (ge_balance_positive_mask_toggle_masktableentryvalue) /\ (ge_balance_negative_mask_toggle_masktableentryvalue) = 0) \/ exists ge_signed_half_mask_toggle_masktableentryvaluedecode. (((dst_value_mask_toggle_masktable) = 2 * ge_signed_half_mask_toggle_masktableentryvaluedecode + 1 /\ (ge_balance_positive_mask_toggle_masktableentryvalue) = 0) /\ (ge_balance_negative_mask_toggle_masktableentryvalue) = S ge_signed_half_mask_toggle_masktableentryvaluedecode))) /\ ((dst_positive_mask_toggle_masktable) + ge_balance_negative_mask_toggle_masktableentryvalue = (dst_negative_mask_toggle_masktable) + ge_balance_positive_mask_toggle_masktableentryvalue))))))))) /\ (forall dm_index_mask_toggle_mask dm_value_mask_toggle_mask. (exists pvs_le_gap_mask_toggle_maskdomain. pvs_le_gap_mask_toggle_maskdomain + (dm_index_mask_toggle_mask) = (n)) -> (exists dst_positive_code_mask_toggle_masklookup dst_positive_scale_mask_toggle_masklookup dst_negative_code_mask_toggle_masklookup dst_negative_scale_mask_toggle_masklookup dst_positive_mask_toggle_masklookup dst_negative_mask_toggle_masklookup. (((K) = (((((dst_positive_code_mask_toggle_masklookup) + (dst_positive_scale_mask_toggle_masklookup)) * S ((dst_positive_code_mask_toggle_masklookup) + (dst_positive_scale_mask_toggle_masklookup)) + ((dst_positive_scale_mask_toggle_masklookup) + (dst_positive_scale_mask_toggle_masklookup))) + (((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) * S ((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) + ((dst_negative_scale_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)))) * S ((((dst_positive_code_mask_toggle_masklookup) + (dst_positive_scale_mask_toggle_masklookup)) * S ((dst_positive_code_mask_toggle_masklookup) + (dst_positive_scale_mask_toggle_masklookup)) + ((dst_positive_scale_mask_toggle_masklookup) + (dst_positive_scale_mask_toggle_masklookup))) + (((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) * S ((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) + ((dst_negative_scale_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)))) + ((((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) * S ((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) + ((dst_negative_scale_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup))) + (((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) * S ((dst_negative_code_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)) + ((dst_negative_scale_mask_toggle_masklookup) + (dst_negative_scale_mask_toggle_masklookup)))))) /\ (((((exists ff_h_pvs_mask_toggle_masklookuppositive. ff_h_pvs_mask_toggle_masklookuppositive + S (dst_positive_mask_toggle_masklookup) = S ((S (dm_index_mask_toggle_mask)) * dst_positive_scale_mask_toggle_masklookup)) /\ exists ff_q_pvs_mask_toggle_masklookuppositive. dst_positive_code_mask_toggle_masklookup = ff_q_pvs_mask_toggle_masklookuppositive * S ((S (dm_index_mask_toggle_mask)) * dst_positive_scale_mask_toggle_masklookup) + (dst_positive_mask_toggle_masklookup))) /\ (((((exists ff_h_pvs_mask_toggle_masklookupnegative. ff_h_pvs_mask_toggle_masklookupnegative + S (dst_negative_mask_toggle_masklookup) = S ((S (dm_index_mask_toggle_mask)) * dst_negative_scale_mask_toggle_masklookup)) /\ exists ff_q_pvs_mask_toggle_masklookupnegative. dst_negative_code_mask_toggle_masklookup = ff_q_pvs_mask_toggle_masklookupnegative * S ((S (dm_index_mask_toggle_mask)) * dst_negative_scale_mask_toggle_masklookup) + (dst_negative_mask_toggle_masklookup))) /\ (exists ge_balance_positive_mask_toggle_masklookupvalue ge_balance_negative_mask_toggle_masklookupvalue. (((((dm_value_mask_toggle_mask) = 2 * (ge_balance_positive_mask_toggle_masklookupvalue) /\ (ge_balance_negative_mask_toggle_masklookupvalue) = 0) \/ exists ge_signed_half_mask_toggle_masklookupvaluedecode. (((dm_value_mask_toggle_mask) = 2 * ge_signed_half_mask_toggle_masklookupvaluedecode + 1 /\ (ge_balance_positive_mask_toggle_masklookupvalue) = 0) /\ (ge_balance_negative_mask_toggle_masklookupvalue) = S ge_signed_half_mask_toggle_masklookupvaluedecode))) /\ ((dst_positive_mask_toggle_masklookup) + ge_balance_negative_mask_toggle_masklookupvalue = (dst_negative_mask_toggle_masklookup) + ge_balance_positive_mask_toggle_masklookupvalue))))))))) -> ((((~((dm_index_mask_toggle_mask)=0)) /\ (exists dm_quotient_mask_toggle_maskentry. (((n)=(dm_index_mask_toggle_mask)*dm_quotient_mask_toggle_maskentry) /\ (exists dst_positive_code_mask_toggle_maskentryinput dst_positive_scale_mask_toggle_maskentryinput dst_negative_code_mask_toggle_maskentryinput dst_negative_scale_mask_toggle_maskentryinput dst_positive_mask_toggle_maskentryinput dst_negative_mask_toggle_maskentryinput. (((M) = (((((dst_positive_code_mask_toggle_maskentryinput) + (dst_positive_scale_mask_toggle_maskentryinput)) * S ((dst_positive_code_mask_toggle_maskentryinput) + (dst_positive_scale_mask_toggle_maskentryinput)) + ((dst_positive_scale_mask_toggle_maskentryinput) + (dst_positive_scale_mask_toggle_maskentryinput))) + (((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) * S ((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) + ((dst_negative_scale_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)))) * S ((((dst_positive_code_mask_toggle_maskentryinput) + (dst_positive_scale_mask_toggle_maskentryinput)) * S ((dst_positive_code_mask_toggle_maskentryinput) + (dst_positive_scale_mask_toggle_maskentryinput)) + ((dst_positive_scale_mask_toggle_maskentryinput) + (dst_positive_scale_mask_toggle_maskentryinput))) + (((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) * S ((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) + ((dst_negative_scale_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)))) + ((((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) * S ((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) + ((dst_negative_scale_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput))) + (((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) * S ((dst_negative_code_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)) + ((dst_negative_scale_mask_toggle_maskentryinput) + (dst_negative_scale_mask_toggle_maskentryinput)))))) /\ (((((exists ff_h_pvs_mask_toggle_maskentryinputpositive. ff_h_pvs_mask_toggle_maskentryinputpositive + S (dst_positive_mask_toggle_maskentryinput) = S ((S (dm_index_mask_toggle_mask)) * dst_positive_scale_mask_toggle_maskentryinput)) /\ exists ff_q_pvs_mask_toggle_maskentryinputpositive. dst_positive_code_mask_toggle_maskentryinput = ff_q_pvs_mask_toggle_maskentryinputpositive * S ((S (dm_index_mask_toggle_mask)) * dst_positive_scale_mask_toggle_maskentryinput) + (dst_positive_mask_toggle_maskentryinput))) /\ (((((exists ff_h_pvs_mask_toggle_maskentryinputnegative. ff_h_pvs_mask_toggle_maskentryinputnegative + S (dst_negative_mask_toggle_maskentryinput) = S ((S (dm_index_mask_toggle_mask)) * dst_negative_scale_mask_toggle_maskentryinput)) /\ exists ff_q_pvs_mask_toggle_maskentryinputnegative. dst_negative_code_mask_toggle_maskentryinput = ff_q_pvs_mask_toggle_maskentryinputnegative * S ((S (dm_index_mask_toggle_mask)) * dst_negative_scale_mask_toggle_maskentryinput) + (dst_negative_mask_toggle_maskentryinput))) /\ (exists ge_balance_positive_mask_toggle_maskentryinputvalue ge_balance_negative_mask_toggle_maskentryinputvalue. (((((dm_value_mask_toggle_mask) = 2 * (ge_balance_positive_mask_toggle_maskentryinputvalue) /\ (ge_balance_negative_mask_toggle_maskentryinputvalue) = 0) \/ exists ge_signed_half_mask_toggle_maskentryinputvaluedecode. (((dm_value_mask_toggle_mask) = 2 * ge_signed_half_mask_toggle_maskentryinputvaluedecode + 1 /\ (ge_balance_positive_mask_toggle_maskentryinputvalue) = 0) /\ (ge_balance_negative_mask_toggle_maskentryinputvalue) = S ge_signed_half_mask_toggle_maskentryinputvaluedecode))) /\ ((dst_positive_mask_toggle_maskentryinput) + ge_balance_negative_mask_toggle_maskentryinputvalue = (dst_negative_mask_toggle_maskentryinput) + ge_balance_positive_mask_toggle_maskentryinputvalue))))))))))))) \/ ((((dm_index_mask_toggle_mask)=0 \/ ~(exists pvs_factor_mask_toggle_maskentrynondivisor. (n) = (dm_index_mask_toggle_mask) * pvs_factor_mask_toggle_maskentrynondivisor)) /\ ((dm_value_mask_toggle_mask)=0))))))) -> (exists pvs_le_gap_mask_toggle_input. pvs_le_gap_mask_toggle_input + (d) = (n)) -> ((((~((d)=0)) /\ (((exists pvs_factor_mask_toggle_graphdivisor. (n) = (d) * pvs_factor_mask_toggle_graphdivisor) /\ ((((~(exists pvs_factor_mask_toggle_graphtogglefresh_input. (d) = (p) * pvs_factor_mask_toggle_graphtogglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_mask_toggle_graphtogglefresh_output. (e) = (p) * pvs_factor_mask_toggle_graphtogglefresh_output)))) \/ (((exists pvs_factor_mask_toggle_graphtogglesquare. (d) = ((p)*(p)) * pvs_factor_mask_toggle_graphtogglesquare) /\ ((e)=(d)))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_mask_toggle_graphnondivisor. (n) = (d) * pvs_factor_mask_toggle_graphnondivisor)) /\ ((e)=(d))))) -> (exists dst_positive_code_mask_toggle_source dst_positive_scale_mask_toggle_source dst_negative_code_mask_toggle_source dst_negative_scale_mask_toggle_source dst_positive_mask_toggle_source dst_negative_mask_toggle_source. (((K) = (((((dst_positive_code_mask_toggle_source) + (dst_positive_scale_mask_toggle_source)) * S ((dst_positive_code_mask_toggle_source) + (dst_positive_scale_mask_toggle_source)) + ((dst_positive_scale_mask_toggle_source) + (dst_positive_scale_mask_toggle_source))) + (((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) * S ((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) + ((dst_negative_scale_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)))) * S ((((dst_positive_code_mask_toggle_source) + (dst_positive_scale_mask_toggle_source)) * S ((dst_positive_code_mask_toggle_source) + (dst_positive_scale_mask_toggle_source)) + ((dst_positive_scale_mask_toggle_source) + (dst_positive_scale_mask_toggle_source))) + (((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) * S ((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) + ((dst_negative_scale_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)))) + ((((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) * S ((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) + ((dst_negative_scale_mask_toggle_source) + (dst_negative_scale_mask_toggle_source))) + (((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) * S ((dst_negative_code_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)) + ((dst_negative_scale_mask_toggle_source) + (dst_negative_scale_mask_toggle_source)))))) /\ (((((exists ff_h_pvs_mask_toggle_sourcepositive. ff_h_pvs_mask_toggle_sourcepositive + S (dst_positive_mask_toggle_source) = S ((S (d)) * dst_positive_scale_mask_toggle_source)) /\ exists ff_q_pvs_mask_toggle_sourcepositive. dst_positive_code_mask_toggle_source = ff_q_pvs_mask_toggle_sourcepositive * S ((S (d)) * dst_positive_scale_mask_toggle_source) + (dst_positive_mask_toggle_source))) /\ (((((exists ff_h_pvs_mask_toggle_sourcenegative. ff_h_pvs_mask_toggle_sourcenegative + S (dst_negative_mask_toggle_source) = S ((S (d)) * dst_negative_scale_mask_toggle_source)) /\ exists ff_q_pvs_mask_toggle_sourcenegative. dst_negative_code_mask_toggle_source = ff_q_pvs_mask_toggle_sourcenegative * S ((S (d)) * dst_negative_scale_mask_toggle_source) + (dst_negative_mask_toggle_source))) /\ (exists ge_balance_positive_mask_toggle_sourcevalue ge_balance_negative_mask_toggle_sourcevalue. (((((a) = 2 * (ge_balance_positive_mask_toggle_sourcevalue) /\ (ge_balance_negative_mask_toggle_sourcevalue) = 0) \/ exists ge_signed_half_mask_toggle_sourcevaluedecode. (((a) = 2 * ge_signed_half_mask_toggle_sourcevaluedecode + 1 /\ (ge_balance_positive_mask_toggle_sourcevalue) = 0) /\ (ge_balance_negative_mask_toggle_sourcevalue) = S ge_signed_half_mask_toggle_sourcevaluedecode))) /\ ((dst_positive_mask_toggle_source) + ge_balance_negative_mask_toggle_sourcevalue = (dst_negative_mask_toggle_source) + ge_balance_positive_mask_toggle_sourcevalue))))))))) -> (exists dst_positive_code_mask_toggle_target dst_positive_scale_mask_toggle_target dst_negative_code_mask_toggle_target dst_negative_scale_mask_toggle_target dst_positive_mask_toggle_target dst_negative_mask_toggle_target. (((K) = (((((dst_positive_code_mask_toggle_target) + (dst_positive_scale_mask_toggle_target)) * S ((dst_positive_code_mask_toggle_target) + (dst_positive_scale_mask_toggle_target)) + ((dst_positive_scale_mask_toggle_target) + (dst_positive_scale_mask_toggle_target))) + (((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) * S ((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) + ((dst_negative_scale_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)))) * S ((((dst_positive_code_mask_toggle_target) + (dst_positive_scale_mask_toggle_target)) * S ((dst_positive_code_mask_toggle_target) + (dst_positive_scale_mask_toggle_target)) + ((dst_positive_scale_mask_toggle_target) + (dst_positive_scale_mask_toggle_target))) + (((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) * S ((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) + ((dst_negative_scale_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)))) + ((((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) * S ((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) + ((dst_negative_scale_mask_toggle_target) + (dst_negative_scale_mask_toggle_target))) + (((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) * S ((dst_negative_code_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)) + ((dst_negative_scale_mask_toggle_target) + (dst_negative_scale_mask_toggle_target)))))) /\ (((((exists ff_h_pvs_mask_toggle_targetpositive. ff_h_pvs_mask_toggle_targetpositive + S (dst_positive_mask_toggle_target) = S ((S (e)) * dst_positive_scale_mask_toggle_target)) /\ exists ff_q_pvs_mask_toggle_targetpositive. dst_positive_code_mask_toggle_target = ff_q_pvs_mask_toggle_targetpositive * S ((S (e)) * dst_positive_scale_mask_toggle_target) + (dst_positive_mask_toggle_target))) /\ (((((exists ff_h_pvs_mask_toggle_targetnegative. ff_h_pvs_mask_toggle_targetnegative + S (dst_negative_mask_toggle_target) = S ((S (e)) * dst_negative_scale_mask_toggle_target)) /\ exists ff_q_pvs_mask_toggle_targetnegative. dst_negative_code_mask_toggle_target = ff_q_pvs_mask_toggle_targetnegative * S ((S (e)) * dst_negative_scale_mask_toggle_target) + (dst_negative_mask_toggle_target))) /\ (exists ge_balance_positive_mask_toggle_targetvalue ge_balance_negative_mask_toggle_targetvalue. (((((b) = 2 * (ge_balance_positive_mask_toggle_targetvalue) /\ (ge_balance_negative_mask_toggle_targetvalue) = 0) \/ exists ge_signed_half_mask_toggle_targetvaluedecode. (((b) = 2 * ge_signed_half_mask_toggle_targetvaluedecode + 1 /\ (ge_balance_positive_mask_toggle_targetvalue) = 0) /\ (ge_balance_negative_mask_toggle_targetvalue) = S ge_signed_half_mask_toggle_targetvaluedecode))) /\ ((dst_positive_mask_toggle_target) + ge_balance_negative_mask_toggle_targetvalue = (dst_negative_mask_toggle_target) + ge_balance_positive_mask_toggle_targetvalue))))))))) -> (exists mps_positive_mask_toggle_result mps_negative_mask_toggle_result. (((((a) = 2 * (mps_positive_mask_toggle_result) /\ (mps_negative_mask_toggle_result) = 0) \/ exists ge_signed_half_mask_toggle_resultsource. (((a) = 2 * ge_signed_half_mask_toggle_resultsource + 1 /\ (mps_positive_mask_toggle_result) = 0) /\ (mps_negative_mask_toggle_result) = S ge_signed_half_mask_toggle_resultsource))) /\ ((((b) = 2 * (mps_negative_mask_toggle_result) /\ (mps_positive_mask_toggle_result) = 0) \/ exists ge_signed_half_mask_toggle_resulttarget. (((b) = 2 * ge_signed_half_mask_toggle_resulttarget + 1 /\ (mps_negative_mask_toggle_result) = 0) /\ (mps_positive_mask_toggle_result) = S ge_signed_half_mask_toggle_resulttarget)))))

Complete tactic proof in conservative notation

All 124 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

124 script commands · 23 reading checkpoints · 3 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 (5)
divisor prime toggle boundedmobius prime factor toggle negatesmobius divisor mask actual valueprime factor toggle positiveprime factor toggle preserves divisor
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 d
  7. L7
    intro e
  8. L8
    intro a
  9. L9
    intro b
  10. L10
    intro hmu
02Fix variables and assumptionsL11–19

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

  1. L11
    intro hn
  2. L12
    intro hnN
  3. L13
    intro hp
  4. L14
    intro hpn
  5. L15
    intro hm
  6. L16
    intro hd
  7. L17
    intro ht
  8. L18
    intro ha
  9. L19
    intro hb
03Establish heL20–29

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

  1. L20
  2. L21
    specialize divisor_prime_toggle_bounded (n)
  3. L22
    specialize divisor_prime_toggle_bounded (p)
  4. L23
    specialize divisor_prime_toggle_bounded (d)
  5. L24
    specialize divisor_prime_toggle_bounded (e)
  6. L25
    apply divisor_prime_toggle_bounded
  7. L26
    exact hn
  8. L27
    exact hp
  9. L28
    exact hpn
  10. L29
    exact hd
04Use earlier factsL30–30

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

  1. L30
    exact ht
05Separate the logical casesL31–33

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

  1. L31
    cases ht
  2. L32
    cases ht_left
  3. L33
    cases ht_left_right
06Use earlier factsL34–43

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

  1. L34
    specialize mobius_prime_factor_toggle_negates (p)
  2. L35
    specialize mobius_prime_factor_toggle_negates (d)
  3. L36
    specialize mobius_prime_factor_toggle_negates (e)
  4. L37
    specialize mobius_prime_factor_toggle_negates (a)
  5. L38
    specialize mobius_prime_factor_toggle_negates (b)
  6. L39
    apply mobius_prime_factor_toggle_negates
  7. L40
    exact hp
  8. L41
    exact ht_left_right_right
  9. L42
    specialize mobius_divisor_mask_actual_value (N)
  10. L43
    specialize mobius_divisor_mask_actual_value (M)
07Use earlier factsL44–53

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

  1. L44
    specialize mobius_divisor_mask_actual_value (n)
  2. L45
    specialize mobius_divisor_mask_actual_value (K)
  3. L46
    specialize mobius_divisor_mask_actual_value (d)
  4. L47
    specialize mobius_divisor_mask_actual_value (a)
  5. L48
    apply mobius_divisor_mask_actual_value
  6. L49
    exact hmu
  7. L50
    exact hnN
  8. L51
    exact hm
  9. L52
    exact ht_left_left
  10. L53
    exact ht_left_right_left
08Use earlier factsL54–63

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

  1. L54
    exact hd
  2. L55
    exact ha
  3. L56
    specialize mobius_divisor_mask_actual_value (N)
  4. L57
    specialize mobius_divisor_mask_actual_value (M)
  5. L58
    specialize mobius_divisor_mask_actual_value (n)
  6. L59
    specialize mobius_divisor_mask_actual_value (K)
  7. L60
    specialize mobius_divisor_mask_actual_value (e)
  8. L61
    specialize mobius_divisor_mask_actual_value (b)
  9. L62
    apply mobius_divisor_mask_actual_value
  10. L63
    exact hmu
09Use earlier factsL64–65

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

  1. L64
    exact hnN
  2. L65
    exact hm
10Fix variables and assumptionsL66–66

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

  1. L66
    intro hezero
11Use earlier factsL67–70

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

  1. L67
    specialize prime_factor_toggle_positive (p)
  2. L68
    specialize prime_factor_toggle_positive (d)
  3. L69
    specialize prime_factor_toggle_positive (e)
  4. L70
    apply prime_factor_toggle_positive
12Fix variables and assumptionsL71–71

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

  1. L71
    intro hpzero
13Use earlier factsL72–81

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

  1. L72
    specialize prime_nonzero (p)
  2. L73
    apply prime_nonzero
  3. L74
    exact hp
  4. L75
    exact hpzero
  5. L76
    exact ht_left_left
  6. L77
    exact ht_left_right_right
  7. L78
    exact hezero
  8. L79
    specialize prime_factor_toggle_preserves_divisor (p)
  9. L80
    specialize prime_factor_toggle_preserves_divisor (n)
  10. L81
    specialize prime_factor_toggle_preserves_divisor (d)
14Use earlier factsL82–89

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

  1. L82
    specialize prime_factor_toggle_preserves_divisor (e)
  2. L83
    apply prime_factor_toggle_preserves_divisor
  3. L84
    exact hp
  4. L85
    exact hpn
  5. L86
    exact ht_left_right_left
  6. L87
    exact ht_left_right_right
  7. L88
    exact he
  8. L89
    exact hb
15Separate the logical casesL90–91

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

  1. L90
    cases ht_right
  2. L91
    cases hm
16Establish hzeroaL92–101

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor mask entry omitted value.

  1. L92
    have hzeroa : a=0
  2. L93
    specialize divisor_mask_entry_omitted_value (M)
  3. L94
    specialize divisor_mask_entry_omitted_value (n)
  4. L95
    specialize divisor_mask_entry_omitted_value (d)
  5. L96
    specialize divisor_mask_entry_omitted_value (a)
  6. L97
    apply divisor_mask_entry_omitted_value
  7. L98
    exact ht_right_left
  8. L99
    specialize hm_right (d)
  9. L100
    specialize hm_right (a)
  10. L101
    apply hm_right
17Use earlier factsL102–103

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

  1. L102
    exact hd
  2. L103
    exact ha
18Establish hzerobL104–113

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor mask entry omitted value.

  1. L104
    have hzerob : b=0
  2. L105
    specialize divisor_mask_entry_omitted_value (M)
  3. L106
    specialize divisor_mask_entry_omitted_value (n)
  4. L107
    specialize divisor_mask_entry_omitted_value (d)
  5. L108
    specialize divisor_mask_entry_omitted_value (b)
  6. L109
    apply divisor_mask_entry_omitted_value
  7. L110
    exact ht_right_left
  8. L111
    specialize hm_right (d)
  9. L112
    specialize hm_right (b)
  10. L113
    apply hm_right
19Use earlier factsL114–114

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

  1. L114
    exact hd
20Calculate and transport equalitiesL115–118

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

  1. L115
    rewrite ht_right_right at hb
  2. L116
    rewrite ht_right_right at hb
  3. L117
    rewrite ht_right_right at hb
  4. L118
    rewrite ht_right_right at hb
21Use earlier factsL119–119

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

  1. L119
    exact hb
22Calculate and transport equalitiesL120–123

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

  1. L120
    rewrite hzeroa
  2. L121
    rewrite hzeroa
  3. L122
    rewrite hzerob
  4. L123
    rewrite hzerob
23Use earlier factsL124–124

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

  1. L124
    apply signed_negate_zero

Library-wide reading audit

Original defined command ledger · 124 lines
  1. 0001intro N
  2. 0002intro M
  3. 0003intro n
  4. 0004intro K
  5. 0005intro p
  6. 0006intro d
  7. 0007intro e
  8. 0008intro a
  9. 0009intro b
  10. 0010intro hmu
  11. 0011intro hn
  12. 0012intro hnN
  13. 0013intro hp
  14. 0014intro hpn
  15. 0015intro hm
  16. 0016intro hd
  17. 0017intro ht
  18. 0018intro ha
  19. 0019intro hb
  20. 0020have he : Le(e,n)
  21. 0021specialize divisor_prime_toggle_bounded (n)
  22. 0022specialize divisor_prime_toggle_bounded (p)
  23. 0023specialize divisor_prime_toggle_bounded (d)
  24. 0024specialize divisor_prime_toggle_bounded (e)
  25. 0025apply divisor_prime_toggle_bounded
  26. 0026exact hn
  27. 0027exact hp
  28. 0028exact hpn
  29. 0029exact hd
  30. 0030exact ht
  31. 0031cases ht
  32. 0032cases ht_left
  33. 0033cases ht_left_right
  34. 0034specialize mobius_prime_factor_toggle_negates (p)
  35. 0035specialize mobius_prime_factor_toggle_negates (d)
  36. 0036specialize mobius_prime_factor_toggle_negates (e)
  37. 0037specialize mobius_prime_factor_toggle_negates (a)
  38. 0038specialize mobius_prime_factor_toggle_negates (b)
  39. 0039apply mobius_prime_factor_toggle_negates
  40. 0040exact hp
  41. 0041exact ht_left_right_right
  42. 0042specialize mobius_divisor_mask_actual_value (N)
  43. 0043specialize mobius_divisor_mask_actual_value (M)
  44. 0044specialize mobius_divisor_mask_actual_value (n)
  45. 0045specialize mobius_divisor_mask_actual_value (K)
  46. 0046specialize mobius_divisor_mask_actual_value (d)
  47. 0047specialize mobius_divisor_mask_actual_value (a)
  48. 0048apply mobius_divisor_mask_actual_value
  49. 0049exact hmu
  50. 0050exact hnN
  51. 0051exact hm
  52. 0052exact ht_left_left
  53. 0053exact ht_left_right_left
  54. 0054exact hd
  55. 0055exact ha
  56. 0056specialize mobius_divisor_mask_actual_value (N)
  57. 0057specialize mobius_divisor_mask_actual_value (M)
  58. 0058specialize mobius_divisor_mask_actual_value (n)
  59. 0059specialize mobius_divisor_mask_actual_value (K)
  60. 0060specialize mobius_divisor_mask_actual_value (e)
  61. 0061specialize mobius_divisor_mask_actual_value (b)
  62. 0062apply mobius_divisor_mask_actual_value
  63. 0063exact hmu
  64. 0064exact hnN
  65. 0065exact hm
  66. 0066intro hezero
  67. 0067specialize prime_factor_toggle_positive (p)
  68. 0068specialize prime_factor_toggle_positive (d)
  69. 0069specialize prime_factor_toggle_positive (e)
  70. 0070apply prime_factor_toggle_positive
  71. 0071intro hpzero
  72. 0072specialize prime_nonzero (p)
  73. 0073apply prime_nonzero
  74. 0074exact hp
  75. 0075exact hpzero
  76. 0076exact ht_left_left
  77. 0077exact ht_left_right_right
  78. 0078exact hezero
  79. 0079specialize prime_factor_toggle_preserves_divisor (p)
  80. 0080specialize prime_factor_toggle_preserves_divisor (n)
  81. 0081specialize prime_factor_toggle_preserves_divisor (d)
  82. 0082specialize prime_factor_toggle_preserves_divisor (e)
  83. 0083apply prime_factor_toggle_preserves_divisor
  84. 0084exact hp
  85. 0085exact hpn
  86. 0086exact ht_left_right_left
  87. 0087exact ht_left_right_right
  88. 0088exact he
  89. 0089exact hb
  90. 0090cases ht_right
  91. 0091cases hm
  92. 0092have hzeroa : a=0
  93. 0093specialize divisor_mask_entry_omitted_value (M)
  94. 0094specialize divisor_mask_entry_omitted_value (n)
  95. 0095specialize divisor_mask_entry_omitted_value (d)
  96. 0096specialize divisor_mask_entry_omitted_value (a)
  97. 0097apply divisor_mask_entry_omitted_value
  98. 0098exact ht_right_left
  99. 0099specialize hm_right (d)
  100. 0100specialize hm_right (a)
  101. 0101apply hm_right
  102. 0102exact hd
  103. 0103exact ha
  104. 0104have hzerob : b=0
  105. 0105specialize divisor_mask_entry_omitted_value (M)
  106. 0106specialize divisor_mask_entry_omitted_value (n)
  107. 0107specialize divisor_mask_entry_omitted_value (d)
  108. 0108specialize divisor_mask_entry_omitted_value (b)
  109. 0109apply divisor_mask_entry_omitted_value
  110. 0110exact ht_right_left
  111. 0111specialize hm_right (d)
  112. 0112specialize hm_right (b)
  113. 0113apply hm_right
  114. 0114exact hd
  115. 0115rewrite ht_right_right at hb
  116. 0116rewrite ht_right_right at hb
  117. 0117rewrite ht_right_right at hb
  118. 0118rewrite ht_right_right at hb
  119. 0119exact hb
  120. 0120rewrite hzeroa
  121. 0121rewrite hzeroa
  122. 0122rewrite hzerob
  123. 0123rewrite hzerob
  124. 0124apply signed_negate_zero