The rewrite relation of the following TRS is considered.
| Term_sub(Case(m,xi,n),s) | → | Frozen(m,Sum_sub(xi,s),n,s) | (1) |
| Frozen(m,Sum_constant(Left),n,s) | → | Term_sub(m,s) | (2) |
| Frozen(m,Sum_constant(Right),n,s) | → | Term_sub(n,s) | (3) |
| Frozen(m,Sum_term_var(xi),n,s) | → | Case(Term_sub(m,s),xi,Term_sub(n,s)) | (4) |
| Term_sub(Term_app(m,n),s) | → | Term_app(Term_sub(m,s),Term_sub(n,s)) | (5) |
| Term_sub(Term_pair(m,n),s) | → | Term_pair(Term_sub(m,s),Term_sub(n,s)) | (6) |
| Term_sub(Term_inl(m),s) | → | Term_inl(Term_sub(m,s)) | (7) |
| Term_sub(Term_inr(m),s) | → | Term_inr(Term_sub(m,s)) | (8) |
| Term_sub(Term_var(x),Id) | → | Term_var(x) | (9) |
| Term_sub(Term_var(x),Cons_usual(y,m,s)) | → | m | (10) |
| Term_sub(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub(Term_var(x),s) | (11) |
| Term_sub(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub(Term_var(x),s) | (12) |
| Term_sub(Term_sub(m,s),t) | → | Term_sub(m,Concat(s,t)) | (13) |
| Sum_sub(xi,Id) | → | Sum_term_var(xi) | (14) |
| Sum_sub(xi,Cons_sum(psi,k,s)) | → | Sum_constant(k) | (15) |
| Sum_sub(xi,Cons_sum(psi,k,s)) | → | Sum_sub(xi,s) | (16) |
| Sum_sub(xi,Cons_usual(y,m,s)) | → | Sum_sub(xi,s) | (17) |
| Concat(Concat(s,t),u) | → | Concat(s,Concat(t,u)) | (18) |
| Concat(Cons_usual(x,m,s),t) | → | Cons_usual(x,Term_sub(m,t),Concat(s,t)) | (19) |
| Concat(Cons_sum(xi,k,s),t) | → | Cons_sum(xi,k,Concat(s,t)) | (20) |
| Concat(Id,s) | → | s | (21) |
| Term_sub#(Case(m,xi,n),s) | → | Sum_sub#(xi,s) | (22) |
| Term_sub#(Case(m,xi,n),s) | → | Frozen#(m,Sum_sub(xi,s),n,s) | (23) |
| Frozen#(m,Sum_constant(Left),n,s) | → | Term_sub#(m,s) | (24) |
| Frozen#(m,Sum_constant(Right),n,s) | → | Term_sub#(n,s) | (25) |
| Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(n,s) | (26) |
| Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(m,s) | (27) |
| Term_sub#(Term_app(m,n),s) | → | Term_sub#(n,s) | (28) |
| Term_sub#(Term_app(m,n),s) | → | Term_sub#(m,s) | (29) |
| Term_sub#(Term_pair(m,n),s) | → | Term_sub#(n,s) | (30) |
| Term_sub#(Term_pair(m,n),s) | → | Term_sub#(m,s) | (31) |
| Term_sub#(Term_inl(m),s) | → | Term_sub#(m,s) | (32) |
| Term_sub#(Term_inr(m),s) | → | Term_sub#(m,s) | (33) |
| Term_sub#(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub#(Term_var(x),s) | (34) |
| Term_sub#(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub#(Term_var(x),s) | (35) |
| Term_sub#(Term_sub(m,s),t) | → | Concat#(s,t) | (36) |
| Term_sub#(Term_sub(m,s),t) | → | Term_sub#(m,Concat(s,t)) | (37) |
| Sum_sub#(xi,Cons_sum(psi,k,s)) | → | Sum_sub#(xi,s) | (38) |
| Sum_sub#(xi,Cons_usual(y,m,s)) | → | Sum_sub#(xi,s) | (39) |
| Concat#(Concat(s,t),u) | → | Concat#(t,u) | (40) |
| Concat#(Concat(s,t),u) | → | Concat#(s,Concat(t,u)) | (41) |
| Concat#(Cons_usual(x,m,s),t) | → | Concat#(s,t) | (42) |
| Concat#(Cons_usual(x,m,s),t) | → | Term_sub#(m,t) | (43) |
| Concat#(Cons_sum(xi,k,s),t) | → | Concat#(s,t) | (44) |
The dependency pairs are split into 3 components.
| Concat#(Concat(s,t),u) | → | Concat#(t,u) | (40) |
| Concat#(Cons_sum(xi,k,s),t) | → | Concat#(s,t) | (44) |
| Concat#(Cons_usual(x,m,s),t) | → | Term_sub#(m,t) | (43) |
| Term_sub#(Term_sub(m,s),t) | → | Term_sub#(m,Concat(s,t)) | (37) |
| Term_sub#(Term_sub(m,s),t) | → | Concat#(s,t) | (36) |
| Concat#(Cons_usual(x,m,s),t) | → | Concat#(s,t) | (42) |
| Concat#(Concat(s,t),u) | → | Concat#(s,Concat(t,u)) | (41) |
| Term_sub#(Term_inr(m),s) | → | Term_sub#(m,s) | (33) |
| Term_sub#(Term_inl(m),s) | → | Term_sub#(m,s) | (32) |
| Term_sub#(Term_pair(m,n),s) | → | Term_sub#(m,s) | (31) |
| Term_sub#(Term_pair(m,n),s) | → | Term_sub#(n,s) | (30) |
| Term_sub#(Term_app(m,n),s) | → | Term_sub#(m,s) | (29) |
| Term_sub#(Term_app(m,n),s) | → | Term_sub#(n,s) | (28) |
| Term_sub#(Case(m,xi,n),s) | → | Frozen#(m,Sum_sub(xi,s),n,s) | (23) |
| Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(m,s) | (27) |
| Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(n,s) | (26) |
| Frozen#(m,Sum_constant(Right),n,s) | → | Term_sub#(n,s) | (25) |
| Frozen#(m,Sum_constant(Left),n,s) | → | Term_sub#(m,s) | (24) |
| π(Concat#) | = | { 1, 1 } |
| π(Frozen#) | = | { 1, 1, 3, 3 } |
| π(Term_sub#) | = | { 1, 1 } |
| π(Term_inr) | = | { 1 } |
| π(Term_inl) | = | { 1 } |
| π(Term_pair) | = | { 1, 1, 2 } |
| π(Term_app) | = | { 1, 2, 2 } |
| π(Sum_term_var) | = | { 1 } |
| π(Sum_constant) | = | { 1, 1 } |
| π(Sum_sub) | = | { 1, 2, 2 } |
| π(Case) | = | { 1, 3, 3 } |
| Concat#(Concat(s,t),u) | → | Concat#(t,u) | (40) |
| Concat#(Cons_sum(xi,k,s),t) | → | Concat#(s,t) | (44) |
| Concat#(Cons_usual(x,m,s),t) | → | Term_sub#(m,t) | (43) |
| Term_sub#(Term_sub(m,s),t) | → | Term_sub#(m,Concat(s,t)) | (37) |
| Term_sub#(Term_sub(m,s),t) | → | Concat#(s,t) | (36) |
| Concat#(Cons_usual(x,m,s),t) | → | Concat#(s,t) | (42) |
| Concat#(Concat(s,t),u) | → | Concat#(s,Concat(t,u)) | (41) |
| Term_sub#(Term_pair(m,n),s) | → | Term_sub#(m,s) | (31) |
| Term_sub#(Term_pair(m,n),s) | → | Term_sub#(n,s) | (30) |
| Term_sub#(Term_app(m,n),s) | → | Term_sub#(m,s) | (29) |
| Term_sub#(Term_app(m,n),s) | → | Term_sub#(n,s) | (28) |
| Term_sub#(Case(m,xi,n),s) | → | Frozen#(m,Sum_sub(xi,s),n,s) | (23) |
| Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(m,s) | (27) |
| Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(n,s) | (26) |
| Frozen#(m,Sum_constant(Right),n,s) | → | Term_sub#(n,s) | (25) |
| Frozen#(m,Sum_constant(Left),n,s) | → | Term_sub#(m,s) | (24) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| Term_sub#(Term_inr(m),s) | → | Term_sub#(m,s) | (33) |
| 2 | ≥ | 2 | |
| 1 | > | 1 | |
| Term_sub#(Term_inl(m),s) | → | Term_sub#(m,s) | (32) |
| 2 | ≥ | 2 | |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| Sum_sub#(xi,Cons_usual(y,m,s)) | → | Sum_sub#(xi,s) | (39) |
| Sum_sub#(xi,Cons_sum(psi,k,s)) | → | Sum_sub#(xi,s) | (38) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| Sum_sub#(xi,Cons_usual(y,m,s)) | → | Sum_sub#(xi,s) | (39) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| Sum_sub#(xi,Cons_sum(psi,k,s)) | → | Sum_sub#(xi,s) | (38) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| Term_sub#(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub#(Term_var(x),s) | (35) |
| Term_sub#(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub#(Term_var(x),s) | (34) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| Term_sub#(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub#(Term_var(x),s) | (35) |
| 2 | > | 2 | |
| 1 | ≥ | 1 | |
| Term_sub#(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub#(Term_var(x),s) | (34) |
| 2 | > | 2 | |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.