(VAR X Y )
(STRATEGY CONTEXTSENSITIVE
        (from 1) 
        (cons 1) 
        (s 1) 
        (length ) 
        (nil ) 
        (0 ) 
        (length1 ) 
)
(RULES 
        from(X) -> cons(X, from(s(X)))
        length(nil) -> 0
        length(cons(X, Y)) -> s(length1(Y))
        length1(X) -> length(X)
        
)