Comando: Rewrite

1. Usa equality substitute (ex: PreMakeReceiver)

Comando: Reduce

1. Usa invoke
2. Usa frule
3. Usa grule
4. Usa rules

Comando: Trivial rewrite

1. Usa regra de reescrita
2. Não faz reason aritmético
3. Não usa grules
4. Não faz simplificação
5. Talvez não use regra de reescrita com Generic actuals

Comando: Simplify

1. Não usa regra de reescrita.
2. Usa foward rules.
3. Usa grule
4. Faz reason aritmético
Ex: identidades
5. Não infere: A \in \power A
6. Faz simplificações lógicas
Ex: (PREDICATE \iff true) é substituído por (PREDICATE)