0 QTRS
↳1 QTRSToCSRProof (⇔)
↳2 CSR
↳3 CSRInnermostProof (⇔)
↳4 CSR
↳5 CSDependencyPairsProof (⇔)
↳6 QCSDP
↳7 QCSDependencyGraphProof (⇔)
↳8 AND
↳9 QCSDP
↳10 QCSDPSubtermProof (⇔)
↳11 QCSDP
↳12 PIsEmptyProof (⇔)
↳13 TRUE
↳14 QCSDP
↳15 QCSDPSubtermProof (⇔)
↳16 QCSDP
↳17 PIsEmptyProof (⇔)
↳18 TRUE
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(plus(x(N, M), N))
active(and(X1, X2)) → and(active(X1), X2)
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(s(X)) → s(active(X))
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
s(mark(X)) → mark(s(X))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
s(ok(X)) → ok(s(X))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(and(tt, X)) → mark(X)
active(plus(N, 0)) → mark(N)
active(plus(N, s(M))) → mark(s(plus(N, M)))
active(x(N, 0)) → mark(0)
active(x(N, s(M))) → mark(plus(x(N, M), N))
active(and(X1, X2)) → and(active(X1), X2)
active(plus(X1, X2)) → plus(active(X1), X2)
active(plus(X1, X2)) → plus(X1, active(X2))
active(s(X)) → s(active(X))
active(x(X1, X2)) → x(active(X1), X2)
active(x(X1, X2)) → x(X1, active(X2))
and(mark(X1), X2) → mark(and(X1, X2))
plus(mark(X1), X2) → mark(plus(X1, X2))
plus(X1, mark(X2)) → mark(plus(X1, X2))
s(mark(X)) → mark(s(X))
x(mark(X1), X2) → mark(x(X1, X2))
x(X1, mark(X2)) → mark(x(X1, X2))
proper(and(X1, X2)) → and(proper(X1), proper(X2))
proper(tt) → ok(tt)
proper(plus(X1, X2)) → plus(proper(X1), proper(X2))
proper(0) → ok(0)
proper(s(X)) → s(proper(X))
proper(x(X1, X2)) → x(proper(X1), proper(X2))
and(ok(X1), ok(X2)) → ok(and(X1, X2))
plus(ok(X1), ok(X2)) → ok(plus(X1, X2))
s(ok(X)) → ok(s(X))
x(ok(X1), ok(X2)) → ok(x(X1, X2))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
and: {1}
tt: empty set
plus: {1, 2}
0: empty set
s: {1}
x: {1, 2}
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and: {1}
tt: empty set
plus: {1, 2}
0: empty set
s: {1}
x: {1, 2}
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and: {1}
tt: empty set
plus: {1, 2}
0: empty set
s: {1}
x: {1, 2}
Innermost Strategy.
PLUS(N, s(M)) → PLUS(N, M)
X(N, s(M)) → PLUS(x(N, M), N)
X(N, s(M)) → X(N, M)
AND(tt, X) → X
AND(tt, X) → U(X)
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))
x(x0, 0)
x(x0, s(x1))
PLUS(N, s(M)) → PLUS(N, M)
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))
x(x0, 0)
x(x0, s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(N, s(M)) → PLUS(N, M)
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))
x(x0, 0)
x(x0, s(x1))
X(N, s(M)) → X(N, M)
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))
x(x0, 0)
x(x0, s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
X(N, s(M)) → X(N, M)
and(tt, X) → X
plus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))
x(N, 0) → 0
x(N, s(M)) → plus(x(N, M), N)
and(tt, x0)
plus(x0, 0)
plus(x0, s(x1))
x(x0, 0)
x(x0, s(x1))