1\DOC PBETA_RULE
2
3\TYPE {PBETA_RULE : (thm -> thm)}
4
5\SYNOPSIS
6Beta-reduces all the paired beta-redexes in the conclusion of a theorem.
7
8\KEYWORDS
9rule.
10
11\DESCRIBE
12When applied to a theorem {A |- t}, the inference rule {PBETA_RULE} beta-reduces
13all beta-redexes, at any depth, in the conclusion {t}. Variables are renamed
14where necessary to avoid free variable capture.
15{
16    A |- ....((\p. s1) s2)....
17   ----------------------------  BETA_RULE
18      A |- ....(s1[s2/p])....
19}
20
21
22\FAILURE
23Never fails, but will have no effect if there are no paired beta-redexes.
24
25\SEEALSO
26Conv.BETA_RULE, PairRules.PBETA_CONV, PairRules.PBETA_TAC, PairRules.RIGHT_PBETA, PairRules.LEFT_PBETA.
27\ENDDOC
28