YES Termination proof of ../tpdb/TRS/CSR_Maude/my-nat/MYNAT_nokinds-noand.trs
Termination of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(V2))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(V2))
U32(tt) → tt
U41(tt, N) → N
U51(tt, M, N) → U52(isNat(N), M, N)
U52(tt, M, N) → s(plus(N, M))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(N), M, N)
U72(tt, M, N) → plus(x(N, M), N)
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
isNat(x(V1, V2)) → U31(isNat(V1), V2)
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
isNat: empty set
U21: {1}
U31: {1}
U32: {1}
U41: {1}
U51: {1}
U52: {1}
s: {1}
plus: {1, 2}
U61: {1}
0: empty set
U71: {1}
U72: {1}
x: {1, 2}


↳ CSR
  ↳ Zantema-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(V2))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(V2))
U32(tt) → tt
U41(tt, N) → N
U51(tt, M, N) → U52(isNat(N), M, N)
U52(tt, M, N) → s(plus(N, M))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(N), M, N)
U72(tt, M, N) → plus(x(N, M), N)
isNat(0) → tt
isNat(plus(V1, V2)) → U11(isNat(V1), V2)
isNat(s(V1)) → U21(isNat(V1))
isNat(x(V1, V2)) → U31(isNat(V1), V2)
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)

The replacement map contains the following entries:

U11: {1}
tt: empty set
U12: {1}
isNat: empty set
U21: {1}
U31: {1}
U32: {1}
U41: {1}
U51: {1}
U52: {1}
s: {1}
plus: {1, 2}
U61: {1}
0: empty set
U71: {1}
U72: {1}
x: {1, 2}

We applied the Zantema [34] to transform the context-sensitive TRS to an usual TRS.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(a(V2)))
U32(tt) → tt
U41(tt, N) → a(N)
U51(tt, M, N) → U52(isNat(a(N)), a(M), a(N))
U52(tt, M, N) → s(plus(a(N), a(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(a(N)), a(M), a(N))
U72(tt, M, N) → plus(x(a(N), a(M)), a(N))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
isNat(xInact(V1, V2)) → U31(isNat(a(V1)), a(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

X(N, s(M)) → U711(isNat(M), M, N)
PLUS(N, s(M)) → U511(isNat(M), M, N)
U711(tt, M, N) → ISNAT(a(N))
U111(tt, V2) → ISNAT(a(V2))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
U721(tt, M, N) → A(N)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
U311(tt, V2) → ISNAT(a(V2))
X(N, 0) → U611(isNat(N))
PLUS(N, s(M)) → ISNAT(M)
PLUS(N, 0) → U411(isNat(N), N)
U511(tt, M, N) → U521(isNat(a(N)), a(M), a(N))
U111(tt, V2) → U121(isNat(a(V2)))
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U611(tt) → 01
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U311(tt, V2) → U321(isNat(a(V2)))
U111(tt, V2) → A(V2)
U521(tt, M, N) → S(plus(a(N), a(M)))
U711(tt, M, N) → A(N)
ISNAT(xInact(V1, V2)) → A(V2)
A(0Inact) → 01
U311(tt, V2) → A(V2)
ISNAT(plusInact(V1, V2)) → A(V2)
U521(tt, M, N) → A(M)
U521(tt, M, N) → A(N)
U711(tt, M, N) → A(M)
A(sInact(x1)) → S(x1)
A(xInact(x1, x2)) → X(x1, x2)
ISNAT(xInact(V1, V2)) → U311(isNat(a(V1)), a(V2))
ISNAT(sInact(V1)) → A(V1)
ISNAT(sInact(V1)) → U211(isNat(a(V1)))
U511(tt, M, N) → A(N)
U511(tt, M, N) → ISNAT(a(N))
X(N, s(M)) → ISNAT(M)
U721(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
U721(tt, M, N) → X(a(N), a(M))
X(N, 0) → ISNAT(N)
U721(tt, M, N) → A(M)
U511(tt, M, N) → A(M)
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U521(tt, M, N) → PLUS(a(N), a(M))
U411(tt, N) → A(N)
U711(tt, M, N) → U721(isNat(a(N)), a(M), a(N))

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(a(V2)))
U32(tt) → tt
U41(tt, N) → a(N)
U51(tt, M, N) → U52(isNat(a(N)), a(M), a(N))
U52(tt, M, N) → s(plus(a(N), a(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(a(N)), a(M), a(N))
U72(tt, M, N) → plus(x(a(N), a(M)), a(N))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
isNat(xInact(V1, V2)) → U31(isNat(a(V1)), a(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

X(N, s(M)) → U711(isNat(M), M, N)
PLUS(N, s(M)) → U511(isNat(M), M, N)
U711(tt, M, N) → ISNAT(a(N))
U111(tt, V2) → ISNAT(a(V2))
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
U721(tt, M, N) → A(N)
PLUS(N, 0) → ISNAT(N)
ISNAT(sInact(V1)) → ISNAT(a(V1))
U311(tt, V2) → ISNAT(a(V2))
X(N, 0) → U611(isNat(N))
PLUS(N, s(M)) → ISNAT(M)
PLUS(N, 0) → U411(isNat(N), N)
U511(tt, M, N) → U521(isNat(a(N)), a(M), a(N))
U111(tt, V2) → U121(isNat(a(V2)))
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
U611(tt) → 01
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U311(tt, V2) → U321(isNat(a(V2)))
U111(tt, V2) → A(V2)
U521(tt, M, N) → S(plus(a(N), a(M)))
U711(tt, M, N) → A(N)
ISNAT(xInact(V1, V2)) → A(V2)
A(0Inact) → 01
U311(tt, V2) → A(V2)
ISNAT(plusInact(V1, V2)) → A(V2)
U521(tt, M, N) → A(M)
U521(tt, M, N) → A(N)
U711(tt, M, N) → A(M)
A(sInact(x1)) → S(x1)
A(xInact(x1, x2)) → X(x1, x2)
ISNAT(xInact(V1, V2)) → U311(isNat(a(V1)), a(V2))
ISNAT(sInact(V1)) → A(V1)
ISNAT(sInact(V1)) → U211(isNat(a(V1)))
U511(tt, M, N) → A(N)
U511(tt, M, N) → ISNAT(a(N))
X(N, s(M)) → ISNAT(M)
U721(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
U721(tt, M, N) → X(a(N), a(M))
X(N, 0) → ISNAT(N)
U721(tt, M, N) → A(M)
U511(tt, M, N) → A(M)
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U521(tt, M, N) → PLUS(a(N), a(M))
U411(tt, N) → A(N)
U711(tt, M, N) → U721(isNat(a(N)), a(M), a(N))

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(a(V2)))
U32(tt) → tt
U41(tt, N) → a(N)
U51(tt, M, N) → U52(isNat(a(N)), a(M), a(N))
U52(tt, M, N) → s(plus(a(N), a(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(a(N)), a(M), a(N))
U72(tt, M, N) → plus(x(a(N), a(M)), a(N))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
isNat(xInact(V1, V2)) → U31(isNat(a(V1)), a(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 8 less nodes.

↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

X(N, s(M)) → U711(isNat(M), M, N)
U711(tt, M, N) → ISNAT(a(N))
PLUS(N, s(M)) → U511(isNat(M), M, N)
U111(tt, V2) → ISNAT(a(V2))
U721(tt, M, N) → A(N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
U311(tt, V2) → ISNAT(a(V2))
PLUS(N, s(M)) → ISNAT(M)
PLUS(N, 0) → U411(isNat(N), N)
U511(tt, M, N) → U521(isNat(a(N)), a(M), a(N))
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U111(tt, V2) → A(V2)
U711(tt, M, N) → A(N)
ISNAT(xInact(V1, V2)) → A(V2)
U311(tt, V2) → A(V2)
U521(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → A(V2)
U521(tt, M, N) → A(N)
U711(tt, M, N) → A(M)
A(xInact(x1, x2)) → X(x1, x2)
ISNAT(sInact(V1)) → A(V1)
ISNAT(xInact(V1, V2)) → U311(isNat(a(V1)), a(V2))
U511(tt, M, N) → A(N)
U511(tt, M, N) → ISNAT(a(N))
X(N, s(M)) → ISNAT(M)
U721(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
U721(tt, M, N) → X(a(N), a(M))
U721(tt, M, N) → A(M)
X(N, 0) → ISNAT(N)
U511(tt, M, N) → A(M)
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
U521(tt, M, N) → PLUS(a(N), a(M))
U411(tt, N) → A(N)
U711(tt, M, N) → U721(isNat(a(N)), a(M), a(N))

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(a(V2)))
U32(tt) → tt
U41(tt, N) → a(N)
U51(tt, M, N) → U52(isNat(a(N)), a(M), a(N))
U52(tt, M, N) → s(plus(a(N), a(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(a(N)), a(M), a(N))
U72(tt, M, N) → plus(x(a(N), a(M)), a(N))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
isNat(xInact(V1, V2)) → U31(isNat(a(V1)), a(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


X(N, s(M)) → U711(isNat(M), M, N)
U711(tt, M, N) → ISNAT(a(N))
PLUS(N, s(M)) → U511(isNat(M), M, N)
U721(tt, M, N) → A(N)
A(plusInact(x1, x2)) → PLUS(x1, x2)
ISNAT(plusInact(V1, V2)) → A(V1)
ISNAT(sInact(V1)) → ISNAT(a(V1))
PLUS(N, 0) → ISNAT(N)
PLUS(N, s(M)) → ISNAT(M)
PLUS(N, 0) → U411(isNat(N), N)
ISNAT(xInact(V1, V2)) → A(V1)
ISNAT(plusInact(V1, V2)) → ISNAT(a(V1))
ISNAT(plusInact(V1, V2)) → U111(isNat(a(V1)), a(V2))
U711(tt, M, N) → A(N)
ISNAT(xInact(V1, V2)) → A(V2)
U521(tt, M, N) → A(M)
ISNAT(plusInact(V1, V2)) → A(V2)
U521(tt, M, N) → A(N)
U711(tt, M, N) → A(M)
ISNAT(sInact(V1)) → A(V1)
ISNAT(xInact(V1, V2)) → U311(isNat(a(V1)), a(V2))
U511(tt, M, N) → A(N)
U511(tt, M, N) → ISNAT(a(N))
X(N, s(M)) → ISNAT(M)
U721(tt, M, N) → PLUS(x(a(N), a(M)), a(N))
U721(tt, M, N) → X(a(N), a(M))
U721(tt, M, N) → A(M)
X(N, 0) → ISNAT(N)
U511(tt, M, N) → A(M)
ISNAT(xInact(V1, V2)) → ISNAT(a(V1))
The remaining pairs can at least be oriented weakly.

U111(tt, V2) → ISNAT(a(V2))
U311(tt, V2) → ISNAT(a(V2))
U511(tt, M, N) → U521(isNat(a(N)), a(M), a(N))
U111(tt, V2) → A(V2)
U311(tt, V2) → A(V2)
A(xInact(x1, x2)) → X(x1, x2)
U521(tt, M, N) → PLUS(a(N), a(M))
U411(tt, N) → A(N)
U711(tt, M, N) → U721(isNat(a(N)), a(M), a(N))
Used ordering: Combined order from the following AFS and order.
X(x1, x2)  =  X(x1, x2)
s(x1)  =  s(x1)
U711(x1, x2, x3)  =  U711(x1, x2, x3)
isNat(x1)  =  isNat
tt  =  tt
ISNAT(x1)  =  x1
a(x1)  =  x1
PLUS(x1, x2)  =  PLUS(x1, x2)
U511(x1, x2, x3)  =  U511(x2, x3)
U111(x1, x2)  =  x2
U721(x1, x2, x3)  =  U721(x1, x2, x3)
A(x1)  =  x1
plusInact(x1, x2)  =  plusInact(x1, x2)
sInact(x1)  =  sInact(x1)
0  =  0
U311(x1, x2)  =  x2
U411(x1, x2)  =  x2
U521(x1, x2, x3)  =  U521(x2, x3)
xInact(x1, x2)  =  xInact(x1, x2)
x(x1, x2)  =  x(x1, x2)
U12(x1)  =  U12
U31(x1, x2)  =  U31
U51(x1, x2, x3)  =  U51(x1, x2, x3)
U52(x1, x2, x3)  =  U52(x1, x2, x3)
0Inact  =  0Inact
U21(x1)  =  x1
U11(x1, x2)  =  U11
U32(x1)  =  U32
plus(x1, x2)  =  plus(x1, x2)
U71(x1, x2, x3)  =  U71(x1, x2, x3)
U72(x1, x2, x3)  =  U72(x1, x2, x3)
U41(x1, x2)  =  x2
U61(x1)  =  U61

Recursive path order with status [2].
Quasi-Precedence:
[X2, U71^13, U72^13, xInact2, x2, U713, U723] > [isNat, tt, plusInact2, U12, U31, U513, U523, U11, U32, plus2] > [s1, sInact1]
[X2, U71^13, U72^13, xInact2, x2, U713, U723] > [isNat, tt, plusInact2, U12, U31, U513, U523, U11, U32, plus2] > [PLUS2, U51^12, U52^12]
[X2, U71^13, U72^13, xInact2, x2, U713, U723] > [isNat, tt, plusInact2, U12, U31, U513, U523, U11, U32, plus2] > [0, 0Inact, U61]

Status:
U523: [3,2,1]
0: multiset
0Inact: multiset
U11: []
U71^13: [3,2,1]
U31: []
X2: [1,2]
s1: [1]
U52^12: multiset
xInact2: [1,2]
U713: [3,2,1]
isNat: []
U32: []
PLUS2: multiset
x2: [1,2]
U12: []
tt: multiset
U61: multiset
U72^13: [3,2,1]
U723: [3,2,1]
U51^12: multiset
plus2: [1,2]
U513: [3,2,1]
sInact1: [1]
plusInact2: [1,2]


The following usable rules [17] were oriented:

U12(tt) → tt
isNat(xInact(V1, V2)) → U31(isNat(a(V1)), a(V2))
U51(tt, M, N) → U52(isNat(a(N)), a(M), a(N))
isNat(0Inact) → tt
U21(tt) → tt
a(x) → x
0 → 0Inact
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
U31(tt, V2) → U32(isNat(a(V2)))
U32(tt) → tt
plus(x1, x2) → plusInact(x1, x2)
U71(tt, M, N) → U72(isNat(a(N)), a(M), a(N))
U72(tt, M, N) → plus(x(a(N), a(M)), a(N))
a(xInact(x1, x2)) → x(x1, x2)
U41(tt, N) → a(N)
x(N, s(M)) → U71(isNat(M), M, N)
plus(N, 0) → U41(isNat(N), N)
a(plusInact(x1, x2)) → plus(x1, x2)
isNat(sInact(V1)) → U21(isNat(a(V1)))
U11(tt, V2) → U12(isNat(a(V2)))
x(x1, x2) → xInact(x1, x2)
U52(tt, M, N) → s(plus(a(N), a(M)))
s(x1) → sInact(x1)
a(0Inact) → 0
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
a(sInact(x1)) → s(x1)
U61(tt) → 0



↳ CSR
  ↳ Zantema-Transformation
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ QDP
              ↳ QDPOrderProof
                ↳ QDP
                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U311(tt, V2) → A(V2)
U511(tt, M, N) → U521(isNat(a(N)), a(M), a(N))
U521(tt, M, N) → PLUS(a(N), a(M))
U411(tt, N) → A(N)
U111(tt, V2) → ISNAT(a(V2))
A(xInact(x1, x2)) → X(x1, x2)
U711(tt, M, N) → U721(isNat(a(N)), a(M), a(N))
U111(tt, V2) → A(V2)
U311(tt, V2) → ISNAT(a(V2))

The TRS R consists of the following rules:

U11(tt, V2) → U12(isNat(a(V2)))
U12(tt) → tt
U21(tt) → tt
U31(tt, V2) → U32(isNat(a(V2)))
U32(tt) → tt
U41(tt, N) → a(N)
U51(tt, M, N) → U52(isNat(a(N)), a(M), a(N))
U52(tt, M, N) → s(plus(a(N), a(M)))
U61(tt) → 0
U71(tt, M, N) → U72(isNat(a(N)), a(M), a(N))
U72(tt, M, N) → plus(x(a(N), a(M)), a(N))
isNat(0Inact) → tt
isNat(plusInact(V1, V2)) → U11(isNat(a(V1)), a(V2))
isNat(sInact(V1)) → U21(isNat(a(V1)))
isNat(xInact(V1, V2)) → U31(isNat(a(V1)), a(V2))
plus(N, 0) → U41(isNat(N), N)
plus(N, s(M)) → U51(isNat(M), M, N)
x(N, 0) → U61(isNat(N))
x(N, s(M)) → U71(isNat(M), M, N)
a(x) → x
0 → 0Inact
a(0Inact) → 0
x(x1, x2) → xInact(x1, x2)
a(xInact(x1, x2)) → x(x1, x2)
plus(x1, x2) → plusInact(x1, x2)
a(plusInact(x1, x2)) → plus(x1, x2)
s(x1) → sInact(x1)
a(sInact(x1)) → s(x1)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 9 less nodes.