0 CpxTRS
↳1 RcToIrcProof (BOTH BOUNDS(ID, ID), 20 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)
first(0, X) → nil
first(s(X), cons(Y)) → cons(Y)
from(X) → cons(X)
As the TRS does not nest defined symbols, we have rc = irc.
first(0, X) → nil
first(s(X), cons(Y)) → cons(Y)
from(X) → cons(X)
Tuples:
first(0, z0) → nil
first(s(z0), cons(z1)) → cons(z1)
from(z0) → cons(z0)
S tuples:
FIRST(0, z0) → c
FIRST(s(z0), cons(z1)) → c1
FROM(z0) → c2
K tuples:none
FIRST(0, z0) → c
FIRST(s(z0), cons(z1)) → c1
FROM(z0) → c2
first, from
FIRST, FROM
c, c1, c2
FIRST(s(z0), cons(z1)) → c1
FROM(z0) → c2
FIRST(0, z0) → c
Tuples:none
first(0, z0) → nil
first(s(z0), cons(z1)) → cons(z1)
from(z0) → cons(z0)
first, from