(COMMENT generated from Maude module 'PEANO-NAT' by 'nosorts-noand' transformation)
(VAR M' M N' N X Z Y)
(THEORY (C gcd)
(C d)
(C _+_)
(C _*_))
(RULES
1 -> s_(0)

2 -> s_(s_(0))

3 -> s_(s_(s_(0)))

4 -> s_(s_(s_(s_(0))))

5 -> s_(s_(s_(s_(s_(0)))))

6 -> s_(s_(s_(s_(s_(s_(0))))))

7 -> s_(s_(s_(s_(s_(s_(s_(0)))))))

U11(tt,M,N) -> U12(tt,M,N)

U12(tt,M,N) -> s_(_+_(N,_+_(M,_*_(N,M))))

U21(tt,M,N) -> U22(tt,M,N)

U22(tt,M,N) -> s_(s_(_+_(N,M)))

U31(tt,M,N) -> U32(tt,M,N)

U32(tt,M,N) -> _>_(M,N)

U41(tt,M,N) -> U42(tt,M,N)

U42(tt,M,N) -> _>_(N,M)

U51(tt,M,N) -> U52(tt,M,N)

U52(tt,M,N) -> d(N,M)

U61(tt,M',N') -> U62(tt,M',N')

U62(tt,M',N') -> U63(equal(_>_(N',M'),true),M',N')

U63(tt,M',N') -> gcd(d(N',M'),M')

U71(tt,M',N) -> U72(tt,M',N)

U72(tt,M',N) -> U73(equal(_>_(M',N),true))

U73(tt) -> 0

U81(tt,M',N) -> U82(tt,M',N)

U82(tt,M',N) -> U83(equal(_>_(N,M'),true),M',N)

U83(tt,M',N) -> s_(quot(d(N,M'),M'))

_*_(N,0) -> 0

_*_(s_(N),s_(M)) -> U11(tt,M,N)

_+_(N,0) -> N

_+_(s_(N),s_(M)) -> U21(tt,M,N)

_<_(N,M) -> U31(tt,M,N)

_>_(0,M) -> false

_>_(N',0) -> true

_>_(s_(N),s_(M)) -> U41(tt,M,N)

d(0,N) -> N

d(s_(N),s_(M)) -> U51(tt,M,N)

equal(X,X) -> tt

gcd(0,N) -> 0

gcd(N',M') -> U61(tt,M',N')

gcd(N',N') -> N'

p_(s_(N)) -> N

quot(M',M') -> s_(0)

quot(N,M') -> U71(tt,M',N)

quot(N,M') -> U81(tt,M',N)
)