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(SRseq(x)) |
→ |
SRseq(Tcpx(x)) |
|
Tcpx(SRseq(x)) |
→ |
SRseq(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(SRlseq(x)) |
→ |
SRlseq(Tcpx(x)) |
|
Tcpx(Answer) |
→ |
Answer |
|
Tcpx(SRcp(x)) |
→ |
SRcp(Tcpx(Tcpx(x))) |
|
SRlll(x) |
→ |
SRlapp(x) |
|
SRlll(x) |
→ |
SRllet(x) |
The evaluation strategy is innermost.Proof
1 Rule Removal
Using the
linear polynomial interpretation over the naturals
| [Tcpx(x1)] |
= |
1 ·
x1
|
| [SRlbeta(x1)] |
= |
1 ·
x1
|
| [SRseq(x1)] |
= |
1 ·
x1
|
| [SRcp(x1)] |
= |
1 ·
x1
|
| [SRllet(x1)] |
= |
1 ·
x1
|
| [SRlapp(x1)] |
= |
1 ·
x1
|
| [SRlseq(x1)] |
= |
1 ·
x1
|
| [Answer] |
= |
0 |
| [SRlll(x1)] |
= |
1 ·
x1 + 1 |
the
rules
|
Tcpx(SRlbeta(x)) |
→ |
SRlbeta(Tcpx(x)) |
|
Tcpx(SRseq(x)) |
→ |
SRseq(Tcpx(x)) |
|
Tcpx(SRseq(x)) |
→ |
SRseq(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(SRlseq(x)) |
→ |
SRlseq(Tcpx(x)) |
|
Tcpx(Answer) |
→ |
Answer |
|
Tcpx(SRcp(x)) |
→ |
SRcp(Tcpx(Tcpx(x))) |
remain.
1.1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
|
Tcpx#(SRlbeta(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRseq(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRcp(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRllet(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRlapp(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRlseq(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRcp(x)) |
→ |
Tcpx#(Tcpx(x)) |
1.1.1 Innermost Lhss Removal Processor
We restrict the innermost strategy to the following left hand sides.
|
Tcpx(SRlbeta(x0)) |
|
Tcpx(SRseq(x0)) |
|
Tcpx(SRcp(x0)) |
|
Tcpx(SRllet(x0)) |
|
Tcpx(SRlapp(x0)) |
|
Tcpx(SRlseq(x0)) |
|
Tcpx(Answer) |
1.1.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
| [Tcpx#(x1)] |
= |
1 ·
x1
|
| [SRlbeta(x1)] |
= |
1 + 1 ·
x1
|
| [SRseq(x1)] |
= |
1 + 1 ·
x1
|
| [SRcp(x1)] |
= |
1 ·
x1
|
| [SRllet(x1)] |
= |
1 + 1 ·
x1
|
| [SRlapp(x1)] |
= |
1 + 1 ·
x1
|
| [SRlseq(x1)] |
= |
1 + 1 ·
x1
|
| [Tcpx(x1)] |
= |
1 ·
x1
|
| [Answer] |
= |
1 |
the
pairs
|
Tcpx#(SRcp(x)) |
→ |
Tcpx#(x) |
|
Tcpx#(SRcp(x)) |
→ |
Tcpx#(Tcpx(x)) |
remain.
1.1.1.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
| [Tcpx#(x1)] |
= |
1 ·
x1
|
| [SRcp(x1)] |
= |
1 + 1 ·
x1
|
| [Tcpx(x1)] |
= |
1 ·
x1
|
| [SRlbeta(x1)] |
= |
1 + 1 ·
x1
|
| [SRseq(x1)] |
= |
1 + 1 ·
x1
|
| [SRllet(x1)] |
= |
1 + 1 ·
x1
|
| [SRlapp(x1)] |
= |
1 + 1 ·
x1
|
| [SRlseq(x1)] |
= |
1 + 1 ·
x1
|
| [Answer] |
= |
1 |
all pairs could be removed.
1.1.1.1.1.1 P is empty
There are no pairs anymore.