Introduction


Transformation
define fact'(x,y) = y * fact(x)
definition of fact'(x,y): 
 	fact'(x,y) 
 {unfolding}       = y * ( case (x = 0) of 
 			True 	-> 1
 			False	-> x * fact(x-1) )
 {distribution}    = case (x = 0) of 
 			True 	-> y * 1
 			False	-> y * (x * fact(x-1)) 
 {elim *1; assoc.} = case (x = 0) of 
 			True 	-> y 
 			False	-> (y * x) * fact(x-1) 
 {folding}         = case (x = 0) of 
 			True 	-> y 
 			False	-> fact'(x-1,y*x)