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
∀ ff_index_mcp_advanced. ∀ ff_source_mcp_advanced. ∀ ff_target_mcp_advanced. Lt(ff_index_mcp_advanced,l) → Beta(b,c,s + d · ff_index_mcp_advanced,ff_source_mcp_advanced) → Beta(u,v,ff_index_mcp_advanced,ff_target_mcp_advanced) → ff_target_mcp_advanced = ff_source_mcp_advancedOnly definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall ff_index_mcp_advanced ff_source_mcp_advanced ff_target_mcp_advanced. (exists mcp_gap_advanced_bound. mcp_gap_advanced_bound + S (ff_index_mcp_advanced) = (l)) -> (((exists fs_h_mcp_advanced_source. fs_h_mcp_advanced_source + S (ff_source_mcp_advanced) = S ((S ((s) + (d) * ff_index_mcp_advanced)) * c)) /\ exists fs_q_mcp_advanced_source. b = fs_q_mcp_advanced_source * S ((S ((s) + (d) * ff_index_mcp_advanced)) * c) + (ff_source_mcp_advanced))) -> (((exists fs_h_mcp_advanced_target. fs_h_mcp_advanced_target + S (ff_target_mcp_advanced) = S ((S (ff_index_mcp_advanced)) * v)) /\ exists fs_q_mcp_advanced_target. u = fs_q_mcp_advanced_target * S ((S (ff_index_mcp_advanced)) * v) + (ff_target_mcp_advanced))) -> ff_target_mcp_advanced = ff_source_mcp_advancedThe unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.