1\DOC RIGHT_PBETA
2
3\TYPE {RIGHT_PBETA : (thm -> thm)}
4
5\KEYWORDS
6rule.
7
8\LIBRARY
9pair
10
11\SYNOPSIS
12Beta-reduces a top-level paired beta-redex on the right-hand side of an
13equation.
14
15\DESCRIBE
16When applied to an equational theorem, {RIGHT_PBETA} applies paired
17beta-reduction at top level to the right-hand side (only).
18Variables are renamed if necessary to avoid free variable capture.
19{
20    A |- s = (\p. t1) t2
21   ----------------------  RIGHT_PBETA
22     A |- s = t1[t2/p]
23}
24
25
26\FAILURE
27Fails unless the theorem is equational, with its right-hand side being
28a top-level paired beta-redex.
29
30\SEEALSO
31Drule.RIGHT_BETA, PairRules.PBETA_CONV, PairRules.PBETA_RULE, PairRules.PBETA_TAC, PairRules.RIGHT_LIST_PBETA, PairRules.LEFT_PBETA, PairRules.LEFT_LIST_PBETA.
32\ENDDOC
33