1\DOC LIST_PBETA_CONV 2 3\TYPE {LIST_PBETA_CONV : conv} 4 5\KEYWORDS 6conversion. 7 8\LIBRARY 9pair 10 11\SYNOPSIS 12Performs an iterated paired beta-conversion. 13 14\DESCRIBE 15The conversion {LIST_PBETA_CONV} maps terms of the form 16{ 17 (\p1 p2 ... pn. t) q1 q2 ... qn 18} 19to the theorems of the form 20{ 21 |- (\p1 p2 ... pn. t) q1 q2 ... qn = t[q1/p1][q2/p2] ... [qn/pn] 22} 23where {t[qi/pi]} denotes the result of substituting {qi} for all free 24occurrences of {pi} in {t}, after renaming sufficient bound variables to avoid 25variable capture. 26 27\FAILURE 28{LIST_PBETA_CONV tm} fails if {tm} does not have the form 29{(\p1 ... pn. t) q1 ... qn} for {n} greater than 0. 30 31\EXAMPLE 32{ 33- LIST_PBETA_CONV (Term `(\(a,b) (c,d) . a + b + c + d) (1,2) (3,4)`); 34> val it = |- (\(a,b) (c,d). a + b + c + d) (1,2) (3,4) = 1 + 2 + 3 + 4 : thm 35} 36 37 38\SEEALSO 39Drule.LIST_BETA_CONV, PairRules.PBETA_CONV, Conv.BETA_RULE, Tactic.BETA_TAC, PairRules.RIGHT_PBETA, PairRules.RIGHT_LIST_PBETA, PairRules.LEFT_PBETA, PairRules.LEFT_LIST_PBETA. 40\ENDDOC 41