Termination Proof

by AProVE (version ba869e7b28377cd372aedcb96abeb62c4ad6aaa5 rene 20130719 unpublished dirty )

Input

The rewrite relation of the following TRS is considered.

Tgc(SRlbeta(x))	→	SRlapp(W273(k,x))
Tgc(SRlbeta(x))	→	W279(k,x)
Tgc(SRcp(x))	→	W301(k,x)
Tgc(SRllet(x))	→	W316(k,x)
Tgc(SRlapp(x))	→	SRlapp(W321(k,x))
Tgc(SRlapp(x))	→	W327(k,x)
Tgc(SRlcase(x))	→	SRlcase(W349(k,x))
Tgc(SRlcase(x))	→	W355(k,x)
Tgc(SRlseq(x))	→	SRlseq(W377(k,x))
Tgc(SRlseq(x))	→	W383(k,x)
Tgc(SRcase(x))	→	SRlcase(W405(k,x))
Tgc(SRcase(x))	→	W411(k,x)
Tgc(SRseq(x))	→	SRlseq(W438(k,x))
Tgc(SRseq(x))	→	W444(k,x)
Tcpcx(SRlbeta(x))	→	SRlbeta(Tcpcx(x))
Tcpcx(SRlapp(x))	→	SRlapp(Tcpcx(x))
Tcpcx(SRlcase(x))	→	SRlcase(Tcpcx(x))
Tcpcx(SRlseq(x))	→	SRlseq(Tcpcx(x))
Tcpcx(SRcase(x))	→	SRcase(Tcpcx(x))
Tcpcx(SRcase(x))	→	SRcase(x)
Tcpcx(SRseq(x))	→	SRseq(Tcpcx(x))
Tcpcx(SRseq(x))	→	SRseq(x)
Tcpcx(Answer)	→	Answer
Tcpcx(SRllet(x))	→	SRllet(Tcpcx(x))
Tcpcx(SRcp(x))	→	SRcp(Tcpcx(x))
Tcpcx(SRcase(x))	→	SRcase(Tabs(x))
Tcpcx(SRcase(x))	→	SRcase(Tabs(Tcpx(Tcpx(Txch(Txch(x))))))
Tcpcx(SRcase(x))	→	SRcase(Tcpcx(Tcpx(Tcpx(Txch(Txch(x))))))
Tcpcx(SRseq(x))	→	SRseq(Tabs(x))
Tcpcx(SRcp(x))	→	SRcp(Tcpcx(Tcpcx(x)))
Tcpcx(SRcp(x))	→	SRcp(Tcpcx(Tcpcx(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x))))))))
SRlll(x)	→	SRlseq(x)
SRlll(x)	→	SRlapp(x)
SRlll(x)	→	SRllet(x)
SRlll(x)	→	SRlcase(x)
Tabs(SRlbeta(x))	→	SRlbeta(Tabs(x))
Tabs(SRcp(x))	→	SRcp(Tabs(x))
Tabs(SRllet(x))	→	SRllet(Tabs(x))
Tabs(SRlapp(x))	→	SRlapp(Tabs(x))
Tabs(SRlcase(x))	→	SRlcase(Tabs(x))
Tabs(SRlseq(x))	→	SRlseq(Tabs(x))
Tabs(SRcase(x))	→	SRcase(Tabs(x))
Tabs(SRcase(x))	→	SRcase(x)
Tabs(SRcase(x))	→	SRcase(Tabs(Tcpx(Tcpx(Txch(Txch(x))))))
Tabs(SRseq(x))	→	SRseq(Tabs(x))
Tabs(SRseq(x))	→	SRseq(x)
Tabs(Answer)	→	Answer
Txch(SRlbeta(x))	→	SRlbeta(Txch(x))
Txch(SRcp(x))	→	SRcp(Txch(x))
Txch(SRllet(x))	→	SRllet(Txch(x))
Txch(SRlapp(x))	→	SRlapp(Txch(x))
Txch(SRlcase(x))	→	SRlcase(Txch(x))
Txch(SRlseq(x))	→	SRlseq(Txch(x))
Txch(SRcase(x))	→	SRcase(Txch(x))
Txch(SRcase(x))	→	SRcase(x)
Txch(SRseq(x))	→	SRseq(Txch(x))
Txch(SRseq(x))	→	SRseq(x)
Txch(Answer)	→	Answer
Tcpx(SRlbeta(x))	→	SRlbeta(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(x)
Tcpx(SRllet(x))	→	SRllet(Tcpx(x))
Tcpx(SRlapp(x))	→	SRlapp(Tcpx(x))
Tcpx(SRlcase(x))	→	SRlcase(Tcpx(x))
Tcpx(SRlseq(x))	→	SRlseq(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(x)
Tcpx(SRseq(x))	→	SRseq(Tcpx(x))
Tcpx(SRseq(x))	→	SRseq(x)
Tcpx(Answer)	→	Answer
Tcpx(SRcp(x))	→	SRcp(Tcpx(Tcpx(x)))
Tgc(SRlbeta(x))	→	SRlbeta(Tgc(x))
Tgc(SRcp(x))	→	SRcp(Tgc(x))
Tgc(SRllet(x))	→	SRllet(Tgc(x))
Tgc(SRlapp(x))	→	SRlapp(Tgc(x))
Tgc(SRlcase(x))	→	SRlcase(Tgc(x))
Tgc(SRlseq(x))	→	SRlseq(Tgc(x))
Tgc(SRcase(x))	→	SRcase(Tgc(x))
Tgc(SRcase(x))	→	SRcase(x)
Tgc(SRseq(x))	→	SRseq(Tgc(x))
Tgc(SRseq(x))	→	SRseq(x)
Tgc(Answer)	→	Answer
W273(s(k),x)	→	SRlll(W273(k,x))
W273(s(k),x)	→	SRlll(SRlbeta(Tgc(x)))
W279(s(k),x)	→	SRlll(W279(k,x))
W279(s(k),x)	→	SRlll(SRlbeta(Tgc(x)))
Tgc(SRlbeta(x))	→	SRlapp(SRlbeta(SRllet(Tgc(x))))
Tgc(SRlbeta(x))	→	SRlapp(SRllet(SRlbeta(Tgc(x))))
Tgc(SRlbeta(x))	→	SRllet(SRlbeta(Tgc(x)))
W301(s(k),x)	→	SRlll(W301(k,x))
W301(s(k),x)	→	SRlll(SRcp(Tgc(x)))
Tgc(SRcp(x))	→	SRllet(SRcp(Tgc(x)))
Tgc(SRllet(x))	→	SRllet(SRllet(Tgc(x)))
W316(s(k),x)	→	SRlll(W316(k,x))
W316(s(k),x)	→	SRlll(SRllet(Tgc(x)))
W321(s(k),x)	→	SRlll(W321(k,x))
W321(s(k),x)	→	SRlll(SRlapp(Tgc(x)))
W327(s(k),x)	→	SRlll(W327(k,x))
W327(s(k),x)	→	SRlll(SRlapp(Tgc(x)))
Tgc(SRlapp(x))	→	SRlapp(SRlapp(SRllet(Tgc(x))))
Tgc(SRlapp(x))	→	SRlapp(SRllet(SRlapp(Tgc(x))))
Tgc(SRlapp(x))	→	SRllet(SRlapp(Tgc(x)))
W349(s(k),x)	→	SRlll(W349(k,x))
W349(s(k),x)	→	SRlll(SRlcase(Tgc(x)))
W355(s(k),x)	→	SRlll(W355(k,x))
W355(s(k),x)	→	SRlll(SRlcase(Tgc(x)))
Tgc(SRlcase(x))	→	SRlcase(SRlcase(SRllet(Tgc(x))))
Tgc(SRlcase(x))	→	SRlcase(SRllet(SRlcase(Tgc(x))))
Tgc(SRlcase(x))	→	SRllet(SRlcase(Tgc(x)))
W377(s(k),x)	→	SRlll(W377(k,x))
W377(s(k),x)	→	SRlll(SRlseq(Tgc(x)))
W383(s(k),x)	→	SRlll(W383(k,x))
W383(s(k),x)	→	SRlll(SRlseq(Tgc(x)))
Tgc(SRlseq(x))	→	SRlseq(SRlseq(SRllet(Tgc(x))))
Tgc(SRlseq(x))	→	SRlseq(SRllet(SRlseq(Tgc(x))))
Tgc(SRlseq(x))	→	SRllet(SRlseq(Tgc(x)))
W405(s(k),x)	→	SRlll(W405(k,x))
W405(s(k),x)	→	SRlll(SRcase(Tgc(x)))
W411(s(k),x)	→	SRlll(W411(k,x))
W411(s(k),x)	→	SRlll(SRcase(Tgc(x)))
Tgc(SRcase(x))	→	SRlcase(SRcase(Tgc(x)))
Tgc(SRcase(x))	→	SRlcase(SRcase(SRllet(Tgc(x))))
Tgc(SRcase(x))	→	SRlcase(SRllet(SRcase(Tgc(x))))
Tgc(SRcase(x))	→	SRllet(SRcase(Tgc(x)))
W438(s(k),x)	→	SRlll(W438(k,x))
W438(s(k),x)	→	SRlll(SRseq(Tgc(x)))
W444(s(k),x)	→	SRlll(W444(k,x))
W444(s(k),x)	→	SRlll(SRseq(Tgc(x)))
Tgc(SRseq(x))	→	SRlseq(SRseq(Tgc(x)))
Tgc(SRseq(x))	→	SRlseq(SRllet(SRseq(Tgc(x))))
Tgc(SRseq(x))	→	SRllet(SRseq(Tgc(x)))
Tgc(Answer)	→	SRllet(Answer)

The evaluation strategy is innermost.

Proof

1 Removal of non-applicable rules

The following rules have arguments which are not in normal form. Due to the strategy restrictions these can be removed.

There are no rules.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

Tgc^#(SRlbeta(x))	→	W273^#(k,x)
Tgc^#(SRlbeta(x))	→	W279^#(k,x)
Tgc^#(SRcp(x))	→	W301^#(k,x)
Tgc^#(SRllet(x))	→	W316^#(k,x)
Tgc^#(SRlapp(x))	→	W321^#(k,x)
Tgc^#(SRlapp(x))	→	W327^#(k,x)
Tgc^#(SRlcase(x))	→	W349^#(k,x)
Tgc^#(SRlcase(x))	→	W355^#(k,x)
Tgc^#(SRlseq(x))	→	W377^#(k,x)
Tgc^#(SRlseq(x))	→	W383^#(k,x)
Tgc^#(SRcase(x))	→	W405^#(k,x)
Tgc^#(SRcase(x))	→	W411^#(k,x)
Tgc^#(SRseq(x))	→	W438^#(k,x)
Tgc^#(SRseq(x))	→	W444^#(k,x)
Tcpcx^#(SRlbeta(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlapp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRllet(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcase(x))	→	Tabs^#(x)
Tcpcx^#(SRcase(x))	→	Tabs^#(Tcpx(Tcpx(Txch(Txch(x)))))
Tcpcx^#(SRcase(x))	→	Tcpx^#(Tcpx(Txch(Txch(x))))
Tcpcx^#(SRcase(x))	→	Tcpx^#(Txch(Txch(x)))
Tcpcx^#(SRcase(x))	→	Txch^#(Txch(x))
Tcpcx^#(SRcase(x))	→	Txch^#(x)
Tcpcx^#(SRcase(x))	→	Tcpcx^#(Tcpx(Tcpx(Txch(Txch(x)))))
Tcpcx^#(SRseq(x))	→	Tabs^#(x)
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(x))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x)))))))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x))))))
Tcpcx^#(SRcp(x))	→	Tcpx^#(Tcpx(Tcpx(Tcpx(Tgc(x)))))
Tcpcx^#(SRcp(x))	→	Tcpx^#(Tcpx(Tcpx(Tgc(x))))
Tcpcx^#(SRcp(x))	→	Tcpx^#(Tcpx(Tgc(x)))
Tcpcx^#(SRcp(x))	→	Tcpx^#(Tgc(x))
Tcpcx^#(SRcp(x))	→	Tgc^#(x)
Tabs^#(SRlbeta(x))	→	Tabs^#(x)
Tabs^#(SRcp(x))	→	Tabs^#(x)
Tabs^#(SRllet(x))	→	Tabs^#(x)
Tabs^#(SRlapp(x))	→	Tabs^#(x)
Tabs^#(SRlcase(x))	→	Tabs^#(x)
Tabs^#(SRlseq(x))	→	Tabs^#(x)
Tabs^#(SRcase(x))	→	Tabs^#(x)
Tabs^#(SRcase(x))	→	Tabs^#(Tcpx(Tcpx(Txch(Txch(x)))))
Tabs^#(SRcase(x))	→	Tcpx^#(Tcpx(Txch(Txch(x))))
Tabs^#(SRcase(x))	→	Tcpx^#(Txch(Txch(x)))
Tabs^#(SRcase(x))	→	Txch^#(Txch(x))
Tabs^#(SRcase(x))	→	Txch^#(x)
Tabs^#(SRseq(x))	→	Tabs^#(x)
Txch^#(SRlbeta(x))	→	Txch^#(x)
Txch^#(SRcp(x))	→	Txch^#(x)
Txch^#(SRllet(x))	→	Txch^#(x)
Txch^#(SRlapp(x))	→	Txch^#(x)
Txch^#(SRlcase(x))	→	Txch^#(x)
Txch^#(SRlseq(x))	→	Txch^#(x)
Txch^#(SRcase(x))	→	Txch^#(x)
Txch^#(SRseq(x))	→	Txch^#(x)
Tcpx^#(SRlbeta(x))	→	Tcpx^#(x)
Tcpx^#(SRcp(x))	→	Tcpx^#(x)
Tcpx^#(SRllet(x))	→	Tcpx^#(x)
Tcpx^#(SRlapp(x))	→	Tcpx^#(x)
Tcpx^#(SRlcase(x))	→	Tcpx^#(x)
Tcpx^#(SRlseq(x))	→	Tcpx^#(x)
Tcpx^#(SRcase(x))	→	Tcpx^#(x)
Tcpx^#(SRseq(x))	→	Tcpx^#(x)
Tcpx^#(SRcp(x))	→	Tcpx^#(Tcpx(x))
Tgc^#(SRlbeta(x))	→	Tgc^#(x)
Tgc^#(SRcp(x))	→	Tgc^#(x)
Tgc^#(SRllet(x))	→	Tgc^#(x)
Tgc^#(SRlapp(x))	→	Tgc^#(x)
Tgc^#(SRlcase(x))	→	Tgc^#(x)
Tgc^#(SRlseq(x))	→	Tgc^#(x)
Tgc^#(SRcase(x))	→	Tgc^#(x)
Tgc^#(SRseq(x))	→	Tgc^#(x)
W273^#(s(k),x)	→	SRlll^#(W273(k,x))
W273^#(s(k),x)	→	W273^#(k,x)
W273^#(s(k),x)	→	SRlll^#(SRlbeta(Tgc(x)))
W273^#(s(k),x)	→	Tgc^#(x)
W279^#(s(k),x)	→	SRlll^#(W279(k,x))
W279^#(s(k),x)	→	W279^#(k,x)
W279^#(s(k),x)	→	SRlll^#(SRlbeta(Tgc(x)))
W279^#(s(k),x)	→	Tgc^#(x)
W301^#(s(k),x)	→	SRlll^#(W301(k,x))
W301^#(s(k),x)	→	W301^#(k,x)
W301^#(s(k),x)	→	SRlll^#(SRcp(Tgc(x)))
W301^#(s(k),x)	→	Tgc^#(x)
W316^#(s(k),x)	→	SRlll^#(W316(k,x))
W316^#(s(k),x)	→	W316^#(k,x)
W316^#(s(k),x)	→	SRlll^#(SRllet(Tgc(x)))
W316^#(s(k),x)	→	Tgc^#(x)
W321^#(s(k),x)	→	SRlll^#(W321(k,x))
W321^#(s(k),x)	→	W321^#(k,x)
W321^#(s(k),x)	→	SRlll^#(SRlapp(Tgc(x)))
W321^#(s(k),x)	→	Tgc^#(x)
W327^#(s(k),x)	→	SRlll^#(W327(k,x))
W327^#(s(k),x)	→	W327^#(k,x)
W327^#(s(k),x)	→	SRlll^#(SRlapp(Tgc(x)))
W327^#(s(k),x)	→	Tgc^#(x)
W349^#(s(k),x)	→	SRlll^#(W349(k,x))
W349^#(s(k),x)	→	W349^#(k,x)
W349^#(s(k),x)	→	SRlll^#(SRlcase(Tgc(x)))
W349^#(s(k),x)	→	Tgc^#(x)
W355^#(s(k),x)	→	SRlll^#(W355(k,x))
W355^#(s(k),x)	→	W355^#(k,x)
W355^#(s(k),x)	→	SRlll^#(SRlcase(Tgc(x)))
W355^#(s(k),x)	→	Tgc^#(x)
W377^#(s(k),x)	→	SRlll^#(W377(k,x))
W377^#(s(k),x)	→	W377^#(k,x)
W377^#(s(k),x)	→	SRlll^#(SRlseq(Tgc(x)))
W377^#(s(k),x)	→	Tgc^#(x)
W383^#(s(k),x)	→	SRlll^#(W383(k,x))
W383^#(s(k),x)	→	W383^#(k,x)
W383^#(s(k),x)	→	SRlll^#(SRlseq(Tgc(x)))
W383^#(s(k),x)	→	Tgc^#(x)
W405^#(s(k),x)	→	SRlll^#(W405(k,x))
W405^#(s(k),x)	→	W405^#(k,x)
W405^#(s(k),x)	→	SRlll^#(SRcase(Tgc(x)))
W405^#(s(k),x)	→	Tgc^#(x)
W411^#(s(k),x)	→	SRlll^#(W411(k,x))
W411^#(s(k),x)	→	W411^#(k,x)
W411^#(s(k),x)	→	SRlll^#(SRcase(Tgc(x)))
W411^#(s(k),x)	→	Tgc^#(x)
W438^#(s(k),x)	→	SRlll^#(W438(k,x))
W438^#(s(k),x)	→	W438^#(k,x)
W438^#(s(k),x)	→	SRlll^#(SRseq(Tgc(x)))
W438^#(s(k),x)	→	Tgc^#(x)
W444^#(s(k),x)	→	SRlll^#(W444(k,x))
W444^#(s(k),x)	→	W444^#(k,x)
W444^#(s(k),x)	→	SRlll^#(SRseq(Tgc(x)))
W444^#(s(k),x)	→	Tgc^#(x)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pairs

Tcpcx^#(SRlapp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlbeta(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRllet(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcase(x))	→	Tcpcx^#(Tcpx(Tcpx(Txch(Txch(x)))))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(x))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x)))))))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x))))))

1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[Tcpcx^#(x₁)]	=	1 · x₁
[SRlapp(x₁)]	=	1 · x₁
[SRlbeta(x₁)]	=	1 + 1 · x₁
[SRlcase(x₁)]	=	1 · x₁
[SRlseq(x₁)]	=	1 · x₁
[SRcase(x₁)]	=	1 · x₁
[SRseq(x₁)]	=	1 + 1 · x₁
[SRllet(x₁)]	=	1 · x₁
[SRcp(x₁)]	=	1 · x₁
[Tcpx(x₁)]	=	1 · x₁
[Txch(x₁)]	=	1 · x₁
[Tcpcx(x₁)]	=	1 · x₁
[Tgc(x₁)]	=	1 · x₁
[Answer]	=	1
[Tabs(x₁)]	=	1 · x₁
[W273(x₁, x₂)]	=	1 + 1 · x₂
[W279(x₁, x₂)]	=	1 + 1 · x₂
[W301(x₁, x₂)]	=	1 · x₂
[W316(x₁, x₂)]	=	1 · x₂
[W321(x₁, x₂)]	=	1 · x₂
[W327(x₁, x₂)]	=	1 · x₂
[W349(x₁, x₂)]	=	1 · x₂
[W355(x₁, x₂)]	=	1 · x₂
[W377(x₁, x₂)]	=	1 · x₂
[W383(x₁, x₂)]	=	1 · x₂
[W405(x₁, x₂)]	=	1 · x₂
[W411(x₁, x₂)]	=	1 · x₂
[W438(x₁, x₂)]	=	1 + 1 · x₂
[W444(x₁, x₂)]	=	1 + 1 · x₂
[s(x₁)]	=	1 + 1 · x₁
[SRlll(x₁)]	=	1 · x₁

the pairs

Tcpcx^#(SRlapp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRllet(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcase(x))	→	Tcpcx^#(Tcpx(Tcpx(Txch(Txch(x)))))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(x))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x)))))))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x))))))

remain.

1.1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[Tcpcx^#(x₁)]	=	1 · x₁
[SRlapp(x₁)]	=	1 · x₁
[SRlcase(x₁)]	=	1 · x₁
[SRlseq(x₁)]	=	1 · x₁
[SRcase(x₁)]	=	1 + 1 · x₁
[SRllet(x₁)]	=	1 · x₁
[SRcp(x₁)]	=	1 · x₁
[Tcpx(x₁)]	=	1 · x₁
[Txch(x₁)]	=	1 · x₁
[Tcpcx(x₁)]	=	1 · x₁
[Tgc(x₁)]	=	1 · x₁
[SRlbeta(x₁)]	=	1 + 1 · x₁
[SRseq(x₁)]	=	1 + 1 · x₁
[Answer]	=	1
[Tabs(x₁)]	=	1 · x₁
[W273(x₁, x₂)]	=	1 + 1 · x₂
[W279(x₁, x₂)]	=	1 + 1 · x₂
[W301(x₁, x₂)]	=	1 · x₂
[W316(x₁, x₂)]	=	1 · x₂
[W321(x₁, x₂)]	=	1 · x₂
[W327(x₁, x₂)]	=	1 · x₂
[W349(x₁, x₂)]	=	1 · x₂
[W355(x₁, x₂)]	=	1 · x₂
[W377(x₁, x₂)]	=	1 · x₂
[W383(x₁, x₂)]	=	1 · x₂
[W405(x₁, x₂)]	=	1 + 1 · x₂
[W411(x₁, x₂)]	=	1 + 1 · x₂
[W438(x₁, x₂)]	=	1 + 1 · x₂
[W444(x₁, x₂)]	=	1 + 1 · x₂
[s(x₁)]	=	1 + 1 · x₁
[SRlll(x₁)]	=	1 · x₁

the pairs

Tcpcx^#(SRlapp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRllet(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(x))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpcx(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x)))))))
Tcpcx^#(SRcp(x))	→	Tcpcx^#(Tcpx(Tcpx(Tcpx(Tcpx(Tgc(x))))))

remain.

1.1.1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[Tcpcx^#(x₁)]	=	1 · x₁
[SRlapp(x₁)]	=	1 · x₁
[SRlcase(x₁)]	=	1 · x₁
[SRlseq(x₁)]	=	1 · x₁
[SRllet(x₁)]	=	1 · x₁
[SRcp(x₁)]	=	1 + 1 · x₁
[Tcpcx(x₁)]	=	1 · x₁
[Tcpx(x₁)]	=	1 · x₁
[Tgc(x₁)]	=	1 · x₁
[SRlbeta(x₁)]	=	1 + 1 · x₁
[SRcase(x₁)]	=	1 + 1 · x₁
[SRseq(x₁)]	=	1 + 1 · x₁
[Answer]	=	1
[Tabs(x₁)]	=	1 · x₁
[Txch(x₁)]	=	1 · x₁
[W273(x₁, x₂)]	=	1 + 1 · x₂
[W279(x₁, x₂)]	=	1 + 1 · x₂
[W301(x₁, x₂)]	=	1 + 1 · x₂
[W316(x₁, x₂)]	=	1 · x₂
[W321(x₁, x₂)]	=	1 · x₂
[W327(x₁, x₂)]	=	1 · x₂
[W349(x₁, x₂)]	=	1 · x₂
[W355(x₁, x₂)]	=	1 · x₂
[W377(x₁, x₂)]	=	1 · x₂
[W383(x₁, x₂)]	=	1 · x₂
[W405(x₁, x₂)]	=	1 + 1 · x₂
[W411(x₁, x₂)]	=	1 + 1 · x₂
[W438(x₁, x₂)]	=	1 + 1 · x₂
[W444(x₁, x₂)]	=	1 + 1 · x₂
[s(x₁)]	=	1 + 1 · x₁
[SRlll(x₁)]	=	1 · x₁

the pairs

Tcpcx^#(SRlapp(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlcase(x))	→	Tcpcx^#(x)
Tcpcx^#(SRlseq(x))	→	Tcpcx^#(x)
Tcpcx^#(SRllet(x))	→	Tcpcx^#(x)

remain.

1.1.1.1.1.1.1 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

There are no rules.

1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

There are no lhss.

1.1.1.1.1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

Tcpcx^#(SRlapp(x)) → Tcpcx^#(x):
1>1
Tcpcx^#(SRlcase(x)) → Tcpcx^#(x):
1>1
Tcpcx^#(SRlseq(x)) → Tcpcx^#(x):
1>1
Tcpcx^#(SRllet(x)) → Tcpcx^#(x):
1>1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 2^nd component contains the pairs

Tabs^#(SRcp(x))	→	Tabs^#(x)
Tabs^#(SRlbeta(x))	→	Tabs^#(x)
Tabs^#(SRllet(x))	→	Tabs^#(x)
Tabs^#(SRlapp(x))	→	Tabs^#(x)
Tabs^#(SRlcase(x))	→	Tabs^#(x)
Tabs^#(SRlseq(x))	→	Tabs^#(x)
Tabs^#(SRcase(x))	→	Tabs^#(x)
Tabs^#(SRcase(x))	→	Tabs^#(Tcpx(Tcpx(Txch(Txch(x)))))
Tabs^#(SRseq(x))	→	Tabs^#(x)

1.1.1.2 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

Txch(SRlbeta(x))	→	SRlbeta(Txch(x))
Txch(SRcp(x))	→	SRcp(Txch(x))
Txch(SRllet(x))	→	SRllet(Txch(x))
Txch(SRlapp(x))	→	SRlapp(Txch(x))
Txch(SRlcase(x))	→	SRlcase(Txch(x))
Txch(SRlseq(x))	→	SRlseq(Txch(x))
Txch(SRcase(x))	→	SRcase(Txch(x))
Txch(SRcase(x))	→	SRcase(x)
Txch(SRseq(x))	→	SRseq(Txch(x))
Txch(SRseq(x))	→	SRseq(x)
Txch(Answer)	→	Answer
Tcpx(SRlbeta(x))	→	SRlbeta(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(x)
Tcpx(SRllet(x))	→	SRllet(Tcpx(x))
Tcpx(SRlapp(x))	→	SRlapp(Tcpx(x))
Tcpx(SRlcase(x))	→	SRlcase(Tcpx(x))
Tcpx(SRlseq(x))	→	SRlseq(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(x)
Tcpx(SRseq(x))	→	SRseq(Tcpx(x))
Tcpx(SRseq(x))	→	SRseq(x)
Tcpx(Answer)	→	Answer
Tcpx(SRcp(x))	→	SRcp(Tcpx(Tcpx(x)))

1.1.1.2.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

Txch(SRlbeta(x0))

Txch(SRcp(x0))

Txch(SRllet(x0))

Txch(SRlapp(x0))

Txch(SRlcase(x0))

Txch(SRlseq(x0))

Txch(SRcase(x0))

Txch(SRseq(x0))

Txch(Answer)

Tcpx(SRlbeta(x0))

Tcpx(SRcp(x0))

Tcpx(SRllet(x0))

Tcpx(SRlapp(x0))

Tcpx(SRlcase(x0))

Tcpx(SRlseq(x0))

Tcpx(SRcase(x0))

Tcpx(SRseq(x0))

Tcpx(Answer)

1.1.1.2.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[Tabs^#(x₁)]	=	1 · x₁
[SRcp(x₁)]	=	1 + 1 · x₁
[SRlbeta(x₁)]	=	1 + 1 · x₁
[SRllet(x₁)]	=	1 + 1 · x₁
[SRlapp(x₁)]	=	1 + 1 · x₁
[SRlcase(x₁)]	=	1 + 1 · x₁
[SRlseq(x₁)]	=	1 + 1 · x₁
[SRcase(x₁)]	=	1 + 1 · x₁
[Tcpx(x₁)]	=	1 · x₁
[Txch(x₁)]	=	1 · x₁
[SRseq(x₁)]	=	1 + 1 · x₁
[Answer]	=	1

all pairs could be removed.

1.1.1.2.1.1.1 P is empty

There are no pairs anymore.

The 3^rd component contains the pairs

W273^#(s(k),x)	→	W273^#(k,x)
W273^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlbeta(x))	→	W273^#(k,x)
Tgc^#(SRlbeta(x))	→	W279^#(k,x)
W279^#(s(k),x)	→	W279^#(k,x)
W279^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRcp(x))	→	W301^#(k,x)
W301^#(s(k),x)	→	W301^#(k,x)
W301^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRllet(x))	→	W316^#(k,x)
W316^#(s(k),x)	→	W316^#(k,x)
W316^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlapp(x))	→	W321^#(k,x)
W321^#(s(k),x)	→	W321^#(k,x)
W321^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlapp(x))	→	W327^#(k,x)
W327^#(s(k),x)	→	W327^#(k,x)
W327^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlcase(x))	→	W349^#(k,x)
W349^#(s(k),x)	→	W349^#(k,x)
W349^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlcase(x))	→	W355^#(k,x)
W355^#(s(k),x)	→	W355^#(k,x)
W355^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlseq(x))	→	W377^#(k,x)
W377^#(s(k),x)	→	W377^#(k,x)
W377^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlseq(x))	→	W383^#(k,x)
W383^#(s(k),x)	→	W383^#(k,x)
W383^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRcase(x))	→	W405^#(k,x)
W405^#(s(k),x)	→	W405^#(k,x)
W405^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRcase(x))	→	W411^#(k,x)
W411^#(s(k),x)	→	W411^#(k,x)
W411^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRseq(x))	→	W438^#(k,x)
W438^#(s(k),x)	→	W438^#(k,x)
W438^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRseq(x))	→	W444^#(k,x)
W444^#(s(k),x)	→	W444^#(k,x)
W444^#(s(k),x)	→	Tgc^#(x)
Tgc^#(SRlbeta(x))	→	Tgc^#(x)
Tgc^#(SRcp(x))	→	Tgc^#(x)
Tgc^#(SRllet(x))	→	Tgc^#(x)
Tgc^#(SRlapp(x))	→	Tgc^#(x)
Tgc^#(SRlcase(x))	→	Tgc^#(x)
Tgc^#(SRlseq(x))	→	Tgc^#(x)
Tgc^#(SRcase(x))	→	Tgc^#(x)
Tgc^#(SRseq(x))	→	Tgc^#(x)

1.1.1.3 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

There are no rules.

1.1.1.3.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

There are no lhss.

1.1.1.3.1.1 Reduction Pair Processor

Using the matrix interpretations of dimension 3 with strict dimension 1 over the naturals

[W273^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[s(x₁)]

1	1	1
1	1	1
1	1	1

· x₁

[Tgc^#(x₁)]

1	1	1
0	0	0
0	0	0

· x₁

[SRlbeta(x₁)]

0	0	1
1	1	1
0	1	1

· x₁

[W279^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRcp(x₁)]

1	1	1
0	0	0
0	1	0

· x₁

[W301^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRllet(x₁)]

1	1	0
0	0	1
0	0	1

· x₁

[W316^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRlapp(x₁)]

0	0	1
1	1	1
0	1	1

· x₁

[W321^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[W327^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRlcase(x₁)]

1	1	1
0	0	1
0	0	1

· x₁

[W349^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[W355^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRlseq(x₁)]

1	0	1
1	1	1
1	0	1

· x₁

[W377^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[W383^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRcase(x₁)]

1	0	1
0	1	1
0	0	1

· x₁

[W405^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[W411^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[SRseq(x₁)]

1	0	0
1	1	1
1	1	1

· x₁

[W438^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

[W444^#(x₁, x₂)]

0	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂

the pairs

W273^#(s(k),x)	→	W273^#(k,x)
W273^#(s(k),x)	→	Tgc^#(x)
W279^#(s(k),x)	→	W279^#(k,x)
W279^#(s(k),x)	→	Tgc^#(x)
W301^#(s(k),x)	→	W301^#(k,x)
W301^#(s(k),x)	→	Tgc^#(x)
W316^#(s(k),x)	→	W316^#(k,x)
W316^#(s(k),x)	→	Tgc^#(x)
W321^#(s(k),x)	→	W321^#(k,x)
W321^#(s(k),x)	→	Tgc^#(x)
W327^#(s(k),x)	→	W327^#(k,x)
W327^#(s(k),x)	→	Tgc^#(x)
W349^#(s(k),x)	→	W349^#(k,x)
W349^#(s(k),x)	→	Tgc^#(x)
W355^#(s(k),x)	→	W355^#(k,x)
W355^#(s(k),x)	→	Tgc^#(x)
W377^#(s(k),x)	→	W377^#(k,x)
W377^#(s(k),x)	→	Tgc^#(x)
W383^#(s(k),x)	→	W383^#(k,x)
W383^#(s(k),x)	→	Tgc^#(x)
W405^#(s(k),x)	→	W405^#(k,x)
W405^#(s(k),x)	→	Tgc^#(x)
W411^#(s(k),x)	→	W411^#(k,x)
W411^#(s(k),x)	→	Tgc^#(x)
W438^#(s(k),x)	→	W438^#(k,x)
W438^#(s(k),x)	→	Tgc^#(x)
W444^#(s(k),x)	→	W444^#(k,x)
W444^#(s(k),x)	→	Tgc^#(x)

remain.

1.1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 14 components.

The 1^st component contains the pair
W273^#(s(k),x) → W273^#(k,x)

1.1.1.3.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W273^#(s(k),x) → W273^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair
W279^#(s(k),x) → W279^#(k,x)

1.1.1.3.1.1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W279^#(s(k),x) → W279^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair
W301^#(s(k),x) → W301^#(k,x)

1.1.1.3.1.1.1.3 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W301^#(s(k),x) → W301^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair
W316^#(s(k),x) → W316^#(k,x)

1.1.1.3.1.1.1.4 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W316^#(s(k),x) → W316^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 5^th component contains the pair
W321^#(s(k),x) → W321^#(k,x)

1.1.1.3.1.1.1.5 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W321^#(s(k),x) → W321^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 6^th component contains the pair
W327^#(s(k),x) → W327^#(k,x)

1.1.1.3.1.1.1.6 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W327^#(s(k),x) → W327^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 7^th component contains the pair
W349^#(s(k),x) → W349^#(k,x)

1.1.1.3.1.1.1.7 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W349^#(s(k),x) → W349^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 8^th component contains the pair
W355^#(s(k),x) → W355^#(k,x)

1.1.1.3.1.1.1.8 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W355^#(s(k),x) → W355^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 9^th component contains the pair
W377^#(s(k),x) → W377^#(k,x)

1.1.1.3.1.1.1.9 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W377^#(s(k),x) → W377^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 10^th component contains the pair
W383^#(s(k),x) → W383^#(k,x)

1.1.1.3.1.1.1.10 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W383^#(s(k),x) → W383^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 11^th component contains the pair
W405^#(s(k),x) → W405^#(k,x)

1.1.1.3.1.1.1.11 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W405^#(s(k),x) → W405^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 12^th component contains the pair
W411^#(s(k),x) → W411^#(k,x)

1.1.1.3.1.1.1.12 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W411^#(s(k),x) → W411^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 13^th component contains the pair
W438^#(s(k),x) → W438^#(k,x)

1.1.1.3.1.1.1.13 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W438^#(s(k),x) → W438^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.
The 14^th component contains the pair
W444^#(s(k),x) → W444^#(k,x)

1.1.1.3.1.1.1.14 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
- W444^#(s(k),x) → W444^#(k,x):
  1>1, 2>=2
As there is no critical graph in the transitive closure, there are no infinite chains.

The 4^th component contains the pairs

Txch^#(SRcp(x))	→	Txch^#(x)
Txch^#(SRlbeta(x))	→	Txch^#(x)
Txch^#(SRllet(x))	→	Txch^#(x)
Txch^#(SRlapp(x))	→	Txch^#(x)
Txch^#(SRlcase(x))	→	Txch^#(x)
Txch^#(SRlseq(x))	→	Txch^#(x)
Txch^#(SRcase(x))	→	Txch^#(x)
Txch^#(SRseq(x))	→	Txch^#(x)

1.1.1.4 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

There are no rules.

1.1.1.4.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

There are no lhss.

1.1.1.4.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

Txch^#(SRcp(x)) → Txch^#(x):
1>1
Txch^#(SRlbeta(x)) → Txch^#(x):
1>1
Txch^#(SRllet(x)) → Txch^#(x):
1>1
Txch^#(SRlapp(x)) → Txch^#(x):
1>1
Txch^#(SRlcase(x)) → Txch^#(x):
1>1
Txch^#(SRlseq(x)) → Txch^#(x):
1>1
Txch^#(SRcase(x)) → Txch^#(x):
1>1
Txch^#(SRseq(x)) → Txch^#(x):
1>1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 5^th component contains the pairs

Tcpx^#(SRcp(x))	→	Tcpx^#(x)
Tcpx^#(SRlbeta(x))	→	Tcpx^#(x)
Tcpx^#(SRllet(x))	→	Tcpx^#(x)
Tcpx^#(SRlapp(x))	→	Tcpx^#(x)
Tcpx^#(SRlcase(x))	→	Tcpx^#(x)
Tcpx^#(SRlseq(x))	→	Tcpx^#(x)
Tcpx^#(SRcase(x))	→	Tcpx^#(x)
Tcpx^#(SRseq(x))	→	Tcpx^#(x)
Tcpx^#(SRcp(x))	→	Tcpx^#(Tcpx(x))

1.1.1.5 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

Tcpx(SRlbeta(x))	→	SRlbeta(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(x)
Tcpx(SRllet(x))	→	SRllet(Tcpx(x))
Tcpx(SRlapp(x))	→	SRlapp(Tcpx(x))
Tcpx(SRlcase(x))	→	SRlcase(Tcpx(x))
Tcpx(SRlseq(x))	→	SRlseq(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(x)
Tcpx(SRseq(x))	→	SRseq(Tcpx(x))
Tcpx(SRseq(x))	→	SRseq(x)
Tcpx(Answer)	→	Answer
Tcpx(SRcp(x))	→	SRcp(Tcpx(Tcpx(x)))

1.1.1.5.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

Tcpx(SRlbeta(x0))

Tcpx(SRcp(x0))

Tcpx(SRllet(x0))

Tcpx(SRlapp(x0))

Tcpx(SRlcase(x0))

Tcpx(SRlseq(x0))

Tcpx(SRcase(x0))

Tcpx(SRseq(x0))

Tcpx(Answer)

1.1.1.5.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[Tcpx^#(x₁)]	=	1 · x₁
[SRcp(x₁)]	=	1 · x₁
[SRlbeta(x₁)]	=	1 + 1 · x₁
[SRllet(x₁)]	=	1 + 1 · x₁
[SRlapp(x₁)]	=	1 + 1 · x₁
[SRlcase(x₁)]	=	1 + 1 · x₁
[SRlseq(x₁)]	=	1 + 1 · x₁
[SRcase(x₁)]	=	1 + 1 · x₁
[SRseq(x₁)]	=	1 + 1 · x₁
[Tcpx(x₁)]	=	1 · x₁
[Answer]	=	1

the pairs

Tcpx^#(SRcp(x))	→	Tcpx^#(x)
Tcpx^#(SRcp(x))	→	Tcpx^#(Tcpx(x))

remain.

1.1.1.5.1.1.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[Tcpx(x₁)]	=	1 · x₁
[SRlbeta(x₁)]	=	2 · x₁
[SRcp(x₁)]	=	1 + 1 · x₁
[SRllet(x₁)]	=	2 · x₁
[SRlapp(x₁)]	=	2 · x₁
[SRlcase(x₁)]	=	2 · x₁
[SRlseq(x₁)]	=	2 · x₁
[SRcase(x₁)]	=	2 · x₁
[SRseq(x₁)]	=	2 · x₁
[Answer]	=	0
[Tcpx^#(x₁)]	=	3 · x₁

all pairs could be removed, but the rules

Tcpx(SRlbeta(x))	→	SRlbeta(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(Tcpx(x))
Tcpx(SRcp(x))	→	SRcp(x)
Tcpx(SRllet(x))	→	SRllet(Tcpx(x))
Tcpx(SRlapp(x))	→	SRlapp(Tcpx(x))
Tcpx(SRlcase(x))	→	SRlcase(Tcpx(x))
Tcpx(SRlseq(x))	→	SRlseq(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(Tcpx(x))
Tcpx(SRcase(x))	→	SRcase(x)
Tcpx(SRseq(x))	→	SRseq(Tcpx(x))
Tcpx(SRseq(x))	→	SRseq(x)
Tcpx(Answer)	→	Answer
Tcpx(SRcp(x))	→	SRcp(Tcpx(Tcpx(x)))

remains.

1.1.1.5.1.1.1.1 P is empty

There are no pairs anymore.

Termination Proof

Input

Proof

1 Removal of non-applicable rules

1.1 Dependency Pair Transformation

1.1.1 Dependency Graph Processor

1.1.1.1 Reduction Pair Processor

1.1.1.1.1 Reduction Pair Processor

1.1.1.1.1.1 Reduction Pair Processor

1.1.1.1.1.1.1 Usable Rules Processor

1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor

1.1.1.1.1.1.1.1.1 Size-Change Termination

1.1.1.2 Usable Rules Processor

1.1.1.2.1 Innermost Lhss Removal Processor

1.1.1.2.1.1 Reduction Pair Processor

1.1.1.2.1.1.1 P is empty

1.1.1.3 Usable Rules Processor

1.1.1.3.1 Innermost Lhss Removal Processor

1.1.1.3.1.1 Reduction Pair Processor

1.1.1.3.1.1.1 Dependency Graph Processor

1.1.1.3.1.1.1.1 Size-Change Termination

1.1.1.3.1.1.1.2 Size-Change Termination

1.1.1.3.1.1.1.3 Size-Change Termination

1.1.1.3.1.1.1.4 Size-Change Termination

1.1.1.3.1.1.1.5 Size-Change Termination

1.1.1.3.1.1.1.6 Size-Change Termination

1.1.1.3.1.1.1.7 Size-Change Termination

1.1.1.3.1.1.1.8 Size-Change Termination

1.1.1.3.1.1.1.9 Size-Change Termination

1.1.1.3.1.1.1.10 Size-Change Termination

1.1.1.3.1.1.1.11 Size-Change Termination

1.1.1.3.1.1.1.12 Size-Change Termination

1.1.1.3.1.1.1.13 Size-Change Termination

1.1.1.3.1.1.1.14 Size-Change Termination

1.1.1.4 Usable Rules Processor

1.1.1.4.1 Innermost Lhss Removal Processor

1.1.1.4.1.1 Size-Change Termination

1.1.1.5 Usable Rules Processor

1.1.1.5.1 Innermost Lhss Removal Processor

1.1.1.5.1.1 Reduction Pair Processor

1.1.1.5.1.1.1 Monotonic Reduction Pair Processor

1.1.1.5.1.1.1.1 P is empty