0 CpxTRS
↳1 RcToIrcProof (BOTH BOUNDS(ID, ID), 25 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtUsableRulesProof (⇔, 0 ms)
↳10 CdtProblem
↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CdtProblem
↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CdtProblem
↳15 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 BOUNDS(1, 1)
f(0) → cons(0)
f(s(0)) → f(p(s(0)))
p(s(X)) → X
As the TRS is a non-duplicating overlay system, we have rc = irc.
f(0) → cons(0)
f(s(0)) → f(p(s(0)))
p(s(X)) → X
Tuples:
f(0) → cons(0)
f(s(0)) → f(p(s(0)))
p(s(z0)) → z0
S tuples:
F(0) → c
F(s(0)) → c1(F(p(s(0))), P(s(0)))
P(s(z0)) → c2
K tuples:none
F(0) → c
F(s(0)) → c1(F(p(s(0))), P(s(0)))
P(s(z0)) → c2
f, p
F, P
c, c1, c2
P(s(z0)) → c2
F(0) → c
Tuples:
f(0) → cons(0)
f(s(0)) → f(p(s(0)))
p(s(z0)) → z0
S tuples:
F(s(0)) → c1(F(p(s(0))), P(s(0)))
K tuples:none
F(s(0)) → c1(F(p(s(0))), P(s(0)))
f, p
F
c1
Tuples:
f(0) → cons(0)
f(s(0)) → f(p(s(0)))
p(s(z0)) → z0
S tuples:
F(s(0)) → c1(F(p(s(0))))
K tuples:none
F(s(0)) → c1(F(p(s(0))))
f, p
F
c1
f(0) → cons(0)
f(s(0)) → f(p(s(0)))
Tuples:
p(s(z0)) → z0
S tuples:
F(s(0)) → c1(F(p(s(0))))
K tuples:none
F(s(0)) → c1(F(p(s(0))))
p
F
c1
F(s(0)) → c1(F(0))
Tuples:
p(s(z0)) → z0
S tuples:
F(s(0)) → c1(F(0))
K tuples:none
F(s(0)) → c1(F(0))
p
F
c1
F(s(0)) → c1(F(0))
Tuples:none
p(s(z0)) → z0
p