(STRATEGY
    INNERMOST)

(VAR
    a b mtmp res res' t tmp x x' y)
(DATATYPES
    A = µX.< S(X), 0, True, False >)
(SIGNATURES
    m2 :: [A x A x A x A] -> A
    m3 :: [A x A x A x A] -> A
    l8 :: [A x A x A x A x A x A] -> A
    l5 :: [A x A x A x A x A x A] -> A
    help1 :: [A] -> A
    e4 :: [A x A x A x A] -> A
    e2 :: [A x A x A x A] -> A
    l15 :: [A x A x A x A x A x A] -> A
    l13 :: [A x A x A x A x A x A] -> A
    m4 :: [A x A x A x A] -> A
    l2 :: [A x A x A x A x A x A] -> A
    l11 :: [A x A x A x A x A x A] -> A
    bool2Nat :: [A] -> A
    m1 :: [A x A x A x A] -> A
    l9 :: [A x A x A x A x A x A] -> A
    l6 :: [A x A x A x A x A x A] -> A
    l4 :: [A x A x A x A x A x A] -> A
    l1 :: [A x A x A x A x A x A] -> A
    e7 :: [A x A x A x A] -> A
    e6 :: [A x A x A x A] -> A
    e5 :: [A x A x A x A] -> A
    monus :: [A x A] -> A
    m5 :: [A x A x A x A] -> A
    l7 :: [A x A x A x A x A x A] -> A
    l3 :: [A x A x A x A x A x A] -> A
    l16 :: [A x A x A x A x A x A] -> A
    l14 :: [A x A x A x A x A x A] -> A
    l12 :: [A x A x A x A x A x A] -> A
    l10 :: [A x A x A x A x A x A] -> A
    gcd :: [A x A] -> A
    equal0 :: [A x A] -> A
    e8 :: [A x A x A x A] -> A
    e3 :: [A x A x A x A] -> A
    e1 :: [A x A x A x A] -> A
    < :: [A x A] -> A)
(RULES
    m2(S(0()),b,res,True()) ->
      False()
    m2(S(S(x)),b,res,True()) ->
      True()
    m2(0(),b,res,True()) -> False()
    m3(S(0()),b,res,t) -> False()
    m3(S(S(x)),b,res,t) -> True()
    m3(0(),b,res,t) -> False()
    l8(res,y,res',True(),mtmp,t) ->
      res
    l5(x,y,res,tmp,mtmp,True()) ->
      0()
    help1(S(0())) -> False()
    help1(S(S(x))) -> True()
    e4(a,b,res,False()) -> False()
    e4(a,b,res,True()) -> True()
    e2(a,b,res,False()) -> False()
    l15(x,y,res,tmp,False(),t) ->
      l16(x
         ,y
         ,gcd(y,0())
         ,tmp
         ,False()
         ,t)
    l15(x,y,res,tmp,True(),t) ->
      l16(x
         ,y
         ,gcd(y,S(0()))
         ,tmp
         ,True()
         ,t)
    l13(x,y,res,tmp,False(),t) ->
      l16(x
         ,y
         ,gcd(0(),y)
         ,tmp
         ,False()
         ,t)
    l13(x,y,res,tmp,True(),t) ->
      l16(x
         ,y
         ,gcd(S(0()),y)
         ,tmp
         ,True()
         ,t)
    m4(S(x'),S(x),res,t) -> m5(S(x')
                              ,S(x)
                              ,monus(x',x)
                              ,t)
    m2(a,b,res,False()) -> m4(a
                             ,b
                             ,res
                             ,False())
    l8(x,y,res,False(),mtmp,t) ->
      l10(x,y,res,False(),mtmp,t)
    l5(x,y,res,tmp,mtmp,False()) ->
      l7(x,y,res,tmp,mtmp,False())
    l2(x,y,res,tmp,mtmp,False()) ->
      l3(x,y,res,tmp,mtmp,False())
    l2(x,y,res,tmp,mtmp,True()) ->
      res
    l11(x,y,res,tmp,mtmp,False()) ->
      l14(x,y,res,tmp,mtmp,False())
    l11(x,y,res,tmp,mtmp,True()) ->
      l12(x,y,res,tmp,mtmp,True())
    help1(0()) -> False()
    e2(a,b,res,True()) -> e3(a
                            ,b
                            ,res
                            ,True())
    bool2Nat(False()) -> 0()
    bool2Nat(True()) -> S(0())
    m1(a,x,res,t) -> m2(a
                       ,x
                       ,res
                       ,False())
    l9(res,y,res',tmp,mtmp,t) -> res
    l6(x,y,res,tmp,mtmp,t) -> 0()
    l4(x',x,res,tmp,mtmp,t) -> l5(x'
                                 ,x
                                 ,res
                                 ,tmp
                                 ,mtmp
                                 ,False())
    l1(x,y,res,tmp,mtmp,t) -> l2(x
                                ,y
                                ,res
                                ,tmp
                                ,mtmp
                                ,False())
    e7(a,b,res,t) -> False()
    e6(a,b,res,t) -> False()
    e5(a,b,res,t) -> True()
    monus(a,b) -> m1(a
                    ,b
                    ,False()
                    ,False())
    m5(a,b,res,t) -> res
    l7(x,y,res,tmp,mtmp,t) -> l8(x
                                ,y
                                ,res
                                ,equal0(x,y)
                                ,mtmp
                                ,t)
    l3(x,y,res,tmp,mtmp,t) -> l4(x
                                ,y
                                ,0()
                                ,tmp
                                ,mtmp
                                ,t)
    l16(x,y,res,tmp,mtmp,t) -> res
    l14(x,y,res,tmp,mtmp,t) -> l15(x
                                  ,y
                                  ,res
                                  ,tmp
                                  ,monus(x,y)
                                  ,t)
    l12(x,y,res,tmp,mtmp,t) -> l13(x
                                  ,y
                                  ,res
                                  ,tmp
                                  ,monus(x,y)
                                  ,t)
    l10(x,y,res,tmp,mtmp,t) -> l11(x
                                  ,y
                                  ,res
                                  ,tmp
                                  ,mtmp
                                  ,<(x,y))
    gcd(x,y) -> l1(x
                  ,y
                  ,0()
                  ,False()
                  ,False()
                  ,False())
    equal0(a,b) -> e1(a
                     ,b
                     ,False()
                     ,False())
    e8(a,b,res,t) -> res
    e3(a,b,res,t) -> e4(a
                       ,b
                       ,res
                       ,<(b,a))
    e1(a,b,res,t) -> e2(a
                       ,b
                       ,res
                       ,<(a,b))
    <(S(x),S(y)) ->= <(x,y)
    <(0(),S(y)) ->= True()
    <(x,0()) ->= False())