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.
Readable signature
AllPrime(b,c,l)Exact expansion
forall dp_i. (exists dp_gap. dp_gap + S dp_i = l) -> exists dp_p. ((((exists ff_h_defined_all_prime_entry. ff_h_defined_all_prime_entry + S (dp_p) = S ((S (dp_i)) * c)) /\ exists ff_q_defined_all_prime_entry. b = ff_q_defined_all_prime_entry * S ((S (dp_i)) * c) + (dp_p))) /\ (~(dp_p = 1) /\ forall dp_a dp_d. dp_p = dp_a * dp_d -> dp_a = 1 \/ dp_d = 1))This node is notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.
Definition neighborhood
Expands using
Used by definitions
none
Used by theorem statements or local proof propositions
none