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
∀ sph_i_secondwave. ∀ sph_A_secondwave. ∀ sph_B_secondwave. ∀ sph_C_secondwave. Lt(sph_i_secondwave,l) → BetaAt(pb,pc,sph_i_secondwave,sph_A_secondwave) → BetaAt(nb,nc,sph_i_secondwave,sph_B_secondwave) → BetaAt(gb,gc,sph_i_secondwave,sph_C_secondwave) → sph_C_secondwave = sph_A_secondwave + h · sph_B_secondwaveOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall sph_i_secondwave sph_A_secondwave sph_B_secondwave sph_C_secondwave. (exists hpl_gap_secondwave. hpl_gap_secondwave + S (sph_i_secondwave) = (l)) -> (((exists fs_h_sph_secondwave_positive. fs_h_sph_secondwave_positive + S (sph_A_secondwave) = S ((S (sph_i_secondwave)) * pc)) /\ exists fs_q_sph_secondwave_positive. pb = fs_q_sph_secondwave_positive * S ((S (sph_i_secondwave)) * pc) + (sph_A_secondwave))) -> (((exists fs_h_sph_secondwave_negative. fs_h_sph_secondwave_negative + S (sph_B_secondwave) = S ((S (sph_i_secondwave)) * nc)) /\ exists fs_q_sph_secondwave_negative. nb = fs_q_sph_secondwave_negative * S ((S (sph_i_secondwave)) * nc) + (sph_B_secondwave))) -> (((exists fs_h_sph_secondwave_combined. fs_h_sph_secondwave_combined + S (sph_C_secondwave) = S ((S (sph_i_secondwave)) * gc)) /\ exists fs_q_sph_secondwave_combined. gb = fs_q_sph_secondwave_combined * S ((S (sph_i_secondwave)) * gc) + (sph_C_secondwave))) -> sph_C_secondwave = sph_A_secondwave + h * sph_B_secondwaveThe 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