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
IdentityMatrixSelector(b,c,p) ∧ ((∀ x. ∀ y. Lt(x,p) → BetaAt(b,c,x,y) → Lt(y,p)) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,p) → Lt(y,p) → BetaAt(b,c,x,z) → BetaAt(b,c,y,z) → x = y) ∧ (∀ x. Lt(x,p) → ∃ y. Lt(y,p) ∧ BetaAt(b,c,y,x))))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((forall pff_enumeration_index_bottomlayerenumeration. (exists pfa_gap_bottomlayerenumerationbound. pfa_gap_bottomlayerenumerationbound + S (pff_enumeration_index_bottomlayerenumeration) = ((p))) -> (((exists ff_h_pft_bottomlayerenumerationentry. ff_h_pft_bottomlayerenumerationentry + S (pff_enumeration_index_bottomlayerenumeration) = S ((S (pff_enumeration_index_bottomlayerenumeration)) * (c))) /\ exists ff_q_pft_bottomlayerenumerationentry. (b) = ff_q_pft_bottomlayerenumerationentry * S ((S (pff_enumeration_index_bottomlayerenumeration)) * (c)) + (pff_enumeration_index_bottomlayerenumeration)))) /\ (((forall pff_cardinality_i_bottomlayer pff_cardinality_a_bottomlayer. (exists pfa_gap_bottomlayerbounded_index. pfa_gap_bottomlayerbounded_index + S (pff_cardinality_i_bottomlayer) = ((p))) -> (((exists ff_h_pft_bottomlayerbounded_entry. ff_h_pft_bottomlayerbounded_entry + S (pff_cardinality_a_bottomlayer) = S ((S (pff_cardinality_i_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayerbounded_entry. (b) = ff_q_pft_bottomlayerbounded_entry * S ((S (pff_cardinality_i_bottomlayer)) * (c)) + (pff_cardinality_a_bottomlayer))) -> (exists pfa_gap_bottomlayerbounded_value. pfa_gap_bottomlayerbounded_value + S (pff_cardinality_a_bottomlayer) = ((p)))) /\ (((forall pff_cardinality_i_bottomlayer pff_cardinality_j_bottomlayer pff_cardinality_a_bottomlayer. (exists pfa_gap_bottomlayerinjective_i. pfa_gap_bottomlayerinjective_i + S (pff_cardinality_i_bottomlayer) = ((p))) -> (exists pfa_gap_bottomlayerinjective_j. pfa_gap_bottomlayerinjective_j + S (pff_cardinality_j_bottomlayer) = ((p))) -> (((exists ff_h_pft_bottomlayerinjective_first. ff_h_pft_bottomlayerinjective_first + S (pff_cardinality_a_bottomlayer) = S ((S (pff_cardinality_i_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayerinjective_first. (b) = ff_q_pft_bottomlayerinjective_first * S ((S (pff_cardinality_i_bottomlayer)) * (c)) + (pff_cardinality_a_bottomlayer))) -> (((exists ff_h_pft_bottomlayerinjective_second. ff_h_pft_bottomlayerinjective_second + S (pff_cardinality_a_bottomlayer) = S ((S (pff_cardinality_j_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayerinjective_second. (b) = ff_q_pft_bottomlayerinjective_second * S ((S (pff_cardinality_j_bottomlayer)) * (c)) + (pff_cardinality_a_bottomlayer))) -> pff_cardinality_i_bottomlayer = pff_cardinality_j_bottomlayer) /\ ((forall pff_cardinality_a_bottomlayer. (exists pfa_gap_bottomlayersurjective_value. pfa_gap_bottomlayersurjective_value + S (pff_cardinality_a_bottomlayer) = ((p))) -> exists pff_cardinality_i_bottomlayer. (exists pfa_gap_bottomlayersurjective_index. pfa_gap_bottomlayersurjective_index + S (pff_cardinality_i_bottomlayer) = ((p))) /\ (((exists ff_h_pft_bottomlayersurjective_entry. ff_h_pft_bottomlayersurjective_entry + S (pff_cardinality_a_bottomlayer) = S ((S (pff_cardinality_i_bottomlayer)) * (c))) /\ exists ff_q_pft_bottomlayersurjective_entry. (b) = ff_q_pft_bottomlayersurjective_entry * S ((S (pff_cardinality_i_bottomlayer)) * (c)) + (pff_cardinality_a_bottomlayer))))))))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.