(COMMENT lessElements takes a list and a tree as input and returns that data-structure which has stored less elements. problems: termination by bounded increase not confluent ) (VAR l l1 l2 t t1 t2 n m b) (RULES lessElements(l,t) -> lessE(l,t,0) lessE(l,t,n) -> if(le(length(l),n),le(length(toList(t)),n),l,t,n) if(true,b,l,t,n) -> l if(false,true,l,t,n) -> t if(false,false,l,t,n) -> lessE(l,t,s(n)) length(nil) -> 0 length(cons(n,l)) -> s(length(l)) toList(leaf) -> nil toList(node(t1,n,t2)) -> append(toList(t1),cons(n,toList(t2))) append(nil,l2) -> l2 append(cons(n,l1),l2) -> cons(n,append(l1,l2)) le(s(n), 0) -> false le(0, m) -> true le(s(n), s(m)) -> le(n,m) a -> c a -> d )