(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTOR-BASED)
(STRATEGY INNERMOST)



  

(VAR
    x xs ys tLeq tGt e n m nr up nrs t ts data)
(DATATYPES
    Bool = µX.< True, False >
    Nat = µX.< 0, S(X)>
    ListNat = µX.< ConsNat(Nat, X), NilNat >
    ListBTree = µX.< ConsBTree(BTree, X), NilBTree >
    BTree = µX.< Node(ListNat,ListBTree) >)
(RULES

    ite(True, t, e)  ->= t
    ite(False, t, e) ->= e
    leq(0,0)         ->= True
    leq(S(n), 0)     ->= False
    leq(0,S(m))      ->= True
    leq(S(n),S(m))   ->= leq(n,m)


    append(NilNat, ys)      -> ys
    append(ConsNat(x,xs), ys) -> ConsNat(x,append(xs, ys))

    filterLeq(nr,NilNat) -> NilNat
    filterLeq(nr,ConsNat(x,xs)) -> ite(leq(nr,x),ConsNat(x,filterLeq(nr,xs)),filterLeq(nr,xs))

    takeWhileLeq(nr,Leaf(data)) -> data
    takeWhileLeq(nr,Node(ConsNat(up,NilNat),ConsBTree(tLeq,ConsBTree(tGt,NilBTree)))) ->
        ite(leq(nr,up), append(takeWhileLeq(nr,tLeq),filterLeq(nr,takeWhileLeq(nr,tGt))), NilNat)
    takeWhileLeq(nr,Node(ConsNat(up,nrs),ConsBTree(t,ts))) ->
        ite(leq(nr,up), append(takeWhileLeq(nr,t),takeWhileLeq(nr,Node(nrs,ts))), NilNat))