YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QDPSizeChangeProof (⇔, 0 ms)
↳9 YES
↳10 QDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
↳15 QDP
↳16 UsableRulesProof (⇔, 0 ms)
↳17 QDP
↳18 QDPSizeChangeProof (⇔, 0 ms)
↳19 YES
↳20 QDP
↳21 UsableRulesReductionPairsProof (⇔, 0 ms)
↳22 QDP
↳23 TransformationProof (⇔, 0 ms)
↳24 QDP
↳25 DependencyGraphProof (⇔, 0 ms)
↳26 QDP
↳27 TransformationProof (⇔, 0 ms)
↳28 QDP
↳29 DependencyGraphProof (⇔, 0 ms)
↳30 QDP
↳31 SemLabProof (⇒, 9249 ms)
↳32 QDP
↳33 DependencyGraphProof (⇔, 0 ms)
↳34 QDP
↳35 QDPOrderProof (⇔, 0 ms)
↳36 QDP
↳37 QDPOrderProof (⇔, 15 ms)
↳38 QDP
↳39 QDPOrderProof (⇔, 0 ms)
↳40 QDP
↳41 QDPOrderProof (⇔, 0 ms)
↳42 QDP
↳43 QDPOrderProof (⇔, 4 ms)
↳44 QDP
↳45 QDPOrderProof (⇔, 0 ms)
↳46 QDP
↳47 QDPOrderProof (⇔, 17 ms)
↳48 QDP
↳49 QDPOrderProof (⇔, 0 ms)
↳50 QDP
↳51 PisEmptyProof (⇔, 0 ms)
↳52 YES
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
ACTIVE(f(b, c, x)) → F(x, x, x)
ACTIVE(f(x, y, z)) → F(x, y, active(z))
ACTIVE(f(x, y, z)) → ACTIVE(z)
F(x, y, mark(z)) → F(x, y, z)
PROPER(f(x, y, z)) → F(proper(x), proper(y), proper(z))
PROPER(f(x, y, z)) → PROPER(x)
PROPER(f(x, y, z)) → PROPER(y)
PROPER(f(x, y, z)) → PROPER(z)
F(ok(x), ok(y), ok(z)) → F(x, y, z)
TOP(mark(x)) → TOP(proper(x))
TOP(mark(x)) → PROPER(x)
TOP(ok(x)) → TOP(active(x))
TOP(ok(x)) → ACTIVE(x)
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
F(ok(x), ok(y), ok(z)) → F(x, y, z)
F(x, y, mark(z)) → F(x, y, z)
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
F(ok(x), ok(y), ok(z)) → F(x, y, z)
F(x, y, mark(z)) → F(x, y, z)
From the DPs we obtained the following set of size-change graphs:
PROPER(f(x, y, z)) → PROPER(y)
PROPER(f(x, y, z)) → PROPER(x)
PROPER(f(x, y, z)) → PROPER(z)
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
PROPER(f(x, y, z)) → PROPER(y)
PROPER(f(x, y, z)) → PROPER(x)
PROPER(f(x, y, z)) → PROPER(z)
From the DPs we obtained the following set of size-change graphs:
ACTIVE(f(x, y, z)) → ACTIVE(z)
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
ACTIVE(f(x, y, z)) → ACTIVE(z)
From the DPs we obtained the following set of size-change graphs:
TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
f(x, y, mark(z)) → mark(f(x, y, z))
active(d) → mark(c)
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
Used ordering: POLO with Polynomial interpretation [POLO]:
top(mark(x)) → top(proper(x))
top(ok(x)) → top(active(x))
POL(TOP(x1)) = x1
POL(active(x1)) = 2·x1
POL(b) = 0
POL(c) = 0
POL(d) = 0
POL(f(x1, x2, x3)) = x1 + x2 + 2·x3
POL(m(x1)) = 2·x1
POL(mark(x1)) = x1
POL(ok(x1)) = 2·x1
POL(proper(x1)) = x1
TOP(ok(x)) → TOP(active(x))
TOP(mark(x)) → TOP(proper(x))
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(x, y, mark(z)) → mark(f(x, y, z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
active(d) → mark(c)
TOP(ok(f(b, c, x0))) → TOP(mark(f(x0, x0, x0))) → TOP(ok(f(b, c, x0))) → TOP(mark(f(x0, x0, x0)))
TOP(ok(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2))) → TOP(ok(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2)))
TOP(ok(d)) → TOP(m(b)) → TOP(ok(d)) → TOP(m(b))
TOP(ok(d)) → TOP(mark(c)) → TOP(ok(d)) → TOP(mark(c))
TOP(mark(x)) → TOP(proper(x))
TOP(ok(f(b, c, x0))) → TOP(mark(f(x0, x0, x0)))
TOP(ok(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2)))
TOP(ok(d)) → TOP(m(b))
TOP(ok(d)) → TOP(mark(c))
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(x, y, mark(z)) → mark(f(x, y, z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
active(d) → mark(c)
TOP(mark(x)) → TOP(proper(x))
TOP(ok(f(b, c, x0))) → TOP(mark(f(x0, x0, x0)))
TOP(ok(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2)))
TOP(ok(d)) → TOP(mark(c))
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(x, y, mark(z)) → mark(f(x, y, z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
active(d) → mark(c)
TOP(mark(b)) → TOP(ok(b)) → TOP(mark(b)) → TOP(ok(b))
TOP(mark(c)) → TOP(ok(c)) → TOP(mark(c)) → TOP(ok(c))
TOP(mark(d)) → TOP(ok(d)) → TOP(mark(d)) → TOP(ok(d))
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2))) → TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))
TOP(ok(f(b, c, x0))) → TOP(mark(f(x0, x0, x0)))
TOP(ok(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2)))
TOP(ok(d)) → TOP(mark(c))
TOP(mark(b)) → TOP(ok(b))
TOP(mark(c)) → TOP(ok(c))
TOP(mark(d)) → TOP(ok(d))
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(x, y, mark(z)) → mark(f(x, y, z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
active(d) → mark(c)
TOP(mark(f(x0, x1, x2))) → TOP(f(proper(x0), proper(x1), proper(x2)))
TOP(ok(f(b, c, x0))) → TOP(mark(f(x0, x0, x0)))
TOP(ok(f(x0, x1, x2))) → TOP(f(x0, x1, active(x2)))
proper(b) → ok(b)
proper(c) → ok(c)
proper(d) → ok(d)
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z))
f(x, y, mark(z)) → mark(f(x, y, z))
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z))
active(f(b, c, x)) → mark(f(x, x, x))
active(f(x, y, z)) → f(x, y, active(z))
active(d) → m(b)
active(d) → mark(c)
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.1-0-0(b., c., x0))) → TOP.0(mark.0(f.0-0-0(x0, x0, x0)))
TOP.0(ok.0(f.1-0-1(b., c., x0))) → TOP.0(mark.0(f.1-1-1(x0, x0, x0)))
TOP.0(mark.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-1(proper.0(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.1-1-1(x0, x1, x2))) → TOP.0(f.1-1-1(proper.1(x0), proper.1(x1), proper.1(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.1(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.1(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.1(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-1(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.1(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
TOP.0(ok.0(f.1-0-0(b., c., x0))) → TOP.0(mark.0(f.0-0-0(x0, x0, x0)))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.1-0-1(b., c., x0))) → TOP.0(mark.0(f.1-1-1(x0, x0, x0)))
TOP.0(mark.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-1(proper.0(x0), proper.0(x1), proper.1(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.1-1-1(x0, x1, x2))) → TOP.0(f.1-1-1(proper.1(x0), proper.1(x1), proper.1(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(mark.0(f.1-1-1(x0, x1, x2))) → TOP.0(f.1-1-1(proper.1(x0), proper.1(x1), proper.1(x2)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = x1
POL(active.1(x1)) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 1
POL(f.0-0-0(x1, x2, x3)) = 1
POL(f.0-0-1(x1, x2, x3)) = 1
POL(f.0-1-0(x1, x2, x3)) = 1
POL(f.0-1-1(x1, x2, x3)) = 1
POL(f.1-0-0(x1, x2, x3)) = 1
POL(f.1-0-1(x1, x2, x3)) = 1 + x3
POL(f.1-1-0(x1, x2, x3)) = x1 + x3
POL(f.1-1-1(x1, x2, x3)) = x1
POL(m.1(x1)) = 0
POL(mark.0(x1)) = 1
POL(mark.1(x1)) = 1 + x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = 1
POL(proper.1(x1)) = 0
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
proper.1(b.) → ok.1(b.)
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
TOP.0(ok.0(f.1-0-0(b., c., x0))) → TOP.0(mark.0(f.0-0-0(x0, x0, x0)))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.1-0-1(b., c., x0))) → TOP.0(mark.0(f.1-1-1(x0, x0, x0)))
TOP.0(mark.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-1(proper.0(x0), proper.0(x1), proper.1(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(ok.0(f.1-0-0(b., c., x0))) → TOP.0(mark.0(f.0-0-0(x0, x0, x0)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = 1
POL(active.1(x1)) = 0
POL(b.) = 1
POL(c.) = 1
POL(d.) = 0
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = 0
POL(f.0-1-0(x1, x2, x3)) = 0
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = x1
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = 0
POL(f.1-1-1(x1, x2, x3)) = 0
POL(m.1(x1)) = 0
POL(mark.0(x1)) = x1
POL(mark.1(x1)) = x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = 0
POL(proper.1(x1)) = x1
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
proper.1(b.) → ok.1(b.)
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.1-0-1(b., c., x0))) → TOP.0(mark.0(f.1-1-1(x0, x0, x0)))
TOP.0(mark.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-1(proper.0(x0), proper.0(x1), proper.1(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(ok.0(f.1-0-1(b., c., x0))) → TOP.0(mark.0(f.1-1-1(x0, x0, x0)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = 0
POL(active.1(x1)) = 0
POL(b.) = 1
POL(c.) = 0
POL(d.) = 0
POL(f.0-0-0(x1, x2, x3)) = 0
POL(f.0-0-1(x1, x2, x3)) = 0
POL(f.0-1-0(x1, x2, x3)) = 1
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = 1 + x1
POL(f.1-0-1(x1, x2, x3)) = 1 + x1
POL(f.1-1-0(x1, x2, x3)) = 1
POL(f.1-1-1(x1, x2, x3)) = 1
POL(m.1(x1)) = 0
POL(mark.0(x1)) = x1
POL(mark.1(x1)) = x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = 0
POL(proper.1(x1)) = x1
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
proper.1(b.) → ok.1(b.)
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-1(proper.0(x0), proper.0(x1), proper.1(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(mark.0(f.0-0-1(x0, x1, x2))) → TOP.0(f.0-0-1(proper.0(x0), proper.0(x1), proper.1(x2)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = 0
POL(active.1(x1)) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 0
POL(f.0-0-0(x1, x2, x3)) = 1
POL(f.0-0-1(x1, x2, x3)) = x3
POL(f.0-1-0(x1, x2, x3)) = 1
POL(f.0-1-1(x1, x2, x3)) = 1
POL(f.1-0-0(x1, x2, x3)) = 1
POL(f.1-0-1(x1, x2, x3)) = 1
POL(f.1-1-0(x1, x2, x3)) = 1
POL(f.1-1-1(x1, x2, x3)) = 1
POL(m.1(x1)) = 0
POL(mark.0(x1)) = 1
POL(mark.1(x1)) = x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = 0
POL(proper.1(x1)) = 0
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
proper.1(b.) → ok.1(b.)
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(mark.0(f.0-1-1(x0, x1, x2))) → TOP.0(f.0-1-1(proper.0(x0), proper.1(x1), proper.1(x2)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = 0
POL(active.1(x1)) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 0
POL(f.0-0-0(x1, x2, x3)) = 1
POL(f.0-0-1(x1, x2, x3)) = 1
POL(f.0-1-0(x1, x2, x3)) = 1
POL(f.0-1-1(x1, x2, x3)) = x2 + x3
POL(f.1-0-0(x1, x2, x3)) = 1
POL(f.1-0-1(x1, x2, x3)) = 1 + x1
POL(f.1-1-0(x1, x2, x3)) = 1
POL(f.1-1-1(x1, x2, x3)) = 1
POL(m.1(x1)) = 0
POL(mark.0(x1)) = 1
POL(mark.1(x1)) = x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = 0
POL(proper.1(x1)) = 0
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
proper.1(b.) → ok.1(b.)
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(mark.0(f.1-0-1(x0, x1, x2))) → TOP.0(f.1-0-1(proper.1(x0), proper.0(x1), proper.1(x2)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = 0
POL(active.1(x1)) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 0
POL(f.0-0-0(x1, x2, x3)) = 1
POL(f.0-0-1(x1, x2, x3)) = 0
POL(f.0-1-0(x1, x2, x3)) = 1
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = 1
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = 1 + x1
POL(f.1-1-1(x1, x2, x3)) = 0
POL(m.1(x1)) = 0
POL(mark.0(x1)) = 1
POL(mark.1(x1)) = x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = 0
POL(proper.1(x1)) = 0
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
proper.1(b.) → ok.1(b.)
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(mark.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(proper.0(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(proper.0(x0), proper.1(x1), proper.0(x2)))
TOP.0(mark.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(proper.1(x0), proper.0(x1), proper.0(x2)))
TOP.0(mark.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(proper.1(x0), proper.1(x1), proper.0(x2)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = x1
POL(active.1(x1)) = 0
POL(b.) = 1
POL(c.) = 0
POL(d.) = 1
POL(f.0-0-0(x1, x2, x3)) = 1 + x3
POL(f.0-0-1(x1, x2, x3)) = 1
POL(f.0-1-0(x1, x2, x3)) = 1 + x1 + x2 + x3
POL(f.0-1-1(x1, x2, x3)) = 1 + x1 + x2
POL(f.1-0-0(x1, x2, x3)) = 1 + x1 + x3
POL(f.1-0-1(x1, x2, x3)) = 1 + x1
POL(f.1-1-0(x1, x2, x3)) = 1 + x3
POL(f.1-1-1(x1, x2, x3)) = 1
POL(m.1(x1)) = 0
POL(mark.0(x1)) = 1 + x1
POL(mark.1(x1)) = 1 + x1
POL(ok.0(x1)) = x1
POL(ok.1(x1)) = x1
POL(proper.0(x1)) = x1
POL(proper.1(x1)) = x1
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
proper.1(b.) → ok.1(b.)
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TOP.0(ok.0(f.0-0-0(x0, x1, x2))) → TOP.0(f.0-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.0-1-0(x0, x1, x2))) → TOP.0(f.0-1-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-0-0(x0, x1, x2))) → TOP.0(f.1-0-0(x0, x1, active.0(x2)))
TOP.0(ok.0(f.1-1-0(x0, x1, x2))) → TOP.0(f.1-1-0(x0, x1, active.0(x2)))
POL(TOP.0(x1)) = x1
POL(active.0(x1)) = 0
POL(active.1(x1)) = 0
POL(b.) = 0
POL(c.) = 0
POL(d.) = 1
POL(f.0-0-0(x1, x2, x3)) = x1
POL(f.0-0-1(x1, x2, x3)) = 0
POL(f.0-1-0(x1, x2, x3)) = x1
POL(f.0-1-1(x1, x2, x3)) = 0
POL(f.1-0-0(x1, x2, x3)) = x1
POL(f.1-0-1(x1, x2, x3)) = 0
POL(f.1-1-0(x1, x2, x3)) = x1
POL(f.1-1-1(x1, x2, x3)) = 0
POL(m.1(x1)) = 0
POL(mark.0(x1)) = 0
POL(mark.1(x1)) = x1
POL(ok.0(x1)) = 1 + x1
POL(ok.1(x1)) = 1 + x1
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
proper.1(b.) → ok.1(b.)
proper.0(c.) → ok.0(c.)
proper.0(d.) → ok.0(d.)
proper.0(f.0-0-0(x, y, z)) → f.0-0-0(proper.0(x), proper.0(y), proper.0(z))
proper.0(f.0-0-1(x, y, z)) → f.0-0-1(proper.0(x), proper.0(y), proper.1(z))
proper.0(f.0-1-0(x, y, z)) → f.0-1-0(proper.0(x), proper.1(y), proper.0(z))
proper.0(f.0-1-1(x, y, z)) → f.0-1-1(proper.0(x), proper.1(y), proper.1(z))
proper.0(f.1-0-0(x, y, z)) → f.1-0-0(proper.1(x), proper.0(y), proper.0(z))
proper.0(f.1-0-1(x, y, z)) → f.1-0-1(proper.1(x), proper.0(y), proper.1(z))
proper.0(f.1-1-0(x, y, z)) → f.1-1-0(proper.1(x), proper.1(y), proper.0(z))
proper.0(f.1-1-1(x, y, z)) → f.1-1-1(proper.1(x), proper.1(y), proper.1(z))
f.0-0-0(x, y, mark.0(z)) → mark.0(f.0-0-0(x, y, z))
f.0-0-0(x, y, mark.1(z)) → mark.0(f.0-0-1(x, y, z))
f.0-1-0(x, y, mark.0(z)) → mark.0(f.0-1-0(x, y, z))
f.0-1-0(x, y, mark.1(z)) → mark.0(f.0-1-1(x, y, z))
f.1-0-0(x, y, mark.0(z)) → mark.0(f.1-0-0(x, y, z))
f.1-0-0(x, y, mark.1(z)) → mark.0(f.1-0-1(x, y, z))
f.1-1-0(x, y, mark.0(z)) → mark.0(f.1-1-0(x, y, z))
f.1-1-0(x, y, mark.1(z)) → mark.0(f.1-1-1(x, y, z))
f.0-0-0(ok.0(x), ok.0(y), ok.0(z)) → ok.0(f.0-0-0(x, y, z))
f.0-0-1(ok.0(x), ok.0(y), ok.1(z)) → ok.0(f.0-0-1(x, y, z))
f.0-1-0(ok.0(x), ok.1(y), ok.0(z)) → ok.0(f.0-1-0(x, y, z))
f.0-1-1(ok.0(x), ok.1(y), ok.1(z)) → ok.0(f.0-1-1(x, y, z))
f.1-0-0(ok.1(x), ok.0(y), ok.0(z)) → ok.0(f.1-0-0(x, y, z))
f.1-0-1(ok.1(x), ok.0(y), ok.1(z)) → ok.0(f.1-0-1(x, y, z))
f.1-1-0(ok.1(x), ok.1(y), ok.0(z)) → ok.0(f.1-1-0(x, y, z))
f.1-1-1(ok.1(x), ok.1(y), ok.1(z)) → ok.0(f.1-1-1(x, y, z))
active.0(f.1-0-0(b., c., x)) → mark.0(f.0-0-0(x, x, x))
active.0(f.1-0-1(b., c., x)) → mark.0(f.1-1-1(x, x, x))
active.0(f.0-0-0(x, y, z)) → f.0-0-0(x, y, active.0(z))
active.0(f.0-0-1(x, y, z)) → f.0-0-0(x, y, active.1(z))
active.0(f.0-1-0(x, y, z)) → f.0-1-0(x, y, active.0(z))
active.0(f.0-1-1(x, y, z)) → f.0-1-0(x, y, active.1(z))
active.0(f.1-0-0(x, y, z)) → f.1-0-0(x, y, active.0(z))
active.0(f.1-0-1(x, y, z)) → f.1-0-0(x, y, active.1(z))
active.0(f.1-1-0(x, y, z)) → f.1-1-0(x, y, active.0(z))
active.0(f.1-1-1(x, y, z)) → f.1-1-0(x, y, active.1(z))
active.0(d.) → m.1(b.)
active.0(d.) → mark.0(c.)