(STRATEGY
    INNERMOST)

(VAR
    a b x x' y)
(DATATYPES
    A = µX.< S(X), 0, True, False >)
(SIGNATURES
    monus :: [A x A] -> A
    gcd :: [A x A] -> A
    equal0 :: [A x A] -> A
    < :: [A x A] -> A
    gcd[Ite] :: [A x A x A] -> A
    gcd[False][Ite] :: [A x A x A] -> A
    equal0[Ite] :: [A x A x A] -> A
    equal0[True][Ite] :: [A x A x A] -> A)
(RULES
    monus(S(x'),S(x)) -> monus(x',x)
    gcd(x,y) -> gcd[Ite](equal0(x,y)
                        ,x
                        ,y)
    equal0(a,b) -> equal0[Ite](<(a
                                ,b)
                              ,a
                              ,b)
    <(S(x),S(y)) ->= <(x,y)
    <(0(),S(y)) ->= True()
    <(x,0()) ->= False()
    gcd[Ite](False(),x,y) ->=
      gcd[False][Ite](<(x,y),x,y)
    gcd[Ite](True(),x,y) ->= x
    gcd[False][Ite](False(),x,y) ->=
      gcd(y,monus(y,x))
    gcd[False][Ite](True(),x,y) ->=
      gcd(monus(x,y),y)
    equal0[Ite](False(),a,b) ->=
      False()
    equal0[Ite](True(),a,b) ->=
      equal0[True][Ite](<(b,a),a,b)
    equal0[True][Ite](False()
                     ,a
                     ,b) ->= False()
    equal0[True][Ite](True()
                     ,a
                     ,b) ->= True())