0 CpxTRS
↳1 RcToIrcProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 BOUNDS(1, 1)
app(nil, YS) → YS
app(cons(X), YS) → cons(X)
from(X) → cons(X)
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X), cons(Y)) → cons(app(Y, cons(X)))
prefix(L) → cons(nil)
As the TRS does not nest defined symbols, we have rc = irc.
app(nil, YS) → YS
app(cons(X), YS) → cons(X)
from(X) → cons(X)
zWadr(nil, YS) → nil
zWadr(XS, nil) → nil
zWadr(cons(X), cons(Y)) → cons(app(Y, cons(X)))
prefix(L) → cons(nil)
Tuples:
app(nil, z0) → z0
app(cons(z0), z1) → cons(z0)
from(z0) → cons(z0)
zWadr(nil, z0) → nil
zWadr(z0, nil) → nil
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0)))
prefix(z0) → cons(nil)
S tuples:
APP(nil, z0) → c
APP(cons(z0), z1) → c1
FROM(z0) → c2
ZWADR(nil, z0) → c3
ZWADR(z0, nil) → c4
ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))
PREFIX(z0) → c6
K tuples:none
APP(nil, z0) → c
APP(cons(z0), z1) → c1
FROM(z0) → c2
ZWADR(nil, z0) → c3
ZWADR(z0, nil) → c4
ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))
PREFIX(z0) → c6
app, from, zWadr, prefix
APP, FROM, ZWADR, PREFIX
c, c1, c2, c3, c4, c5, c6
FROM(z0) → c2
PREFIX(z0) → c6
ZWADR(nil, z0) → c3
APP(nil, z0) → c
ZWADR(cons(z0), cons(z1)) → c5(APP(z1, cons(z0)))
APP(cons(z0), z1) → c1
ZWADR(z0, nil) → c4
Tuples:none
app(nil, z0) → z0
app(cons(z0), z1) → cons(z0)
from(z0) → cons(z0)
zWadr(nil, z0) → nil
zWadr(z0, nil) → nil
zWadr(cons(z0), cons(z1)) → cons(app(z1, cons(z0)))
prefix(z0) → cons(nil)
app, from, zWadr, prefix