The six key parts of PLT Redex are language, reduction-relation, define-metafunction, stepper, redex-check, and test-->. There are many other functions in the library that build on these (and provide variations and extensions), but these illustrate the key services that PLT Redex provides. The first, specifies a BNF grammar for a regular tree language. Each right-hand side is written in PLT Redex's pattern language (consisting of a mixture of concrete syntax elements and non-terminals, roughly speaking). With a language definition in place, the reduction-relation form is used to define the reduction relation: Syntactically, it consists of three sub-expressions: a language to which the reduction applies, a source pattern specifying which terms the rule matches, and Racket code that, when evaluated, produces the resulting term as an S-expression. Metafunctions are defined like this: The define-metafunction form defines the metafunction name by cases. Unlike the reduction relation, the branches for a metafunction are ordered. As soon as one of the patterns matches, that branch is taken regardless of other matches that might happen. The functions open GUI windows that let you explore the reduction graph of terms reachable from the initial term. The stepper behaves in a manner similar to DrRacket's stepper, and traces shows the reduction graph in a graph-viewing window. Redex can randomly generate example expressions to try to falsify conjectures about the rewriting system. For example, this expression randomly generates expressions matching pattern (typically a non-terminal) from the language language-name and then evaluates predicate. If it ever returns false, redex-check reports the expression that falsified the predicate. Finally, can be used to develop test suites for PLT Redex programs. It accepts a reduction relation and an example term and applies the reduction relation until it cannot reduce any further, at which point it checks to make sure that each the given final terms match.