(STRATEGY
    INNERMOST)

(VAR
    X Y)
(DATATYPES
    A = µX.< s(X), 0, false, true >)
(SIGNATURES
    minus :: [A x A] -> A
    pred :: [A] -> A
    le :: [A x A] -> A
    gcd :: [A x A] -> A
    if :: [A x A x A] -> A)
(RULES
    minus(X,s(Y)) -> pred(minus(X
                               ,Y))
    minus(X,0()) -> X
    pred(s(X)) -> X
    le(s(X),s(Y)) -> le(X,Y)
    le(s(X),0()) -> false()
    le(0(),Y) -> true()
    gcd(0(),Y) -> 0()
    gcd(s(X),0()) -> s(X)
    gcd(s(X),s(Y)) -> if(le(Y,X)
                        ,s(X)
                        ,s(Y))
    if(true(),s(X),s(Y)) ->
      gcd(minus(X,Y),s(Y))
    if(false(),s(X),s(Y)) ->
      gcd(minus(Y,X),s(X)))