(COMMENT generated from Maude module 'PEANO-NAT' by 'nokinds-noand' transformation)
(VAR M' M N' N V1 V2 V 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)))))))

U101(tt,M,N) -> U102(isNat(N),M,N)

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

U11(tt) -> 0

U111(tt) -> 0

U121(tt,M',N') -> U122(isNzNat(N'),M',N')

U122(tt,M',N') -> U123(equal(_>_(N',M'),true),M',N')

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

U131(tt,N') -> N'

U141(tt,V2) -> U142(isNat(V2))

U142(tt) -> tt

U151(tt,V2) -> U152(isNat(V2))

U152(tt) -> tt

U161(tt) -> tt

U171(tt,V2) -> U172(isNat(V2))

U172(tt) -> tt

U181(tt,V2) -> U182(isNat(V2))

U182(tt) -> tt

U191(tt,V2) -> U192(isNat(V2))

U192(tt) -> tt

U201(tt,V2) -> U202(isNat(V2))

U202(tt) -> tt

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

U211(tt) -> tt

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

U221(tt,V2) -> U222(isNzNat(V2))

U222(tt) -> tt

U231(tt,V2) -> U232(isNzNat(V2))

U232(tt) -> tt

U241(tt,V2) -> U242(isNzNat(V2))

U242(tt) -> tt

U251(tt) -> tt

U261(tt,N) -> N

U271(tt) -> s_(0)

U281(tt,M',N) -> U282(isNat(N),M',N)

U282(tt,M',N) -> U283(equal(_>_(M',N),true))

U283(tt) -> 0

U291(tt,M',N) -> U292(isNat(N),M',N)

U292(tt,M',N) -> U293(equal(_>_(N,M'),true),M',N)

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

U31(tt,N) -> N

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

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

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

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

U61(tt) -> false

U71(tt) -> true

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

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

U91(tt,N) -> N

_*_(N,0) -> U11(isNat(N))

_*_(s_(N),s_(M)) -> U21(isNat(M),M,N)

_+_(N,0) -> U31(isNat(N),N)

_+_(s_(N),s_(M)) -> U41(isNat(M),M,N)

_<_(N,M) -> U51(isNat(M),M,N)

_>_(0,M) -> U61(isNat(M))

_>_(N',0) -> U71(isNzNat(N'))

_>_(s_(N),s_(M)) -> U81(isNat(M),M,N)

d(0,N) -> U91(isNat(N),N)

d(s_(N),s_(M)) -> U101(isNat(M),M,N)

equal(X,X) -> tt

gcd(0,N) -> U111(isNat(N))

gcd(N',M') -> U121(isNzNat(M'),M',N')

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

isBoolean(false) -> tt

isBoolean(true) -> tt

isBoolean(_<_(V1,V2)) -> U141(isNat(V1),V2)

isBoolean(_>_(V1,V2)) -> U151(isNat(V1),V2)

isNat(0) -> tt

isNat(V) -> U161(isNzNat(V))

isNat(_*_(V1,V2)) -> U171(isNat(V1),V2)

isNat(_+_(V1,V2)) -> U181(isNat(V1),V2)

isNat(d(V1,V2)) -> U191(isNat(V1),V2)

isNat(gcd(V1,V2)) -> U201(isNat(V1),V2)

isNat(p_(V1)) -> U211(isNzNat(V1))

isNat(quot(V1,V2)) -> U221(isNat(V1),V2)

isNzNat(1) -> tt

isNzNat(2) -> tt

isNzNat(3) -> tt

isNzNat(4) -> tt

isNzNat(5) -> tt

isNzNat(6) -> tt

isNzNat(7) -> tt

isNzNat(_*_(V1,V2)) -> U231(isNzNat(V1),V2)

isNzNat(gcd(V1,V2)) -> U241(isNzNat(V1),V2)

isNzNat(s_(V1)) -> U251(isNat(V1))

p_(s_(N)) -> U261(isNat(N),N)

quot(M',M') -> U271(isNzNat(M'))

quot(N,M') -> U281(isNzNat(M'),M',N)

quot(N,M') -> U291(isNzNat(M'),M',N)
)