\DOC PBETA_RULE

\TYPE {PBETA_RULE : (thm -> thm)}

\SYNOPSIS
Beta-reduces all the paired beta-redexes in the conclusion of a theorem.

\KEYWORDS
rule.

\DESCRIBE
When applied to a theorem {A |- t}, the inference rule {PBETA_RULE} beta-reduces
all beta-redexes, at any depth, in the conclusion {t}. Variables are renamed
where necessary to avoid free variable capture.
{
    A |- ....((\p. s1) s2)....
   ----------------------------  BETA_RULE
      A |- ....(s1[s2/p])....
}


\FAILURE
Never fails, but will have no effect if there are no paired beta-redexes.

\SEEALSO
Conv.BETA_RULE, PairRules.PBETA_CONV, PairRules.PBETA_TAC, PairRules.RIGHT_PBETA, PairRules.LEFT_PBETA.
\ENDDOC