(STRATEGY
    INNERMOST)

(VAR
    M N NzM NzN)
(DATATYPES
    A = µX.< s(X), 0, False, True >)
(SIGNATURES
    p :: [A] -> A
    + :: [A x A] -> A
    * :: [A x A] -> A
    gt :: [A x A] -> A
    u_4 :: [A] -> A
    is_NzNat :: [A] -> A
    lt :: [A x A] -> A
    d :: [A x A] -> A
    quot :: [A x A] -> A
    u_11 :: [A x A x A] -> A
    u_1 :: [A x A x A] -> A
    u_01 :: [A] -> A
    u_21 :: [A x A x A] -> A
    u_2 :: [A] -> A
    gcd :: [A x A] -> A
    u_02 :: [A x A] -> A
    u_31 :: [A x A x A x A] -> A
    u_3 :: [A x A x A] -> A)
(RULES
    p(s(N)) -> N
    +(N,0()) -> N
    +(s(N),s(M)) -> s(s(+(N,M)))
    *(N,0()) -> 0()
    *(s(N),s(M)) -> s(+(N
                       ,+(M,*(N,M))))
    gt(0(),M) -> False()
    gt(NzN,0()) ->
      u_4(is_NzNat(NzN))
    u_4(True()) -> True()
    is_NzNat(0()) -> False()
    is_NzNat(s(N)) -> True()
    gt(s(N),s(M)) -> gt(N,M)
    lt(N,M) -> gt(M,N)
    d(0(),N) -> N
    d(s(N),s(M)) -> d(N,M)
    quot(N,NzM) ->
      u_11(is_NzNat(NzM),N,NzM)
    u_11(True(),N,NzM) -> u_1(gt(N
                                ,NzM)
                             ,N
                             ,NzM)
    u_1(True(),N,NzM) -> s(quot(d(N
                                 ,NzM)
                               ,NzM))
    quot(NzM,NzM) ->
      u_01(is_NzNat(NzM))
    u_01(True()) -> s(0())
    quot(N,NzM) ->
      u_21(is_NzNat(NzM),NzM,N)
    u_21(True(),NzM,N) -> u_2(gt(NzM
                                ,N))
    u_2(True()) -> 0()
    gcd(0(),N) -> 0()
    gcd(NzM,NzM) ->
      u_02(is_NzNat(NzM),NzM)
    u_02(True(),NzM) -> NzM
    gcd(NzN,NzM) ->
      u_31(is_NzNat(NzN)
          ,is_NzNat(NzM)
          ,NzN
          ,NzM)
    u_31(True(),True(),NzN,NzM) ->
      u_3(gt(NzN,NzM),NzN,NzM)
    u_3(True(),NzN,NzM) -> gcd(d(NzN
                                ,NzM)
                              ,NzM))