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.
Hygienic expanded first-order definition
((((exists bcf_height_bpc_explorer_start. bcf_height_bpc_explorer_start + S (n) = S ((S (0)) * c)) /\ exists bcf_quotient_bpc_explorer_start. b = bcf_quotient_bpc_explorer_start * S ((S (0)) * c) + (n))) /\ forall bcf_index_bpc_explorer_chain. (exists bcf_lt_gap_bpc_explorer_index. bcf_lt_gap_bpc_explorer_index + S (bcf_index_bpc_explorer_chain) = k) -> exists bcf_previous_bpc_explorer_chain bcf_following_bpc_explorer_chain. ((((exists bcf_height_bpc_explorer_previous. bcf_height_bpc_explorer_previous + S (bcf_previous_bpc_explorer_chain) = S ((S (bcf_index_bpc_explorer_chain)) * c)) /\ exists bcf_quotient_bpc_explorer_previous. b = bcf_quotient_bpc_explorer_previous * S ((S (bcf_index_bpc_explorer_chain)) * c) + (bcf_previous_bpc_explorer_chain))) /\ ((((exists bcf_height_bpc_explorer_following. bcf_height_bpc_explorer_following + S (bcf_following_bpc_explorer_chain) = S ((S (S bcf_index_bpc_explorer_chain)) * c)) /\ exists bcf_quotient_bpc_explorer_following. b = bcf_quotient_bpc_explorer_following * S ((S (S bcf_index_bpc_explorer_chain)) * c) + (bcf_following_bpc_explorer_chain))) /\ ((((~(bcf_following_bpc_explorer_chain = 1) /\ forall frm_prime_left_bpc_explorer_successor_prime frm_prime_right_bpc_explorer_successor_prime. bcf_following_bpc_explorer_chain = frm_prime_left_bpc_explorer_successor_prime * frm_prime_right_bpc_explorer_successor_prime -> frm_prime_left_bpc_explorer_successor_prime = 1 \/ frm_prime_right_bpc_explorer_successor_prime = 1)) /\ ((exists bcf_lt_gap_bpc_explorer_successor_lower. bcf_lt_gap_bpc_explorer_successor_lower + S (bcf_previous_bpc_explorer_chain) = bcf_following_bpc_explorer_chain) /\ (exists bcf_lt_gap_bpc_explorer_successor_upper. bcf_lt_gap_bpc_explorer_successor_upper + S (bcf_following_bpc_explorer_chain) = bcf_previous_bpc_explorer_chain + bcf_previous_bpc_explorer_chain)))))))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