Note: The first word of the <statistics-option> command can be abbreviated.<statistics-command> ::= statistics [ <statistics-option> ] <statistics-option> ::= time | usage [ <names> ]
statistics stat usage nat
The usage option displays information about the use of the rewrite and deduction rules matched by <names>, which defaults to "*". For rewrite rules, the information includes the number of successful applications, the number of attempted applications, and the number of nontrivial critical pairs computed from the rule. For deduction rules, the information includes the number of successful applications. In the display, each name is preceded by (rr) or (dr) to indicate whether the named fact is a rewrite rule or a deduction rule. If two or more facts had the same name, then the display show separate statistics for each incarnation of the name (for example, if two theorems, thm.1 and thm.2, were proved by cases, then two separate rewrite rules would have received the name thmCaseHyp1.1).