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
∀ ff_index_mce_alternating_breakthrough. Lt(ff_index_mce_alternating_breakthrough,l) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. Beta(ab,ac,ff_index_mce_alternating_breakthrough,x) ∧ (Beta(db,dc,ff_index_mce_alternating_breakthrough,y) ∧ (Beta(eb,ec,ff_index_mce_alternating_breakthrough,z) ∧ (Beta(fb,fc,ff_index_mce_alternating_breakthrough,n) ∧ (Beta(ub,uc,ff_index_mce_alternating_breakthrough,m) ∧ (Beta(vb,vc,ff_index_mce_alternating_breakthrough,k) ∧ SignedAlternatingCofactorTerm(x,y,z,n,ff_index_mce_alternating_breakthrough,m,k))))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall ff_index_mce_alternating_breakthrough. (exists ff_gap_mce_breakthrough_index. ff_gap_mce_breakthrough_index + S (ff_index_mce_alternating_breakthrough) = (l)) -> exists ff_ap_mce_alternating_breakthrough ff_an_mce_alternating_breakthrough ff_bp_mce_alternating_breakthrough ff_bn_mce_alternating_breakthrough ff_p_mce_alternating_breakthrough ff_n_mce_alternating_breakthrough. ((((exists ff_h_mce_breakthrough_ap. ff_h_mce_breakthrough_ap + S (ff_ap_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * ac)) /\ exists ff_q_mce_breakthrough_ap. ab = ff_q_mce_breakthrough_ap * S ((S (ff_index_mce_alternating_breakthrough)) * ac) + (ff_ap_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_an. ff_h_mce_breakthrough_an + S (ff_an_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * dc)) /\ exists ff_q_mce_breakthrough_an. db = ff_q_mce_breakthrough_an * S ((S (ff_index_mce_alternating_breakthrough)) * dc) + (ff_an_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_bp. ff_h_mce_breakthrough_bp + S (ff_bp_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * ec)) /\ exists ff_q_mce_breakthrough_bp. eb = ff_q_mce_breakthrough_bp * S ((S (ff_index_mce_alternating_breakthrough)) * ec) + (ff_bp_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_bn. ff_h_mce_breakthrough_bn + S (ff_bn_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * fc)) /\ exists ff_q_mce_breakthrough_bn. fb = ff_q_mce_breakthrough_bn * S ((S (ff_index_mce_alternating_breakthrough)) * fc) + (ff_bn_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_positive. ff_h_mce_breakthrough_positive + S (ff_p_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * uc)) /\ exists ff_q_mce_breakthrough_positive. ub = ff_q_mce_breakthrough_positive * S ((S (ff_index_mce_alternating_breakthrough)) * uc) + (ff_p_mce_alternating_breakthrough))) /\ ((((exists ff_h_mce_breakthrough_negative. ff_h_mce_breakthrough_negative + S (ff_n_mce_alternating_breakthrough) = S ((S (ff_index_mce_alternating_breakthrough)) * vc)) /\ exists ff_q_mce_breakthrough_negative. vb = ff_q_mce_breakthrough_negative * S ((S (ff_index_mce_alternating_breakthrough)) * vc) + (ff_n_mce_alternating_breakthrough))) /\ (((exists ff_even_mce_term_breakthrough_term. ff_index_mce_alternating_breakthrough = 2 * ff_even_mce_term_breakthrough_term) /\ (ff_p_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough) /\ ff_n_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough))) \/ ((exists ff_odd_mce_term_breakthrough_term. ff_index_mce_alternating_breakthrough = 2 * ff_odd_mce_term_breakthrough_term + 1) /\ (ff_p_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough) /\ ff_n_mce_alternating_breakthrough = (ff_ap_mce_alternating_breakthrough) * (ff_bp_mce_alternating_breakthrough) + (ff_an_mce_alternating_breakthrough) * (ff_bn_mce_alternating_breakthrough))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.