Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
∃ eut_code_prioritylayer. ∃ eut_scale_prioritylayer. UnitBitPrefix(n,eut_code_prioritylayer,eut_scale_prioritylayer,l) ∧ Sum(eut_code_prioritylayer,eut_scale_prioritylayer,l,t)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists eut_code_prioritylayer eut_scale_prioritylayer. (forall eut_index_prioritylayer_mask. (exists eut_gap_prioritylayer_mask_bound. eut_gap_prioritylayer_mask_bound + S (eut_index_prioritylayer_mask) = (l)) -> exists eut_bit_prioritylayer_mask. (((exists fs_h_eut_prioritylayer_mask_entry. fs_h_eut_prioritylayer_mask_entry + S (eut_bit_prioritylayer_mask) = S ((S (eut_index_prioritylayer_mask)) * eut_scale_prioritylayer)) /\ exists fs_q_eut_prioritylayer_mask_entry. eut_code_prioritylayer = fs_q_eut_prioritylayer_mask_entry * S ((S (eut_index_prioritylayer_mask)) * eut_scale_prioritylayer) + (eut_bit_prioritylayer_mask))) /\ ((((forall eut_divisor_prioritylayer_mask_choice_coprime. (exists eut_left_prioritylayer_mask_choice_coprime. (eut_index_prioritylayer_mask) = eut_divisor_prioritylayer_mask_choice_coprime * eut_left_prioritylayer_mask_choice_coprime) -> (exists eut_right_prioritylayer_mask_choice_coprime. (n) = eut_divisor_prioritylayer_mask_choice_coprime * eut_right_prioritylayer_mask_choice_coprime) -> eut_divisor_prioritylayer_mask_choice_coprime = 1) /\ (eut_bit_prioritylayer_mask) = 1) \/ (~(forall eut_divisor_prioritylayer_mask_choice_coprime. (exists eut_left_prioritylayer_mask_choice_coprime. (eut_index_prioritylayer_mask) = eut_divisor_prioritylayer_mask_choice_coprime * eut_left_prioritylayer_mask_choice_coprime) -> (exists eut_right_prioritylayer_mask_choice_coprime. (n) = eut_divisor_prioritylayer_mask_choice_coprime * eut_right_prioritylayer_mask_choice_coprime) -> eut_divisor_prioritylayer_mask_choice_coprime = 1) /\ (eut_bit_prioritylayer_mask) = 0)))) /\ (exists fs_u_eut_prioritylayer_sum fs_v_eut_prioritylayer_sum. ((((exists fs_h_eut_prioritylayer_sum_body_start. fs_h_eut_prioritylayer_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_prioritylayer_sum)) /\ exists fs_q_eut_prioritylayer_sum_body_start. fs_u_eut_prioritylayer_sum = fs_q_eut_prioritylayer_sum_body_start * S ((S (0)) * fs_v_eut_prioritylayer_sum) + (0))) /\ ((((exists fs_h_eut_prioritylayer_sum_body_terminal. fs_h_eut_prioritylayer_sum_body_terminal + S (t) = S ((S (l)) * fs_v_eut_prioritylayer_sum)) /\ exists fs_q_eut_prioritylayer_sum_body_terminal. fs_u_eut_prioritylayer_sum = fs_q_eut_prioritylayer_sum_body_terminal * S ((S (l)) * fs_v_eut_prioritylayer_sum) + (t))) /\ forall fs_i_eut_prioritylayer_sum_body_steps. (exists fs_lt_eut_prioritylayer_sum_body_steps_bound. fs_lt_eut_prioritylayer_sum_body_steps_bound + S fs_i_eut_prioritylayer_sum_body_steps = l) -> exists fs_a_eut_prioritylayer_sum_body_steps fs_r_eut_prioritylayer_sum_body_steps fs_s_eut_prioritylayer_sum_body_steps. ((((exists fs_h_eut_prioritylayer_sum_body_steps_summand. fs_h_eut_prioritylayer_sum_body_steps_summand + S (fs_a_eut_prioritylayer_sum_body_steps) = S ((S (fs_i_eut_prioritylayer_sum_body_steps)) * eut_scale_prioritylayer)) /\ exists fs_q_eut_prioritylayer_sum_body_steps_summand. eut_code_prioritylayer = fs_q_eut_prioritylayer_sum_body_steps_summand * S ((S (fs_i_eut_prioritylayer_sum_body_steps)) * eut_scale_prioritylayer) + (fs_a_eut_prioritylayer_sum_body_steps))) /\ ((((exists fs_h_eut_prioritylayer_sum_body_steps_partial. fs_h_eut_prioritylayer_sum_body_steps_partial + S (fs_r_eut_prioritylayer_sum_body_steps) = S ((S (fs_i_eut_prioritylayer_sum_body_steps)) * fs_v_eut_prioritylayer_sum)) /\ exists fs_q_eut_prioritylayer_sum_body_steps_partial. fs_u_eut_prioritylayer_sum = fs_q_eut_prioritylayer_sum_body_steps_partial * S ((S (fs_i_eut_prioritylayer_sum_body_steps)) * fs_v_eut_prioritylayer_sum) + (fs_r_eut_prioritylayer_sum_body_steps))) /\ ((((exists fs_h_eut_prioritylayer_sum_body_steps_successor. fs_h_eut_prioritylayer_sum_body_steps_successor + S (fs_s_eut_prioritylayer_sum_body_steps) = S ((S (S fs_i_eut_prioritylayer_sum_body_steps)) * fs_v_eut_prioritylayer_sum)) /\ exists fs_q_eut_prioritylayer_sum_body_steps_successor. fs_u_eut_prioritylayer_sum = fs_q_eut_prioritylayer_sum_body_steps_successor * S ((S (S fs_i_eut_prioritylayer_sum_body_steps)) * fs_v_eut_prioritylayer_sum) + (fs_s_eut_prioritylayer_sum_body_steps))) /\ fs_s_eut_prioritylayer_sum_body_steps = fs_r_eut_prioritylayer_sum_body_steps + fs_a_eut_prioritylayer_sum_body_steps))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.