Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.
Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable
041f1a3471002ff3cd5fc3da2a6cc751ad2f4a4458a497b3de2a26276fd314b8.18cc5aef4d4710a09bd8f2eac063ae2ccf54049a68eaab33d6b9ce7df87af9e0f6fe75aa8e5c899baff761edea21dc82a3b76ea52ef165511d20f34a6d332af7Bundle node 215; exact statement SHA-256 813b3e387681b8430c9679903198ae7a2c996d215f7877cee0fc2d4a1a2a6365
forall n. exists z. ((((exists mv_even_half_totaleven. (n) = 2 * mv_even_half_totaleven) /\ ((z) = 2))) \/ (((exists mv_odd_half_totalodd. (n) = 2 * mv_odd_half_totalodd + 1) /\ ((z) = 1))))
Bundle node 216; exact statement SHA-256 5194ebe1bcf99180157a8957f1b97f1e7ec332599fb5ccb495d6e64710c22e73
forall n a b. ((((exists mv_even_half_firsteven. (n) = 2 * mv_even_half_firsteven) /\ ((a) = 2))) \/ (((exists mv_odd_half_firstodd. (n) = 2 * mv_odd_half_firstodd + 1) /\ ((a) = 1)))) -> ((((exists mv_even_half_secondeven. (n) = 2 * mv_even_half_secondeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_secondodd. (n) = 2 * mv_odd_half_secondodd + 1) /\ ((b) = 1)))) -> a = b
Bundle node 217; exact statement SHA-256 b1bef2aff69743b2b7e49803648f233d7919ebb4770a60287c8c895a41c79b27
(((exists mv_even_half_zeroeven. (0) = 2 * mv_even_half_zeroeven) /\ ((2) = 2))) \/ (((exists mv_odd_half_zeroodd. (0) = 2 * mv_odd_half_zeroodd + 1) /\ ((2) = 1)))
Bundle node 218; exact statement SHA-256 fe8496e776d5a018527080e6bfe82b2bc67ef992506572a1787bd58fbbb1f3c8
forall n b c l d e m. ((~(n = 0) /\ ((exists ff_u_fsat_mv_count_first_product ff_v_fsat_mv_count_first_product. ((((exists ff_h_fsat_mv_count_first_product_start. ff_h_fsat_mv_count_first_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_count_first_product)) /\ exists ff_q_fsat_mv_count_first_product_start. ff_u_fsat_mv_count_first_product = ff_q_fsat_mv_count_first_product_start * S ((S (0)) * ff_v_fsat_mv_count_first_product) + (1))) /\ ((((exists ff_h_fsat_mv_count_first_product_terminal. ff_h_fsat_mv_count_first_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mv_count_first_product)) /\ exists ff_q_fsat_mv_count_first_product_terminal. ff_u_fsat_mv_count_first_product = ff_q_fsat_mv_count_first_product_terminal * S ((S (l)) * ff_v_fsat_mv_count_first_product) + (n))) /\ forall ff_i_fsat_mv_count_first_product. (exists ff_lt_fsat_mv_count_first_product_bound. ff_lt_fsat_mv_count_first_product_bound + S ff_i_fsat_mv_count_first_product = l) -> exists ff_p_fsat_mv_count_first_product ff_r_fsat_mv_count_first_product ff_s_fsat_mv_count_first_product. ((((exists ff_h_fsat_mv_count_first_product_factor. ff_h_fsat_mv_count_first_product_factor + S (ff_p_fsat_mv_count_first_product) = S ((S (ff_i_fsat_mv_count_first_product)) * c)) /\ exists ff_q_fsat_mv_count_first_product_factor. b = ff_q_fsat_mv_count_first_product_factor * S ((S (ff_i_fsat_mv_count_first_product)) * c) + (ff_p_fsat_mv_count_first_product))) /\ ((((exists ff_h_fsat_mv_count_first_product_partial. ff_h_fsat_mv_count_first_product_partial + S (ff_r_fsat_mv_count_first_product) = S ((S (ff_i_fsat_mv_count_first_product)) * ff_v_fsat_mv_count_first_product)) /\ exists ff_q_fsat_mv_count_first_product_partial. ff_u_fsat_mv_count_first_product = ff_q_fsat_mv_count_first_product_partial * S ((S (ff_i_fsat_mv_count_first_product)) * ff_v_fsat_mv_count_first_product) + (ff_r_fsat_mv_count_first_product))) /\ ((((exists ff_h_fsat_mv_count_first_product_successor. ff_h_fsat_mv_count_first_product_successor + S (ff_s_fsat_mv_count_first_product) = S ((S (S ff_i_fsat_mv_count_first_product)) * ff_v_fsat_mv_count_first_product)) /\ exists ff_q_fsat_mv_count_first_product_successor. ff_u_fsat_mv_count_first_product = ff_q_fsat_mv_count_first_product_successor * S ((S (S ff_i_fsat_mv_count_first_product)) * ff_v_fsat_mv_count_first_product) + (ff_s_fsat_mv_count_first_product))) /\ ff_s_fsat_mv_count_first_product = ff_r_fsat_mv_count_first_product * ff_p_fsat_mv_count_first_product)))))) /\ (forall ftsf_index_fsat_mv_count_first_primes. (exists ftsf_gap_fsat_mv_count_first_primes_bound. ftsf_gap_fsat_mv_count_first_primes_bound + S ftsf_index_fsat_mv_count_first_primes = (l)) -> exists ftsf_factor_fsat_mv_count_first_primes. ((((exists ff_h_ftsf_fsat_mv_count_first_primes_entry. ff_h_ftsf_fsat_mv_count_first_primes_entry + S (ftsf_factor_fsat_mv_count_first_primes) = S ((S (ftsf_index_fsat_mv_count_first_primes)) * c)) /\ exists ff_q_ftsf_fsat_mv_count_first_primes_entry. b = ff_q_ftsf_fsat_mv_count_first_primes_entry * S ((S (ftsf_index_fsat_mv_count_first_primes)) * c) + (ftsf_factor_fsat_mv_count_first_primes))) /\ ((~(ftsf_factor_fsat_mv_count_first_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_count_first_primes_prime frm_prime_right_ftsf_fsat_mv_count_first_primes_prime. ftsf_factor_fsat_mv_count_first_primes = frm_prime_left_ftsf_fsat_mv_count_first_primes_prime * frm_prime_right_ftsf_fsat_mv_count_first_primes_prime -> frm_prime_left_ftsf_fsat_mv_count_first_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_count_first_primes_prime = 1))))))) -> ((~(n = 0) /\ ((exists ff_u_fsat_mv_count_second_product ff_v_fsat_mv_count_second_product. ((((exists ff_h_fsat_mv_count_second_product_start. ff_h_fsat_mv_count_second_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_count_second_product)) /\ exists ff_q_fsat_mv_count_second_product_start. ff_u_fsat_mv_count_second_product = ff_q_fsat_mv_count_second_product_start * S ((S (0)) * ff_v_fsat_mv_count_second_product) + (1))) /\ ((((exists ff_h_fsat_mv_count_second_product_terminal. ff_h_fsat_mv_count_second_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_mv_count_second_product)) /\ exists ff_q_fsat_mv_count_second_product_terminal. ff_u_fsat_mv_count_second_product = ff_q_fsat_mv_count_second_product_terminal * S ((S (m)) * ff_v_fsat_mv_count_second_product) + (n))) /\ forall ff_i_fsat_mv_count_second_product. (exists ff_lt_fsat_mv_count_second_product_bound. ff_lt_fsat_mv_count_second_product_bound + S ff_i_fsat_mv_count_second_product = m) -> exists ff_p_fsat_mv_count_second_product ff_r_fsat_mv_count_second_product ff_s_fsat_mv_count_second_product. ((((exists ff_h_fsat_mv_count_second_product_factor. ff_h_fsat_mv_count_second_product_factor + S (ff_p_fsat_mv_count_second_product) = S ((S (ff_i_fsat_mv_count_second_product)) * e)) /\ exists ff_q_fsat_mv_count_second_product_factor. d = ff_q_fsat_mv_count_second_product_factor * S ((S (ff_i_fsat_mv_count_second_product)) * e) + (ff_p_fsat_mv_count_second_product))) /\ ((((exists ff_h_fsat_mv_count_second_product_partial. ff_h_fsat_mv_count_second_product_partial + S (ff_r_fsat_mv_count_second_product) = S ((S (ff_i_fsat_mv_count_second_product)) * ff_v_fsat_mv_count_second_product)) /\ exists ff_q_fsat_mv_count_second_product_partial. ff_u_fsat_mv_count_second_product = ff_q_fsat_mv_count_second_product_partial * S ((S (ff_i_fsat_mv_count_second_product)) * ff_v_fsat_mv_count_second_product) + (ff_r_fsat_mv_count_second_product))) /\ ((((exists ff_h_fsat_mv_count_second_product_successor. ff_h_fsat_mv_count_second_product_successor + S (ff_s_fsat_mv_count_second_product) = S ((S (S ff_i_fsat_mv_count_second_product)) * ff_v_fsat_mv_count_second_product)) /\ exists ff_q_fsat_mv_count_second_product_successor. ff_u_fsat_mv_count_second_product = ff_q_fsat_mv_count_second_product_successor * S ((S (S ff_i_fsat_mv_count_second_product)) * ff_v_fsat_mv_count_second_product) + (ff_s_fsat_mv_count_second_product))) /\ ff_s_fsat_mv_count_second_product = ff_r_fsat_mv_count_second_product * ff_p_fsat_mv_count_second_product)))))) /\ (forall ftsf_index_fsat_mv_count_second_primes. (exists ftsf_gap_fsat_mv_count_second_primes_bound. ftsf_gap_fsat_mv_count_second_primes_bound + S ftsf_index_fsat_mv_count_second_primes = (m)) -> exists ftsf_factor_fsat_mv_count_second_primes. ((((exists ff_h_ftsf_fsat_mv_count_second_primes_entry. ff_h_ftsf_fsat_mv_count_second_primes_entry + S (ftsf_factor_fsat_mv_count_second_primes) = S ((S (ftsf_index_fsat_mv_count_second_primes)) * e)) /\ exists ff_q_ftsf_fsat_mv_count_second_primes_entry. d = ff_q_ftsf_fsat_mv_count_second_primes_entry * S ((S (ftsf_index_fsat_mv_count_second_primes)) * e) + (ftsf_factor_fsat_mv_count_second_primes))) /\ ((~(ftsf_factor_fsat_mv_count_second_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_count_second_primes_prime frm_prime_right_ftsf_fsat_mv_count_second_primes_prime. ftsf_factor_fsat_mv_count_second_primes = frm_prime_left_ftsf_fsat_mv_count_second_primes_prime * frm_prime_right_ftsf_fsat_mv_count_second_primes_prime -> frm_prime_left_ftsf_fsat_mv_count_second_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_count_second_primes_prime = 1))))))) -> l = m
Bundle node 219; exact statement SHA-256 241850395062196a80457ae78195e0c967327a45c465701e9e0191d60dcf143d
forall n z. (((~((n) = 0)) /\ ((((exists mv_square_prime_positivesquare. ((~((mv_square_prime_positivesquare) = 1) /\ forall pvs_left_positivesquareprime pvs_right_positivesquareprime. (mv_square_prime_positivesquare) = pvs_left_positivesquareprime * pvs_right_positivesquareprime -> pvs_left_positivesquareprime = 1 \/ pvs_right_positivesquareprime = 1) /\ (exists pvs_factor_positivesquaredivisor. (n) = (mv_square_prime_positivesquare * mv_square_prime_positivesquare) * pvs_factor_positivesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_positivesquarefree. (~((sfd_prime_positivesquarefree) = 1) /\ forall pvs_left_positivesquarefreedomain pvs_right_positivesquarefreedomain. (sfd_prime_positivesquarefree) = pvs_left_positivesquarefreedomain * pvs_right_positivesquarefreedomain -> pvs_left_positivesquarefreedomain = 1 \/ pvs_right_positivesquarefreedomain = 1) -> (exists pvs_le_gap_positivesquarefreebound. pvs_le_gap_positivesquarefreebound + (sfd_prime_positivesquarefree) = (n)) -> ~(exists pvs_factor_positivesquarefreesquare. (n) = (sfd_prime_positivesquarefree * sfd_prime_positivesquarefree) * pvs_factor_positivesquarefreesquare)))) /\ (exists mv_factor_code_positivefactors mv_factor_scale_positivefactors mv_factor_count_positivefactors. (((~(n = 0) /\ ((exists ff_u_fsat_positivefactorsfactorization_product ff_v_fsat_positivefactorsfactorization_product. ((((exists ff_h_fsat_positivefactorsfactorization_product_start. ff_h_fsat_positivefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_start. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_positivefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_positivefactorsfactorization_product_terminal. ff_h_fsat_positivefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_positivefactors)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_terminal. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_terminal * S ((S (mv_factor_count_positivefactors)) * ff_v_fsat_positivefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_positivefactorsfactorization_product. (exists ff_lt_fsat_positivefactorsfactorization_product_bound. ff_lt_fsat_positivefactorsfactorization_product_bound + S ff_i_fsat_positivefactorsfactorization_product = mv_factor_count_positivefactors) -> exists ff_p_fsat_positivefactorsfactorization_product ff_r_fsat_positivefactorsfactorization_product ff_s_fsat_positivefactorsfactorization_product. ((((exists ff_h_fsat_positivefactorsfactorization_product_factor. ff_h_fsat_positivefactorsfactorization_product_factor + S (ff_p_fsat_positivefactorsfactorization_product) = S ((S (ff_i_fsat_positivefactorsfactorization_product)) * mv_factor_scale_positivefactors)) /\ exists ff_q_fsat_positivefactorsfactorization_product_factor. mv_factor_code_positivefactors = ff_q_fsat_positivefactorsfactorization_product_factor * S ((S (ff_i_fsat_positivefactorsfactorization_product)) * mv_factor_scale_positivefactors) + (ff_p_fsat_positivefactorsfactorization_product))) /\ ((((exists ff_h_fsat_positivefactorsfactorization_product_partial. ff_h_fsat_positivefactorsfactorization_product_partial + S (ff_r_fsat_positivefactorsfactorization_product) = S ((S (ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_partial. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_partial * S ((S (ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product) + (ff_r_fsat_positivefactorsfactorization_product))) /\ ((((exists ff_h_fsat_positivefactorsfactorization_product_successor. ff_h_fsat_positivefactorsfactorization_product_successor + S (ff_s_fsat_positivefactorsfactorization_product) = S ((S (S ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product)) /\ exists ff_q_fsat_positivefactorsfactorization_product_successor. ff_u_fsat_positivefactorsfactorization_product = ff_q_fsat_positivefactorsfactorization_product_successor * S ((S (S ff_i_fsat_positivefactorsfactorization_product)) * ff_v_fsat_positivefactorsfactorization_product) + (ff_s_fsat_positivefactorsfactorization_product))) /\ ff_s_fsat_positivefactorsfactorization_product = ff_r_fsat_positivefactorsfactorization_product * ff_p_fsat_positivefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_positivefactorsfactorization_primes. (exists ftsf_gap_fsat_positivefactorsfactorization_primes_bound. ftsf_gap_fsat_positivefactorsfactorization_primes_bound + S ftsf_index_fsat_positivefactorsfactorization_primes = (mv_factor_count_positivefactors)) -> exists ftsf_factor_fsat_positivefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_positivefactorsfactorization_primes_entry. ff_h_ftsf_fsat_positivefactorsfactorization_primes_entry + S (ftsf_factor_fsat_positivefactorsfactorization_primes) = S ((S (ftsf_index_fsat_positivefactorsfactorization_primes)) * mv_factor_scale_positivefactors)) /\ exists ff_q_ftsf_fsat_positivefactorsfactorization_primes_entry. mv_factor_code_positivefactors = ff_q_ftsf_fsat_positivefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_positivefactorsfactorization_primes)) * mv_factor_scale_positivefactors) + (ftsf_factor_fsat_positivefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_positivefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_positivefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_positivefactorsfactorization_primes_prime. ftsf_factor_fsat_positivefactorsfactorization_primes = frm_prime_left_ftsf_fsat_positivefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_positivefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_positivefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_positivefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_positivefactorsparityeven. (mv_factor_count_positivefactors) = 2 * mv_even_half_positivefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_positivefactorsparityodd. (mv_factor_count_positivefactors) = 2 * mv_odd_half_positivefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> ~(n = 0)
Bundle node 220; exact statement SHA-256 59a34d9fef563bfde51da513e76b88f3a368ce67aaf93b5d4bf1dca8d6505fe2
forall z. (((~((0) = 0)) /\ ((((exists mv_square_prime_zero_excludedsquare. ((~((mv_square_prime_zero_excludedsquare) = 1) /\ forall pvs_left_zero_excludedsquareprime pvs_right_zero_excludedsquareprime. (mv_square_prime_zero_excludedsquare) = pvs_left_zero_excludedsquareprime * pvs_right_zero_excludedsquareprime -> pvs_left_zero_excludedsquareprime = 1 \/ pvs_right_zero_excludedsquareprime = 1) /\ (exists pvs_factor_zero_excludedsquaredivisor. (0) = (mv_square_prime_zero_excludedsquare * mv_square_prime_zero_excludedsquare) * pvs_factor_zero_excludedsquaredivisor))) /\ ((z) = 0))) \/ (((((~((0) = 0)) /\ (forall sfd_prime_zero_excludedsquarefree. (~((sfd_prime_zero_excludedsquarefree) = 1) /\ forall pvs_left_zero_excludedsquarefreedomain pvs_right_zero_excludedsquarefreedomain. (sfd_prime_zero_excludedsquarefree) = pvs_left_zero_excludedsquarefreedomain * pvs_right_zero_excludedsquarefreedomain -> pvs_left_zero_excludedsquarefreedomain = 1 \/ pvs_right_zero_excludedsquarefreedomain = 1) -> (exists pvs_le_gap_zero_excludedsquarefreebound. pvs_le_gap_zero_excludedsquarefreebound + (sfd_prime_zero_excludedsquarefree) = (0)) -> ~(exists pvs_factor_zero_excludedsquarefreesquare. (0) = (sfd_prime_zero_excludedsquarefree * sfd_prime_zero_excludedsquarefree) * pvs_factor_zero_excludedsquarefreesquare)))) /\ (exists mv_factor_code_zero_excludedfactors mv_factor_scale_zero_excludedfactors mv_factor_count_zero_excludedfactors. (((~(0 = 0) /\ ((exists ff_u_fsat_zero_excludedfactorsfactorization_product ff_v_fsat_zero_excludedfactorsfactorization_product. ((((exists ff_h_fsat_zero_excludedfactorsfactorization_product_start. ff_h_fsat_zero_excludedfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_zero_excludedfactorsfactorization_product)) /\ exists ff_q_fsat_zero_excludedfactorsfactorization_product_start. ff_u_fsat_zero_excludedfactorsfactorization_product = ff_q_fsat_zero_excludedfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_zero_excludedfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_zero_excludedfactorsfactorization_product_terminal. ff_h_fsat_zero_excludedfactorsfactorization_product_terminal + S (0) = S ((S (mv_factor_count_zero_excludedfactors)) * ff_v_fsat_zero_excludedfactorsfactorization_product)) /\ exists ff_q_fsat_zero_excludedfactorsfactorization_product_terminal. ff_u_fsat_zero_excludedfactorsfactorization_product = ff_q_fsat_zero_excludedfactorsfactorization_product_terminal * S ((S (mv_factor_count_zero_excludedfactors)) * ff_v_fsat_zero_excludedfactorsfactorization_product) + (0))) /\ forall ff_i_fsat_zero_excludedfactorsfactorization_product. (exists ff_lt_fsat_zero_excludedfactorsfactorization_product_bound. ff_lt_fsat_zero_excludedfactorsfactorization_product_bound + S ff_i_fsat_zero_excludedfactorsfactorization_product = mv_factor_count_zero_excludedfactors) -> exists ff_p_fsat_zero_excludedfactorsfactorization_product ff_r_fsat_zero_excludedfactorsfactorization_product ff_s_fsat_zero_excludedfactorsfactorization_product. ((((exists ff_h_fsat_zero_excludedfactorsfactorization_product_factor. ff_h_fsat_zero_excludedfactorsfactorization_product_factor + S (ff_p_fsat_zero_excludedfactorsfactorization_product) = S ((S (ff_i_fsat_zero_excludedfactorsfactorization_product)) * mv_factor_scale_zero_excludedfactors)) /\ exists ff_q_fsat_zero_excludedfactorsfactorization_product_factor. mv_factor_code_zero_excludedfactors = ff_q_fsat_zero_excludedfactorsfactorization_product_factor * S ((S (ff_i_fsat_zero_excludedfactorsfactorization_product)) * mv_factor_scale_zero_excludedfactors) + (ff_p_fsat_zero_excludedfactorsfactorization_product))) /\ ((((exists ff_h_fsat_zero_excludedfactorsfactorization_product_partial. ff_h_fsat_zero_excludedfactorsfactorization_product_partial + S (ff_r_fsat_zero_excludedfactorsfactorization_product) = S ((S (ff_i_fsat_zero_excludedfactorsfactorization_product)) * ff_v_fsat_zero_excludedfactorsfactorization_product)) /\ exists ff_q_fsat_zero_excludedfactorsfactorization_product_partial. ff_u_fsat_zero_excludedfactorsfactorization_product = ff_q_fsat_zero_excludedfactorsfactorization_product_partial * S ((S (ff_i_fsat_zero_excludedfactorsfactorization_product)) * ff_v_fsat_zero_excludedfactorsfactorization_product) + (ff_r_fsat_zero_excludedfactorsfactorization_product))) /\ ((((exists ff_h_fsat_zero_excludedfactorsfactorization_product_successor. ff_h_fsat_zero_excludedfactorsfactorization_product_successor + S (ff_s_fsat_zero_excludedfactorsfactorization_product) = S ((S (S ff_i_fsat_zero_excludedfactorsfactorization_product)) * ff_v_fsat_zero_excludedfactorsfactorization_product)) /\ exists ff_q_fsat_zero_excludedfactorsfactorization_product_successor. ff_u_fsat_zero_excludedfactorsfactorization_product = ff_q_fsat_zero_excludedfactorsfactorization_product_successor * S ((S (S ff_i_fsat_zero_excludedfactorsfactorization_product)) * ff_v_fsat_zero_excludedfactorsfactorization_product) + (ff_s_fsat_zero_excludedfactorsfactorization_product))) /\ ff_s_fsat_zero_excludedfactorsfactorization_product = ff_r_fsat_zero_excludedfactorsfactorization_product * ff_p_fsat_zero_excludedfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_zero_excludedfactorsfactorization_primes. (exists ftsf_gap_fsat_zero_excludedfactorsfactorization_primes_bound. ftsf_gap_fsat_zero_excludedfactorsfactorization_primes_bound + S ftsf_index_fsat_zero_excludedfactorsfactorization_primes = (mv_factor_count_zero_excludedfactors)) -> exists ftsf_factor_fsat_zero_excludedfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_zero_excludedfactorsfactorization_primes_entry. ff_h_ftsf_fsat_zero_excludedfactorsfactorization_primes_entry + S (ftsf_factor_fsat_zero_excludedfactorsfactorization_primes) = S ((S (ftsf_index_fsat_zero_excludedfactorsfactorization_primes)) * mv_factor_scale_zero_excludedfactors)) /\ exists ff_q_ftsf_fsat_zero_excludedfactorsfactorization_primes_entry. mv_factor_code_zero_excludedfactors = ff_q_ftsf_fsat_zero_excludedfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_zero_excludedfactorsfactorization_primes)) * mv_factor_scale_zero_excludedfactors) + (ftsf_factor_fsat_zero_excludedfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_zero_excludedfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_zero_excludedfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_zero_excludedfactorsfactorization_primes_prime. ftsf_factor_fsat_zero_excludedfactorsfactorization_primes = frm_prime_left_ftsf_fsat_zero_excludedfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_zero_excludedfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_zero_excludedfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_zero_excludedfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_zero_excludedfactorsparityeven. (mv_factor_count_zero_excludedfactors) = 2 * mv_even_half_zero_excludedfactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_zero_excludedfactorsparityodd. (mv_factor_count_zero_excludedfactors) = 2 * mv_odd_half_zero_excludedfactorsparityodd + 1) /\ ((z) = 1))))))))))) -> false
Bundle node 221; exact statement SHA-256 d4939003ea99a37daea16178f694e25ae3aa5aeeadc98e4d535ac88529da12ba
forall n p. ~(n = 0) -> (~((p) = 1) /\ forall pvs_left_zero_prime pvs_right_zero_prime. (p) = pvs_left_zero_prime * pvs_right_zero_prime -> pvs_left_zero_prime = 1 \/ pvs_right_zero_prime = 1) -> (exists pvs_factor_zero_divisor. (n) = (p * p) * pvs_factor_zero_divisor) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_zero_valuesquare. ((~((mv_square_prime_zero_valuesquare) = 1) /\ forall pvs_left_zero_valuesquareprime pvs_right_zero_valuesquareprime. (mv_square_prime_zero_valuesquare) = pvs_left_zero_valuesquareprime * pvs_right_zero_valuesquareprime -> pvs_left_zero_valuesquareprime = 1 \/ pvs_right_zero_valuesquareprime = 1) /\ (exists pvs_factor_zero_valuesquaredivisor. (n) = (mv_square_prime_zero_valuesquare * mv_square_prime_zero_valuesquare) * pvs_factor_zero_valuesquaredivisor))) /\ ((0) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_zero_valuesquarefree. (~((sfd_prime_zero_valuesquarefree) = 1) /\ forall pvs_left_zero_valuesquarefreedomain pvs_right_zero_valuesquarefreedomain. (sfd_prime_zero_valuesquarefree) = pvs_left_zero_valuesquarefreedomain * pvs_right_zero_valuesquarefreedomain -> pvs_left_zero_valuesquarefreedomain = 1 \/ pvs_right_zero_valuesquarefreedomain = 1) -> (exists pvs_le_gap_zero_valuesquarefreebound. pvs_le_gap_zero_valuesquarefreebound + (sfd_prime_zero_valuesquarefree) = (n)) -> ~(exists pvs_factor_zero_valuesquarefreesquare. (n) = (sfd_prime_zero_valuesquarefree * sfd_prime_zero_valuesquarefree) * pvs_factor_zero_valuesquarefreesquare)))) /\ (exists mv_factor_code_zero_valuefactors mv_factor_scale_zero_valuefactors mv_factor_count_zero_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_zero_valuefactorsfactorization_product ff_v_fsat_zero_valuefactorsfactorization_product. ((((exists ff_h_fsat_zero_valuefactorsfactorization_product_start. ff_h_fsat_zero_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_zero_valuefactorsfactorization_product)) /\ exists ff_q_fsat_zero_valuefactorsfactorization_product_start. ff_u_fsat_zero_valuefactorsfactorization_product = ff_q_fsat_zero_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_zero_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_zero_valuefactorsfactorization_product_terminal. ff_h_fsat_zero_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_zero_valuefactors)) * ff_v_fsat_zero_valuefactorsfactorization_product)) /\ exists ff_q_fsat_zero_valuefactorsfactorization_product_terminal. ff_u_fsat_zero_valuefactorsfactorization_product = ff_q_fsat_zero_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_zero_valuefactors)) * ff_v_fsat_zero_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_zero_valuefactorsfactorization_product. (exists ff_lt_fsat_zero_valuefactorsfactorization_product_bound. ff_lt_fsat_zero_valuefactorsfactorization_product_bound + S ff_i_fsat_zero_valuefactorsfactorization_product = mv_factor_count_zero_valuefactors) -> exists ff_p_fsat_zero_valuefactorsfactorization_product ff_r_fsat_zero_valuefactorsfactorization_product ff_s_fsat_zero_valuefactorsfactorization_product. ((((exists ff_h_fsat_zero_valuefactorsfactorization_product_factor. ff_h_fsat_zero_valuefactorsfactorization_product_factor + S (ff_p_fsat_zero_valuefactorsfactorization_product) = S ((S (ff_i_fsat_zero_valuefactorsfactorization_product)) * mv_factor_scale_zero_valuefactors)) /\ exists ff_q_fsat_zero_valuefactorsfactorization_product_factor. mv_factor_code_zero_valuefactors = ff_q_fsat_zero_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_zero_valuefactorsfactorization_product)) * mv_factor_scale_zero_valuefactors) + (ff_p_fsat_zero_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_zero_valuefactorsfactorization_product_partial. ff_h_fsat_zero_valuefactorsfactorization_product_partial + S (ff_r_fsat_zero_valuefactorsfactorization_product) = S ((S (ff_i_fsat_zero_valuefactorsfactorization_product)) * ff_v_fsat_zero_valuefactorsfactorization_product)) /\ exists ff_q_fsat_zero_valuefactorsfactorization_product_partial. ff_u_fsat_zero_valuefactorsfactorization_product = ff_q_fsat_zero_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_zero_valuefactorsfactorization_product)) * ff_v_fsat_zero_valuefactorsfactorization_product) + (ff_r_fsat_zero_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_zero_valuefactorsfactorization_product_successor. ff_h_fsat_zero_valuefactorsfactorization_product_successor + S (ff_s_fsat_zero_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_zero_valuefactorsfactorization_product)) * ff_v_fsat_zero_valuefactorsfactorization_product)) /\ exists ff_q_fsat_zero_valuefactorsfactorization_product_successor. ff_u_fsat_zero_valuefactorsfactorization_product = ff_q_fsat_zero_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_zero_valuefactorsfactorization_product)) * ff_v_fsat_zero_valuefactorsfactorization_product) + (ff_s_fsat_zero_valuefactorsfactorization_product))) /\ ff_s_fsat_zero_valuefactorsfactorization_product = ff_r_fsat_zero_valuefactorsfactorization_product * ff_p_fsat_zero_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_zero_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_zero_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_zero_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_zero_valuefactorsfactorization_primes = (mv_factor_count_zero_valuefactors)) -> exists ftsf_factor_fsat_zero_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_zero_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_zero_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_zero_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_zero_valuefactorsfactorization_primes)) * mv_factor_scale_zero_valuefactors)) /\ exists ff_q_ftsf_fsat_zero_valuefactorsfactorization_primes_entry. mv_factor_code_zero_valuefactors = ff_q_ftsf_fsat_zero_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_zero_valuefactorsfactorization_primes)) * mv_factor_scale_zero_valuefactors) + (ftsf_factor_fsat_zero_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_zero_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_zero_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_zero_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_zero_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_zero_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_zero_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_zero_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_zero_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_zero_valuefactorsparityeven. (mv_factor_count_zero_valuefactors) = 2 * mv_even_half_zero_valuefactorsparityeven) /\ ((0) = 2))) \/ (((exists mv_odd_half_zero_valuefactorsparityodd. (mv_factor_count_zero_valuefactors) = 2 * mv_odd_half_zero_valuefactorsparityodd + 1) /\ ((0) = 1)))))))))))
Bundle node 222; exact statement SHA-256 af94f7f9242bb7d0d94d074224952bb3db154b4deaff9935fd7a94b91d1f2b96
forall n b c l z. (((~((n) = 0)) /\ (forall sfd_prime_constructor_sf. (~((sfd_prime_constructor_sf) = 1) /\ forall pvs_left_constructor_sfdomain pvs_right_constructor_sfdomain. (sfd_prime_constructor_sf) = pvs_left_constructor_sfdomain * pvs_right_constructor_sfdomain -> pvs_left_constructor_sfdomain = 1 \/ pvs_right_constructor_sfdomain = 1) -> (exists pvs_le_gap_constructor_sfbound. pvs_le_gap_constructor_sfbound + (sfd_prime_constructor_sf) = (n)) -> ~(exists pvs_factor_constructor_sfsquare. (n) = (sfd_prime_constructor_sf * sfd_prime_constructor_sf) * pvs_factor_constructor_sfsquare)))) -> ((~(n = 0) /\ ((exists ff_u_fsat_mv_constructor_factors_product ff_v_fsat_mv_constructor_factors_product. ((((exists ff_h_fsat_mv_constructor_factors_product_start. ff_h_fsat_mv_constructor_factors_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_constructor_factors_product)) /\ exists ff_q_fsat_mv_constructor_factors_product_start. ff_u_fsat_mv_constructor_factors_product = ff_q_fsat_mv_constructor_factors_product_start * S ((S (0)) * ff_v_fsat_mv_constructor_factors_product) + (1))) /\ ((((exists ff_h_fsat_mv_constructor_factors_product_terminal. ff_h_fsat_mv_constructor_factors_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mv_constructor_factors_product)) /\ exists ff_q_fsat_mv_constructor_factors_product_terminal. ff_u_fsat_mv_constructor_factors_product = ff_q_fsat_mv_constructor_factors_product_terminal * S ((S (l)) * ff_v_fsat_mv_constructor_factors_product) + (n))) /\ forall ff_i_fsat_mv_constructor_factors_product. (exists ff_lt_fsat_mv_constructor_factors_product_bound. ff_lt_fsat_mv_constructor_factors_product_bound + S ff_i_fsat_mv_constructor_factors_product = l) -> exists ff_p_fsat_mv_constructor_factors_product ff_r_fsat_mv_constructor_factors_product ff_s_fsat_mv_constructor_factors_product. ((((exists ff_h_fsat_mv_constructor_factors_product_factor. ff_h_fsat_mv_constructor_factors_product_factor + S (ff_p_fsat_mv_constructor_factors_product) = S ((S (ff_i_fsat_mv_constructor_factors_product)) * c)) /\ exists ff_q_fsat_mv_constructor_factors_product_factor. b = ff_q_fsat_mv_constructor_factors_product_factor * S ((S (ff_i_fsat_mv_constructor_factors_product)) * c) + (ff_p_fsat_mv_constructor_factors_product))) /\ ((((exists ff_h_fsat_mv_constructor_factors_product_partial. ff_h_fsat_mv_constructor_factors_product_partial + S (ff_r_fsat_mv_constructor_factors_product) = S ((S (ff_i_fsat_mv_constructor_factors_product)) * ff_v_fsat_mv_constructor_factors_product)) /\ exists ff_q_fsat_mv_constructor_factors_product_partial. ff_u_fsat_mv_constructor_factors_product = ff_q_fsat_mv_constructor_factors_product_partial * S ((S (ff_i_fsat_mv_constructor_factors_product)) * ff_v_fsat_mv_constructor_factors_product) + (ff_r_fsat_mv_constructor_factors_product))) /\ ((((exists ff_h_fsat_mv_constructor_factors_product_successor. ff_h_fsat_mv_constructor_factors_product_successor + S (ff_s_fsat_mv_constructor_factors_product) = S ((S (S ff_i_fsat_mv_constructor_factors_product)) * ff_v_fsat_mv_constructor_factors_product)) /\ exists ff_q_fsat_mv_constructor_factors_product_successor. ff_u_fsat_mv_constructor_factors_product = ff_q_fsat_mv_constructor_factors_product_successor * S ((S (S ff_i_fsat_mv_constructor_factors_product)) * ff_v_fsat_mv_constructor_factors_product) + (ff_s_fsat_mv_constructor_factors_product))) /\ ff_s_fsat_mv_constructor_factors_product = ff_r_fsat_mv_constructor_factors_product * ff_p_fsat_mv_constructor_factors_product)))))) /\ (forall ftsf_index_fsat_mv_constructor_factors_primes. (exists ftsf_gap_fsat_mv_constructor_factors_primes_bound. ftsf_gap_fsat_mv_constructor_factors_primes_bound + S ftsf_index_fsat_mv_constructor_factors_primes = (l)) -> exists ftsf_factor_fsat_mv_constructor_factors_primes. ((((exists ff_h_ftsf_fsat_mv_constructor_factors_primes_entry. ff_h_ftsf_fsat_mv_constructor_factors_primes_entry + S (ftsf_factor_fsat_mv_constructor_factors_primes) = S ((S (ftsf_index_fsat_mv_constructor_factors_primes)) * c)) /\ exists ff_q_ftsf_fsat_mv_constructor_factors_primes_entry. b = ff_q_ftsf_fsat_mv_constructor_factors_primes_entry * S ((S (ftsf_index_fsat_mv_constructor_factors_primes)) * c) + (ftsf_factor_fsat_mv_constructor_factors_primes))) /\ ((~(ftsf_factor_fsat_mv_constructor_factors_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_constructor_factors_primes_prime frm_prime_right_ftsf_fsat_mv_constructor_factors_primes_prime. ftsf_factor_fsat_mv_constructor_factors_primes = frm_prime_left_ftsf_fsat_mv_constructor_factors_primes_prime * frm_prime_right_ftsf_fsat_mv_constructor_factors_primes_prime -> frm_prime_left_ftsf_fsat_mv_constructor_factors_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_constructor_factors_primes_prime = 1))))))) -> ((((exists mv_even_half_constructor_signeven. (l) = 2 * mv_even_half_constructor_signeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_constructor_signodd. (l) = 2 * mv_odd_half_constructor_signodd + 1) /\ ((z) = 1)))) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_constructor_valuesquare. ((~((mv_square_prime_constructor_valuesquare) = 1) /\ forall pvs_left_constructor_valuesquareprime pvs_right_constructor_valuesquareprime. (mv_square_prime_constructor_valuesquare) = pvs_left_constructor_valuesquareprime * pvs_right_constructor_valuesquareprime -> pvs_left_constructor_valuesquareprime = 1 \/ pvs_right_constructor_valuesquareprime = 1) /\ (exists pvs_factor_constructor_valuesquaredivisor. (n) = (mv_square_prime_constructor_valuesquare * mv_square_prime_constructor_valuesquare) * pvs_factor_constructor_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_constructor_valuesquarefree. (~((sfd_prime_constructor_valuesquarefree) = 1) /\ forall pvs_left_constructor_valuesquarefreedomain pvs_right_constructor_valuesquarefreedomain. (sfd_prime_constructor_valuesquarefree) = pvs_left_constructor_valuesquarefreedomain * pvs_right_constructor_valuesquarefreedomain -> pvs_left_constructor_valuesquarefreedomain = 1 \/ pvs_right_constructor_valuesquarefreedomain = 1) -> (exists pvs_le_gap_constructor_valuesquarefreebound. pvs_le_gap_constructor_valuesquarefreebound + (sfd_prime_constructor_valuesquarefree) = (n)) -> ~(exists pvs_factor_constructor_valuesquarefreesquare. (n) = (sfd_prime_constructor_valuesquarefree * sfd_prime_constructor_valuesquarefree) * pvs_factor_constructor_valuesquarefreesquare)))) /\ (exists mv_factor_code_constructor_valuefactors mv_factor_scale_constructor_valuefactors mv_factor_count_constructor_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_constructor_valuefactorsfactorization_product ff_v_fsat_constructor_valuefactorsfactorization_product. ((((exists ff_h_fsat_constructor_valuefactorsfactorization_product_start. ff_h_fsat_constructor_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_constructor_valuefactorsfactorization_product)) /\ exists ff_q_fsat_constructor_valuefactorsfactorization_product_start. ff_u_fsat_constructor_valuefactorsfactorization_product = ff_q_fsat_constructor_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_constructor_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_constructor_valuefactorsfactorization_product_terminal. ff_h_fsat_constructor_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_constructor_valuefactors)) * ff_v_fsat_constructor_valuefactorsfactorization_product)) /\ exists ff_q_fsat_constructor_valuefactorsfactorization_product_terminal. ff_u_fsat_constructor_valuefactorsfactorization_product = ff_q_fsat_constructor_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_constructor_valuefactors)) * ff_v_fsat_constructor_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_constructor_valuefactorsfactorization_product. (exists ff_lt_fsat_constructor_valuefactorsfactorization_product_bound. ff_lt_fsat_constructor_valuefactorsfactorization_product_bound + S ff_i_fsat_constructor_valuefactorsfactorization_product = mv_factor_count_constructor_valuefactors) -> exists ff_p_fsat_constructor_valuefactorsfactorization_product ff_r_fsat_constructor_valuefactorsfactorization_product ff_s_fsat_constructor_valuefactorsfactorization_product. ((((exists ff_h_fsat_constructor_valuefactorsfactorization_product_factor. ff_h_fsat_constructor_valuefactorsfactorization_product_factor + S (ff_p_fsat_constructor_valuefactorsfactorization_product) = S ((S (ff_i_fsat_constructor_valuefactorsfactorization_product)) * mv_factor_scale_constructor_valuefactors)) /\ exists ff_q_fsat_constructor_valuefactorsfactorization_product_factor. mv_factor_code_constructor_valuefactors = ff_q_fsat_constructor_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_constructor_valuefactorsfactorization_product)) * mv_factor_scale_constructor_valuefactors) + (ff_p_fsat_constructor_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_constructor_valuefactorsfactorization_product_partial. ff_h_fsat_constructor_valuefactorsfactorization_product_partial + S (ff_r_fsat_constructor_valuefactorsfactorization_product) = S ((S (ff_i_fsat_constructor_valuefactorsfactorization_product)) * ff_v_fsat_constructor_valuefactorsfactorization_product)) /\ exists ff_q_fsat_constructor_valuefactorsfactorization_product_partial. ff_u_fsat_constructor_valuefactorsfactorization_product = ff_q_fsat_constructor_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_constructor_valuefactorsfactorization_product)) * ff_v_fsat_constructor_valuefactorsfactorization_product) + (ff_r_fsat_constructor_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_constructor_valuefactorsfactorization_product_successor. ff_h_fsat_constructor_valuefactorsfactorization_product_successor + S (ff_s_fsat_constructor_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_constructor_valuefactorsfactorization_product)) * ff_v_fsat_constructor_valuefactorsfactorization_product)) /\ exists ff_q_fsat_constructor_valuefactorsfactorization_product_successor. ff_u_fsat_constructor_valuefactorsfactorization_product = ff_q_fsat_constructor_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_constructor_valuefactorsfactorization_product)) * ff_v_fsat_constructor_valuefactorsfactorization_product) + (ff_s_fsat_constructor_valuefactorsfactorization_product))) /\ ff_s_fsat_constructor_valuefactorsfactorization_product = ff_r_fsat_constructor_valuefactorsfactorization_product * ff_p_fsat_constructor_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_constructor_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_constructor_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_constructor_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_constructor_valuefactorsfactorization_primes = (mv_factor_count_constructor_valuefactors)) -> exists ftsf_factor_fsat_constructor_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_constructor_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_constructor_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_constructor_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_constructor_valuefactorsfactorization_primes)) * mv_factor_scale_constructor_valuefactors)) /\ exists ff_q_ftsf_fsat_constructor_valuefactorsfactorization_primes_entry. mv_factor_code_constructor_valuefactors = ff_q_ftsf_fsat_constructor_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_constructor_valuefactorsfactorization_primes)) * mv_factor_scale_constructor_valuefactors) + (ftsf_factor_fsat_constructor_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_constructor_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_constructor_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_constructor_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_constructor_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_constructor_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_constructor_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_constructor_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_constructor_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_constructor_valuefactorsparityeven. (mv_factor_count_constructor_valuefactors) = 2 * mv_even_half_constructor_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_constructor_valuefactorsparityodd. (mv_factor_count_constructor_valuefactors) = 2 * mv_odd_half_constructor_valuefactorsparityodd + 1) /\ ((z) = 1)))))))))))
Bundle node 223; exact statement SHA-256 66d70409d9b65a8d69997c5ed6ccb6e002ae29046eb3d1dd1e563685fc4897da
forall n. ~(n = 0) -> exists z. (((~((n) = 0)) /\ ((((exists mv_square_prime_exists_valuesquare. ((~((mv_square_prime_exists_valuesquare) = 1) /\ forall pvs_left_exists_valuesquareprime pvs_right_exists_valuesquareprime. (mv_square_prime_exists_valuesquare) = pvs_left_exists_valuesquareprime * pvs_right_exists_valuesquareprime -> pvs_left_exists_valuesquareprime = 1 \/ pvs_right_exists_valuesquareprime = 1) /\ (exists pvs_factor_exists_valuesquaredivisor. (n) = (mv_square_prime_exists_valuesquare * mv_square_prime_exists_valuesquare) * pvs_factor_exists_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_exists_valuesquarefree. (~((sfd_prime_exists_valuesquarefree) = 1) /\ forall pvs_left_exists_valuesquarefreedomain pvs_right_exists_valuesquarefreedomain. (sfd_prime_exists_valuesquarefree) = pvs_left_exists_valuesquarefreedomain * pvs_right_exists_valuesquarefreedomain -> pvs_left_exists_valuesquarefreedomain = 1 \/ pvs_right_exists_valuesquarefreedomain = 1) -> (exists pvs_le_gap_exists_valuesquarefreebound. pvs_le_gap_exists_valuesquarefreebound + (sfd_prime_exists_valuesquarefree) = (n)) -> ~(exists pvs_factor_exists_valuesquarefreesquare. (n) = (sfd_prime_exists_valuesquarefree * sfd_prime_exists_valuesquarefree) * pvs_factor_exists_valuesquarefreesquare)))) /\ (exists mv_factor_code_exists_valuefactors mv_factor_scale_exists_valuefactors mv_factor_count_exists_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_exists_valuefactorsfactorization_product ff_v_fsat_exists_valuefactorsfactorization_product. ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_start. ff_h_fsat_exists_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_start. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_terminal. ff_h_fsat_exists_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_exists_valuefactors)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_terminal. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_exists_valuefactors)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_exists_valuefactorsfactorization_product. (exists ff_lt_fsat_exists_valuefactorsfactorization_product_bound. ff_lt_fsat_exists_valuefactorsfactorization_product_bound + S ff_i_fsat_exists_valuefactorsfactorization_product = mv_factor_count_exists_valuefactors) -> exists ff_p_fsat_exists_valuefactorsfactorization_product ff_r_fsat_exists_valuefactorsfactorization_product ff_s_fsat_exists_valuefactorsfactorization_product. ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_factor. ff_h_fsat_exists_valuefactorsfactorization_product_factor + S (ff_p_fsat_exists_valuefactorsfactorization_product) = S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * mv_factor_scale_exists_valuefactors)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_factor. mv_factor_code_exists_valuefactors = ff_q_fsat_exists_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * mv_factor_scale_exists_valuefactors) + (ff_p_fsat_exists_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_partial. ff_h_fsat_exists_valuefactorsfactorization_product_partial + S (ff_r_fsat_exists_valuefactorsfactorization_product) = S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_partial. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (ff_r_fsat_exists_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_valuefactorsfactorization_product_successor. ff_h_fsat_exists_valuefactorsfactorization_product_successor + S (ff_s_fsat_exists_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_valuefactorsfactorization_product_successor. ff_u_fsat_exists_valuefactorsfactorization_product = ff_q_fsat_exists_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_exists_valuefactorsfactorization_product)) * ff_v_fsat_exists_valuefactorsfactorization_product) + (ff_s_fsat_exists_valuefactorsfactorization_product))) /\ ff_s_fsat_exists_valuefactorsfactorization_product = ff_r_fsat_exists_valuefactorsfactorization_product * ff_p_fsat_exists_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_exists_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_exists_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_exists_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_exists_valuefactorsfactorization_primes = (mv_factor_count_exists_valuefactors)) -> exists ftsf_factor_fsat_exists_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_exists_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_exists_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_exists_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_exists_valuefactorsfactorization_primes)) * mv_factor_scale_exists_valuefactors)) /\ exists ff_q_ftsf_fsat_exists_valuefactorsfactorization_primes_entry. mv_factor_code_exists_valuefactors = ff_q_ftsf_fsat_exists_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_exists_valuefactorsfactorization_primes)) * mv_factor_scale_exists_valuefactors) + (ftsf_factor_fsat_exists_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_exists_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_exists_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_exists_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_exists_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_exists_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_exists_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_exists_valuefactorsparityeven. (mv_factor_count_exists_valuefactors) = 2 * mv_even_half_exists_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_exists_valuefactorsparityodd. (mv_factor_count_exists_valuefactors) = 2 * mv_odd_half_exists_valuefactorsparityodd + 1) /\ ((z) = 1)))))))))))
Bundle node 224; exact statement SHA-256 90196a9966b1fa7ab9107257bb645f2c4b6c1662a84c4e50b1a3273eb8aa00fd
forall n b c l z. (((~((n) = 0)) /\ (forall sfd_prime_evaluation_sf. (~((sfd_prime_evaluation_sf) = 1) /\ forall pvs_left_evaluation_sfdomain pvs_right_evaluation_sfdomain. (sfd_prime_evaluation_sf) = pvs_left_evaluation_sfdomain * pvs_right_evaluation_sfdomain -> pvs_left_evaluation_sfdomain = 1 \/ pvs_right_evaluation_sfdomain = 1) -> (exists pvs_le_gap_evaluation_sfbound. pvs_le_gap_evaluation_sfbound + (sfd_prime_evaluation_sf) = (n)) -> ~(exists pvs_factor_evaluation_sfsquare. (n) = (sfd_prime_evaluation_sf * sfd_prime_evaluation_sf) * pvs_factor_evaluation_sfsquare)))) -> ((~(n = 0) /\ ((exists ff_u_fsat_mv_evaluation_factors_product ff_v_fsat_mv_evaluation_factors_product. ((((exists ff_h_fsat_mv_evaluation_factors_product_start. ff_h_fsat_mv_evaluation_factors_product_start + S (1) = S ((S (0)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_start. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_start * S ((S (0)) * ff_v_fsat_mv_evaluation_factors_product) + (1))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_terminal. ff_h_fsat_mv_evaluation_factors_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_terminal. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_terminal * S ((S (l)) * ff_v_fsat_mv_evaluation_factors_product) + (n))) /\ forall ff_i_fsat_mv_evaluation_factors_product. (exists ff_lt_fsat_mv_evaluation_factors_product_bound. ff_lt_fsat_mv_evaluation_factors_product_bound + S ff_i_fsat_mv_evaluation_factors_product = l) -> exists ff_p_fsat_mv_evaluation_factors_product ff_r_fsat_mv_evaluation_factors_product ff_s_fsat_mv_evaluation_factors_product. ((((exists ff_h_fsat_mv_evaluation_factors_product_factor. ff_h_fsat_mv_evaluation_factors_product_factor + S (ff_p_fsat_mv_evaluation_factors_product) = S ((S (ff_i_fsat_mv_evaluation_factors_product)) * c)) /\ exists ff_q_fsat_mv_evaluation_factors_product_factor. b = ff_q_fsat_mv_evaluation_factors_product_factor * S ((S (ff_i_fsat_mv_evaluation_factors_product)) * c) + (ff_p_fsat_mv_evaluation_factors_product))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_partial. ff_h_fsat_mv_evaluation_factors_product_partial + S (ff_r_fsat_mv_evaluation_factors_product) = S ((S (ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_partial. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_partial * S ((S (ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product) + (ff_r_fsat_mv_evaluation_factors_product))) /\ ((((exists ff_h_fsat_mv_evaluation_factors_product_successor. ff_h_fsat_mv_evaluation_factors_product_successor + S (ff_s_fsat_mv_evaluation_factors_product) = S ((S (S ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product)) /\ exists ff_q_fsat_mv_evaluation_factors_product_successor. ff_u_fsat_mv_evaluation_factors_product = ff_q_fsat_mv_evaluation_factors_product_successor * S ((S (S ff_i_fsat_mv_evaluation_factors_product)) * ff_v_fsat_mv_evaluation_factors_product) + (ff_s_fsat_mv_evaluation_factors_product))) /\ ff_s_fsat_mv_evaluation_factors_product = ff_r_fsat_mv_evaluation_factors_product * ff_p_fsat_mv_evaluation_factors_product)))))) /\ (forall ftsf_index_fsat_mv_evaluation_factors_primes. (exists ftsf_gap_fsat_mv_evaluation_factors_primes_bound. ftsf_gap_fsat_mv_evaluation_factors_primes_bound + S ftsf_index_fsat_mv_evaluation_factors_primes = (l)) -> exists ftsf_factor_fsat_mv_evaluation_factors_primes. ((((exists ff_h_ftsf_fsat_mv_evaluation_factors_primes_entry. ff_h_ftsf_fsat_mv_evaluation_factors_primes_entry + S (ftsf_factor_fsat_mv_evaluation_factors_primes) = S ((S (ftsf_index_fsat_mv_evaluation_factors_primes)) * c)) /\ exists ff_q_ftsf_fsat_mv_evaluation_factors_primes_entry. b = ff_q_ftsf_fsat_mv_evaluation_factors_primes_entry * S ((S (ftsf_index_fsat_mv_evaluation_factors_primes)) * c) + (ftsf_factor_fsat_mv_evaluation_factors_primes))) /\ ((~(ftsf_factor_fsat_mv_evaluation_factors_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime. ftsf_factor_fsat_mv_evaluation_factors_primes = frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime * frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime -> frm_prime_left_ftsf_fsat_mv_evaluation_factors_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mv_evaluation_factors_primes_prime = 1))))))) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_evaluation_valuesquare. ((~((mv_square_prime_evaluation_valuesquare) = 1) /\ forall pvs_left_evaluation_valuesquareprime pvs_right_evaluation_valuesquareprime. (mv_square_prime_evaluation_valuesquare) = pvs_left_evaluation_valuesquareprime * pvs_right_evaluation_valuesquareprime -> pvs_left_evaluation_valuesquareprime = 1 \/ pvs_right_evaluation_valuesquareprime = 1) /\ (exists pvs_factor_evaluation_valuesquaredivisor. (n) = (mv_square_prime_evaluation_valuesquare * mv_square_prime_evaluation_valuesquare) * pvs_factor_evaluation_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_evaluation_valuesquarefree. (~((sfd_prime_evaluation_valuesquarefree) = 1) /\ forall pvs_left_evaluation_valuesquarefreedomain pvs_right_evaluation_valuesquarefreedomain. (sfd_prime_evaluation_valuesquarefree) = pvs_left_evaluation_valuesquarefreedomain * pvs_right_evaluation_valuesquarefreedomain -> pvs_left_evaluation_valuesquarefreedomain = 1 \/ pvs_right_evaluation_valuesquarefreedomain = 1) -> (exists pvs_le_gap_evaluation_valuesquarefreebound. pvs_le_gap_evaluation_valuesquarefreebound + (sfd_prime_evaluation_valuesquarefree) = (n)) -> ~(exists pvs_factor_evaluation_valuesquarefreesquare. (n) = (sfd_prime_evaluation_valuesquarefree * sfd_prime_evaluation_valuesquarefree) * pvs_factor_evaluation_valuesquarefreesquare)))) /\ (exists mv_factor_code_evaluation_valuefactors mv_factor_scale_evaluation_valuefactors mv_factor_count_evaluation_valuefactors. (((~(n = 0) /\ ((exists ff_u_fsat_evaluation_valuefactorsfactorization_product ff_v_fsat_evaluation_valuefactorsfactorization_product. ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_start. ff_h_fsat_evaluation_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_start. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_terminal. ff_h_fsat_evaluation_valuefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_evaluation_valuefactors)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_terminal. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_evaluation_valuefactors)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_evaluation_valuefactorsfactorization_product. (exists ff_lt_fsat_evaluation_valuefactorsfactorization_product_bound. ff_lt_fsat_evaluation_valuefactorsfactorization_product_bound + S ff_i_fsat_evaluation_valuefactorsfactorization_product = mv_factor_count_evaluation_valuefactors) -> exists ff_p_fsat_evaluation_valuefactorsfactorization_product ff_r_fsat_evaluation_valuefactorsfactorization_product ff_s_fsat_evaluation_valuefactorsfactorization_product. ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_factor. ff_h_fsat_evaluation_valuefactorsfactorization_product_factor + S (ff_p_fsat_evaluation_valuefactorsfactorization_product) = S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * mv_factor_scale_evaluation_valuefactors)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_factor. mv_factor_code_evaluation_valuefactors = ff_q_fsat_evaluation_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * mv_factor_scale_evaluation_valuefactors) + (ff_p_fsat_evaluation_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_partial. ff_h_fsat_evaluation_valuefactorsfactorization_product_partial + S (ff_r_fsat_evaluation_valuefactorsfactorization_product) = S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_partial. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (ff_r_fsat_evaluation_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_evaluation_valuefactorsfactorization_product_successor. ff_h_fsat_evaluation_valuefactorsfactorization_product_successor + S (ff_s_fsat_evaluation_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product)) /\ exists ff_q_fsat_evaluation_valuefactorsfactorization_product_successor. ff_u_fsat_evaluation_valuefactorsfactorization_product = ff_q_fsat_evaluation_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_evaluation_valuefactorsfactorization_product)) * ff_v_fsat_evaluation_valuefactorsfactorization_product) + (ff_s_fsat_evaluation_valuefactorsfactorization_product))) /\ ff_s_fsat_evaluation_valuefactorsfactorization_product = ff_r_fsat_evaluation_valuefactorsfactorization_product * ff_p_fsat_evaluation_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_evaluation_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_evaluation_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_evaluation_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_evaluation_valuefactorsfactorization_primes = (mv_factor_count_evaluation_valuefactors)) -> exists ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_evaluation_valuefactorsfactorization_primes)) * mv_factor_scale_evaluation_valuefactors)) /\ exists ff_q_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry. mv_factor_code_evaluation_valuefactors = ff_q_ftsf_fsat_evaluation_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_evaluation_valuefactorsfactorization_primes)) * mv_factor_scale_evaluation_valuefactors) + (ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_evaluation_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_evaluation_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_evaluation_valuefactorsparityeven. (mv_factor_count_evaluation_valuefactors) = 2 * mv_even_half_evaluation_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_evaluation_valuefactorsparityodd. (mv_factor_count_evaluation_valuefactors) = 2 * mv_odd_half_evaluation_valuefactorsparityodd + 1) /\ ((z) = 1))))))))))) -> ((((exists mv_even_half_evaluation_resulteven. (l) = 2 * mv_even_half_evaluation_resulteven) /\ ((z) = 2))) \/ (((exists mv_odd_half_evaluation_resultodd. (l) = 2 * mv_odd_half_evaluation_resultodd + 1) /\ ((z) = 1))))
Bundle node 225; exact statement SHA-256 d6bf764d3fcc08f8b8f2294fb16cb0d1fb91dc58b9563920db33dc522b7e4eb3
forall n a b. (((~((n) = 0)) /\ ((((exists mv_square_prime_functional_firstsquare. ((~((mv_square_prime_functional_firstsquare) = 1) /\ forall pvs_left_functional_firstsquareprime pvs_right_functional_firstsquareprime. (mv_square_prime_functional_firstsquare) = pvs_left_functional_firstsquareprime * pvs_right_functional_firstsquareprime -> pvs_left_functional_firstsquareprime = 1 \/ pvs_right_functional_firstsquareprime = 1) /\ (exists pvs_factor_functional_firstsquaredivisor. (n) = (mv_square_prime_functional_firstsquare * mv_square_prime_functional_firstsquare) * pvs_factor_functional_firstsquaredivisor))) /\ ((a) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_functional_firstsquarefree. (~((sfd_prime_functional_firstsquarefree) = 1) /\ forall pvs_left_functional_firstsquarefreedomain pvs_right_functional_firstsquarefreedomain. (sfd_prime_functional_firstsquarefree) = pvs_left_functional_firstsquarefreedomain * pvs_right_functional_firstsquarefreedomain -> pvs_left_functional_firstsquarefreedomain = 1 \/ pvs_right_functional_firstsquarefreedomain = 1) -> (exists pvs_le_gap_functional_firstsquarefreebound. pvs_le_gap_functional_firstsquarefreebound + (sfd_prime_functional_firstsquarefree) = (n)) -> ~(exists pvs_factor_functional_firstsquarefreesquare. (n) = (sfd_prime_functional_firstsquarefree * sfd_prime_functional_firstsquarefree) * pvs_factor_functional_firstsquarefreesquare)))) /\ (exists mv_factor_code_functional_firstfactors mv_factor_scale_functional_firstfactors mv_factor_count_functional_firstfactors. (((~(n = 0) /\ ((exists ff_u_fsat_functional_firstfactorsfactorization_product ff_v_fsat_functional_firstfactorsfactorization_product. ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_start. ff_h_fsat_functional_firstfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_start. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_terminal. ff_h_fsat_functional_firstfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_functional_firstfactors)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_terminal. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_terminal * S ((S (mv_factor_count_functional_firstfactors)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_functional_firstfactorsfactorization_product. (exists ff_lt_fsat_functional_firstfactorsfactorization_product_bound. ff_lt_fsat_functional_firstfactorsfactorization_product_bound + S ff_i_fsat_functional_firstfactorsfactorization_product = mv_factor_count_functional_firstfactors) -> exists ff_p_fsat_functional_firstfactorsfactorization_product ff_r_fsat_functional_firstfactorsfactorization_product ff_s_fsat_functional_firstfactorsfactorization_product. ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_factor. ff_h_fsat_functional_firstfactorsfactorization_product_factor + S (ff_p_fsat_functional_firstfactorsfactorization_product) = S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * mv_factor_scale_functional_firstfactors)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_factor. mv_factor_code_functional_firstfactors = ff_q_fsat_functional_firstfactorsfactorization_product_factor * S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * mv_factor_scale_functional_firstfactors) + (ff_p_fsat_functional_firstfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_partial. ff_h_fsat_functional_firstfactorsfactorization_product_partial + S (ff_r_fsat_functional_firstfactorsfactorization_product) = S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_partial. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_partial * S ((S (ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (ff_r_fsat_functional_firstfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_firstfactorsfactorization_product_successor. ff_h_fsat_functional_firstfactorsfactorization_product_successor + S (ff_s_fsat_functional_firstfactorsfactorization_product) = S ((S (S ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product)) /\ exists ff_q_fsat_functional_firstfactorsfactorization_product_successor. ff_u_fsat_functional_firstfactorsfactorization_product = ff_q_fsat_functional_firstfactorsfactorization_product_successor * S ((S (S ff_i_fsat_functional_firstfactorsfactorization_product)) * ff_v_fsat_functional_firstfactorsfactorization_product) + (ff_s_fsat_functional_firstfactorsfactorization_product))) /\ ff_s_fsat_functional_firstfactorsfactorization_product = ff_r_fsat_functional_firstfactorsfactorization_product * ff_p_fsat_functional_firstfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_functional_firstfactorsfactorization_primes. (exists ftsf_gap_fsat_functional_firstfactorsfactorization_primes_bound. ftsf_gap_fsat_functional_firstfactorsfactorization_primes_bound + S ftsf_index_fsat_functional_firstfactorsfactorization_primes = (mv_factor_count_functional_firstfactors)) -> exists ftsf_factor_fsat_functional_firstfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_functional_firstfactorsfactorization_primes_entry. ff_h_ftsf_fsat_functional_firstfactorsfactorization_primes_entry + S (ftsf_factor_fsat_functional_firstfactorsfactorization_primes) = S ((S (ftsf_index_fsat_functional_firstfactorsfactorization_primes)) * mv_factor_scale_functional_firstfactors)) /\ exists ff_q_ftsf_fsat_functional_firstfactorsfactorization_primes_entry. mv_factor_code_functional_firstfactors = ff_q_ftsf_fsat_functional_firstfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_functional_firstfactorsfactorization_primes)) * mv_factor_scale_functional_firstfactors) + (ftsf_factor_fsat_functional_firstfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_functional_firstfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_functional_firstfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_functional_firstfactorsfactorization_primes_prime. ftsf_factor_fsat_functional_firstfactorsfactorization_primes = frm_prime_left_ftsf_fsat_functional_firstfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_functional_firstfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_functional_firstfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_functional_firstfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_functional_firstfactorsparityeven. (mv_factor_count_functional_firstfactors) = 2 * mv_even_half_functional_firstfactorsparityeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_functional_firstfactorsparityodd. (mv_factor_count_functional_firstfactors) = 2 * mv_odd_half_functional_firstfactorsparityodd + 1) /\ ((a) = 1))))))))))) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_functional_secondsquare. ((~((mv_square_prime_functional_secondsquare) = 1) /\ forall pvs_left_functional_secondsquareprime pvs_right_functional_secondsquareprime. (mv_square_prime_functional_secondsquare) = pvs_left_functional_secondsquareprime * pvs_right_functional_secondsquareprime -> pvs_left_functional_secondsquareprime = 1 \/ pvs_right_functional_secondsquareprime = 1) /\ (exists pvs_factor_functional_secondsquaredivisor. (n) = (mv_square_prime_functional_secondsquare * mv_square_prime_functional_secondsquare) * pvs_factor_functional_secondsquaredivisor))) /\ ((b) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_functional_secondsquarefree. (~((sfd_prime_functional_secondsquarefree) = 1) /\ forall pvs_left_functional_secondsquarefreedomain pvs_right_functional_secondsquarefreedomain. (sfd_prime_functional_secondsquarefree) = pvs_left_functional_secondsquarefreedomain * pvs_right_functional_secondsquarefreedomain -> pvs_left_functional_secondsquarefreedomain = 1 \/ pvs_right_functional_secondsquarefreedomain = 1) -> (exists pvs_le_gap_functional_secondsquarefreebound. pvs_le_gap_functional_secondsquarefreebound + (sfd_prime_functional_secondsquarefree) = (n)) -> ~(exists pvs_factor_functional_secondsquarefreesquare. (n) = (sfd_prime_functional_secondsquarefree * sfd_prime_functional_secondsquarefree) * pvs_factor_functional_secondsquarefreesquare)))) /\ (exists mv_factor_code_functional_secondfactors mv_factor_scale_functional_secondfactors mv_factor_count_functional_secondfactors. (((~(n = 0) /\ ((exists ff_u_fsat_functional_secondfactorsfactorization_product ff_v_fsat_functional_secondfactorsfactorization_product. ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_start. ff_h_fsat_functional_secondfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_start. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_terminal. ff_h_fsat_functional_secondfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_functional_secondfactors)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_terminal. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_terminal * S ((S (mv_factor_count_functional_secondfactors)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_functional_secondfactorsfactorization_product. (exists ff_lt_fsat_functional_secondfactorsfactorization_product_bound. ff_lt_fsat_functional_secondfactorsfactorization_product_bound + S ff_i_fsat_functional_secondfactorsfactorization_product = mv_factor_count_functional_secondfactors) -> exists ff_p_fsat_functional_secondfactorsfactorization_product ff_r_fsat_functional_secondfactorsfactorization_product ff_s_fsat_functional_secondfactorsfactorization_product. ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_factor. ff_h_fsat_functional_secondfactorsfactorization_product_factor + S (ff_p_fsat_functional_secondfactorsfactorization_product) = S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * mv_factor_scale_functional_secondfactors)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_factor. mv_factor_code_functional_secondfactors = ff_q_fsat_functional_secondfactorsfactorization_product_factor * S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * mv_factor_scale_functional_secondfactors) + (ff_p_fsat_functional_secondfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_partial. ff_h_fsat_functional_secondfactorsfactorization_product_partial + S (ff_r_fsat_functional_secondfactorsfactorization_product) = S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_partial. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_partial * S ((S (ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (ff_r_fsat_functional_secondfactorsfactorization_product))) /\ ((((exists ff_h_fsat_functional_secondfactorsfactorization_product_successor. ff_h_fsat_functional_secondfactorsfactorization_product_successor + S (ff_s_fsat_functional_secondfactorsfactorization_product) = S ((S (S ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product)) /\ exists ff_q_fsat_functional_secondfactorsfactorization_product_successor. ff_u_fsat_functional_secondfactorsfactorization_product = ff_q_fsat_functional_secondfactorsfactorization_product_successor * S ((S (S ff_i_fsat_functional_secondfactorsfactorization_product)) * ff_v_fsat_functional_secondfactorsfactorization_product) + (ff_s_fsat_functional_secondfactorsfactorization_product))) /\ ff_s_fsat_functional_secondfactorsfactorization_product = ff_r_fsat_functional_secondfactorsfactorization_product * ff_p_fsat_functional_secondfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_functional_secondfactorsfactorization_primes. (exists ftsf_gap_fsat_functional_secondfactorsfactorization_primes_bound. ftsf_gap_fsat_functional_secondfactorsfactorization_primes_bound + S ftsf_index_fsat_functional_secondfactorsfactorization_primes = (mv_factor_count_functional_secondfactors)) -> exists ftsf_factor_fsat_functional_secondfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_functional_secondfactorsfactorization_primes_entry. ff_h_ftsf_fsat_functional_secondfactorsfactorization_primes_entry + S (ftsf_factor_fsat_functional_secondfactorsfactorization_primes) = S ((S (ftsf_index_fsat_functional_secondfactorsfactorization_primes)) * mv_factor_scale_functional_secondfactors)) /\ exists ff_q_ftsf_fsat_functional_secondfactorsfactorization_primes_entry. mv_factor_code_functional_secondfactors = ff_q_ftsf_fsat_functional_secondfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_functional_secondfactorsfactorization_primes)) * mv_factor_scale_functional_secondfactors) + (ftsf_factor_fsat_functional_secondfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_functional_secondfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_functional_secondfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_functional_secondfactorsfactorization_primes_prime. ftsf_factor_fsat_functional_secondfactorsfactorization_primes = frm_prime_left_ftsf_fsat_functional_secondfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_functional_secondfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_functional_secondfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_functional_secondfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_functional_secondfactorsparityeven. (mv_factor_count_functional_secondfactors) = 2 * mv_even_half_functional_secondfactorsparityeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_functional_secondfactorsparityodd. (mv_factor_count_functional_secondfactors) = 2 * mv_odd_half_functional_secondfactorsparityodd + 1) /\ ((b) = 1))))))))))) -> a = b
Bundle node 226; exact statement SHA-256 eb41094b2ceb2273e89e8966ced4cc921decf56dd6bc6dbcb5349c2087aa1135
forall n. ~(n = 0) -> exists z. (((~((n) = 0)) /\ ((((exists mv_square_prime_unique_chosensquare. ((~((mv_square_prime_unique_chosensquare) = 1) /\ forall pvs_left_unique_chosensquareprime pvs_right_unique_chosensquareprime. (mv_square_prime_unique_chosensquare) = pvs_left_unique_chosensquareprime * pvs_right_unique_chosensquareprime -> pvs_left_unique_chosensquareprime = 1 \/ pvs_right_unique_chosensquareprime = 1) /\ (exists pvs_factor_unique_chosensquaredivisor. (n) = (mv_square_prime_unique_chosensquare * mv_square_prime_unique_chosensquare) * pvs_factor_unique_chosensquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_unique_chosensquarefree. (~((sfd_prime_unique_chosensquarefree) = 1) /\ forall pvs_left_unique_chosensquarefreedomain pvs_right_unique_chosensquarefreedomain. (sfd_prime_unique_chosensquarefree) = pvs_left_unique_chosensquarefreedomain * pvs_right_unique_chosensquarefreedomain -> pvs_left_unique_chosensquarefreedomain = 1 \/ pvs_right_unique_chosensquarefreedomain = 1) -> (exists pvs_le_gap_unique_chosensquarefreebound. pvs_le_gap_unique_chosensquarefreebound + (sfd_prime_unique_chosensquarefree) = (n)) -> ~(exists pvs_factor_unique_chosensquarefreesquare. (n) = (sfd_prime_unique_chosensquarefree * sfd_prime_unique_chosensquarefree) * pvs_factor_unique_chosensquarefreesquare)))) /\ (exists mv_factor_code_unique_chosenfactors mv_factor_scale_unique_chosenfactors mv_factor_count_unique_chosenfactors. (((~(n = 0) /\ ((exists ff_u_fsat_unique_chosenfactorsfactorization_product ff_v_fsat_unique_chosenfactorsfactorization_product. ((((exists ff_h_fsat_unique_chosenfactorsfactorization_product_start. ff_h_fsat_unique_chosenfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_unique_chosenfactorsfactorization_product)) /\ exists ff_q_fsat_unique_chosenfactorsfactorization_product_start. ff_u_fsat_unique_chosenfactorsfactorization_product = ff_q_fsat_unique_chosenfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_unique_chosenfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_unique_chosenfactorsfactorization_product_terminal. ff_h_fsat_unique_chosenfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_unique_chosenfactors)) * ff_v_fsat_unique_chosenfactorsfactorization_product)) /\ exists ff_q_fsat_unique_chosenfactorsfactorization_product_terminal. ff_u_fsat_unique_chosenfactorsfactorization_product = ff_q_fsat_unique_chosenfactorsfactorization_product_terminal * S ((S (mv_factor_count_unique_chosenfactors)) * ff_v_fsat_unique_chosenfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_unique_chosenfactorsfactorization_product. (exists ff_lt_fsat_unique_chosenfactorsfactorization_product_bound. ff_lt_fsat_unique_chosenfactorsfactorization_product_bound + S ff_i_fsat_unique_chosenfactorsfactorization_product = mv_factor_count_unique_chosenfactors) -> exists ff_p_fsat_unique_chosenfactorsfactorization_product ff_r_fsat_unique_chosenfactorsfactorization_product ff_s_fsat_unique_chosenfactorsfactorization_product. ((((exists ff_h_fsat_unique_chosenfactorsfactorization_product_factor. ff_h_fsat_unique_chosenfactorsfactorization_product_factor + S (ff_p_fsat_unique_chosenfactorsfactorization_product) = S ((S (ff_i_fsat_unique_chosenfactorsfactorization_product)) * mv_factor_scale_unique_chosenfactors)) /\ exists ff_q_fsat_unique_chosenfactorsfactorization_product_factor. mv_factor_code_unique_chosenfactors = ff_q_fsat_unique_chosenfactorsfactorization_product_factor * S ((S (ff_i_fsat_unique_chosenfactorsfactorization_product)) * mv_factor_scale_unique_chosenfactors) + (ff_p_fsat_unique_chosenfactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_chosenfactorsfactorization_product_partial. ff_h_fsat_unique_chosenfactorsfactorization_product_partial + S (ff_r_fsat_unique_chosenfactorsfactorization_product) = S ((S (ff_i_fsat_unique_chosenfactorsfactorization_product)) * ff_v_fsat_unique_chosenfactorsfactorization_product)) /\ exists ff_q_fsat_unique_chosenfactorsfactorization_product_partial. ff_u_fsat_unique_chosenfactorsfactorization_product = ff_q_fsat_unique_chosenfactorsfactorization_product_partial * S ((S (ff_i_fsat_unique_chosenfactorsfactorization_product)) * ff_v_fsat_unique_chosenfactorsfactorization_product) + (ff_r_fsat_unique_chosenfactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_chosenfactorsfactorization_product_successor. ff_h_fsat_unique_chosenfactorsfactorization_product_successor + S (ff_s_fsat_unique_chosenfactorsfactorization_product) = S ((S (S ff_i_fsat_unique_chosenfactorsfactorization_product)) * ff_v_fsat_unique_chosenfactorsfactorization_product)) /\ exists ff_q_fsat_unique_chosenfactorsfactorization_product_successor. ff_u_fsat_unique_chosenfactorsfactorization_product = ff_q_fsat_unique_chosenfactorsfactorization_product_successor * S ((S (S ff_i_fsat_unique_chosenfactorsfactorization_product)) * ff_v_fsat_unique_chosenfactorsfactorization_product) + (ff_s_fsat_unique_chosenfactorsfactorization_product))) /\ ff_s_fsat_unique_chosenfactorsfactorization_product = ff_r_fsat_unique_chosenfactorsfactorization_product * ff_p_fsat_unique_chosenfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_unique_chosenfactorsfactorization_primes. (exists ftsf_gap_fsat_unique_chosenfactorsfactorization_primes_bound. ftsf_gap_fsat_unique_chosenfactorsfactorization_primes_bound + S ftsf_index_fsat_unique_chosenfactorsfactorization_primes = (mv_factor_count_unique_chosenfactors)) -> exists ftsf_factor_fsat_unique_chosenfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_unique_chosenfactorsfactorization_primes_entry. ff_h_ftsf_fsat_unique_chosenfactorsfactorization_primes_entry + S (ftsf_factor_fsat_unique_chosenfactorsfactorization_primes) = S ((S (ftsf_index_fsat_unique_chosenfactorsfactorization_primes)) * mv_factor_scale_unique_chosenfactors)) /\ exists ff_q_ftsf_fsat_unique_chosenfactorsfactorization_primes_entry. mv_factor_code_unique_chosenfactors = ff_q_ftsf_fsat_unique_chosenfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_unique_chosenfactorsfactorization_primes)) * mv_factor_scale_unique_chosenfactors) + (ftsf_factor_fsat_unique_chosenfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_unique_chosenfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_unique_chosenfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_unique_chosenfactorsfactorization_primes_prime. ftsf_factor_fsat_unique_chosenfactorsfactorization_primes = frm_prime_left_ftsf_fsat_unique_chosenfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_unique_chosenfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_unique_chosenfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_unique_chosenfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_unique_chosenfactorsparityeven. (mv_factor_count_unique_chosenfactors) = 2 * mv_even_half_unique_chosenfactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_unique_chosenfactorsparityodd. (mv_factor_count_unique_chosenfactors) = 2 * mv_odd_half_unique_chosenfactorsparityodd + 1) /\ ((z) = 1))))))))))) /\ forall w. (((~((n) = 0)) /\ ((((exists mv_square_prime_unique_othersquare. ((~((mv_square_prime_unique_othersquare) = 1) /\ forall pvs_left_unique_othersquareprime pvs_right_unique_othersquareprime. (mv_square_prime_unique_othersquare) = pvs_left_unique_othersquareprime * pvs_right_unique_othersquareprime -> pvs_left_unique_othersquareprime = 1 \/ pvs_right_unique_othersquareprime = 1) /\ (exists pvs_factor_unique_othersquaredivisor. (n) = (mv_square_prime_unique_othersquare * mv_square_prime_unique_othersquare) * pvs_factor_unique_othersquaredivisor))) /\ ((w) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_unique_othersquarefree. (~((sfd_prime_unique_othersquarefree) = 1) /\ forall pvs_left_unique_othersquarefreedomain pvs_right_unique_othersquarefreedomain. (sfd_prime_unique_othersquarefree) = pvs_left_unique_othersquarefreedomain * pvs_right_unique_othersquarefreedomain -> pvs_left_unique_othersquarefreedomain = 1 \/ pvs_right_unique_othersquarefreedomain = 1) -> (exists pvs_le_gap_unique_othersquarefreebound. pvs_le_gap_unique_othersquarefreebound + (sfd_prime_unique_othersquarefree) = (n)) -> ~(exists pvs_factor_unique_othersquarefreesquare. (n) = (sfd_prime_unique_othersquarefree * sfd_prime_unique_othersquarefree) * pvs_factor_unique_othersquarefreesquare)))) /\ (exists mv_factor_code_unique_otherfactors mv_factor_scale_unique_otherfactors mv_factor_count_unique_otherfactors. (((~(n = 0) /\ ((exists ff_u_fsat_unique_otherfactorsfactorization_product ff_v_fsat_unique_otherfactorsfactorization_product. ((((exists ff_h_fsat_unique_otherfactorsfactorization_product_start. ff_h_fsat_unique_otherfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_unique_otherfactorsfactorization_product)) /\ exists ff_q_fsat_unique_otherfactorsfactorization_product_start. ff_u_fsat_unique_otherfactorsfactorization_product = ff_q_fsat_unique_otherfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_unique_otherfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_unique_otherfactorsfactorization_product_terminal. ff_h_fsat_unique_otherfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_unique_otherfactors)) * ff_v_fsat_unique_otherfactorsfactorization_product)) /\ exists ff_q_fsat_unique_otherfactorsfactorization_product_terminal. ff_u_fsat_unique_otherfactorsfactorization_product = ff_q_fsat_unique_otherfactorsfactorization_product_terminal * S ((S (mv_factor_count_unique_otherfactors)) * ff_v_fsat_unique_otherfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_unique_otherfactorsfactorization_product. (exists ff_lt_fsat_unique_otherfactorsfactorization_product_bound. ff_lt_fsat_unique_otherfactorsfactorization_product_bound + S ff_i_fsat_unique_otherfactorsfactorization_product = mv_factor_count_unique_otherfactors) -> exists ff_p_fsat_unique_otherfactorsfactorization_product ff_r_fsat_unique_otherfactorsfactorization_product ff_s_fsat_unique_otherfactorsfactorization_product. ((((exists ff_h_fsat_unique_otherfactorsfactorization_product_factor. ff_h_fsat_unique_otherfactorsfactorization_product_factor + S (ff_p_fsat_unique_otherfactorsfactorization_product) = S ((S (ff_i_fsat_unique_otherfactorsfactorization_product)) * mv_factor_scale_unique_otherfactors)) /\ exists ff_q_fsat_unique_otherfactorsfactorization_product_factor. mv_factor_code_unique_otherfactors = ff_q_fsat_unique_otherfactorsfactorization_product_factor * S ((S (ff_i_fsat_unique_otherfactorsfactorization_product)) * mv_factor_scale_unique_otherfactors) + (ff_p_fsat_unique_otherfactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_otherfactorsfactorization_product_partial. ff_h_fsat_unique_otherfactorsfactorization_product_partial + S (ff_r_fsat_unique_otherfactorsfactorization_product) = S ((S (ff_i_fsat_unique_otherfactorsfactorization_product)) * ff_v_fsat_unique_otherfactorsfactorization_product)) /\ exists ff_q_fsat_unique_otherfactorsfactorization_product_partial. ff_u_fsat_unique_otherfactorsfactorization_product = ff_q_fsat_unique_otherfactorsfactorization_product_partial * S ((S (ff_i_fsat_unique_otherfactorsfactorization_product)) * ff_v_fsat_unique_otherfactorsfactorization_product) + (ff_r_fsat_unique_otherfactorsfactorization_product))) /\ ((((exists ff_h_fsat_unique_otherfactorsfactorization_product_successor. ff_h_fsat_unique_otherfactorsfactorization_product_successor + S (ff_s_fsat_unique_otherfactorsfactorization_product) = S ((S (S ff_i_fsat_unique_otherfactorsfactorization_product)) * ff_v_fsat_unique_otherfactorsfactorization_product)) /\ exists ff_q_fsat_unique_otherfactorsfactorization_product_successor. ff_u_fsat_unique_otherfactorsfactorization_product = ff_q_fsat_unique_otherfactorsfactorization_product_successor * S ((S (S ff_i_fsat_unique_otherfactorsfactorization_product)) * ff_v_fsat_unique_otherfactorsfactorization_product) + (ff_s_fsat_unique_otherfactorsfactorization_product))) /\ ff_s_fsat_unique_otherfactorsfactorization_product = ff_r_fsat_unique_otherfactorsfactorization_product * ff_p_fsat_unique_otherfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_unique_otherfactorsfactorization_primes. (exists ftsf_gap_fsat_unique_otherfactorsfactorization_primes_bound. ftsf_gap_fsat_unique_otherfactorsfactorization_primes_bound + S ftsf_index_fsat_unique_otherfactorsfactorization_primes = (mv_factor_count_unique_otherfactors)) -> exists ftsf_factor_fsat_unique_otherfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_unique_otherfactorsfactorization_primes_entry. ff_h_ftsf_fsat_unique_otherfactorsfactorization_primes_entry + S (ftsf_factor_fsat_unique_otherfactorsfactorization_primes) = S ((S (ftsf_index_fsat_unique_otherfactorsfactorization_primes)) * mv_factor_scale_unique_otherfactors)) /\ exists ff_q_ftsf_fsat_unique_otherfactorsfactorization_primes_entry. mv_factor_code_unique_otherfactors = ff_q_ftsf_fsat_unique_otherfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_unique_otherfactorsfactorization_primes)) * mv_factor_scale_unique_otherfactors) + (ftsf_factor_fsat_unique_otherfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_unique_otherfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_unique_otherfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_unique_otherfactorsfactorization_primes_prime. ftsf_factor_fsat_unique_otherfactorsfactorization_primes = frm_prime_left_ftsf_fsat_unique_otherfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_unique_otherfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_unique_otherfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_unique_otherfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_unique_otherfactorsparityeven. (mv_factor_count_unique_otherfactors) = 2 * mv_even_half_unique_otherfactorsparityeven) /\ ((w) = 2))) \/ (((exists mv_odd_half_unique_otherfactorsparityodd. (mv_factor_count_unique_otherfactors) = 2 * mv_odd_half_unique_otherfactorsparityodd + 1) /\ ((w) = 1))))))))))) -> w = z
Bundle node 227; exact statement SHA-256 7e25b6ee50f327823f711ec20cfbd25178b198c7210f11bc73f08441e73273e6
((~((1) = 0)) /\ ((((exists mv_square_prime_one_valuesquare. ((~((mv_square_prime_one_valuesquare) = 1) /\ forall pvs_left_one_valuesquareprime pvs_right_one_valuesquareprime. (mv_square_prime_one_valuesquare) = pvs_left_one_valuesquareprime * pvs_right_one_valuesquareprime -> pvs_left_one_valuesquareprime = 1 \/ pvs_right_one_valuesquareprime = 1) /\ (exists pvs_factor_one_valuesquaredivisor. (1) = (mv_square_prime_one_valuesquare * mv_square_prime_one_valuesquare) * pvs_factor_one_valuesquaredivisor))) /\ ((2) = 0))) \/ (((((~((1) = 0)) /\ (forall sfd_prime_one_valuesquarefree. (~((sfd_prime_one_valuesquarefree) = 1) /\ forall pvs_left_one_valuesquarefreedomain pvs_right_one_valuesquarefreedomain. (sfd_prime_one_valuesquarefree) = pvs_left_one_valuesquarefreedomain * pvs_right_one_valuesquarefreedomain -> pvs_left_one_valuesquarefreedomain = 1 \/ pvs_right_one_valuesquarefreedomain = 1) -> (exists pvs_le_gap_one_valuesquarefreebound. pvs_le_gap_one_valuesquarefreebound + (sfd_prime_one_valuesquarefree) = (1)) -> ~(exists pvs_factor_one_valuesquarefreesquare. (1) = (sfd_prime_one_valuesquarefree * sfd_prime_one_valuesquarefree) * pvs_factor_one_valuesquarefreesquare)))) /\ (exists mv_factor_code_one_valuefactors mv_factor_scale_one_valuefactors mv_factor_count_one_valuefactors. (((~(1 = 0) /\ ((exists ff_u_fsat_one_valuefactorsfactorization_product ff_v_fsat_one_valuefactorsfactorization_product. ((((exists ff_h_fsat_one_valuefactorsfactorization_product_start. ff_h_fsat_one_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_one_valuefactorsfactorization_product)) /\ exists ff_q_fsat_one_valuefactorsfactorization_product_start. ff_u_fsat_one_valuefactorsfactorization_product = ff_q_fsat_one_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_one_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_one_valuefactorsfactorization_product_terminal. ff_h_fsat_one_valuefactorsfactorization_product_terminal + S (1) = S ((S (mv_factor_count_one_valuefactors)) * ff_v_fsat_one_valuefactorsfactorization_product)) /\ exists ff_q_fsat_one_valuefactorsfactorization_product_terminal. ff_u_fsat_one_valuefactorsfactorization_product = ff_q_fsat_one_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_one_valuefactors)) * ff_v_fsat_one_valuefactorsfactorization_product) + (1))) /\ forall ff_i_fsat_one_valuefactorsfactorization_product. (exists ff_lt_fsat_one_valuefactorsfactorization_product_bound. ff_lt_fsat_one_valuefactorsfactorization_product_bound + S ff_i_fsat_one_valuefactorsfactorization_product = mv_factor_count_one_valuefactors) -> exists ff_p_fsat_one_valuefactorsfactorization_product ff_r_fsat_one_valuefactorsfactorization_product ff_s_fsat_one_valuefactorsfactorization_product. ((((exists ff_h_fsat_one_valuefactorsfactorization_product_factor. ff_h_fsat_one_valuefactorsfactorization_product_factor + S (ff_p_fsat_one_valuefactorsfactorization_product) = S ((S (ff_i_fsat_one_valuefactorsfactorization_product)) * mv_factor_scale_one_valuefactors)) /\ exists ff_q_fsat_one_valuefactorsfactorization_product_factor. mv_factor_code_one_valuefactors = ff_q_fsat_one_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_one_valuefactorsfactorization_product)) * mv_factor_scale_one_valuefactors) + (ff_p_fsat_one_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_one_valuefactorsfactorization_product_partial. ff_h_fsat_one_valuefactorsfactorization_product_partial + S (ff_r_fsat_one_valuefactorsfactorization_product) = S ((S (ff_i_fsat_one_valuefactorsfactorization_product)) * ff_v_fsat_one_valuefactorsfactorization_product)) /\ exists ff_q_fsat_one_valuefactorsfactorization_product_partial. ff_u_fsat_one_valuefactorsfactorization_product = ff_q_fsat_one_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_one_valuefactorsfactorization_product)) * ff_v_fsat_one_valuefactorsfactorization_product) + (ff_r_fsat_one_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_one_valuefactorsfactorization_product_successor. ff_h_fsat_one_valuefactorsfactorization_product_successor + S (ff_s_fsat_one_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_one_valuefactorsfactorization_product)) * ff_v_fsat_one_valuefactorsfactorization_product)) /\ exists ff_q_fsat_one_valuefactorsfactorization_product_successor. ff_u_fsat_one_valuefactorsfactorization_product = ff_q_fsat_one_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_one_valuefactorsfactorization_product)) * ff_v_fsat_one_valuefactorsfactorization_product) + (ff_s_fsat_one_valuefactorsfactorization_product))) /\ ff_s_fsat_one_valuefactorsfactorization_product = ff_r_fsat_one_valuefactorsfactorization_product * ff_p_fsat_one_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_one_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_one_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_one_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_one_valuefactorsfactorization_primes = (mv_factor_count_one_valuefactors)) -> exists ftsf_factor_fsat_one_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_one_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_one_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_one_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_one_valuefactorsfactorization_primes)) * mv_factor_scale_one_valuefactors)) /\ exists ff_q_ftsf_fsat_one_valuefactorsfactorization_primes_entry. mv_factor_code_one_valuefactors = ff_q_ftsf_fsat_one_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_one_valuefactorsfactorization_primes)) * mv_factor_scale_one_valuefactors) + (ftsf_factor_fsat_one_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_one_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_one_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_one_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_one_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_one_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_one_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_one_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_one_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_one_valuefactorsparityeven. (mv_factor_count_one_valuefactors) = 2 * mv_even_half_one_valuefactorsparityeven) /\ ((2) = 2))) \/ (((exists mv_odd_half_one_valuefactorsparityodd. (mv_factor_count_one_valuefactors) = 2 * mv_odd_half_one_valuefactorsparityodd + 1) /\ ((2) = 1))))))))))
Bundle node 228; exact statement SHA-256 18e75b910b5a1825152440613d1ca15e8b951a7fd7020066e104a22d5d6833a7
forall n d. (((~((n) = 0)) /\ (forall sfd_prime_divisor_source. (~((sfd_prime_divisor_source) = 1) /\ forall pvs_left_divisor_sourcedomain pvs_right_divisor_sourcedomain. (sfd_prime_divisor_source) = pvs_left_divisor_sourcedomain * pvs_right_divisor_sourcedomain -> pvs_left_divisor_sourcedomain = 1 \/ pvs_right_divisor_sourcedomain = 1) -> (exists pvs_le_gap_divisor_sourcebound. pvs_le_gap_divisor_sourcebound + (sfd_prime_divisor_source) = (n)) -> ~(exists pvs_factor_divisor_sourcesquare. (n) = (sfd_prime_divisor_source * sfd_prime_divisor_source) * pvs_factor_divisor_sourcesquare)))) -> (exists pvs_factor_divisor_at. (n) = (d) * pvs_factor_divisor_at) -> (((~((d) = 0)) /\ (forall sfd_prime_divisor_target. (~((sfd_prime_divisor_target) = 1) /\ forall pvs_left_divisor_targetdomain pvs_right_divisor_targetdomain. (sfd_prime_divisor_target) = pvs_left_divisor_targetdomain * pvs_right_divisor_targetdomain -> pvs_left_divisor_targetdomain = 1 \/ pvs_right_divisor_targetdomain = 1) -> (exists pvs_le_gap_divisor_targetbound. pvs_le_gap_divisor_targetbound + (sfd_prime_divisor_target) = (d)) -> ~(exists pvs_factor_divisor_targetsquare. (d) = (sfd_prime_divisor_target * sfd_prime_divisor_target) * pvs_factor_divisor_targetsquare))))
Bundle node 229; exact statement SHA-256 c51862a507ea4c30431199732d527fcbebfaa4a2c37b7ae7d62edbbada9a7f26
forall p. (~((p) = 1) /\ forall pvs_left_squarefree_prime pvs_right_squarefree_prime. (p) = pvs_left_squarefree_prime * pvs_right_squarefree_prime -> pvs_left_squarefree_prime = 1 \/ pvs_right_squarefree_prime = 1) -> (((~((p) = 0)) /\ (forall sfd_prime_prime_result. (~((sfd_prime_prime_result) = 1) /\ forall pvs_left_prime_resultdomain pvs_right_prime_resultdomain. (sfd_prime_prime_result) = pvs_left_prime_resultdomain * pvs_right_prime_resultdomain -> pvs_left_prime_resultdomain = 1 \/ pvs_right_prime_resultdomain = 1) -> (exists pvs_le_gap_prime_resultbound. pvs_le_gap_prime_resultbound + (sfd_prime_prime_result) = (p)) -> ~(exists pvs_factor_prime_resultsquare. (p) = (sfd_prime_prime_result * sfd_prime_prime_result) * pvs_factor_prime_resultsquare))))
Bundle node 230; exact statement SHA-256 6c8b8ec36c0aa7b8741753a928b524bb4b049a4a5ca8b046f52b2cb456a0244a
forall p n. (~((p) = 1) /\ forall pvs_left_fresh_prime pvs_right_fresh_prime. (p) = pvs_left_fresh_prime * pvs_right_fresh_prime -> pvs_left_fresh_prime = 1 \/ pvs_right_fresh_prime = 1) -> (((~((n) = 0)) /\ (forall sfd_prime_fresh_squarefree. (~((sfd_prime_fresh_squarefree) = 1) /\ forall pvs_left_fresh_squarefreedomain pvs_right_fresh_squarefreedomain. (sfd_prime_fresh_squarefree) = pvs_left_fresh_squarefreedomain * pvs_right_fresh_squarefreedomain -> pvs_left_fresh_squarefreedomain = 1 \/ pvs_right_fresh_squarefreedomain = 1) -> (exists pvs_le_gap_fresh_squarefreebound. pvs_le_gap_fresh_squarefreebound + (sfd_prime_fresh_squarefree) = (n)) -> ~(exists pvs_factor_fresh_squarefreesquare. (n) = (sfd_prime_fresh_squarefree * sfd_prime_fresh_squarefree) * pvs_factor_fresh_squarefreesquare)))) -> ~(exists pvs_factor_fresh_nondivisor. (n) = (p) * pvs_factor_fresh_nondivisor) -> (((~((p * n) = 0)) /\ (forall sfd_prime_fresh_product. (~((sfd_prime_fresh_product) = 1) /\ forall pvs_left_fresh_productdomain pvs_right_fresh_productdomain. (sfd_prime_fresh_product) = pvs_left_fresh_productdomain * pvs_right_fresh_productdomain -> pvs_left_fresh_productdomain = 1 \/ pvs_right_fresh_productdomain = 1) -> (exists pvs_le_gap_fresh_productbound. pvs_le_gap_fresh_productbound + (sfd_prime_fresh_product) = (p * n)) -> ~(exists pvs_factor_fresh_productsquare. (p * n) = (sfd_prime_fresh_product * sfd_prime_fresh_product) * pvs_factor_fresh_productsquare))))
Bundle node 231; exact statement SHA-256 1536449156e44f130343327ed2f57635f67299e450aeefef8681d9fdac6e8cfe
forall n b c l p. ((~(n = 0) /\ ((exists ff_u_fsat_mps_append_source_product ff_v_fsat_mps_append_source_product. ((((exists ff_h_fsat_mps_append_source_product_start. ff_h_fsat_mps_append_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_start. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_start * S ((S (0)) * ff_v_fsat_mps_append_source_product) + (1))) /\ ((((exists ff_h_fsat_mps_append_source_product_terminal. ff_h_fsat_mps_append_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_terminal. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_terminal * S ((S (l)) * ff_v_fsat_mps_append_source_product) + (n))) /\ forall ff_i_fsat_mps_append_source_product. (exists ff_lt_fsat_mps_append_source_product_bound. ff_lt_fsat_mps_append_source_product_bound + S ff_i_fsat_mps_append_source_product = l) -> exists ff_p_fsat_mps_append_source_product ff_r_fsat_mps_append_source_product ff_s_fsat_mps_append_source_product. ((((exists ff_h_fsat_mps_append_source_product_factor. ff_h_fsat_mps_append_source_product_factor + S (ff_p_fsat_mps_append_source_product) = S ((S (ff_i_fsat_mps_append_source_product)) * c)) /\ exists ff_q_fsat_mps_append_source_product_factor. b = ff_q_fsat_mps_append_source_product_factor * S ((S (ff_i_fsat_mps_append_source_product)) * c) + (ff_p_fsat_mps_append_source_product))) /\ ((((exists ff_h_fsat_mps_append_source_product_partial. ff_h_fsat_mps_append_source_product_partial + S (ff_r_fsat_mps_append_source_product) = S ((S (ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_partial. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_partial * S ((S (ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product) + (ff_r_fsat_mps_append_source_product))) /\ ((((exists ff_h_fsat_mps_append_source_product_successor. ff_h_fsat_mps_append_source_product_successor + S (ff_s_fsat_mps_append_source_product) = S ((S (S ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product)) /\ exists ff_q_fsat_mps_append_source_product_successor. ff_u_fsat_mps_append_source_product = ff_q_fsat_mps_append_source_product_successor * S ((S (S ff_i_fsat_mps_append_source_product)) * ff_v_fsat_mps_append_source_product) + (ff_s_fsat_mps_append_source_product))) /\ ff_s_fsat_mps_append_source_product = ff_r_fsat_mps_append_source_product * ff_p_fsat_mps_append_source_product)))))) /\ (forall ftsf_index_fsat_mps_append_source_primes. (exists ftsf_gap_fsat_mps_append_source_primes_bound. ftsf_gap_fsat_mps_append_source_primes_bound + S ftsf_index_fsat_mps_append_source_primes = (l)) -> exists ftsf_factor_fsat_mps_append_source_primes. ((((exists ff_h_ftsf_fsat_mps_append_source_primes_entry. ff_h_ftsf_fsat_mps_append_source_primes_entry + S (ftsf_factor_fsat_mps_append_source_primes) = S ((S (ftsf_index_fsat_mps_append_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_mps_append_source_primes_entry. b = ff_q_ftsf_fsat_mps_append_source_primes_entry * S ((S (ftsf_index_fsat_mps_append_source_primes)) * c) + (ftsf_factor_fsat_mps_append_source_primes))) /\ ((~(ftsf_factor_fsat_mps_append_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mps_append_source_primes_prime frm_prime_right_ftsf_fsat_mps_append_source_primes_prime. ftsf_factor_fsat_mps_append_source_primes = frm_prime_left_ftsf_fsat_mps_append_source_primes_prime * frm_prime_right_ftsf_fsat_mps_append_source_primes_prime -> frm_prime_left_ftsf_fsat_mps_append_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mps_append_source_primes_prime = 1))))))) -> (~((p) = 1) /\ forall pvs_left_append_prime pvs_right_append_prime. (p) = pvs_left_append_prime * pvs_right_append_prime -> pvs_left_append_prime = 1 \/ pvs_right_append_prime = 1) -> exists d e. ((~(n * p = 0) /\ ((exists ff_u_fsat_mps_append_target_product ff_v_fsat_mps_append_target_product. ((((exists ff_h_fsat_mps_append_target_product_start. ff_h_fsat_mps_append_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_start. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_start * S ((S (0)) * ff_v_fsat_mps_append_target_product) + (1))) /\ ((((exists ff_h_fsat_mps_append_target_product_terminal. ff_h_fsat_mps_append_target_product_terminal + S (n * p) = S ((S (S l)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_terminal. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_terminal * S ((S (S l)) * ff_v_fsat_mps_append_target_product) + (n * p))) /\ forall ff_i_fsat_mps_append_target_product. (exists ff_lt_fsat_mps_append_target_product_bound. ff_lt_fsat_mps_append_target_product_bound + S ff_i_fsat_mps_append_target_product = S l) -> exists ff_p_fsat_mps_append_target_product ff_r_fsat_mps_append_target_product ff_s_fsat_mps_append_target_product. ((((exists ff_h_fsat_mps_append_target_product_factor. ff_h_fsat_mps_append_target_product_factor + S (ff_p_fsat_mps_append_target_product) = S ((S (ff_i_fsat_mps_append_target_product)) * e)) /\ exists ff_q_fsat_mps_append_target_product_factor. d = ff_q_fsat_mps_append_target_product_factor * S ((S (ff_i_fsat_mps_append_target_product)) * e) + (ff_p_fsat_mps_append_target_product))) /\ ((((exists ff_h_fsat_mps_append_target_product_partial. ff_h_fsat_mps_append_target_product_partial + S (ff_r_fsat_mps_append_target_product) = S ((S (ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_partial. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_partial * S ((S (ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product) + (ff_r_fsat_mps_append_target_product))) /\ ((((exists ff_h_fsat_mps_append_target_product_successor. ff_h_fsat_mps_append_target_product_successor + S (ff_s_fsat_mps_append_target_product) = S ((S (S ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product)) /\ exists ff_q_fsat_mps_append_target_product_successor. ff_u_fsat_mps_append_target_product = ff_q_fsat_mps_append_target_product_successor * S ((S (S ff_i_fsat_mps_append_target_product)) * ff_v_fsat_mps_append_target_product) + (ff_s_fsat_mps_append_target_product))) /\ ff_s_fsat_mps_append_target_product = ff_r_fsat_mps_append_target_product * ff_p_fsat_mps_append_target_product)))))) /\ (forall ftsf_index_fsat_mps_append_target_primes. (exists ftsf_gap_fsat_mps_append_target_primes_bound. ftsf_gap_fsat_mps_append_target_primes_bound + S ftsf_index_fsat_mps_append_target_primes = (S l)) -> exists ftsf_factor_fsat_mps_append_target_primes. ((((exists ff_h_ftsf_fsat_mps_append_target_primes_entry. ff_h_ftsf_fsat_mps_append_target_primes_entry + S (ftsf_factor_fsat_mps_append_target_primes) = S ((S (ftsf_index_fsat_mps_append_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_mps_append_target_primes_entry. d = ff_q_ftsf_fsat_mps_append_target_primes_entry * S ((S (ftsf_index_fsat_mps_append_target_primes)) * e) + (ftsf_factor_fsat_mps_append_target_primes))) /\ ((~(ftsf_factor_fsat_mps_append_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_mps_append_target_primes_prime frm_prime_right_ftsf_fsat_mps_append_target_primes_prime. ftsf_factor_fsat_mps_append_target_primes = frm_prime_left_ftsf_fsat_mps_append_target_primes_prime * frm_prime_right_ftsf_fsat_mps_append_target_primes_prime -> frm_prime_left_ftsf_fsat_mps_append_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_mps_append_target_primes_prime = 1)))))))
Bundle node 232; exact statement SHA-256 279162e9773a3aa35ac83c96557290090cd9686942e5c882d9bafbf849763a64
exists mps_positive_unit_negation mps_negative_unit_negation. (((((2) = 2 * (mps_positive_unit_negation) /\ (mps_negative_unit_negation) = 0) \/ exists ge_signed_half_unit_negationsource. (((2) = 2 * ge_signed_half_unit_negationsource + 1 /\ (mps_positive_unit_negation) = 0) /\ (mps_negative_unit_negation) = S ge_signed_half_unit_negationsource))) /\ ((((1) = 2 * (mps_negative_unit_negation) /\ (mps_positive_unit_negation) = 0) \/ exists ge_signed_half_unit_negationtarget. (((1) = 2 * ge_signed_half_unit_negationtarget + 1 /\ (mps_negative_unit_negation) = 0) /\ (mps_positive_unit_negation) = S ge_signed_half_unit_negationtarget))))
Bundle node 233; exact statement SHA-256 6966042ee3f11a8d46af7773ff9dabf6cb048a649b3c294b5fea003ea5091bb0
forall n a b. ((((exists mv_even_half_successor_sourceeven. (n) = 2 * mv_even_half_successor_sourceeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_successor_sourceodd. (n) = 2 * mv_odd_half_successor_sourceodd + 1) /\ ((a) = 1)))) -> ((((exists mv_even_half_successor_targeteven. (S n) = 2 * mv_even_half_successor_targeteven) /\ ((b) = 2))) \/ (((exists mv_odd_half_successor_targetodd. (S n) = 2 * mv_odd_half_successor_targetodd + 1) /\ ((b) = 1)))) -> (exists mps_positive_successor_negation mps_negative_successor_negation. (((((a) = 2 * (mps_positive_successor_negation) /\ (mps_negative_successor_negation) = 0) \/ exists ge_signed_half_successor_negationsource. (((a) = 2 * ge_signed_half_successor_negationsource + 1 /\ (mps_positive_successor_negation) = 0) /\ (mps_negative_successor_negation) = S ge_signed_half_successor_negationsource))) /\ ((((b) = 2 * (mps_negative_successor_negation) /\ (mps_positive_successor_negation) = 0) \/ exists ge_signed_half_successor_negationtarget. (((b) = 2 * ge_signed_half_successor_negationtarget + 1 /\ (mps_negative_successor_negation) = 0) /\ (mps_positive_successor_negation) = S ge_signed_half_successor_negationtarget)))))
Bundle node 234; exact statement SHA-256 91a233976cfdb569c20bf7af0bd3e27cf984aeb8bcdabb76a000851f579d613c
forall n p z. (~((p) = 1) /\ forall pvs_left_square_value_prime pvs_right_square_value_prime. (p) = pvs_left_square_value_prime * pvs_right_square_value_prime -> pvs_left_square_value_prime = 1 \/ pvs_right_square_value_prime = 1) -> (exists pvs_factor_square_value_divisor. (n) = (p * p) * pvs_factor_square_value_divisor) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_square_value_inputsquare. ((~((mv_square_prime_square_value_inputsquare) = 1) /\ forall pvs_left_square_value_inputsquareprime pvs_right_square_value_inputsquareprime. (mv_square_prime_square_value_inputsquare) = pvs_left_square_value_inputsquareprime * pvs_right_square_value_inputsquareprime -> pvs_left_square_value_inputsquareprime = 1 \/ pvs_right_square_value_inputsquareprime = 1) /\ (exists pvs_factor_square_value_inputsquaredivisor. (n) = (mv_square_prime_square_value_inputsquare * mv_square_prime_square_value_inputsquare) * pvs_factor_square_value_inputsquaredivisor))) /\ ((z) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_square_value_inputsquarefree. (~((sfd_prime_square_value_inputsquarefree) = 1) /\ forall pvs_left_square_value_inputsquarefreedomain pvs_right_square_value_inputsquarefreedomain. (sfd_prime_square_value_inputsquarefree) = pvs_left_square_value_inputsquarefreedomain * pvs_right_square_value_inputsquarefreedomain -> pvs_left_square_value_inputsquarefreedomain = 1 \/ pvs_right_square_value_inputsquarefreedomain = 1) -> (exists pvs_le_gap_square_value_inputsquarefreebound. pvs_le_gap_square_value_inputsquarefreebound + (sfd_prime_square_value_inputsquarefree) = (n)) -> ~(exists pvs_factor_square_value_inputsquarefreesquare. (n) = (sfd_prime_square_value_inputsquarefree * sfd_prime_square_value_inputsquarefree) * pvs_factor_square_value_inputsquarefreesquare)))) /\ (exists mv_factor_code_square_value_inputfactors mv_factor_scale_square_value_inputfactors mv_factor_count_square_value_inputfactors. (((~(n = 0) /\ ((exists ff_u_fsat_square_value_inputfactorsfactorization_product ff_v_fsat_square_value_inputfactorsfactorization_product. ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_start. ff_h_fsat_square_value_inputfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_start. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_terminal. ff_h_fsat_square_value_inputfactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_square_value_inputfactors)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_terminal. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_terminal * S ((S (mv_factor_count_square_value_inputfactors)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (n))) /\ forall ff_i_fsat_square_value_inputfactorsfactorization_product. (exists ff_lt_fsat_square_value_inputfactorsfactorization_product_bound. ff_lt_fsat_square_value_inputfactorsfactorization_product_bound + S ff_i_fsat_square_value_inputfactorsfactorization_product = mv_factor_count_square_value_inputfactors) -> exists ff_p_fsat_square_value_inputfactorsfactorization_product ff_r_fsat_square_value_inputfactorsfactorization_product ff_s_fsat_square_value_inputfactorsfactorization_product. ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_factor. ff_h_fsat_square_value_inputfactorsfactorization_product_factor + S (ff_p_fsat_square_value_inputfactorsfactorization_product) = S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * mv_factor_scale_square_value_inputfactors)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_factor. mv_factor_code_square_value_inputfactors = ff_q_fsat_square_value_inputfactorsfactorization_product_factor * S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * mv_factor_scale_square_value_inputfactors) + (ff_p_fsat_square_value_inputfactorsfactorization_product))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_partial. ff_h_fsat_square_value_inputfactorsfactorization_product_partial + S (ff_r_fsat_square_value_inputfactorsfactorization_product) = S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_partial. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_partial * S ((S (ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (ff_r_fsat_square_value_inputfactorsfactorization_product))) /\ ((((exists ff_h_fsat_square_value_inputfactorsfactorization_product_successor. ff_h_fsat_square_value_inputfactorsfactorization_product_successor + S (ff_s_fsat_square_value_inputfactorsfactorization_product) = S ((S (S ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product)) /\ exists ff_q_fsat_square_value_inputfactorsfactorization_product_successor. ff_u_fsat_square_value_inputfactorsfactorization_product = ff_q_fsat_square_value_inputfactorsfactorization_product_successor * S ((S (S ff_i_fsat_square_value_inputfactorsfactorization_product)) * ff_v_fsat_square_value_inputfactorsfactorization_product) + (ff_s_fsat_square_value_inputfactorsfactorization_product))) /\ ff_s_fsat_square_value_inputfactorsfactorization_product = ff_r_fsat_square_value_inputfactorsfactorization_product * ff_p_fsat_square_value_inputfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_square_value_inputfactorsfactorization_primes. (exists ftsf_gap_fsat_square_value_inputfactorsfactorization_primes_bound. ftsf_gap_fsat_square_value_inputfactorsfactorization_primes_bound + S ftsf_index_fsat_square_value_inputfactorsfactorization_primes = (mv_factor_count_square_value_inputfactors)) -> exists ftsf_factor_fsat_square_value_inputfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry. ff_h_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry + S (ftsf_factor_fsat_square_value_inputfactorsfactorization_primes) = S ((S (ftsf_index_fsat_square_value_inputfactorsfactorization_primes)) * mv_factor_scale_square_value_inputfactors)) /\ exists ff_q_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry. mv_factor_code_square_value_inputfactors = ff_q_ftsf_fsat_square_value_inputfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_square_value_inputfactorsfactorization_primes)) * mv_factor_scale_square_value_inputfactors) + (ftsf_factor_fsat_square_value_inputfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_square_value_inputfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime. ftsf_factor_fsat_square_value_inputfactorsfactorization_primes = frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_square_value_inputfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_square_value_inputfactorsparityeven. (mv_factor_count_square_value_inputfactors) = 2 * mv_even_half_square_value_inputfactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_square_value_inputfactorsparityodd. (mv_factor_count_square_value_inputfactors) = 2 * mv_odd_half_square_value_inputfactorsparityodd + 1) /\ ((z) = 1))))))))))) -> z = 0
Bundle node 235; exact statement SHA-256 2b0116e6d32e45fe7ae5e9a8bd7c11e5f95a88021cd42786276cff6e7ec303d2
forall p n a b. (~((p) = 1) /\ forall pvs_left_step_prime pvs_right_step_prime. (p) = pvs_left_step_prime * pvs_right_step_prime -> pvs_left_step_prime = 1 \/ pvs_right_step_prime = 1) -> ~(exists pvs_factor_step_fresh. (n) = (p) * pvs_factor_step_fresh) -> (((~((n) = 0)) /\ ((((exists mv_square_prime_step_sourcesquare. ((~((mv_square_prime_step_sourcesquare) = 1) /\ forall pvs_left_step_sourcesquareprime pvs_right_step_sourcesquareprime. (mv_square_prime_step_sourcesquare) = pvs_left_step_sourcesquareprime * pvs_right_step_sourcesquareprime -> pvs_left_step_sourcesquareprime = 1 \/ pvs_right_step_sourcesquareprime = 1) /\ (exists pvs_factor_step_sourcesquaredivisor. (n) = (mv_square_prime_step_sourcesquare * mv_square_prime_step_sourcesquare) * pvs_factor_step_sourcesquaredivisor))) /\ ((a) = 0))) \/ (((((~((n) = 0)) /\ (forall sfd_prime_step_sourcesquarefree. (~((sfd_prime_step_sourcesquarefree) = 1) /\ forall pvs_left_step_sourcesquarefreedomain pvs_right_step_sourcesquarefreedomain. (sfd_prime_step_sourcesquarefree) = pvs_left_step_sourcesquarefreedomain * pvs_right_step_sourcesquarefreedomain -> pvs_left_step_sourcesquarefreedomain = 1 \/ pvs_right_step_sourcesquarefreedomain = 1) -> (exists pvs_le_gap_step_sourcesquarefreebound. pvs_le_gap_step_sourcesquarefreebound + (sfd_prime_step_sourcesquarefree) = (n)) -> ~(exists pvs_factor_step_sourcesquarefreesquare. (n) = (sfd_prime_step_sourcesquarefree * sfd_prime_step_sourcesquarefree) * pvs_factor_step_sourcesquarefreesquare)))) /\ (exists mv_factor_code_step_sourcefactors mv_factor_scale_step_sourcefactors mv_factor_count_step_sourcefactors. (((~(n = 0) /\ ((exists ff_u_fsat_step_sourcefactorsfactorization_product ff_v_fsat_step_sourcefactorsfactorization_product. ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_start. ff_h_fsat_step_sourcefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_start. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_terminal. ff_h_fsat_step_sourcefactorsfactorization_product_terminal + S (n) = S ((S (mv_factor_count_step_sourcefactors)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_terminal. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_terminal * S ((S (mv_factor_count_step_sourcefactors)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (n))) /\ forall ff_i_fsat_step_sourcefactorsfactorization_product. (exists ff_lt_fsat_step_sourcefactorsfactorization_product_bound. ff_lt_fsat_step_sourcefactorsfactorization_product_bound + S ff_i_fsat_step_sourcefactorsfactorization_product = mv_factor_count_step_sourcefactors) -> exists ff_p_fsat_step_sourcefactorsfactorization_product ff_r_fsat_step_sourcefactorsfactorization_product ff_s_fsat_step_sourcefactorsfactorization_product. ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_factor. ff_h_fsat_step_sourcefactorsfactorization_product_factor + S (ff_p_fsat_step_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * mv_factor_scale_step_sourcefactors)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_factor. mv_factor_code_step_sourcefactors = ff_q_fsat_step_sourcefactorsfactorization_product_factor * S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * mv_factor_scale_step_sourcefactors) + (ff_p_fsat_step_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_partial. ff_h_fsat_step_sourcefactorsfactorization_product_partial + S (ff_r_fsat_step_sourcefactorsfactorization_product) = S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_partial. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_partial * S ((S (ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (ff_r_fsat_step_sourcefactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_sourcefactorsfactorization_product_successor. ff_h_fsat_step_sourcefactorsfactorization_product_successor + S (ff_s_fsat_step_sourcefactorsfactorization_product) = S ((S (S ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product)) /\ exists ff_q_fsat_step_sourcefactorsfactorization_product_successor. ff_u_fsat_step_sourcefactorsfactorization_product = ff_q_fsat_step_sourcefactorsfactorization_product_successor * S ((S (S ff_i_fsat_step_sourcefactorsfactorization_product)) * ff_v_fsat_step_sourcefactorsfactorization_product) + (ff_s_fsat_step_sourcefactorsfactorization_product))) /\ ff_s_fsat_step_sourcefactorsfactorization_product = ff_r_fsat_step_sourcefactorsfactorization_product * ff_p_fsat_step_sourcefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_step_sourcefactorsfactorization_primes. (exists ftsf_gap_fsat_step_sourcefactorsfactorization_primes_bound. ftsf_gap_fsat_step_sourcefactorsfactorization_primes_bound + S ftsf_index_fsat_step_sourcefactorsfactorization_primes = (mv_factor_count_step_sourcefactors)) -> exists ftsf_factor_fsat_step_sourcefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_step_sourcefactorsfactorization_primes_entry. ff_h_ftsf_fsat_step_sourcefactorsfactorization_primes_entry + S (ftsf_factor_fsat_step_sourcefactorsfactorization_primes) = S ((S (ftsf_index_fsat_step_sourcefactorsfactorization_primes)) * mv_factor_scale_step_sourcefactors)) /\ exists ff_q_ftsf_fsat_step_sourcefactorsfactorization_primes_entry. mv_factor_code_step_sourcefactors = ff_q_ftsf_fsat_step_sourcefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_step_sourcefactorsfactorization_primes)) * mv_factor_scale_step_sourcefactors) + (ftsf_factor_fsat_step_sourcefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_step_sourcefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_step_sourcefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_step_sourcefactorsfactorization_primes_prime. ftsf_factor_fsat_step_sourcefactorsfactorization_primes = frm_prime_left_ftsf_fsat_step_sourcefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_step_sourcefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_step_sourcefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_step_sourcefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_step_sourcefactorsparityeven. (mv_factor_count_step_sourcefactors) = 2 * mv_even_half_step_sourcefactorsparityeven) /\ ((a) = 2))) \/ (((exists mv_odd_half_step_sourcefactorsparityodd. (mv_factor_count_step_sourcefactors) = 2 * mv_odd_half_step_sourcefactorsparityodd + 1) /\ ((a) = 1))))))))))) -> (((~((p * n) = 0)) /\ ((((exists mv_square_prime_step_targetsquare. ((~((mv_square_prime_step_targetsquare) = 1) /\ forall pvs_left_step_targetsquareprime pvs_right_step_targetsquareprime. (mv_square_prime_step_targetsquare) = pvs_left_step_targetsquareprime * pvs_right_step_targetsquareprime -> pvs_left_step_targetsquareprime = 1 \/ pvs_right_step_targetsquareprime = 1) /\ (exists pvs_factor_step_targetsquaredivisor. (p * n) = (mv_square_prime_step_targetsquare * mv_square_prime_step_targetsquare) * pvs_factor_step_targetsquaredivisor))) /\ ((b) = 0))) \/ (((((~((p * n) = 0)) /\ (forall sfd_prime_step_targetsquarefree. (~((sfd_prime_step_targetsquarefree) = 1) /\ forall pvs_left_step_targetsquarefreedomain pvs_right_step_targetsquarefreedomain. (sfd_prime_step_targetsquarefree) = pvs_left_step_targetsquarefreedomain * pvs_right_step_targetsquarefreedomain -> pvs_left_step_targetsquarefreedomain = 1 \/ pvs_right_step_targetsquarefreedomain = 1) -> (exists pvs_le_gap_step_targetsquarefreebound. pvs_le_gap_step_targetsquarefreebound + (sfd_prime_step_targetsquarefree) = (p * n)) -> ~(exists pvs_factor_step_targetsquarefreesquare. (p * n) = (sfd_prime_step_targetsquarefree * sfd_prime_step_targetsquarefree) * pvs_factor_step_targetsquarefreesquare)))) /\ (exists mv_factor_code_step_targetfactors mv_factor_scale_step_targetfactors mv_factor_count_step_targetfactors. (((~(p * n = 0) /\ ((exists ff_u_fsat_step_targetfactorsfactorization_product ff_v_fsat_step_targetfactorsfactorization_product. ((((exists ff_h_fsat_step_targetfactorsfactorization_product_start. ff_h_fsat_step_targetfactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_start. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_step_targetfactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_step_targetfactorsfactorization_product_terminal. ff_h_fsat_step_targetfactorsfactorization_product_terminal + S (p * n) = S ((S (mv_factor_count_step_targetfactors)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_terminal. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_terminal * S ((S (mv_factor_count_step_targetfactors)) * ff_v_fsat_step_targetfactorsfactorization_product) + (p * n))) /\ forall ff_i_fsat_step_targetfactorsfactorization_product. (exists ff_lt_fsat_step_targetfactorsfactorization_product_bound. ff_lt_fsat_step_targetfactorsfactorization_product_bound + S ff_i_fsat_step_targetfactorsfactorization_product = mv_factor_count_step_targetfactors) -> exists ff_p_fsat_step_targetfactorsfactorization_product ff_r_fsat_step_targetfactorsfactorization_product ff_s_fsat_step_targetfactorsfactorization_product. ((((exists ff_h_fsat_step_targetfactorsfactorization_product_factor. ff_h_fsat_step_targetfactorsfactorization_product_factor + S (ff_p_fsat_step_targetfactorsfactorization_product) = S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * mv_factor_scale_step_targetfactors)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_factor. mv_factor_code_step_targetfactors = ff_q_fsat_step_targetfactorsfactorization_product_factor * S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * mv_factor_scale_step_targetfactors) + (ff_p_fsat_step_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_targetfactorsfactorization_product_partial. ff_h_fsat_step_targetfactorsfactorization_product_partial + S (ff_r_fsat_step_targetfactorsfactorization_product) = S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_partial. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_partial * S ((S (ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product) + (ff_r_fsat_step_targetfactorsfactorization_product))) /\ ((((exists ff_h_fsat_step_targetfactorsfactorization_product_successor. ff_h_fsat_step_targetfactorsfactorization_product_successor + S (ff_s_fsat_step_targetfactorsfactorization_product) = S ((S (S ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product)) /\ exists ff_q_fsat_step_targetfactorsfactorization_product_successor. ff_u_fsat_step_targetfactorsfactorization_product = ff_q_fsat_step_targetfactorsfactorization_product_successor * S ((S (S ff_i_fsat_step_targetfactorsfactorization_product)) * ff_v_fsat_step_targetfactorsfactorization_product) + (ff_s_fsat_step_targetfactorsfactorization_product))) /\ ff_s_fsat_step_targetfactorsfactorization_product = ff_r_fsat_step_targetfactorsfactorization_product * ff_p_fsat_step_targetfactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_step_targetfactorsfactorization_primes. (exists ftsf_gap_fsat_step_targetfactorsfactorization_primes_bound. ftsf_gap_fsat_step_targetfactorsfactorization_primes_bound + S ftsf_index_fsat_step_targetfactorsfactorization_primes = (mv_factor_count_step_targetfactors)) -> exists ftsf_factor_fsat_step_targetfactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_step_targetfactorsfactorization_primes_entry. ff_h_ftsf_fsat_step_targetfactorsfactorization_primes_entry + S (ftsf_factor_fsat_step_targetfactorsfactorization_primes) = S ((S (ftsf_index_fsat_step_targetfactorsfactorization_primes)) * mv_factor_scale_step_targetfactors)) /\ exists ff_q_ftsf_fsat_step_targetfactorsfactorization_primes_entry. mv_factor_code_step_targetfactors = ff_q_ftsf_fsat_step_targetfactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_step_targetfactorsfactorization_primes)) * mv_factor_scale_step_targetfactors) + (ftsf_factor_fsat_step_targetfactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_step_targetfactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_step_targetfactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_step_targetfactorsfactorization_primes_prime. ftsf_factor_fsat_step_targetfactorsfactorization_primes = frm_prime_left_ftsf_fsat_step_targetfactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_step_targetfactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_step_targetfactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_step_targetfactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_step_targetfactorsparityeven. (mv_factor_count_step_targetfactors) = 2 * mv_even_half_step_targetfactorsparityeven) /\ ((b) = 2))) \/ (((exists mv_odd_half_step_targetfactorsparityodd. (mv_factor_count_step_targetfactors) = 2 * mv_odd_half_step_targetfactorsparityodd + 1) /\ ((b) = 1))))))))))) -> (exists mps_positive_step_result mps_negative_step_result. (((((a) = 2 * (mps_positive_step_result) /\ (mps_negative_step_result) = 0) \/ exists ge_signed_half_step_resultsource. (((a) = 2 * ge_signed_half_step_resultsource + 1 /\ (mps_positive_step_result) = 0) /\ (mps_negative_step_result) = S ge_signed_half_step_resultsource))) /\ ((((b) = 2 * (mps_negative_step_result) /\ (mps_positive_step_result) = 0) \/ exists ge_signed_half_step_resulttarget. (((b) = 2 * ge_signed_half_step_resulttarget + 1 /\ (mps_negative_step_result) = 0) /\ (mps_positive_step_result) = S ge_signed_half_step_resulttarget)))))
Inherited Alpha proof; no standalone historical explorer page · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 136; exact statement SHA-256 d3bdcbb783fd64b1702d5cec4dc1cf9549c8f6a062e7666b9d8018c499eb177b
forall b c l p. (forall i. (exists h. h + S i = l) -> exists p. (((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1))) -> (((exists h. h + S p = S ((S l) * c)) /\ exists w. b = w * S ((S l) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1)) -> (forall i. (exists h. h + S i = S l) -> exists p. (((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1)))
Inherited Alpha proof; no standalone historical explorer page · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 139; exact statement SHA-256 6f2dc8af6b545e13025c45663e49cd41cf9f9dd58c4b0a1bec9b7382eddc4639
forall b c z d l. (forall i. (exists h. h + S i = l) -> exists p. (((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1))) -> (forall i p. (exists h. h + S i = l) -> ((exists h. h + S p = S ((S i) * c)) /\ exists w. b = w * S ((S i) * c) + p) -> ((exists h. h + S p = S ((S i) * d)) /\ exists w. z = w * S ((S i) * d) + p)) -> (forall i. (exists h. h + S i = l) -> exists p. (((exists h. h + S p = S ((S i) * d)) /\ exists w. z = w * S ((S i) * d) + p) /\ (~(p = 1) /\ forall a d. p = a * d -> a = 1 \/ d = 1)))
Inherited Alpha proof; no standalone historical explorer page · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 134; exact statement SHA-256 239265fa49cb97217f7c4dd13adb568af4010183e89f0d88edc37a1bfb4b320f
forall b c l r p. (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S r = S ((S l) * v)) /\ exists q. u = q * S ((S l) * v) + r) /\ forall i. (exists h. h + S i = l) -> exists p r s. (((exists h. h + S p = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p)))))) -> exists z e. (((exists h. h + S p = S ((S l) * e)) /\ exists q. z = q * S ((S l) * e) + p) /\ ((forall i a. (exists h. h + S i = l) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + a)) /\ (exists u v. (((exists h. h + S 1 = S ((S 0) * v)) /\ exists q. u = q * S ((S 0) * v) + 1) /\ (((exists h. h + S (r * p) = S ((S S l) * v)) /\ exists q. u = q * S ((S S l) * v) + (r * p)) /\ forall i. (exists h. h + S i = S l) -> exists p r s. (((exists h. h + S p = S ((S i) * e)) /\ exists q. z = q * S ((S i) * e) + p) /\ (((exists h. h + S r = S ((S i) * v)) /\ exists q. u = q * S ((S i) * v) + r) /\ (((exists h. h + S s = S ((S S i) * v)) /\ exists q. u = q * S ((S S i) * v) + s) /\ s = r * p))))))))
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 112; exact statement SHA-256 1060b24a0e43b4388c2ac9ecac0e76f60914ccf6cd449d37592e4b4d22461735
forall a b n. (forall d. (exists x. a = d * x) -> (exists y. n = d * y) -> d = 1) -> (forall d. (exists x. b = d * x) -> (exists y. n = d * y) -> d = 1) -> forall d. (exists x. a * b = d * x) -> (exists y. n = d * y) -> d = 1
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 164; exact statement SHA-256 0b699f9f386b21d36725118db53a45d614e3fb0a4114a1212c44c1126c56369e
forall p q. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> (~(q = 1) /\ forall c e. q = c * e -> c = 1 \/ e = 1) -> ~(p = q) -> forall d. (exists x. p = d * x) -> (exists y. q = d * y) -> d = 1
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 56; exact statement SHA-256 1fe13b628abe4610ddc4c81d29f2daa0399dd69a81efbdc1547fbcf431482475
forall d. (exists y. 1 = d * y) -> d = 1
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 74; exact statement SHA-256 c13a817645afe596d7f55f88eb9400073ae742c17213dfbf907f4c497aa1aca1
forall a b. a = b \/ ~(a = b)
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 158; exact statement SHA-256 d66091baec2eb0b33c6e68aa8da5742d2bcb11b6340c6e33aaeb363a61e92bef
forall n. (exists a. n = 2 * a) -> ~(exists b. n = 2 * b + 1)
Inherited Alpha proof; no standalone historical explorer page · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 82; exact statement SHA-256 733059a7f0a7b0efc0a06d04eefd2cf3e9cad880ef29754fcd2d6dfacf76cf28
forall n c d. ~(n = 0) -> n = c * d -> ~(c = 0)
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 196; exact statement SHA-256 bb16a740d4c971c54429a2a9491e8d28abf1a2756c732cca6e72aca17c802e85
forall n b c l. ((~(n = 0) /\ ((exists ff_u_fsat_unit_product ff_v_fsat_unit_product. ((((exists ff_h_fsat_unit_product_start. ff_h_fsat_unit_product_start + S (1) = S ((S (0)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_start. ff_u_fsat_unit_product = ff_q_fsat_unit_product_start * S ((S (0)) * ff_v_fsat_unit_product) + (1))) /\ ((((exists ff_h_fsat_unit_product_terminal. ff_h_fsat_unit_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_terminal. ff_u_fsat_unit_product = ff_q_fsat_unit_product_terminal * S ((S (l)) * ff_v_fsat_unit_product) + (n))) /\ forall ff_i_fsat_unit_product. (exists ff_lt_fsat_unit_product_bound. ff_lt_fsat_unit_product_bound + S ff_i_fsat_unit_product = l) -> exists ff_p_fsat_unit_product ff_r_fsat_unit_product ff_s_fsat_unit_product. ((((exists ff_h_fsat_unit_product_factor. ff_h_fsat_unit_product_factor + S (ff_p_fsat_unit_product) = S ((S (ff_i_fsat_unit_product)) * c)) /\ exists ff_q_fsat_unit_product_factor. b = ff_q_fsat_unit_product_factor * S ((S (ff_i_fsat_unit_product)) * c) + (ff_p_fsat_unit_product))) /\ ((((exists ff_h_fsat_unit_product_partial. ff_h_fsat_unit_product_partial + S (ff_r_fsat_unit_product) = S ((S (ff_i_fsat_unit_product)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_partial. ff_u_fsat_unit_product = ff_q_fsat_unit_product_partial * S ((S (ff_i_fsat_unit_product)) * ff_v_fsat_unit_product) + (ff_r_fsat_unit_product))) /\ ((((exists ff_h_fsat_unit_product_successor. ff_h_fsat_unit_product_successor + S (ff_s_fsat_unit_product) = S ((S (S ff_i_fsat_unit_product)) * ff_v_fsat_unit_product)) /\ exists ff_q_fsat_unit_product_successor. ff_u_fsat_unit_product = ff_q_fsat_unit_product_successor * S ((S (S ff_i_fsat_unit_product)) * ff_v_fsat_unit_product) + (ff_s_fsat_unit_product))) /\ ff_s_fsat_unit_product = ff_r_fsat_unit_product * ff_p_fsat_unit_product)))))) /\ (forall ftsf_index_fsat_unit_primes. (exists ftsf_gap_fsat_unit_primes_bound. ftsf_gap_fsat_unit_primes_bound + S ftsf_index_fsat_unit_primes = (l)) -> exists ftsf_factor_fsat_unit_primes. ((((exists ff_h_ftsf_fsat_unit_primes_entry. ff_h_ftsf_fsat_unit_primes_entry + S (ftsf_factor_fsat_unit_primes) = S ((S (ftsf_index_fsat_unit_primes)) * c)) /\ exists ff_q_ftsf_fsat_unit_primes_entry. b = ff_q_ftsf_fsat_unit_primes_entry * S ((S (ftsf_index_fsat_unit_primes)) * c) + (ftsf_factor_fsat_unit_primes))) /\ ((~(ftsf_factor_fsat_unit_primes = 1) /\ forall frm_prime_left_ftsf_fsat_unit_primes_prime frm_prime_right_ftsf_fsat_unit_primes_prime. ftsf_factor_fsat_unit_primes = frm_prime_left_ftsf_fsat_unit_primes_prime * frm_prime_right_ftsf_fsat_unit_primes_prime -> frm_prime_left_ftsf_fsat_unit_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_unit_primes_prime = 1))))))) -> n = 1 -> l = 0
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 189; exact statement SHA-256 af68e2e841fe13eafddb375135f9f1abde79b0185d5722d3851c0fcf61af56dc
forall n. ~(n = 0) -> exists l b c. ((~(n = 0) /\ ((exists ff_u_fsat_exists_product ff_v_fsat_exists_product. ((((exists ff_h_fsat_exists_product_start. ff_h_fsat_exists_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_start. ff_u_fsat_exists_product = ff_q_fsat_exists_product_start * S ((S (0)) * ff_v_fsat_exists_product) + (1))) /\ ((((exists ff_h_fsat_exists_product_terminal. ff_h_fsat_exists_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_terminal. ff_u_fsat_exists_product = ff_q_fsat_exists_product_terminal * S ((S (l)) * ff_v_fsat_exists_product) + (n))) /\ forall ff_i_fsat_exists_product. (exists ff_lt_fsat_exists_product_bound. ff_lt_fsat_exists_product_bound + S ff_i_fsat_exists_product = l) -> exists ff_p_fsat_exists_product ff_r_fsat_exists_product ff_s_fsat_exists_product. ((((exists ff_h_fsat_exists_product_factor. ff_h_fsat_exists_product_factor + S (ff_p_fsat_exists_product) = S ((S (ff_i_fsat_exists_product)) * c)) /\ exists ff_q_fsat_exists_product_factor. b = ff_q_fsat_exists_product_factor * S ((S (ff_i_fsat_exists_product)) * c) + (ff_p_fsat_exists_product))) /\ ((((exists ff_h_fsat_exists_product_partial. ff_h_fsat_exists_product_partial + S (ff_r_fsat_exists_product) = S ((S (ff_i_fsat_exists_product)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_partial. ff_u_fsat_exists_product = ff_q_fsat_exists_product_partial * S ((S (ff_i_fsat_exists_product)) * ff_v_fsat_exists_product) + (ff_r_fsat_exists_product))) /\ ((((exists ff_h_fsat_exists_product_successor. ff_h_fsat_exists_product_successor + S (ff_s_fsat_exists_product) = S ((S (S ff_i_fsat_exists_product)) * ff_v_fsat_exists_product)) /\ exists ff_q_fsat_exists_product_successor. ff_u_fsat_exists_product = ff_q_fsat_exists_product_successor * S ((S (S ff_i_fsat_exists_product)) * ff_v_fsat_exists_product) + (ff_s_fsat_exists_product))) /\ ff_s_fsat_exists_product = ff_r_fsat_exists_product * ff_p_fsat_exists_product)))))) /\ (forall ftsf_index_fsat_exists_primes. (exists ftsf_gap_fsat_exists_primes_bound. ftsf_gap_fsat_exists_primes_bound + S ftsf_index_fsat_exists_primes = (l)) -> exists ftsf_factor_fsat_exists_primes. ((((exists ff_h_ftsf_fsat_exists_primes_entry. ff_h_ftsf_fsat_exists_primes_entry + S (ftsf_factor_fsat_exists_primes) = S ((S (ftsf_index_fsat_exists_primes)) * c)) /\ exists ff_q_ftsf_fsat_exists_primes_entry. b = ff_q_ftsf_fsat_exists_primes_entry * S ((S (ftsf_index_fsat_exists_primes)) * c) + (ftsf_factor_fsat_exists_primes))) /\ ((~(ftsf_factor_fsat_exists_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_primes_prime frm_prime_right_ftsf_fsat_exists_primes_prime. ftsf_factor_fsat_exists_primes = frm_prime_left_ftsf_fsat_exists_primes_prime * frm_prime_right_ftsf_fsat_exists_primes_prime -> frm_prime_left_ftsf_fsat_exists_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_primes_prime = 1)))))))
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 73; exact statement SHA-256 1c3666be9deded79202818d9d6228aa230fefc0d123b60b73614b8a34483ff9c
forall a b z. (forall d. (exists x. a = d * x) -> (exists y. b = d * y) -> d = 1) -> (exists q. b * z = a * q) -> exists w. z = a * w
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 8; exact statement SHA-256 085c35afadeb1fafeb905d334c75f2799104ead8ddd8e59a301230d6e5b290d6
forall n m k. (n * m) * k = n * (m * k)
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 6; exact statement SHA-256 b5277583d2ad3b537c2ccf0fecc33912b9ff69674ec9659cf8d70f58b691b65d
forall n m. n * m = m * n
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 48; exact statement SHA-256 a638ef946cc44e0951e75b8e0e067fdb016a1b2335c57215acd24871e9dc6a17
forall a b c. ~(a = 0) -> a * b = a * c -> b = c
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 47; exact statement SHA-256 6735bc30f9bc8b28c3d07715c40ff48104313bf5ef4356b2f67502aebe9ac675
forall a b. ~(a = 0) -> ~(b = 0) -> ~(a * b = 0)
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 10; exact statement SHA-256 1c5292d92762aae47f3833dd3c85aa1275122554525aae695a40d1380c74c24e
forall n. n * 1 = n
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 53; exact statement SHA-256 d91b9eb2e5269ffcc8cd344f0c48e0da507153406cd991333ed0cc36327b9f40
forall a n m. (exists q. n = a * q) -> exists s. m * n = a * s
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 54; exact statement SHA-256 2ba2b335c4bf2e997debd3b94a8dbb40cc2798f8ac297a1f1d1b467f87a23d70
forall a b n. (exists q. n = a * q) -> (exists r. a = b * r) -> exists s. n = b * s
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 159; exact statement SHA-256 e1565df7f5a7e268cf4d65f9d298498ea2a4bed8e00f09ce5078e386c2448827
forall n. (exists b. n = 2 * b + 1) -> ~(exists a. n = 2 * a)
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 156; exact statement SHA-256 44703e32a0dd9b0c57a83f302061ae8d9b347664615deb0fd5159d5fa6ebb7c0
forall n. exists k. n = 2 * k \/ n = 2 * k + 1
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 188; exact statement SHA-256 70cd2b17e04eba064043ef32f66bb9335b1d94f21918927da628a741a9b6dc11
forall p q. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ((~(q = 1) /\ forall frm_prime_left_ftsp_q frm_prime_right_ftsp_q. q = frm_prime_left_ftsp_q * frm_prime_right_ftsp_q -> frm_prime_left_ftsp_q = 1 \/ frm_prime_right_ftsp_q = 1)) -> (exists ftcn_factor_ftsp_prime_divides_prime. (q) = (p) * ftcn_factor_ftsp_prime_divides_prime) -> p = q
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 210; exact statement SHA-256 95c94b01fda58b534085977b14f017960ce2479b3e7bb38ba30f2631523798d2
forall l n b c m d e. ((~(n = 0) /\ ((exists ff_u_fsat_uniqueness_source_product ff_v_fsat_uniqueness_source_product. ((((exists ff_h_fsat_uniqueness_source_product_start. ff_h_fsat_uniqueness_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_start. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_start * S ((S (0)) * ff_v_fsat_uniqueness_source_product) + (1))) /\ ((((exists ff_h_fsat_uniqueness_source_product_terminal. ff_h_fsat_uniqueness_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_terminal. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_terminal * S ((S (l)) * ff_v_fsat_uniqueness_source_product) + (n))) /\ forall ff_i_fsat_uniqueness_source_product. (exists ff_lt_fsat_uniqueness_source_product_bound. ff_lt_fsat_uniqueness_source_product_bound + S ff_i_fsat_uniqueness_source_product = l) -> exists ff_p_fsat_uniqueness_source_product ff_r_fsat_uniqueness_source_product ff_s_fsat_uniqueness_source_product. ((((exists ff_h_fsat_uniqueness_source_product_factor. ff_h_fsat_uniqueness_source_product_factor + S (ff_p_fsat_uniqueness_source_product) = S ((S (ff_i_fsat_uniqueness_source_product)) * c)) /\ exists ff_q_fsat_uniqueness_source_product_factor. b = ff_q_fsat_uniqueness_source_product_factor * S ((S (ff_i_fsat_uniqueness_source_product)) * c) + (ff_p_fsat_uniqueness_source_product))) /\ ((((exists ff_h_fsat_uniqueness_source_product_partial. ff_h_fsat_uniqueness_source_product_partial + S (ff_r_fsat_uniqueness_source_product) = S ((S (ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_partial. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_partial * S ((S (ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product) + (ff_r_fsat_uniqueness_source_product))) /\ ((((exists ff_h_fsat_uniqueness_source_product_successor. ff_h_fsat_uniqueness_source_product_successor + S (ff_s_fsat_uniqueness_source_product) = S ((S (S ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product)) /\ exists ff_q_fsat_uniqueness_source_product_successor. ff_u_fsat_uniqueness_source_product = ff_q_fsat_uniqueness_source_product_successor * S ((S (S ff_i_fsat_uniqueness_source_product)) * ff_v_fsat_uniqueness_source_product) + (ff_s_fsat_uniqueness_source_product))) /\ ff_s_fsat_uniqueness_source_product = ff_r_fsat_uniqueness_source_product * ff_p_fsat_uniqueness_source_product)))))) /\ (forall ftsf_index_fsat_uniqueness_source_primes. (exists ftsf_gap_fsat_uniqueness_source_primes_bound. ftsf_gap_fsat_uniqueness_source_primes_bound + S ftsf_index_fsat_uniqueness_source_primes = (l)) -> exists ftsf_factor_fsat_uniqueness_source_primes. ((((exists ff_h_ftsf_fsat_uniqueness_source_primes_entry. ff_h_ftsf_fsat_uniqueness_source_primes_entry + S (ftsf_factor_fsat_uniqueness_source_primes) = S ((S (ftsf_index_fsat_uniqueness_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_uniqueness_source_primes_entry. b = ff_q_ftsf_fsat_uniqueness_source_primes_entry * S ((S (ftsf_index_fsat_uniqueness_source_primes)) * c) + (ftsf_factor_fsat_uniqueness_source_primes))) /\ ((~(ftsf_factor_fsat_uniqueness_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime. ftsf_factor_fsat_uniqueness_source_primes = frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime * frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime -> frm_prime_left_ftsf_fsat_uniqueness_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_uniqueness_source_primes_prime = 1))))))) -> ((~(n = 0) /\ ((exists ff_u_fsat_uniqueness_target_product ff_v_fsat_uniqueness_target_product. ((((exists ff_h_fsat_uniqueness_target_product_start. ff_h_fsat_uniqueness_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_start. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_start * S ((S (0)) * ff_v_fsat_uniqueness_target_product) + (1))) /\ ((((exists ff_h_fsat_uniqueness_target_product_terminal. ff_h_fsat_uniqueness_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_terminal. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_terminal * S ((S (m)) * ff_v_fsat_uniqueness_target_product) + (n))) /\ forall ff_i_fsat_uniqueness_target_product. (exists ff_lt_fsat_uniqueness_target_product_bound. ff_lt_fsat_uniqueness_target_product_bound + S ff_i_fsat_uniqueness_target_product = m) -> exists ff_p_fsat_uniqueness_target_product ff_r_fsat_uniqueness_target_product ff_s_fsat_uniqueness_target_product. ((((exists ff_h_fsat_uniqueness_target_product_factor. ff_h_fsat_uniqueness_target_product_factor + S (ff_p_fsat_uniqueness_target_product) = S ((S (ff_i_fsat_uniqueness_target_product)) * e)) /\ exists ff_q_fsat_uniqueness_target_product_factor. d = ff_q_fsat_uniqueness_target_product_factor * S ((S (ff_i_fsat_uniqueness_target_product)) * e) + (ff_p_fsat_uniqueness_target_product))) /\ ((((exists ff_h_fsat_uniqueness_target_product_partial. ff_h_fsat_uniqueness_target_product_partial + S (ff_r_fsat_uniqueness_target_product) = S ((S (ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_partial. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_partial * S ((S (ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product) + (ff_r_fsat_uniqueness_target_product))) /\ ((((exists ff_h_fsat_uniqueness_target_product_successor. ff_h_fsat_uniqueness_target_product_successor + S (ff_s_fsat_uniqueness_target_product) = S ((S (S ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product)) /\ exists ff_q_fsat_uniqueness_target_product_successor. ff_u_fsat_uniqueness_target_product = ff_q_fsat_uniqueness_target_product_successor * S ((S (S ff_i_fsat_uniqueness_target_product)) * ff_v_fsat_uniqueness_target_product) + (ff_s_fsat_uniqueness_target_product))) /\ ff_s_fsat_uniqueness_target_product = ff_r_fsat_uniqueness_target_product * ff_p_fsat_uniqueness_target_product)))))) /\ (forall ftsf_index_fsat_uniqueness_target_primes. (exists ftsf_gap_fsat_uniqueness_target_primes_bound. ftsf_gap_fsat_uniqueness_target_primes_bound + S ftsf_index_fsat_uniqueness_target_primes = (m)) -> exists ftsf_factor_fsat_uniqueness_target_primes. ((((exists ff_h_ftsf_fsat_uniqueness_target_primes_entry. ff_h_ftsf_fsat_uniqueness_target_primes_entry + S (ftsf_factor_fsat_uniqueness_target_primes) = S ((S (ftsf_index_fsat_uniqueness_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_uniqueness_target_primes_entry. d = ff_q_ftsf_fsat_uniqueness_target_primes_entry * S ((S (ftsf_index_fsat_uniqueness_target_primes)) * e) + (ftsf_factor_fsat_uniqueness_target_primes))) /\ ((~(ftsf_factor_fsat_uniqueness_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime. ftsf_factor_fsat_uniqueness_target_primes = frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime * frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime -> frm_prime_left_ftsf_fsat_uniqueness_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_uniqueness_target_primes_prime = 1))))))) -> (((l = m) /\ (exists pfp_u_uniqueness_result pfp_v_uniqueness_result. (((((forall pfp_i_uniqueness_resultmatchingpermutationbounded. (exists pfp_gap_uniqueness_resultmatchingpermutationboundedindex. pfp_gap_uniqueness_resultmatchingpermutationboundedindex + S (pfp_i_uniqueness_resultmatchingpermutationbounded) = (l)) -> exists pfp_a_uniqueness_resultmatchingpermutationbounded. (((exists ff_h_pfp_uniqueness_resultmatchingpermutationboundedentry. ff_h_pfp_uniqueness_resultmatchingpermutationboundedentry + S (pfp_a_uniqueness_resultmatchingpermutationbounded) = S ((S (pfp_i_uniqueness_resultmatchingpermutationbounded)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationboundedentry. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationboundedentry * S ((S (pfp_i_uniqueness_resultmatchingpermutationbounded)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationbounded))) /\ (exists pfp_gap_uniqueness_resultmatchingpermutationboundedvalue. pfp_gap_uniqueness_resultmatchingpermutationboundedvalue + S (pfp_a_uniqueness_resultmatchingpermutationbounded) = (l))) /\ (((forall pfp_i_uniqueness_resultmatchingpermutationinjective pfp_j_uniqueness_resultmatchingpermutationinjective pfp_a_uniqueness_resultmatchingpermutationinjective. (exists pfp_gap_uniqueness_resultmatchingpermutationinjectivefirst. pfp_gap_uniqueness_resultmatchingpermutationinjectivefirst + S (pfp_i_uniqueness_resultmatchingpermutationinjective) = (l)) -> (exists pfp_gap_uniqueness_resultmatchingpermutationinjectivesecond. pfp_gap_uniqueness_resultmatchingpermutationinjectivesecond + S (pfp_j_uniqueness_resultmatchingpermutationinjective) = (l)) -> (((exists ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveleft. ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveleft + S (pfp_a_uniqueness_resultmatchingpermutationinjective) = S ((S (pfp_i_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveleft. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveleft * S ((S (pfp_i_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationinjective))) -> (((exists ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveright. ff_h_pfp_uniqueness_resultmatchingpermutationinjectiveright + S (pfp_a_uniqueness_resultmatchingpermutationinjective) = S ((S (pfp_j_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveright. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationinjectiveright * S ((S (pfp_j_uniqueness_resultmatchingpermutationinjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationinjective))) -> pfp_i_uniqueness_resultmatchingpermutationinjective = pfp_j_uniqueness_resultmatchingpermutationinjective) /\ (forall pfp_a_uniqueness_resultmatchingpermutationsurjective. (exists pfp_gap_uniqueness_resultmatchingpermutationsurjectivevalue. pfp_gap_uniqueness_resultmatchingpermutationsurjectivevalue + S (pfp_a_uniqueness_resultmatchingpermutationsurjective) = (l)) -> exists pfp_i_uniqueness_resultmatchingpermutationsurjective. (exists pfp_gap_uniqueness_resultmatchingpermutationsurjectiveindex. pfp_gap_uniqueness_resultmatchingpermutationsurjectiveindex + S (pfp_i_uniqueness_resultmatchingpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_uniqueness_resultmatchingpermutationsurjectiveentry. ff_h_pfp_uniqueness_resultmatchingpermutationsurjectiveentry + S (pfp_a_uniqueness_resultmatchingpermutationsurjective) = S ((S (pfp_i_uniqueness_resultmatchingpermutationsurjective)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingpermutationsurjectiveentry. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingpermutationsurjectiveentry * S ((S (pfp_i_uniqueness_resultmatchingpermutationsurjective)) * pfp_v_uniqueness_result) + (pfp_a_uniqueness_resultmatchingpermutationsurjective)))))))) /\ (forall pfp_i_uniqueness_resultmatchingmatching pfp_j_uniqueness_resultmatchingmatching pfp_a_uniqueness_resultmatchingmatching. (exists pfp_gap_uniqueness_resultmatchingmatchingbound. pfp_gap_uniqueness_resultmatchingmatchingbound + S (pfp_i_uniqueness_resultmatchingmatching) = (l)) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingmap. ff_h_pfp_uniqueness_resultmatchingmatchingmap + S (pfp_j_uniqueness_resultmatchingmatching) = S ((S (pfp_i_uniqueness_resultmatchingmatching)) * pfp_v_uniqueness_result)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingmap. pfp_u_uniqueness_result = ff_q_pfp_uniqueness_resultmatchingmatchingmap * S ((S (pfp_i_uniqueness_resultmatchingmatching)) * pfp_v_uniqueness_result) + (pfp_j_uniqueness_resultmatchingmatching))) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingsource. ff_h_pfp_uniqueness_resultmatchingmatchingsource + S (pfp_a_uniqueness_resultmatchingmatching) = S ((S (pfp_i_uniqueness_resultmatchingmatching)) * c)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingsource. b = ff_q_pfp_uniqueness_resultmatchingmatchingsource * S ((S (pfp_i_uniqueness_resultmatchingmatching)) * c) + (pfp_a_uniqueness_resultmatchingmatching))) -> (((exists ff_h_pfp_uniqueness_resultmatchingmatchingtarget. ff_h_pfp_uniqueness_resultmatchingmatchingtarget + S (pfp_a_uniqueness_resultmatchingmatching) = S ((S (pfp_j_uniqueness_resultmatchingmatching)) * e)) /\ exists ff_q_pfp_uniqueness_resultmatchingmatchingtarget. d = ff_q_pfp_uniqueness_resultmatchingmatchingtarget * S ((S (pfp_j_uniqueness_resultmatchingmatching)) * e) + (pfp_a_uniqueness_resultmatchingmatching)))))))))
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 80; exact statement SHA-256 f74d3a446b0634b8019db1906e37846c34e3d71f60d5261139ed9ed69b465ed7
forall p. (~(p = 1) /\ forall a b. p = a * b -> a = 1 \/ b = 1) -> ~(p = 0)
Inherited Alpha proof; no standalone historical explorer page · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 186; exact statement SHA-256 c36d0368df382c028d5e78b63c0eb972a6f60ce6f01d0c730bb687f81950f3e6
forall input output. (exists sn_pos_symmetric_forward sn_neg_symmetric_forward. (((input = 2 * sn_pos_symmetric_forward /\ sn_neg_symmetric_forward = 0) \/ exists sd_half_symmetric_forward_input. ((input = 2 * sd_half_symmetric_forward_input + 1 /\ sn_pos_symmetric_forward = 0) /\ sn_neg_symmetric_forward = S sd_half_symmetric_forward_input)) /\ ((output = 2 * sn_neg_symmetric_forward /\ sn_pos_symmetric_forward = 0) \/ exists sd_half_symmetric_forward_output. ((output = 2 * sd_half_symmetric_forward_output + 1 /\ sn_neg_symmetric_forward = 0) /\ sn_pos_symmetric_forward = S sd_half_symmetric_forward_output)))) -> (exists sn_pos_symmetric_reverse sn_neg_symmetric_reverse. (((output = 2 * sn_pos_symmetric_reverse /\ sn_neg_symmetric_reverse = 0) \/ exists sd_half_symmetric_reverse_input. ((output = 2 * sd_half_symmetric_reverse_input + 1 /\ sn_pos_symmetric_reverse = 0) /\ sn_neg_symmetric_reverse = S sd_half_symmetric_reverse_input)) /\ ((input = 2 * sn_neg_symmetric_reverse /\ sn_pos_symmetric_reverse = 0) \/ exists sd_half_symmetric_reverse_output. ((input = 2 * sd_half_symmetric_reverse_output + 1 /\ sn_neg_symmetric_reverse = 0) /\ sn_pos_symmetric_reverse = S sd_half_symmetric_reverse_output))))
Inherited Alpha proof; no standalone historical explorer page · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 185; exact statement SHA-256 fccdf1865ae3bff48d1a549b41afec8992e274c72d194197dc519832c63185dc
exists sn_pos_zero sn_neg_zero. (((0 = 2 * sn_pos_zero /\ sn_neg_zero = 0) \/ exists sd_half_zero_input. ((0 = 2 * sd_half_zero_input + 1 /\ sn_pos_zero = 0) /\ sn_neg_zero = S sd_half_zero_input)) /\ ((0 = 2 * sn_neg_zero /\ sn_pos_zero = 0) \/ exists sd_half_zero_output. ((0 = 2 * sd_half_zero_output + 1 /\ sn_neg_zero = 0) /\ sn_pos_zero = S sd_half_zero_output)))
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 211; exact statement SHA-256 4a33c8d554b2388572cfd139ddd59cd1f29c7465c70eb8abbf80ba49c012e5af
forall n p. (((~((n) = 0)) /\ (forall sfd_prime_exclusion_squarefree. (~((sfd_prime_exclusion_squarefree) = 1) /\ forall pvs_left_exclusion_squarefreedomain pvs_right_exclusion_squarefreedomain. (sfd_prime_exclusion_squarefree) = pvs_left_exclusion_squarefreedomain * pvs_right_exclusion_squarefreedomain -> pvs_left_exclusion_squarefreedomain = 1 \/ pvs_right_exclusion_squarefreedomain = 1) -> (exists pvs_le_gap_exclusion_squarefreebound. pvs_le_gap_exclusion_squarefreebound + (sfd_prime_exclusion_squarefree) = (n)) -> ~(exists pvs_factor_exclusion_squarefreesquare. (n) = (sfd_prime_exclusion_squarefree * sfd_prime_exclusion_squarefree) * pvs_factor_exclusion_squarefreesquare)))) -> (~((p) = 1) /\ forall pvs_left_exclusion_prime pvs_right_exclusion_prime. (p) = pvs_left_exclusion_prime * pvs_right_exclusion_prime -> pvs_left_exclusion_prime = 1 \/ pvs_right_exclusion_prime = 1) -> (exists pvs_factor_exclusion_divisor. (n) = (p * p) * pvs_factor_exclusion_divisor) -> false
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 214; exact statement SHA-256 7836966aff0c8d2a23ca95bc525812398670799b96efeb0cb8db831bba43393e
((~((1) = 0)) /\ (forall sfd_prime_one. (~((sfd_prime_one) = 1) /\ forall pvs_left_onedomain pvs_right_onedomain. (sfd_prime_one) = pvs_left_onedomain * pvs_right_onedomain -> pvs_left_onedomain = 1 \/ pvs_right_onedomain = 1) -> (exists pvs_le_gap_onebound. pvs_le_gap_onebound + (sfd_prime_one) = (1)) -> ~(exists pvs_factor_onesquare. (1) = (sfd_prime_one * sfd_prime_one) * pvs_factor_onesquare)))
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 213; exact statement SHA-256 1860fce8369b9c61e23407e14527dac90d9114f42f712f1e5e57170d3e840819
forall n. ~(n = 0) -> (((~((n) = 0)) /\ (forall sfd_prime_decision_squarefree. (~((sfd_prime_decision_squarefree) = 1) /\ forall pvs_left_decision_squarefreedomain pvs_right_decision_squarefreedomain. (sfd_prime_decision_squarefree) = pvs_left_decision_squarefreedomain * pvs_right_decision_squarefreedomain -> pvs_left_decision_squarefreedomain = 1 \/ pvs_right_decision_squarefreedomain = 1) -> (exists pvs_le_gap_decision_squarefreebound. pvs_le_gap_decision_squarefreebound + (sfd_prime_decision_squarefree) = (n)) -> ~(exists pvs_factor_decision_squarefreesquare. (n) = (sfd_prime_decision_squarefree * sfd_prime_decision_squarefree) * pvs_factor_decision_squarefreesquare)))) \/ exists p. (~((p) = 1) /\ forall pvs_left_decision_prime pvs_right_decision_prime. (p) = pvs_left_decision_prime * pvs_right_decision_prime -> pvs_left_decision_prime = 1 \/ pvs_right_decision_prime = 1) /\ (exists pvs_factor_decision_divisor. (n) = (p * p) * pvs_factor_decision_divisor)
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 161; exact statement SHA-256 2e64a8e153b9e7feaacad6274b57022b055fccebd696c2cdd36c7e435913f4aa
forall n. (exists a. n = 2 * a + 1) -> exists b. S n = 2 * b
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 160; exact statement SHA-256 8f6073cd621d47cd912a49dce5c742fb0b84a81fddfb45007af01d9f2809758f
forall n. (exists a. n = 2 * a) -> exists b. S n = 2 * b + 1
Read the exact inherited Alpha proof · freshly checked in this complete bundle; exact statement and bundle node below.
Bundle node 0; exact statement SHA-256 b759e0dfbf2a583a91d2b5db09cc55d201ef09cc1690d6ab1a32fcca5af5cdb9
forall n. 0 + n = n