(STRATEGY
    INNERMOST)

(VAR
    x x' xs y)
(DATATYPES
    A = µX.< S(X), Cons(X, X), 0, Nil, True, False >)
(SIGNATURES
    bsort :: [A x A] -> A
    len :: [A] -> A
    bubble :: [A x A] -> A
    bubblesort :: [A] -> A
    + :: [A x A] -> A
    < :: [A x A] -> A
    bubble[Ite][False][Ite] :: [A x A x A] -> A)
(RULES
    bsort(S(x'),Cons(x,xs)) ->
      bsort(x',bubble(x,xs))
    len(Cons(x,xs)) -> +(S(0())
                        ,len(xs))
    bubble(x',Cons(x,xs)) ->
      bubble[Ite][False][Ite](<(x',x)
                             ,x'
                             ,Cons(x,xs))
    len(Nil()) -> 0()
    bubble(x,Nil()) -> Cons(x,Nil())
    bsort(0(),xs) -> xs
    bubblesort(xs) -> bsort(len(xs)
                           ,xs)
    +(x,S(0())) ->= S(x)
    +(S(0()),y) ->= S(y)
    <(S(x),S(y)) ->= <(x,y)
    <(0(),S(y)) ->= True()
    <(x,0()) ->= False()
    bubble[Ite][False][Ite](False()
                           ,x'
                           ,Cons(x,xs)) ->= Cons(x
                                                ,bubble(x',xs))
    bubble[Ite][False][Ite](True()
                           ,x'
                           ,Cons(x,xs)) ->= Cons(x'
                                                ,bubble(x,xs)))