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
¬T = 0 ∧ (∀ x. ∀ y. (∀ z. Lt(z,l) → ∃ n. BetaAt(x,y,z,n) ∧ Lt(n,B)) → ∃ z. Lt(z,T) ∧ (∀ n. ∀ m. Lt(n,l) → BetaAt(x,y,n,m) → BetaAt(z,c,n,m)))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~(T = 0)) /\ (forall mdr_b_secondwave mdr_e_secondwave. (forall fom_index_mrf_secondwavesource. (exists fom_gap_mrf_secondwavesource_index_bound. fom_gap_mrf_secondwavesource_index_bound + S (fom_index_mrf_secondwavesource) = l) -> exists fom_value_mrf_secondwavesource. ((((exists fom_beta_height_mrf_secondwavesource_entry. fom_beta_height_mrf_secondwavesource_entry + S (fom_value_mrf_secondwavesource) = S ((S (fom_index_mrf_secondwavesource)) * mdr_e_secondwave)) /\ exists fom_beta_quotient_mrf_secondwavesource_entry. mdr_b_secondwave = fom_beta_quotient_mrf_secondwavesource_entry * S ((S (fom_index_mrf_secondwavesource)) * mdr_e_secondwave) + (fom_value_mrf_secondwavesource))) /\ (exists fom_gap_mrf_secondwavesource_value_bound. fom_gap_mrf_secondwavesource_value_bound + S (fom_value_mrf_secondwavesource) = B))) -> exists mdr_z_secondwave. (((exists mdr_gap_secondwavebound. mdr_gap_secondwavebound + S (mdr_z_secondwave) = (T)) /\ (forall mdr_i_secondwaveprefix mdr_a_secondwaveprefix. (exists mdr_gap_secondwaveprefixb. mdr_gap_secondwaveprefixb + S (mdr_i_secondwaveprefix) = (l)) -> (((exists ff_h_mdr_secondwaveprefixo. ff_h_mdr_secondwaveprefixo + S (mdr_a_secondwaveprefix) = S ((S (mdr_i_secondwaveprefix)) * mdr_e_secondwave)) /\ exists ff_q_mdr_secondwaveprefixo. mdr_b_secondwave = ff_q_mdr_secondwaveprefixo * S ((S (mdr_i_secondwaveprefix)) * mdr_e_secondwave) + (mdr_a_secondwaveprefix))) -> (((exists ff_h_mdr_secondwaveprefixn. ff_h_mdr_secondwaveprefixn + S (mdr_a_secondwaveprefix) = S ((S (mdr_i_secondwaveprefix)) * c)) /\ exists ff_q_mdr_secondwaveprefixn. mdr_z_secondwave = ff_q_mdr_secondwaveprefixn * S ((S (mdr_i_secondwaveprefix)) * c) + (mdr_a_secondwaveprefix))))))))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
none