Termination Proof

by AProVE (version ba869e7b28377cd372aedcb96abeb62c4ad6aaa5 rene 20130719 unpublished dirty )

Input

The rewrite relation of the following TRS is considered.

Tcpd(SRlbeta(x)) SRlbeta(Tcpd(x))
Tcpd(SRlbeta(x)) SRlbeta(TcpT(x))
Tcpd(SRcp(x)) SRcp(Tcpd(x))
Tcpd(SRcp(x)) SRcp(Tcpd(Tcpd(x)))
Tcpd(SRllet(x)) SRllet(Tcpd(x))
Tcpd(SRlapp(x)) SRlapp(Tcpd(x))
Tcpd(Answer) Answer
SRlll(x) SRlapp(x)
SRlll(x) SRllet(x)
TcpT(SRlbeta(x)) SRlbeta(TcpT(x))
TcpT(SRcp(x)) SRcp(TcpT(x))
TcpT(SRcp(x)) x
TcpT(SRllet(x)) SRllet(TcpT(x))
TcpT(SRlapp(x)) SRlapp(TcpT(x))
TcpT(Answer) Answer
The evaluation strategy is innermost.

Proof

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[Tcpd(x1)] = 1 · x1
[SRlbeta(x1)] = 1 · x1
[TcpT(x1)] = 1 · x1
[SRcp(x1)] = 1 · x1 + 1
[SRllet(x1)] = 1 · x1
[SRlapp(x1)] = 1 · x1
[Answer] = 0
[SRlll(x1)] = 1 · x1 + 1
the rules
Tcpd(SRlbeta(x)) SRlbeta(Tcpd(x))
Tcpd(SRlbeta(x)) SRlbeta(TcpT(x))
Tcpd(SRcp(x)) SRcp(Tcpd(x))
Tcpd(SRcp(x)) SRcp(Tcpd(Tcpd(x)))
Tcpd(SRllet(x)) SRllet(Tcpd(x))
Tcpd(SRlapp(x)) SRlapp(Tcpd(x))
Tcpd(Answer) Answer
TcpT(SRlbeta(x)) SRlbeta(TcpT(x))
TcpT(SRcp(x)) SRcp(TcpT(x))
TcpT(SRllet(x)) SRllet(TcpT(x))
TcpT(SRlapp(x)) SRlapp(TcpT(x))
TcpT(Answer) Answer
remain.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
Tcpd#(SRlbeta(x)) Tcpd#(x)
Tcpd#(SRlbeta(x)) TcpT#(x)
Tcpd#(SRcp(x)) Tcpd#(x)
Tcpd#(SRcp(x)) Tcpd#(Tcpd(x))
Tcpd#(SRllet(x)) Tcpd#(x)
Tcpd#(SRlapp(x)) Tcpd#(x)
TcpT#(SRlbeta(x)) TcpT#(x)
TcpT#(SRcp(x)) TcpT#(x)
TcpT#(SRllet(x)) TcpT#(x)
TcpT#(SRlapp(x)) TcpT#(x)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.