The rewrite relation of the following TRS is considered.
| circ(cons(a,s),t) | → | cons(msubst(a,t),circ(s,t)) | (1) |
| circ(cons(lift,s),cons(a,t)) | → | cons(a,circ(s,t)) | (2) |
| circ(cons(lift,s),cons(lift,t)) | → | cons(lift,circ(s,t)) | (3) |
| circ(circ(s,t),u) | → | circ(s,circ(t,u)) | (4) |
| circ(s,id) | → | s | (5) |
| circ(id,s) | → | s | (6) |
| circ(cons(lift,s),circ(cons(lift,t),u)) | → | circ(cons(lift,circ(s,t)),u) | (7) |
| subst(a,id) | → | a | (8) |
| msubst(a,id) | → | a | (9) |
| msubst(msubst(a,s),t) | → | msubst(a,circ(s,t)) | (10) |
| circ#(cons(a,s),t) | → | msubst#(a,t) | (11) |
| circ#(cons(a,s),t) | → | circ#(s,t) | (12) |
| circ#(cons(lift,s),cons(a,t)) | → | circ#(s,t) | (13) |
| circ#(cons(lift,s),cons(lift,t)) | → | circ#(s,t) | (14) |
| circ#(circ(s,t),u) | → | circ#(s,circ(t,u)) | (15) |
| circ#(circ(s,t),u) | → | circ#(t,u) | (16) |
| circ#(cons(lift,s),circ(cons(lift,t),u)) | → | circ#(cons(lift,circ(s,t)),u) | (17) |
| circ#(cons(lift,s),circ(cons(lift,t),u)) | → | circ#(s,t) | (18) |
| msubst#(msubst(a,s),t) | → | msubst#(a,circ(s,t)) | (19) |
| msubst#(msubst(a,s),t) | → | circ#(s,t) | (20) |
| [circ#(x1, x2)] | = | 1 · x1 + 1 · x1 · x2 |
| [cons(x1, x2)] | = | 1 + 1 · x2 + 1 · x1 |
| [msubst#(x1, x2)] | = | 1 · x1 + 1 · x1 · x2 |
| [lift] | = | 0 |
| [circ(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
| [msubst(x1, x2)] | = | 1 · x2 + 1 · x1 + 1 · x1 · x2 |
| [id] | = | 1 |
| circ(cons(a,s),t) | → | cons(msubst(a,t),circ(s,t)) | (1) |
| circ(cons(lift,s),cons(a,t)) | → | cons(a,circ(s,t)) | (2) |
| circ(cons(lift,s),cons(lift,t)) | → | cons(lift,circ(s,t)) | (3) |
| circ(circ(s,t),u) | → | circ(s,circ(t,u)) | (4) |
| circ(s,id) | → | s | (5) |
| circ(id,s) | → | s | (6) |
| circ(cons(lift,s),circ(cons(lift,t),u)) | → | circ(cons(lift,circ(s,t)),u) | (7) |
| msubst(msubst(a,s),t) | → | msubst(a,circ(s,t)) | (10) |
| msubst(a,id) | → | a | (9) |
| circ#(cons(a,s),t) | → | msubst#(a,t) | (11) |
| circ#(cons(a,s),t) | → | circ#(s,t) | (12) |
| circ#(cons(lift,s),cons(a,t)) | → | circ#(s,t) | (13) |
| circ#(cons(lift,s),cons(lift,t)) | → | circ#(s,t) | (14) |
| circ#(cons(lift,s),circ(cons(lift,t),u)) | → | circ#(cons(lift,circ(s,t)),u) | (17) |
| circ#(cons(lift,s),circ(cons(lift,t),u)) | → | circ#(s,t) | (18) |
The dependency pairs are split into 2 components.
| msubst#(msubst(a,s),t) | → | msubst#(a,circ(s,t)) | (19) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| msubst#(msubst(a,s),t) | → | msubst#(a,circ(s,t)) | (19) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| circ#(circ(s,t),u) | → | circ#(t,u) | (16) |
| circ#(circ(s,t),u) | → | circ#(s,circ(t,u)) | (15) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| circ#(circ(s,t),u) | → | circ#(t,u) | (16) |
| 1 | > | 1 | |
| 2 | ≥ | 2 | |
| circ#(circ(s,t),u) | → | circ#(s,circ(t,u)) | (15) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.