The process is based upon the simplification procedures in simpLib, but is more persistent in attempting to apply rewrite rules. It automatically incorporates relevant results from datatype declarations (the most important of these are injectivity and distinctness of constructors). It uses the current hypotheses when rewriting the goal. It automatically performs case-splitting on conditional expressions in the goal. It simplifies any equation between constructors occurring in the goal or the hypotheses. It automatically substitutes through the goal any assumption that is an equality v = M or M = v, if v is a variable not occurring in M. It eliminates any boolean variable or negated boolean variable occurring as a hypothesis. It breaks down any conjunctions, disjunctions, double negations, or existentials occurring as hypotheses. It keeps the goal in "stripped" format so that the resulting goal will not be an implication or universally quantified.

The automatic incorporation of datatype facts can be slow when operating in a context with many datatypes (or a few large datatypes). In such cases, SRW_TAC is preferable to RW_TAC.