0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 PisEmptyProof (⇔)
↳23 TRUE
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 QDPOrderProof (⇔)
↳28 QDP
↳29 QDPOrderProof (⇔)
↳30 QDP
↳31 QDPOrderProof (⇔)
↳32 QDP
↳33 QDPOrderProof (⇔)
↳34 QDP
↳35 QDPOrderProof (⇔)
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 DependencyGraphProof (⇔)
↳40 TRUE
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
ACTIVE(and(tt, X)) → MARK(X)
ACTIVE(plus(N, 0)) → MARK(N)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
ACTIVE(plus(N, s(M))) → S(plus(N, M))
ACTIVE(plus(N, s(M))) → PLUS(N, M)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(and(X1, X2)) → AND(mark(X1), X2)
MARK(and(X1, X2)) → MARK(X1)
MARK(tt) → ACTIVE(tt)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(plus(X1, X2)) → PLUS(mark(X1), mark(X2))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(0) → ACTIVE(0)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
AND(mark(X1), X2) → AND(X1, X2)
AND(X1, mark(X2)) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(X1, mark(X2)) → PLUS(X1, X2)
PLUS(active(X1), X2) → PLUS(X1, X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)
S(mark(X)) → S(X)
S(active(X)) → S(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
S(active(X)) → S(X)
S(mark(X)) → S(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(active(X)) → S(X)
S(mark(X)) → S(X)
POL(S(x1)) = x1
POL(active(x1)) = 1 + x1
POL(mark(x1)) = 1 + x1
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
PLUS(X1, mark(X2)) → PLUS(X1, X2)
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(active(X1), X2) → PLUS(X1, X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(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)
PLUS(active(X1), X2) → PLUS(X1, X2)
POL(PLUS(x1, x2)) = x1
POL(active(x1)) = 1 + x1
POL(mark(x1)) = 1 + x1
PLUS(X1, mark(X2)) → PLUS(X1, X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(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)
PLUS(X1, active(X2)) → PLUS(X1, X2)
POL(PLUS(x1, x2)) = x2
POL(active(x1)) = 1 + x1
POL(mark(x1)) = 1 + x1
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
AND(X1, mark(X2)) → AND(X1, X2)
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AND(mark(X1), X2) → AND(X1, X2)
AND(active(X1), X2) → AND(X1, X2)
POL(AND(x1, x2)) = x1
POL(active(x1)) = 1 + x1
POL(mark(x1)) = 1 + x1
AND(X1, mark(X2)) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AND(X1, mark(X2)) → AND(X1, X2)
AND(X1, active(X2)) → AND(X1, X2)
POL(AND(x1, x2)) = x2
POL(active(x1)) = 1 + x1
POL(mark(x1)) = 1 + x1
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
ACTIVE(plus(N, 0)) → MARK(N)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
MARK(s(X)) → MARK(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(s(X)) → ACTIVE(s(mark(X)))
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = 1
POL(active(x1)) = 0
POL(and(x1, x2)) = 1
POL(mark(x1)) = 0
POL(plus(x1, x2)) = 1
POL(s(x1)) = 0
POL(tt) = 0
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
ACTIVE(and(tt, X)) → MARK(X)
MARK(and(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
ACTIVE(plus(N, 0)) → MARK(N)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
MARK(s(X)) → MARK(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(and(tt, X)) → MARK(X)
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = x1
POL(active(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(mark(x1)) = x1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(tt) = 1
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
active(plus(N, 0)) → mark(N)
mark(s(X)) → active(s(mark(X)))
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(tt) → active(tt)
mark(0) → active(0)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
MARK(and(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
ACTIVE(plus(N, 0)) → MARK(N)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
MARK(s(X)) → MARK(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(and(X1, X2)) → ACTIVE(and(mark(X1), X2))
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = 1
POL(active(x1)) = 0
POL(and(x1, x2)) = 0
POL(mark(x1)) = 0
POL(plus(x1, x2)) = 1
POL(s(x1)) = 0
POL(tt) = 0
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
MARK(and(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
ACTIVE(plus(N, 0)) → MARK(N)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
MARK(s(X)) → MARK(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(and(X1, X2)) → MARK(X1)
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = x1
POL(active(x1)) = x1
POL(and(x1, x2)) = 1 + x1 + x2
POL(mark(x1)) = x1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(tt) = 0
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
active(plus(N, 0)) → mark(N)
mark(s(X)) → active(s(mark(X)))
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(tt) → active(tt)
mark(0) → active(0)
plus(X1, mark(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
ACTIVE(plus(N, 0)) → MARK(N)
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
MARK(s(X)) → MARK(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(plus(N, 0)) → MARK(N)
POL(0) = 1
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = x1
POL(active(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(mark(x1)) = x1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(tt) = 0
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
active(plus(N, 0)) → mark(N)
mark(s(X)) → active(s(mark(X)))
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(tt) → active(tt)
mark(0) → active(0)
plus(X1, mark(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
MARK(s(X)) → MARK(X)
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(s(X)) → MARK(X)
POL(0) = 0
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = x1
POL(active(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(mark(x1)) = x1
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
POL(tt) = 0
mark(and(X1, X2)) → active(and(mark(X1), X2))
active(and(tt, X)) → mark(X)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
active(plus(N, 0)) → mark(N)
mark(s(X)) → active(s(mark(X)))
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(tt) → active(tt)
mark(0) → active(0)
plus(X1, mark(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)
and(X1, mark(X2)) → and(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(X1, X2)) → MARK(X2)
POL(0) = 0
POL(ACTIVE(x1)) = 0
POL(MARK(x1)) = x1
POL(active(x1)) = 0
POL(and(x1, x2)) = 0
POL(mark(x1)) = 0
POL(plus(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = 0
POL(tt) = 0
s(active(X)) → s(X)
s(mark(X)) → s(X)
ACTIVE(plus(N, s(M))) → MARK(s(plus(N, M)))
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)