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
(∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,B)) ∧ (∀ x. ∀ y. ∀ z. Lt(x,l) → Lt(y,l) → BetaAt(b,c,x,z) → BetaAt(b,c,y,z) → x = y)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((forall fom_index_mrf_secondwavebound. (exists fom_gap_mrf_secondwavebound_index_bound. fom_gap_mrf_secondwavebound_index_bound + S (fom_index_mrf_secondwavebound) = l) -> exists fom_value_mrf_secondwavebound. ((((exists fom_beta_height_mrf_secondwavebound_entry. fom_beta_height_mrf_secondwavebound_entry + S (fom_value_mrf_secondwavebound) = S ((S (fom_index_mrf_secondwavebound)) * c)) /\ exists fom_beta_quotient_mrf_secondwavebound_entry. b = fom_beta_quotient_mrf_secondwavebound_entry * S ((S (fom_index_mrf_secondwavebound)) * c) + (fom_value_mrf_secondwavebound))) /\ (exists fom_gap_mrf_secondwavebound_value_bound. fom_gap_mrf_secondwavebound_value_bound + S (fom_value_mrf_secondwavebound) = B))) /\ (forall mdr_i_secondwavedistinct mdr_j_secondwavedistinct mdr_a_secondwavedistinct. (exists mdr_gap_secondwavedistincti. mdr_gap_secondwavedistincti + S (mdr_i_secondwavedistinct) = (l)) -> (exists mdr_gap_secondwavedistinctj. mdr_gap_secondwavedistinctj + S (mdr_j_secondwavedistinct) = (l)) -> (((exists ff_h_mdr_secondwavedistinctfirst. ff_h_mdr_secondwavedistinctfirst + S (mdr_a_secondwavedistinct) = S ((S (mdr_i_secondwavedistinct)) * c)) /\ exists ff_q_mdr_secondwavedistinctfirst. b = ff_q_mdr_secondwavedistinctfirst * S ((S (mdr_i_secondwavedistinct)) * c) + (mdr_a_secondwavedistinct))) -> (((exists ff_h_mdr_secondwavedistinctsecond. ff_h_mdr_secondwavedistinctsecond + S (mdr_a_secondwavedistinct) = S ((S (mdr_j_secondwavedistinct)) * c)) /\ exists ff_q_mdr_secondwavedistinctsecond. b = ff_q_mdr_secondwavedistinctsecond * S ((S (mdr_j_secondwavedistinct)) * c) + (mdr_a_secondwavedistinct))) -> mdr_i_secondwavedistinct = mdr_j_secondwavedistinct))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
DL003C · matrix_rank_selector_transportDL003D · matrix_rank_selector_decidableDL003E · matrix_rank_selector_dimension_boundDL003F · matrix_rank_selector_emptyDL0050 · matrix_rank_nonzero_selected_minor_decidableDL0097 · matrix_integer_selected_point_balanceDL0099 · matrix_integer_signed_selected_balanceDL009A · matrix_integer_selected_determinant_balanceDL00AF · matrix_lattice_identity_is_selector