Termination Proof

by AProVE (version ba869e7b28377cd372aedcb96abeb62c4ad6aaa5 rene 20130719 unpublished dirty )

Input

The rewrite relation of the following TRS is considered.

Tllet(SRlbeta(x)) SRlbeta(Tllet(x))
Tllet(SRcp(x)) SRcp(Tllet(x))
Tllet(SRllet(x)) SRllet(Tllet(x))
Tllet(SRllet(x)) x
Tllet(SRlapp(x)) SRlapp(Tllet(x))
Tllet(SRlapp(x)) SRlapp(Tllet(Tlapp(x)))
Tllet(SRlcase(x)) SRlcase(Tllet(x))
Tllet(SRlcase(x)) SRlcase(Tllet(Tlcase(x)))
Tllet(SRlseq(x)) SRlseq(Tllet(x))
Tllet(SRlseq(x)) SRlseq(Tllet(Tlseq(x)))
Tllet(SRcase(x)) SRcase(Tllet(x))
Tllet(SRcase(x)) SRcase(x)
Tllet(SRseq(x)) SRseq(Tllet(x))
Tllet(SRseq(x)) SRseq(x)
Tllet(Answer) Answer
SRlll(x) SRlseq(x)
SRlll(x) SRlapp(x)
SRlll(x) SRllet(x)
SRlll(x) SRlcase(x)
Tlapp(SRlbeta(x)) SRlbeta(Tlapp(x))
Tlapp(SRcp(x)) SRcp(Tlapp(x))
Tlapp(SRllet(x)) SRllet(Tlapp(x))
Tlapp(SRlapp(x)) SRlapp(Tlapp(x))
Tlapp(SRlapp(x)) x
Tlapp(SRlcase(x)) SRlcase(Tlapp(x))
Tlapp(SRlseq(x)) SRlseq(Tlapp(x))
Tlapp(SRcase(x)) SRcase(Tlapp(x))
Tlapp(SRcase(x)) SRcase(x)
Tlapp(SRseq(x)) SRseq(Tlapp(x))
Tlapp(SRseq(x)) SRseq(x)
Tlapp(Answer) Answer
Tlcase(SRlbeta(x)) SRlbeta(Tlcase(x))
Tlcase(SRcp(x)) SRcp(Tlcase(x))
Tlcase(SRllet(x)) SRllet(Tlcase(x))
Tlcase(SRlapp(x)) SRlapp(Tlcase(x))
Tlcase(SRlcase(x)) SRlcase(Tlcase(x))
Tlcase(SRlcase(x)) x
Tlcase(SRlseq(x)) SRlseq(Tlcase(x))
Tlcase(SRcase(x)) SRcase(Tlcase(x))
Tlcase(SRcase(x)) SRcase(x)
Tlcase(SRseq(x)) SRseq(Tlcase(x))
Tlcase(SRseq(x)) SRseq(x)
Tlcase(Answer) Answer
Tlseq(SRlbeta(x)) SRlbeta(Tlseq(x))
Tlseq(SRcp(x)) SRcp(Tlseq(x))
Tlseq(SRllet(x)) SRllet(Tlseq(x))
Tlseq(SRlapp(x)) SRlapp(Tlseq(x))
Tlseq(SRlcase(x)) SRlcase(Tlseq(x))
Tlseq(SRlseq(x)) SRlseq(Tlseq(x))
Tlseq(SRlseq(x)) x
Tlseq(SRcase(x)) SRcase(Tlseq(x))
Tlseq(SRcase(x)) SRcase(x)
Tlseq(SRseq(x)) SRseq(Tlseq(x))
Tlseq(SRseq(x)) SRseq(x)
Tlseq(Answer) Answer
The evaluation strategy is innermost.

Proof

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[Tllet(x1)] = 1 · x1
[SRlbeta(x1)] = 1 · x1
[SRcp(x1)] = 1 · x1
[SRllet(x1)] = 1 · x1 + 1
[SRlapp(x1)] = 1 · x1 + 1
[Tlapp(x1)] = 1 · x1
[SRlcase(x1)] = 1 · x1 + 1
[Tlcase(x1)] = 1 · x1
[SRlseq(x1)] = 1 · x1 + 1
[Tlseq(x1)] = 1 · x1
[SRcase(x1)] = 1 · x1
[SRseq(x1)] = 1 · x1
[Answer] = 0
[SRlll(x1)] = 1 · x1 + 2
the rules
Tllet(SRlbeta(x)) SRlbeta(Tllet(x))
Tllet(SRcp(x)) SRcp(Tllet(x))
Tllet(SRllet(x)) SRllet(Tllet(x))
Tllet(SRlapp(x)) SRlapp(Tllet(x))
Tllet(SRlapp(x)) SRlapp(Tllet(Tlapp(x)))
Tllet(SRlcase(x)) SRlcase(Tllet(x))
Tllet(SRlcase(x)) SRlcase(Tllet(Tlcase(x)))
Tllet(SRlseq(x)) SRlseq(Tllet(x))
Tllet(SRlseq(x)) SRlseq(Tllet(Tlseq(x)))
Tllet(SRcase(x)) SRcase(Tllet(x))
Tllet(SRcase(x)) SRcase(x)
Tllet(SRseq(x)) SRseq(Tllet(x))
Tllet(SRseq(x)) SRseq(x)
Tllet(Answer) Answer
Tlapp(SRlbeta(x)) SRlbeta(Tlapp(x))
Tlapp(SRcp(x)) SRcp(Tlapp(x))
Tlapp(SRllet(x)) SRllet(Tlapp(x))
Tlapp(SRlapp(x)) SRlapp(Tlapp(x))
Tlapp(SRlcase(x)) SRlcase(Tlapp(x))
Tlapp(SRlseq(x)) SRlseq(Tlapp(x))
Tlapp(SRcase(x)) SRcase(Tlapp(x))
Tlapp(SRcase(x)) SRcase(x)
Tlapp(SRseq(x)) SRseq(Tlapp(x))
Tlapp(SRseq(x)) SRseq(x)
Tlapp(Answer) Answer
Tlcase(SRlbeta(x)) SRlbeta(Tlcase(x))
Tlcase(SRcp(x)) SRcp(Tlcase(x))
Tlcase(SRllet(x)) SRllet(Tlcase(x))
Tlcase(SRlapp(x)) SRlapp(Tlcase(x))
Tlcase(SRlcase(x)) SRlcase(Tlcase(x))
Tlcase(SRlseq(x)) SRlseq(Tlcase(x))
Tlcase(SRcase(x)) SRcase(Tlcase(x))
Tlcase(SRcase(x)) SRcase(x)
Tlcase(SRseq(x)) SRseq(Tlcase(x))
Tlcase(SRseq(x)) SRseq(x)
Tlcase(Answer) Answer
Tlseq(SRlbeta(x)) SRlbeta(Tlseq(x))
Tlseq(SRcp(x)) SRcp(Tlseq(x))
Tlseq(SRllet(x)) SRllet(Tlseq(x))
Tlseq(SRlapp(x)) SRlapp(Tlseq(x))
Tlseq(SRlcase(x)) SRlcase(Tlseq(x))
Tlseq(SRlseq(x)) SRlseq(Tlseq(x))
Tlseq(SRcase(x)) SRcase(Tlseq(x))
Tlseq(SRcase(x)) SRcase(x)
Tlseq(SRseq(x)) SRseq(Tlseq(x))
Tlseq(SRseq(x)) SRseq(x)
Tlseq(Answer) Answer
remain.

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[Tllet(x1)] = 1 · x1 + 1
[SRlbeta(x1)] = 1 · x1
[SRcp(x1)] = 1 · x1
[SRllet(x1)] = 1 · x1
[SRlapp(x1)] = 1 · x1
[Tlapp(x1)] = 1 · x1
[SRlcase(x1)] = 1 · x1
[Tlcase(x1)] = 1 · x1
[SRlseq(x1)] = 1 · x1
[Tlseq(x1)] = 1 · x1
[SRcase(x1)] = 1 · x1
[SRseq(x1)] = 1 · x1
[Answer] = 0
the rules
Tllet(SRlbeta(x)) SRlbeta(Tllet(x))
Tllet(SRcp(x)) SRcp(Tllet(x))
Tllet(SRllet(x)) SRllet(Tllet(x))
Tllet(SRlapp(x)) SRlapp(Tllet(x))
Tllet(SRlapp(x)) SRlapp(Tllet(Tlapp(x)))
Tllet(SRlcase(x)) SRlcase(Tllet(x))
Tllet(SRlcase(x)) SRlcase(Tllet(Tlcase(x)))
Tllet(SRlseq(x)) SRlseq(Tllet(x))
Tllet(SRlseq(x)) SRlseq(Tllet(Tlseq(x)))
Tllet(SRcase(x)) SRcase(Tllet(x))
Tllet(SRseq(x)) SRseq(Tllet(x))
Tlapp(SRlbeta(x)) SRlbeta(Tlapp(x))
Tlapp(SRcp(x)) SRcp(Tlapp(x))
Tlapp(SRllet(x)) SRllet(Tlapp(x))
Tlapp(SRlapp(x)) SRlapp(Tlapp(x))
Tlapp(SRlcase(x)) SRlcase(Tlapp(x))
Tlapp(SRlseq(x)) SRlseq(Tlapp(x))
Tlapp(SRcase(x)) SRcase(Tlapp(x))
Tlapp(SRcase(x)) SRcase(x)
Tlapp(SRseq(x)) SRseq(Tlapp(x))
Tlapp(SRseq(x)) SRseq(x)
Tlapp(Answer) Answer
Tlcase(SRlbeta(x)) SRlbeta(Tlcase(x))
Tlcase(SRcp(x)) SRcp(Tlcase(x))
Tlcase(SRllet(x)) SRllet(Tlcase(x))
Tlcase(SRlapp(x)) SRlapp(Tlcase(x))
Tlcase(SRlcase(x)) SRlcase(Tlcase(x))
Tlcase(SRlseq(x)) SRlseq(Tlcase(x))
Tlcase(SRcase(x)) SRcase(Tlcase(x))
Tlcase(SRcase(x)) SRcase(x)
Tlcase(SRseq(x)) SRseq(Tlcase(x))
Tlcase(SRseq(x)) SRseq(x)
Tlcase(Answer) Answer
Tlseq(SRlbeta(x)) SRlbeta(Tlseq(x))
Tlseq(SRcp(x)) SRcp(Tlseq(x))
Tlseq(SRllet(x)) SRllet(Tlseq(x))
Tlseq(SRlapp(x)) SRlapp(Tlseq(x))
Tlseq(SRlcase(x)) SRlcase(Tlseq(x))
Tlseq(SRlseq(x)) SRlseq(Tlseq(x))
Tlseq(SRcase(x)) SRcase(Tlseq(x))
Tlseq(SRcase(x)) SRcase(x)
Tlseq(SRseq(x)) SRseq(Tlseq(x))
Tlseq(SRseq(x)) SRseq(x)
Tlseq(Answer) Answer
remain.

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
Tllet#(SRlbeta(x)) Tllet#(x)
Tllet#(SRcp(x)) Tllet#(x)
Tllet#(SRllet(x)) Tllet#(x)
Tllet#(SRlapp(x)) Tllet#(x)
Tllet#(SRlapp(x)) Tllet#(Tlapp(x))
Tllet#(SRlapp(x)) Tlapp#(x)
Tllet#(SRlcase(x)) Tllet#(x)
Tllet#(SRlcase(x)) Tllet#(Tlcase(x))
Tllet#(SRlcase(x)) Tlcase#(x)
Tllet#(SRlseq(x)) Tllet#(x)
Tllet#(SRlseq(x)) Tllet#(Tlseq(x))
Tllet#(SRlseq(x)) Tlseq#(x)
Tllet#(SRcase(x)) Tllet#(x)
Tllet#(SRseq(x)) Tllet#(x)
Tlapp#(SRlbeta(x)) Tlapp#(x)
Tlapp#(SRcp(x)) Tlapp#(x)
Tlapp#(SRllet(x)) Tlapp#(x)
Tlapp#(SRlapp(x)) Tlapp#(x)
Tlapp#(SRlcase(x)) Tlapp#(x)
Tlapp#(SRlseq(x)) Tlapp#(x)
Tlapp#(SRcase(x)) Tlapp#(x)
Tlapp#(SRseq(x)) Tlapp#(x)
Tlcase#(SRlbeta(x)) Tlcase#(x)
Tlcase#(SRcp(x)) Tlcase#(x)
Tlcase#(SRllet(x)) Tlcase#(x)
Tlcase#(SRlapp(x)) Tlcase#(x)
Tlcase#(SRlcase(x)) Tlcase#(x)
Tlcase#(SRlseq(x)) Tlcase#(x)
Tlcase#(SRcase(x)) Tlcase#(x)
Tlcase#(SRseq(x)) Tlcase#(x)
Tlseq#(SRlbeta(x)) Tlseq#(x)
Tlseq#(SRcp(x)) Tlseq#(x)
Tlseq#(SRllet(x)) Tlseq#(x)
Tlseq#(SRlapp(x)) Tlseq#(x)
Tlseq#(SRlcase(x)) Tlseq#(x)
Tlseq#(SRlseq(x)) Tlseq#(x)
Tlseq#(SRcase(x)) Tlseq#(x)
Tlseq#(SRseq(x)) Tlseq#(x)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.