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