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
BoundedQRes(m,a)Exact expansion
exists qr_x_defined_bounded_qres. (exists qr_h_defined_bounded_qres. qr_h_defined_bounded_qres + S qr_x_defined_bounded_qres = m) /\ exists qr_u_defined_bounded_qres qr_v_defined_bounded_qres. qr_x_defined_bounded_qres * qr_x_defined_bounded_qres + m * qr_u_defined_bounded_qres = a + m * qr_v_defined_bounded_qresThis 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