1\DOC PBETA_RULE 2 3\TYPE {PBETA_RULE : (thm -> thm)} 4 5\SYNOPSIS 6Beta-reduces all the paired beta-redexes in the conclusion of a theorem. 7 8\KEYWORDS 9rule. 10 11\DESCRIBE 12When applied to a theorem {A |- t}, the inference rule {PBETA_RULE} beta-reduces 13all beta-redexes, at any depth, in the conclusion {t}. Variables are renamed 14where necessary to avoid free variable capture. 15{ 16 A |- ....((\p. s1) s2).... 17 ---------------------------- BETA_RULE 18 A |- ....(s1[s2/p]).... 19} 20 21 22\FAILURE 23Never fails, but will have no effect if there are no paired beta-redexes. 24 25\SEEALSO 26Conv.BETA_RULE, PairRules.PBETA_CONV, PairRules.PBETA_TAC, PairRules.RIGHT_PBETA, PairRules.LEFT_PBETA. 27\ENDDOC 28