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