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