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
∀ kmc_index_secondwave. Lt(kmc_index_secondwave,l) → ∃ x. ∃ y. ∃ z. ∃ n. BetaAt(lb,lc,kmc_index_secondwave,x) ∧ (BetaAt(rb,rc,kmc_index_secondwave,y) ∧ (BetaAt(tb,tc,kmc_index_secondwave,z) ∧ (BetaAt(cb,cc,kmc_index_secondwave,n) ∧ (n = 0 ∧ z = x + y ∨ n = 1 ∧ z = S (x + y)))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
forall kmc_index_secondwave. (exists bcf_lt_gap_secondwave_bound. bcf_lt_gap_secondwave_bound + S (kmc_index_secondwave) = l) -> exists kmc_left_secondwave kmc_right_secondwave kmc_total_secondwave kmc_bit_secondwave. (((exists fs_h_secondwave_left. fs_h_secondwave_left + S (kmc_left_secondwave) = S ((S (kmc_index_secondwave)) * lc)) /\ exists fs_q_secondwave_left. lb = fs_q_secondwave_left * S ((S (kmc_index_secondwave)) * lc) + (kmc_left_secondwave))) /\ ((((exists fs_h_secondwave_right. fs_h_secondwave_right + S (kmc_right_secondwave) = S ((S (kmc_index_secondwave)) * rc)) /\ exists fs_q_secondwave_right. rb = fs_q_secondwave_right * S ((S (kmc_index_secondwave)) * rc) + (kmc_right_secondwave))) /\ ((((exists fs_h_secondwave_total. fs_h_secondwave_total + S (kmc_total_secondwave) = S ((S (kmc_index_secondwave)) * tc)) /\ exists fs_q_secondwave_total. tb = fs_q_secondwave_total * S ((S (kmc_index_secondwave)) * tc) + (kmc_total_secondwave))) /\ ((((exists fs_h_secondwave_bit. fs_h_secondwave_bit + S (kmc_bit_secondwave) = S ((S (kmc_index_secondwave)) * cc)) /\ exists fs_q_secondwave_bit. cb = fs_q_secondwave_bit * S ((S (kmc_index_secondwave)) * cc) + (kmc_bit_secondwave))) /\ (((kmc_bit_secondwave = 0 /\ kmc_total_secondwave = kmc_left_secondwave + kmc_right_secondwave) \/ (kmc_bit_secondwave = 1 /\ kmc_total_secondwave = S (kmc_left_secondwave + kmc_right_secondwave)))))))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
Checked theorems using this definition
none directly; see definition consumers