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