Termination Proof

by AProVE (version ba869e7b28377cd372aedcb96abeb62c4ad6aaa5 rene 20130719 unpublished dirty )

Input

The rewrite relation of the following TRS is considered.

Tcpx(SRlbeta(x)) → SRlbeta(Tcpx(x))
Tcpx(SRcp(x)) → SRcp(Tcpx(x))
Tcpx(SRcp(x)) → SRcp(x)
Tcpx(SRlll(x)) → SRlll(Tcpx(x))
Tcpx(Answer) → Answer
Tcpx(SRcp(x)) → SRcp(Tcpx(Tcpx(x)))
The evaluation strategy is innermost.

Proof

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
Tcpx#(SRlbeta(x)) → Tcpx#(x)
Tcpx#(SRcp(x)) → Tcpx#(x)
Tcpx#(SRlll(x)) → Tcpx#(x)
Tcpx#(SRcp(x)) → Tcpx#(Tcpx(x))

1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[Tcpx#(x1)] = 1 · x1
[SRlbeta(x1)] = 1 + 1 · x1
[SRcp(x1)] = 1 + 1 · x1
[SRlll(x1)] = 1 + 1 · x1
[Tcpx(x1)] = 1 · x1
[Answer] = 1
all pairs could be removed.

1.1.1 P is empty

There are no pairs anymore.