Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Definition in prerequisite notation
∀ pvs_index_prioritylayer. Lt(pvs_index_prioritylayer,l) → ∃ x. ∃ y. ∃ z. BetaAt(pb,pc,pvs_index_prioritylayer,x) ∧ (BetaAt(eb,ec,pvs_index_prioritylayer,y) ∧ (BetaAt(vb,vc,pvs_index_prioritylayer,z) ∧ (Prime(x) ∧ (¬y = 0 ∧ (BoundedPowerValuation(x,n,n,y) ∧ Pow(x,y,z))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall pvs_index_prioritylayer. (exists pvs_gap_prioritylayerindex. pvs_gap_prioritylayerindex + S (pvs_index_prioritylayer) = ((l))) -> exists pvs_prime_prioritylayer pvs_exponent_prioritylayer pvs_power_prioritylayer. (((((exists ff_h_pvs_prioritylayerprime. ff_h_pvs_prioritylayerprime + S (pvs_prime_prioritylayer) = S ((S (pvs_index_prioritylayer)) * (pc))) /\ exists ff_q_pvs_prioritylayerprime. (pb) = ff_q_pvs_prioritylayerprime * S ((S (pvs_index_prioritylayer)) * (pc)) + (pvs_prime_prioritylayer))) /\ (((((exists ff_h_pvs_prioritylayerexponent. ff_h_pvs_prioritylayerexponent + S (pvs_exponent_prioritylayer) = S ((S (pvs_index_prioritylayer)) * (ec))) /\ exists ff_q_pvs_prioritylayerexponent. (eb) = ff_q_pvs_prioritylayerexponent * S ((S (pvs_index_prioritylayer)) * (ec)) + (pvs_exponent_prioritylayer))) /\ (((((exists ff_h_pvs_prioritylayerpower. ff_h_pvs_prioritylayerpower + S (pvs_power_prioritylayer) = S ((S (pvs_index_prioritylayer)) * (vc))) /\ exists ff_q_pvs_prioritylayerpower. (vb) = ff_q_pvs_prioritylayerpower * S ((S (pvs_index_prioritylayer)) * (vc)) + (pvs_power_prioritylayer))) /\ (((~((pvs_prime_prioritylayer) = 1) /\ forall pvs_left_prioritylayerdomain pvs_right_prioritylayerdomain. (pvs_prime_prioritylayer) = pvs_left_prioritylayerdomain * pvs_right_prioritylayerdomain -> pvs_left_prioritylayerdomain = 1 \/ pvs_right_prioritylayerdomain = 1) /\ (((~(pvs_exponent_prioritylayer = 0)) /\ (((((exists bpd_gap_pvs_prioritylayervaluation_selected_bound. bpd_gap_pvs_prioritylayervaluation_selected_bound + (pvs_exponent_prioritylayer) = ((n))) /\ (exists bpvi_result_pvs_prioritylayervaluation_selected. ((exists bpvi_b_pvs_prioritylayervaluation_selected_power bpvi_c_pvs_prioritylayervaluation_selected_power. ((forall bpvi_i_pvs_prioritylayervaluation_selected_power. (exists bpvi_repeat_gap_pvs_prioritylayervaluation_selected_power. bpvi_repeat_gap_pvs_prioritylayervaluation_selected_power + S bpvi_i_pvs_prioritylayervaluation_selected_power = pvs_exponent_prioritylayer) -> (((exists bpvi_h_pvs_prioritylayervaluation_selected_power_repeat. bpvi_h_pvs_prioritylayervaluation_selected_power_repeat + S (pvs_prime_prioritylayer) = S ((S (bpvi_i_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_repeat. bpvi_b_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_repeat * S ((S (bpvi_i_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power) + (pvs_prime_prioritylayer)))) /\ (exists bpvi_u_pvs_prioritylayervaluation_selected_power bpvi_v_pvs_prioritylayervaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_start. bpvi_h_pvs_prioritylayervaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_start. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_terminal. bpvi_h_pvs_prioritylayervaluation_selected_power_terminal + S (bpvi_result_pvs_prioritylayervaluation_selected) = S ((S (pvs_exponent_prioritylayer)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_terminal. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_terminal * S ((S (pvs_exponent_prioritylayer)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (bpvi_result_pvs_prioritylayervaluation_selected))) /\ forall bpvi_j_pvs_prioritylayervaluation_selected_power. (exists bpvi_product_gap_pvs_prioritylayervaluation_selected_power. bpvi_product_gap_pvs_prioritylayervaluation_selected_power + S bpvi_j_pvs_prioritylayervaluation_selected_power = pvs_exponent_prioritylayer) -> exists bpvi_factor_pvs_prioritylayervaluation_selected_power bpvi_partial_pvs_prioritylayervaluation_selected_power bpvi_successor_pvs_prioritylayervaluation_selected_power. ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_factor. bpvi_h_pvs_prioritylayervaluation_selected_power_factor + S (bpvi_factor_pvs_prioritylayervaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_factor. bpvi_b_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_factor * S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_c_pvs_prioritylayervaluation_selected_power) + (bpvi_factor_pvs_prioritylayervaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_partial. bpvi_h_pvs_prioritylayervaluation_selected_power_partial + S (bpvi_partial_pvs_prioritylayervaluation_selected_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_partial. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_partial * S ((S (bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (bpvi_partial_pvs_prioritylayervaluation_selected_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_selected_power_successor. bpvi_h_pvs_prioritylayervaluation_selected_power_successor + S (bpvi_successor_pvs_prioritylayervaluation_selected_power) = S ((S (S bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_selected_power_successor. bpvi_u_pvs_prioritylayervaluation_selected_power = bpvi_q_pvs_prioritylayervaluation_selected_power_successor * S ((S (S bpvi_j_pvs_prioritylayervaluation_selected_power)) * bpvi_v_pvs_prioritylayervaluation_selected_power) + (bpvi_successor_pvs_prioritylayervaluation_selected_power))) /\ bpvi_successor_pvs_prioritylayervaluation_selected_power = bpvi_partial_pvs_prioritylayervaluation_selected_power * bpvi_factor_pvs_prioritylayervaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayervaluation_selected. (n) = bpvi_result_pvs_prioritylayervaluation_selected * bpvi_divisor_factor_pvs_prioritylayervaluation_selected))) /\ forall bpd_candidate_pvs_prioritylayervaluation. (exists bpd_gap_pvs_prioritylayervaluation_candidate_bound. bpd_gap_pvs_prioritylayervaluation_candidate_bound + (bpd_candidate_pvs_prioritylayervaluation) = ((n))) -> (exists bpvi_result_pvs_prioritylayervaluation_candidate. ((exists bpvi_b_pvs_prioritylayervaluation_candidate_power bpvi_c_pvs_prioritylayervaluation_candidate_power. ((forall bpvi_i_pvs_prioritylayervaluation_candidate_power. (exists bpvi_repeat_gap_pvs_prioritylayervaluation_candidate_power. bpvi_repeat_gap_pvs_prioritylayervaluation_candidate_power + S bpvi_i_pvs_prioritylayervaluation_candidate_power = bpd_candidate_pvs_prioritylayervaluation) -> (((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_repeat. bpvi_h_pvs_prioritylayervaluation_candidate_power_repeat + S (pvs_prime_prioritylayer) = S ((S (bpvi_i_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_repeat. bpvi_b_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power) + (pvs_prime_prioritylayer)))) /\ (exists bpvi_u_pvs_prioritylayervaluation_candidate_power bpvi_v_pvs_prioritylayervaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_start. bpvi_h_pvs_prioritylayervaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_start. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_terminal. bpvi_h_pvs_prioritylayervaluation_candidate_power_terminal + S (bpvi_result_pvs_prioritylayervaluation_candidate) = S ((S (bpd_candidate_pvs_prioritylayervaluation)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_terminal. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_prioritylayervaluation)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (bpvi_result_pvs_prioritylayervaluation_candidate))) /\ forall bpvi_j_pvs_prioritylayervaluation_candidate_power. (exists bpvi_product_gap_pvs_prioritylayervaluation_candidate_power. bpvi_product_gap_pvs_prioritylayervaluation_candidate_power + S bpvi_j_pvs_prioritylayervaluation_candidate_power = bpd_candidate_pvs_prioritylayervaluation) -> exists bpvi_factor_pvs_prioritylayervaluation_candidate_power bpvi_partial_pvs_prioritylayervaluation_candidate_power bpvi_successor_pvs_prioritylayervaluation_candidate_power. ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_factor. bpvi_h_pvs_prioritylayervaluation_candidate_power_factor + S (bpvi_factor_pvs_prioritylayervaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_factor. bpvi_b_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_factor * S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_c_pvs_prioritylayervaluation_candidate_power) + (bpvi_factor_pvs_prioritylayervaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_partial. bpvi_h_pvs_prioritylayervaluation_candidate_power_partial + S (bpvi_partial_pvs_prioritylayervaluation_candidate_power) = S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_partial. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_partial * S ((S (bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (bpvi_partial_pvs_prioritylayervaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_prioritylayervaluation_candidate_power_successor. bpvi_h_pvs_prioritylayervaluation_candidate_power_successor + S (bpvi_successor_pvs_prioritylayervaluation_candidate_power) = S ((S (S bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power)) /\ exists bpvi_q_pvs_prioritylayervaluation_candidate_power_successor. bpvi_u_pvs_prioritylayervaluation_candidate_power = bpvi_q_pvs_prioritylayervaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_prioritylayervaluation_candidate_power)) * bpvi_v_pvs_prioritylayervaluation_candidate_power) + (bpvi_successor_pvs_prioritylayervaluation_candidate_power))) /\ bpvi_successor_pvs_prioritylayervaluation_candidate_power = bpvi_partial_pvs_prioritylayervaluation_candidate_power * bpvi_factor_pvs_prioritylayervaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_prioritylayervaluation_candidate. (n) = bpvi_result_pvs_prioritylayervaluation_candidate * bpvi_divisor_factor_pvs_prioritylayervaluation_candidate)) -> (exists bpd_gap_pvs_prioritylayervaluation_maximal. bpd_gap_pvs_prioritylayervaluation_maximal + (bpd_candidate_pvs_prioritylayervaluation) = (pvs_exponent_prioritylayer))) /\ (exists pa_b_pvs_prioritylayervalue pa_c_pvs_prioritylayervalue. ((forall pa_i_pvs_prioritylayervalue_repeat. (exists pa_lt_pvs_prioritylayervalue_repeat_bound. pa_lt_pvs_prioritylayervalue_repeat_bound + S pa_i_pvs_prioritylayervalue_repeat = pvs_exponent_prioritylayer) -> (((exists pa_h_pvs_prioritylayervalue_repeat_decoded. pa_h_pvs_prioritylayervalue_repeat_decoded + S (pvs_prime_prioritylayer) = S ((S (pa_i_pvs_prioritylayervalue_repeat)) * pa_c_pvs_prioritylayervalue)) /\ exists pa_q_pvs_prioritylayervalue_repeat_decoded. pa_b_pvs_prioritylayervalue = pa_q_pvs_prioritylayervalue_repeat_decoded * S ((S (pa_i_pvs_prioritylayervalue_repeat)) * pa_c_pvs_prioritylayervalue) + (pvs_prime_prioritylayer)))) /\ (exists pa_u_pvs_prioritylayervalue_product pa_v_pvs_prioritylayervalue_product. ((((exists pa_h_pvs_prioritylayervalue_product_start. pa_h_pvs_prioritylayervalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_prioritylayervalue_product)) /\ exists pa_q_pvs_prioritylayervalue_product_start. pa_u_pvs_prioritylayervalue_product = pa_q_pvs_prioritylayervalue_product_start * S ((S (0)) * pa_v_pvs_prioritylayervalue_product) + (1))) /\ ((((exists pa_h_pvs_prioritylayervalue_product_terminal. pa_h_pvs_prioritylayervalue_product_terminal + S (pvs_power_prioritylayer) = S ((S (pvs_exponent_prioritylayer)) * pa_v_pvs_prioritylayervalue_product)) /\ exists pa_q_pvs_prioritylayervalue_product_terminal. pa_u_pvs_prioritylayervalue_product = pa_q_pvs_prioritylayervalue_product_terminal * S ((S (pvs_exponent_prioritylayer)) * pa_v_pvs_prioritylayervalue_product) + (pvs_power_prioritylayer))) /\ forall pa_i_pvs_prioritylayervalue_product. (exists pa_lt_pvs_prioritylayervalue_product_bound. pa_lt_pvs_prioritylayervalue_product_bound + S pa_i_pvs_prioritylayervalue_product = pvs_exponent_prioritylayer) -> exists pa_p_pvs_prioritylayervalue_product pa_r_pvs_prioritylayervalue_product pa_s_pvs_prioritylayervalue_product. ((((exists pa_h_pvs_prioritylayervalue_product_factor. pa_h_pvs_prioritylayervalue_product_factor + S (pa_p_pvs_prioritylayervalue_product) = S ((S (pa_i_pvs_prioritylayervalue_product)) * pa_c_pvs_prioritylayervalue)) /\ exists pa_q_pvs_prioritylayervalue_product_factor. pa_b_pvs_prioritylayervalue = pa_q_pvs_prioritylayervalue_product_factor * S ((S (pa_i_pvs_prioritylayervalue_product)) * pa_c_pvs_prioritylayervalue) + (pa_p_pvs_prioritylayervalue_product))) /\ ((((exists pa_h_pvs_prioritylayervalue_product_partial. pa_h_pvs_prioritylayervalue_product_partial + S (pa_r_pvs_prioritylayervalue_product) = S ((S (pa_i_pvs_prioritylayervalue_product)) * pa_v_pvs_prioritylayervalue_product)) /\ exists pa_q_pvs_prioritylayervalue_product_partial. pa_u_pvs_prioritylayervalue_product = pa_q_pvs_prioritylayervalue_product_partial * S ((S (pa_i_pvs_prioritylayervalue_product)) * pa_v_pvs_prioritylayervalue_product) + (pa_r_pvs_prioritylayervalue_product))) /\ ((((exists pa_h_pvs_prioritylayervalue_product_successor. pa_h_pvs_prioritylayervalue_product_successor + S (pa_s_pvs_prioritylayervalue_product) = S ((S (S pa_i_pvs_prioritylayervalue_product)) * pa_v_pvs_prioritylayervalue_product)) /\ exists pa_q_pvs_prioritylayervalue_product_successor. pa_u_pvs_prioritylayervalue_product = pa_q_pvs_prioritylayervalue_product_successor * S ((S (S pa_i_pvs_prioritylayervalue_product)) * pa_v_pvs_prioritylayervalue_product) + (pa_s_pvs_prioritylayervalue_product))) /\ pa_s_pvs_prioritylayervalue_product = pa_r_pvs_prioritylayervalue_product * pa_p_pvs_prioritylayervalue_product))))))))))))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.