(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTORBASED)
(VAR k x x' xs xs' y ys )
(STRATEGY INNERMOST)
(RULES 
        @(Cons(x, xs), ys) -> Cons(x, @(xs, ys))
        @(Nil, ys) -> ys
        binom(Cons(x, xs), Cons(x', xs')) -> @(binom(xs, xs'), binom(xs, Cons(x', xs')))
        binom(Cons(x, xs), Nil) -> Cons(Nil, Nil)
        binom(Nil, k) -> Cons(Nil, Nil)
        goal(x, y) -> binom(x, y)
        
)