0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 QDPOrderProof (⇔)
↳16 QDP
↳17 PisEmptyProof (⇔)
↳18 TRUE
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 QDPOrderProof (⇔)
↳23 QDP
↳24 PisEmptyProof (⇔)
↳25 TRUE
↳26 QDP
↳27 QDPOrderProof (⇔)
↳28 QDP
↳29 QDPOrderProof (⇔)
↳30 QDP
↳31 QDPOrderProof (⇔)
↳32 QDP
↳33 PisEmptyProof (⇔)
↳34 TRUE
↳35 QDP
↳36 QDPOrderProof (⇔)
↳37 QDP
↳38 QDPOrderProof (⇔)
↳39 QDP
↳40 PisEmptyProof (⇔)
↳41 TRUE
↳42 QDP
↳43 QDPOrderProof (⇔)
↳44 QDP
↳45 QDPOrderProof (⇔)
↳46 QDP
↳47 PisEmptyProof (⇔)
↳48 TRUE
↳49 QDP
↳50 QDPOrderProof (⇔)
↳51 QDP
↳52 QDPOrderProof (⇔)
↳53 QDP
↳54 PisEmptyProof (⇔)
↳55 TRUE
↳56 QDP
↳57 QDPOrderProof (⇔)
↳58 QDP
↳59 QDPOrderProof (⇔)
↳60 QDP
↳61 PisEmptyProof (⇔)
↳62 TRUE
↳63 QDP
↳64 QDPOrderProof (⇔)
↳65 QDP
↳66 PisEmptyProof (⇔)
↳67 TRUE
↳68 QDP
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(U11(tt, M, N)) → U121(tt, M, N)
ACTIVE(U12(tt, M, N)) → S(plus(N, M))
ACTIVE(U12(tt, M, N)) → PLUS(N, M)
ACTIVE(U21(tt, M, N)) → U221(tt, M, N)
ACTIVE(U22(tt, M, N)) → PLUS(x(N, M), N)
ACTIVE(U22(tt, M, N)) → X(N, M)
ACTIVE(plus(N, s(M))) → U111(tt, M, N)
ACTIVE(x(N, s(M))) → U211(tt, M, N)
ACTIVE(U11(X1, X2, X3)) → U111(active(X1), X2, X3)
ACTIVE(U11(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(U12(X1, X2, X3)) → U121(active(X1), X2, X3)
ACTIVE(U12(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(s(X)) → S(active(X))
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(plus(X1, X2)) → PLUS(active(X1), X2)
ACTIVE(plus(X1, X2)) → ACTIVE(X1)
ACTIVE(plus(X1, X2)) → PLUS(X1, active(X2))
ACTIVE(plus(X1, X2)) → ACTIVE(X2)
ACTIVE(U21(X1, X2, X3)) → U211(active(X1), X2, X3)
ACTIVE(U21(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(U22(X1, X2, X3)) → U221(active(X1), X2, X3)
ACTIVE(U22(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(x(X1, X2)) → X(active(X1), X2)
ACTIVE(x(X1, X2)) → ACTIVE(X1)
ACTIVE(x(X1, X2)) → X(X1, active(X2))
ACTIVE(x(X1, X2)) → ACTIVE(X2)
U111(mark(X1), X2, X3) → U111(X1, X2, X3)
U121(mark(X1), X2, X3) → U121(X1, X2, X3)
S(mark(X)) → S(X)
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(X1, mark(X2)) → PLUS(X1, X2)
U211(mark(X1), X2, X3) → U211(X1, X2, X3)
U221(mark(X1), X2, X3) → U221(X1, X2, X3)
X(mark(X1), X2) → X(X1, X2)
X(X1, mark(X2)) → X(X1, X2)
PROPER(U11(X1, X2, X3)) → U111(proper(X1), proper(X2), proper(X3))
PROPER(U11(X1, X2, X3)) → PROPER(X1)
PROPER(U11(X1, X2, X3)) → PROPER(X2)
PROPER(U11(X1, X2, X3)) → PROPER(X3)
PROPER(U12(X1, X2, X3)) → U121(proper(X1), proper(X2), proper(X3))
PROPER(U12(X1, X2, X3)) → PROPER(X1)
PROPER(U12(X1, X2, X3)) → PROPER(X2)
PROPER(U12(X1, X2, X3)) → PROPER(X3)
PROPER(s(X)) → S(proper(X))
PROPER(s(X)) → PROPER(X)
PROPER(plus(X1, X2)) → PLUS(proper(X1), proper(X2))
PROPER(plus(X1, X2)) → PROPER(X1)
PROPER(plus(X1, X2)) → PROPER(X2)
PROPER(U21(X1, X2, X3)) → U211(proper(X1), proper(X2), proper(X3))
PROPER(U21(X1, X2, X3)) → PROPER(X1)
PROPER(U21(X1, X2, X3)) → PROPER(X2)
PROPER(U21(X1, X2, X3)) → PROPER(X3)
PROPER(U22(X1, X2, X3)) → U221(proper(X1), proper(X2), proper(X3))
PROPER(U22(X1, X2, X3)) → PROPER(X1)
PROPER(U22(X1, X2, X3)) → PROPER(X2)
PROPER(U22(X1, X2, X3)) → PROPER(X3)
PROPER(x(X1, X2)) → X(proper(X1), proper(X2))
PROPER(x(X1, X2)) → PROPER(X1)
PROPER(x(X1, X2)) → PROPER(X2)
U111(ok(X1), ok(X2), ok(X3)) → U111(X1, X2, X3)
U121(ok(X1), ok(X2), ok(X3)) → U121(X1, X2, X3)
S(ok(X)) → S(X)
PLUS(ok(X1), ok(X2)) → PLUS(X1, X2)
U211(ok(X1), ok(X2), ok(X3)) → U211(X1, X2, X3)
U221(ok(X1), ok(X2), ok(X3)) → U221(X1, X2, X3)
X(ok(X1), ok(X2)) → X(X1, X2)
TOP(mark(X)) → TOP(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(ok(X)) → TOP(active(X))
TOP(ok(X)) → ACTIVE(X)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
X(X1, mark(X2)) → X(X1, X2)
X(mark(X1), X2) → X(X1, X2)
X(ok(X1), ok(X2)) → X(X1, X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
X(ok(X1), ok(X2)) → X(X1, X2)
top > active1 > tt > ok1 > X2
top > active1 > U121 > ok1 > X2
top > active1 > plus1 > ok1 > X2
top > active1 > U213 > ok1 > X2
top > active1 > U223 > ok1 > X2
top > active1 > x2 > ok1 > X2
top > active1 > x2 > 0 > X2
top > proper1 > tt > ok1 > X2
top > proper1 > U121 > ok1 > X2
top > proper1 > plus1 > ok1 > X2
top > proper1 > U213 > ok1 > X2
top > proper1 > U223 > ok1 > X2
top > proper1 > x2 > ok1 > X2
top > proper1 > x2 > 0 > X2
X2: [1,2]
ok1: [1]
active1: [1]
tt: multiset
U121: [1]
plus1: [1]
U213: [3,2,1]
U223: [3,2,1]
x2: [1,2]
0: multiset
proper1: multiset
top: multiset
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
X(X1, mark(X2)) → X(X1, X2)
X(mark(X1), X2) → X(X1, X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
X(X1, mark(X2)) → X(X1, X2)
X(mark(X1), X2) → X(X1, X2)
X2 > mark1
top > active1 > U113 > tt > s1 > mark1
top > active1 > U113 > tt > plus2 > ok > U123 > mark1
top > active1 > U113 > tt > plus2 > ok > x2 > mark1
top > active1 > U113 > tt > U223 > x2 > mark1
top > active1 > U213 > mark1
top > active1 > 0 > ok > U123 > mark1
top > active1 > 0 > ok > x2 > mark1
X2: [2,1]
mark1: [1]
active1: [1]
U113: [2,3,1]
tt: multiset
U123: [1,3,2]
s1: [1]
plus2: [2,1]
U213: [3,2,1]
U223: [2,1,3]
x2: [1,2]
0: multiset
ok: []
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U221(ok(X1), ok(X2), ok(X3)) → U221(X1, X2, X3)
U221(mark(X1), X2, X3) → U221(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U221(mark(X1), X2, X3) → U221(X1, X2, X3)
active1 > U113 > tt > U123 > mark1 > U22^11
active1 > U113 > tt > s1 > U213 > mark1 > U22^11
active1 > U113 > tt > U223 > x2 > U213 > mark1 > U22^11
active1 > U113 > tt > U223 > x2 > 0 > U22^11
active1 > plus2 > mark1 > U22^11
top > U22^11
U22^11: multiset
mark1: [1]
active1: [1]
U113: [1,3,2]
tt: multiset
U123: multiset
s1: [1]
plus2: [2,1]
U213: [3,2,1]
U223: multiset
x2: [2,1]
0: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U221(ok(X1), ok(X2), ok(X3)) → U221(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U221(ok(X1), ok(X2), ok(X3)) → U221(X1, X2, X3)
proper > ok1 > U22^12 > mark
proper > tt > mark
proper > 0 > mark
top > mark
U22^12: [2,1]
ok1: [1]
tt: multiset
mark: []
0: multiset
proper: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U211(ok(X1), ok(X2), ok(X3)) → U211(X1, X2, X3)
U211(mark(X1), X2, X3) → U211(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U211(mark(X1), X2, X3) → U211(X1, X2, X3)
active1 > U113 > tt > U123 > mark1 > U21^11
active1 > U113 > tt > s1 > U213 > mark1 > U21^11
active1 > U113 > tt > U223 > x2 > U213 > mark1 > U21^11
active1 > U113 > tt > U223 > x2 > 0 > U21^11
active1 > plus2 > mark1 > U21^11
top > U21^11
U21^11: multiset
mark1: [1]
active1: [1]
U113: [1,3,2]
tt: multiset
U123: multiset
s1: [1]
plus2: [2,1]
U213: [3,2,1]
U223: multiset
x2: [2,1]
0: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U211(ok(X1), ok(X2), ok(X3)) → U211(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U211(ok(X1), ok(X2), ok(X3)) → U211(X1, X2, X3)
proper > ok1 > U21^12 > mark
proper > tt > mark
proper > 0 > mark
top > mark
U21^12: [2,1]
ok1: [1]
tt: multiset
mark: []
0: multiset
proper: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PLUS(X1, mark(X2)) → PLUS(X1, X2)
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(ok(X1), ok(X2)) → PLUS(X1, X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(X1, mark(X2)) → PLUS(X1, X2)
top > active1 > U113 > mark1 > PLUS1
top > active1 > tt > x2 > mark1 > PLUS1
top > active1 > tt > x2 > 0
top > active1 > U123 > mark1 > PLUS1
top > active1 > plus2 > mark1 > PLUS1
top > active1 > U213 > mark1 > PLUS1
top > active1 > U223 > x2 > mark1 > PLUS1
top > active1 > U223 > x2 > 0
PLUS1: multiset
mark1: multiset
active1: [1]
U113: [1,3,2]
tt: multiset
U123: multiset
plus2: [2,1]
U213: [1,2,3]
U223: multiset
x2: [1,2]
0: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(ok(X1), ok(X2)) → PLUS(X1, X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(ok(X1), ok(X2)) → PLUS(X1, X2)
proper > ok1 > PLUS2 > 0
proper > tt > 0
top > 0
PLUS2: multiset
ok1: [1]
tt: multiset
0: multiset
proper: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PLUS(mark(X1), X2) → PLUS(X1, X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS1 > mark1
active1 > tt > ok > plus2 > U113 > U123 > mark1
active1 > tt > ok > x2 > U213 > U223 > mark1
active1 > 0 > ok > plus2 > U113 > U123 > mark1
active1 > 0 > ok > x2 > U213 > U223 > mark1
top > proper1 > plus2 > U113 > U123 > mark1
top > proper1 > x2 > U213 > U223 > mark1
PLUS1: multiset
mark1: [1]
active1: [1]
U113: [3,1,2]
tt: multiset
U123: [1,3,2]
plus2: [2,1]
U213: [2,3,1]
U223: [3,2,1]
x2: [2,1]
0: multiset
proper1: multiset
ok: []
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S(ok(X)) → S(X)
S(mark(X)) → S(X)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(ok(X)) → S(X)
S1 > ok1
active1 > tt > ok1
active1 > 0 > ok1
proper > tt > ok1
proper > 0 > ok1
top > ok1
S1: multiset
ok1: multiset
active1: multiset
tt: multiset
0: multiset
proper: multiset
top: multiset
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
S(mark(X)) → S(X)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(mark(X)) → S(X)
active1 > U113 > ok > plus2 > mark1
active1 > U113 > ok > plus2 > tt
active1 > U113 > ok > U213 > tt
active1 > U113 > ok > U213 > U223 > mark1
active1 > U113 > ok > x2 > mark1
active1 > U113 > ok > x2 > tt
active1 > U123 > ok > plus2 > mark1
active1 > U123 > ok > plus2 > tt
active1 > U123 > ok > U213 > tt
active1 > U123 > ok > U213 > U223 > mark1
active1 > U123 > ok > x2 > mark1
active1 > U123 > ok > x2 > tt
active1 > 0 > mark1
proper1 > U113 > ok > plus2 > mark1
proper1 > U113 > ok > plus2 > tt
proper1 > U113 > ok > U213 > tt
proper1 > U113 > ok > U213 > U223 > mark1
proper1 > U113 > ok > x2 > mark1
proper1 > U113 > ok > x2 > tt
proper1 > U123 > ok > plus2 > mark1
proper1 > U123 > ok > plus2 > tt
proper1 > U123 > ok > U213 > tt
proper1 > U123 > ok > U213 > U223 > mark1
proper1 > U123 > ok > x2 > mark1
proper1 > U123 > ok > x2 > tt
proper1 > 0 > mark1
S1: [1]
mark1: multiset
active1: [1]
U113: [1,2,3]
tt: multiset
U123: [2,3,1]
plus2: [2,1]
U213: [1,2,3]
U223: [3,1,2]
x2: [2,1]
0: multiset
proper1: multiset
ok: multiset
top: multiset
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U121(ok(X1), ok(X2), ok(X3)) → U121(X1, X2, X3)
U121(mark(X1), X2, X3) → U121(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U121(mark(X1), X2, X3) → U121(X1, X2, X3)
active1 > U113 > tt > mark1 > U12^11
active1 > U123 > plus2 > tt > mark1 > U12^11
active1 > U213 > tt > mark1 > U12^11
active1 > U223 > plus2 > tt > mark1 > U12^11
active1 > U223 > x2 > tt > mark1 > U12^11
0 > mark1 > U12^11
proper1 > U113 > tt > mark1 > U12^11
proper1 > U123 > plus2 > tt > mark1 > U12^11
proper1 > U213 > tt > mark1 > U12^11
proper1 > U223 > plus2 > tt > mark1 > U12^11
proper1 > U223 > x2 > tt > mark1 > U12^11
top > U12^11
U12^11: multiset
mark1: [1]
active1: [1]
U113: [2,3,1]
tt: multiset
U123: [1,3,2]
plus2: [2,1]
U213: [3,2,1]
U223: [1,3,2]
x2: [2,1]
0: multiset
proper1: [1]
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U121(ok(X1), ok(X2), ok(X3)) → U121(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U121(ok(X1), ok(X2), ok(X3)) → U121(X1, X2, X3)
U12^12 > ok1
active1 > U113 > U123 > mark1 > ok1
active1 > tt > U123 > mark1 > ok1
active1 > tt > s1 > U213 > mark1 > ok1
active1 > tt > U223 > plus2 > mark1 > ok1
active1 > tt > x2 > U213 > mark1 > ok1
active1 > 0 > mark1 > ok1
top > proper1 > U113 > U123 > mark1 > ok1
top > proper1 > s1 > U213 > mark1 > ok1
top > proper1 > U223 > plus2 > mark1 > ok1
top > proper1 > x2 > U213 > mark1 > ok1
U12^12: [2,1]
ok1: multiset
active1: [1]
U113: [1,2,3]
tt: multiset
mark1: multiset
U123: [1,3,2]
s1: [1]
plus2: [2,1]
U213: [1,2,3]
U223: [3,1,2]
x2: [2,1]
0: multiset
proper1: [1]
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U111(ok(X1), ok(X2), ok(X3)) → U111(X1, X2, X3)
U111(mark(X1), X2, X3) → U111(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U111(mark(X1), X2, X3) → U111(X1, X2, X3)
U11^13 > mark1
active1 > tt > U123 > mark1
active1 > tt > plus2 > U113 > mark1
active1 > tt > U223 > mark1
active1 > tt > x2 > U213 > mark1
active1 > tt > x2 > 0 > mark1
active1 > s1 > U113 > mark1
active1 > s1 > U213 > mark1
proper1 > tt > U123 > mark1
proper1 > tt > plus2 > U113 > mark1
proper1 > tt > U223 > mark1
proper1 > tt > x2 > U213 > mark1
proper1 > tt > x2 > 0 > mark1
proper1 > s1 > U113 > mark1
proper1 > s1 > U213 > mark1
top > mark1
U11^13: multiset
mark1: multiset
active1: [1]
U113: [2,1,3]
tt: multiset
U123: [2,3,1]
s1: [1]
plus2: [2,1]
U213: [2,1,3]
U223: [1,3,2]
x2: [1,2]
0: multiset
proper1: [1]
top: multiset
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
U111(ok(X1), ok(X2), ok(X3)) → U111(X1, X2, X3)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U111(ok(X1), ok(X2), ok(X3)) → U111(X1, X2, X3)
active1 > U111 > tt > ok1 > U11^12 > mark
active1 > U121 > plus2 > ok1 > U11^12 > mark
active1 > U211 > tt > ok1 > U11^12 > mark
active1 > x2 > ok1 > U11^12 > mark
active1 > x2 > 0 > mark
top > proper1 > U111 > tt > ok1 > U11^12 > mark
top > proper1 > U121 > plus2 > ok1 > U11^12 > mark
top > proper1 > U211 > tt > ok1 > U11^12 > mark
top > proper1 > x2 > ok1 > U11^12 > mark
top > proper1 > x2 > 0 > mark
U11^12: multiset
ok1: [1]
active1: [1]
U111: multiset
tt: multiset
mark: []
U121: multiset
plus2: [1,2]
U211: [1]
x2: [1,2]
0: multiset
proper1: [1]
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(U11(X1, X2, X3)) → PROPER(X2)
PROPER(U11(X1, X2, X3)) → PROPER(X1)
PROPER(U11(X1, X2, X3)) → PROPER(X3)
PROPER(U12(X1, X2, X3)) → PROPER(X1)
PROPER(U12(X1, X2, X3)) → PROPER(X2)
PROPER(U12(X1, X2, X3)) → PROPER(X3)
PROPER(s(X)) → PROPER(X)
PROPER(plus(X1, X2)) → PROPER(X1)
PROPER(plus(X1, X2)) → PROPER(X2)
PROPER(U21(X1, X2, X3)) → PROPER(X1)
PROPER(U21(X1, X2, X3)) → PROPER(X2)
PROPER(U21(X1, X2, X3)) → PROPER(X3)
PROPER(U22(X1, X2, X3)) → PROPER(X1)
PROPER(U22(X1, X2, X3)) → PROPER(X2)
PROPER(U22(X1, X2, X3)) → PROPER(X3)
PROPER(x(X1, X2)) → PROPER(X1)
PROPER(x(X1, X2)) → PROPER(X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(U11(X1, X2, X3)) → PROPER(X2)
PROPER(U11(X1, X2, X3)) → PROPER(X1)
PROPER(U11(X1, X2, X3)) → PROPER(X3)
PROPER(U12(X1, X2, X3)) → PROPER(X1)
PROPER(U12(X1, X2, X3)) → PROPER(X2)
PROPER(U12(X1, X2, X3)) → PROPER(X3)
PROPER(plus(X1, X2)) → PROPER(X1)
PROPER(plus(X1, X2)) → PROPER(X2)
PROPER(U21(X1, X2, X3)) → PROPER(X1)
PROPER(U21(X1, X2, X3)) → PROPER(X2)
PROPER(U21(X1, X2, X3)) → PROPER(X3)
PROPER(U22(X1, X2, X3)) → PROPER(X1)
PROPER(U22(X1, X2, X3)) → PROPER(X2)
PROPER(U22(X1, X2, X3)) → PROPER(X3)
PROPER(x(X1, X2)) → PROPER(X1)
PROPER(x(X1, X2)) → PROPER(X2)
PROPER1 > mark
active1 > U113 > mark
active1 > U123 > plus2 > mark
active1 > U223 > plus2 > mark
active1 > U223 > x2 > U213 > mark
active1 > U223 > x2 > 0 > mark
tt > U123 > plus2 > mark
tt > U223 > plus2 > mark
tt > U223 > x2 > U213 > mark
tt > U223 > x2 > 0 > mark
proper1 > U113 > mark
proper1 > U123 > plus2 > mark
proper1 > U223 > plus2 > mark
proper1 > U223 > x2 > U213 > mark
proper1 > U223 > x2 > 0 > mark
top > mark
PROPER1: [1]
U113: [2,3,1]
U123: [1,3,2]
plus2: [2,1]
U213: multiset
U223: [3,1,2]
x2: [1,2]
active1: multiset
tt: multiset
mark: multiset
0: multiset
proper1: [1]
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
PROPER(s(X)) → PROPER(X)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PROPER(s(X)) → PROPER(X)
top > active1 > U122 > s1
top > active1 > U223 > plus1
top > active1 > x2 > U213 > tt > s1
top > active1 > x2 > 0
s1: [1]
active1: multiset
tt: multiset
U122: [2,1]
plus1: [1]
U213: [2,1,3]
U223: [2,3,1]
x2: [1,2]
0: multiset
top: multiset
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
ACTIVE(U12(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(U11(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(plus(X1, X2)) → ACTIVE(X1)
ACTIVE(plus(X1, X2)) → ACTIVE(X2)
ACTIVE(U21(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(U22(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(x(X1, X2)) → ACTIVE(X1)
ACTIVE(x(X1, X2)) → ACTIVE(X2)
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(U12(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(U11(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(s(X)) → ACTIVE(X)
ACTIVE(plus(X1, X2)) → ACTIVE(X1)
ACTIVE(plus(X1, X2)) → ACTIVE(X2)
ACTIVE(U21(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(U22(X1, X2, X3)) → ACTIVE(X1)
ACTIVE(x(X1, X2)) → ACTIVE(X1)
ACTIVE(x(X1, X2)) → ACTIVE(X2)
ACTIVE1 > top
U123 > mark > top
s1 > U113 > top
s1 > tt > U222 > top
s1 > tt > mark > top
plus2 > U113 > top
plus2 > tt > U222 > top
plus2 > tt > mark > top
x2 > U212 > tt > U222 > top
x2 > U212 > tt > mark > top
x2 > 0 > top
ACTIVE1: [1]
U123: [3,1,2]
U113: [2,1,3]
s1: [1]
plus2: [1,2]
U212: [2,1]
U222: [2,1]
x2: [1,2]
tt: multiset
mark: multiset
0: multiset
top: []
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
TOP(ok(X)) → TOP(active(X))
TOP(mark(X)) → TOP(proper(X))
active(U11(tt, M, N)) → mark(U12(tt, M, N))
active(U12(tt, M, N)) → mark(s(plus(N, M)))
active(U21(tt, M, N)) → mark(U22(tt, M, N))
active(U22(tt, M, N)) → mark(plus(x(N, M), N))
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(U11(tt, M, N))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(U21(tt, M, N))
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3)
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3)
active(s(X)) → s(active(X))
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(U21(X1, X2, X3)) → U21(active(X1), X2, X3)
active(U22(X1, X2, X3)) → U22(active(X1), X2, X3)
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3))
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3))
s(mark(X)) → mark(s(X))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
U21(mark(X1), X2, X3) → mark(U21(X1, X2, X3))
U22(mark(X1), X2, X3) → mark(U22(X1, X2, X3))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3))
proper(tt) → ok(tt)
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3))
proper(s(X)) → s(proper(X))
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(U21(X1, X2, X3)) → U21(proper(X1), proper(X2), proper(X3))
proper(U22(X1, X2, X3)) → U22(proper(X1), proper(X2), proper(X3))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
proper(0) → ok(0)
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3))
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3))
s(ok(X)) → ok(s(X))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
U21(ok(X1), ok(X2), ok(X3)) → ok(U21(X1, X2, X3))
U22(ok(X1), ok(X2), ok(X3)) → ok(U22(X1, X2, X3))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))