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