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#(Term_pair(m,n),s) | → | Term_sub#(m,s) | (22) |
Term_sub#(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub#(Term_var(x),s) | (23) |
Concat#(Cons_usual(x,m,s),t) | → | Term_sub#(m,t) | (24) |
Term_sub#(Term_inl(m),s) | → | Term_sub#(m,s) | (25) |
Term_sub#(Term_app(m,n),s) | → | Term_sub#(n,s) | (26) |
Concat#(Concat(s,t),u) | → | Concat#(t,u) | (27) |
Sum_sub#(xi,Cons_usual(y,m,s)) | → | Sum_sub#(xi,s) | (28) |
Concat#(Cons_usual(x,m,s),t) | → | Concat#(s,t) | (29) |
Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(m,s) | (30) |
Term_sub#(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub#(Term_var(x),s) | (31) |
Term_sub#(Term_app(m,n),s) | → | Term_sub#(m,s) | (32) |
Term_sub#(Term_sub(m,s),t) | → | Concat#(s,t) | (33) |
Concat#(Concat(s,t),u) | → | Concat#(s,Concat(t,u)) | (34) |
Term_sub#(Case(m,xi,n),s) | → | Frozen#(m,Sum_sub(xi,s),n,s) | (35) |
Term_sub#(Term_inr(m),s) | → | Term_sub#(m,s) | (36) |
Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(n,s) | (37) |
Frozen#(m,Sum_constant(Right),n,s) | → | Term_sub#(n,s) | (38) |
Term_sub#(Term_pair(m,n),s) | → | Term_sub#(n,s) | (39) |
Frozen#(m,Sum_constant(Left),n,s) | → | Term_sub#(m,s) | (40) |
Concat#(Cons_sum(xi,k,s),t) | → | Concat#(s,t) | (41) |
Sum_sub#(xi,Cons_sum(psi,k,s)) | → | Sum_sub#(xi,s) | (42) |
Term_sub#(Term_sub(m,s),t) | → | Term_sub#(m,Concat(s,t)) | (43) |
Term_sub#(Case(m,xi,n),s) | → | Sum_sub#(xi,s) | (44) |
The dependency pairs are split into 3 components.
Term_sub#(Term_sub(m,s),t) | → | Term_sub#(m,Concat(s,t)) | (43) |
Concat#(Cons_usual(x,m,s),t) | → | Concat#(s,t) | (29) |
Concat#(Cons_sum(xi,k,s),t) | → | Concat#(s,t) | (41) |
Frozen#(m,Sum_constant(Left),n,s) | → | Term_sub#(m,s) | (40) |
Concat#(Concat(s,t),u) | → | Concat#(t,u) | (27) |
Term_sub#(Term_pair(m,n),s) | → | Term_sub#(n,s) | (39) |
Frozen#(m,Sum_constant(Right),n,s) | → | Term_sub#(n,s) | (38) |
Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(n,s) | (37) |
Term_sub#(Term_app(m,n),s) | → | Term_sub#(n,s) | (26) |
Term_sub#(Term_inl(m),s) | → | Term_sub#(m,s) | (25) |
Concat#(Cons_usual(x,m,s),t) | → | Term_sub#(m,t) | (24) |
Term_sub#(Term_inr(m),s) | → | Term_sub#(m,s) | (36) |
Term_sub#(Case(m,xi,n),s) | → | Frozen#(m,Sum_sub(xi,s),n,s) | (35) |
Concat#(Concat(s,t),u) | → | Concat#(s,Concat(t,u)) | (34) |
Term_sub#(Term_sub(m,s),t) | → | Concat#(s,t) | (33) |
Term_sub#(Term_app(m,n),s) | → | Term_sub#(m,s) | (32) |
Term_sub#(Term_pair(m,n),s) | → | Term_sub#(m,s) | (22) |
Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(m,s) | (30) |
[Cons_sum(x1, x2, x3)] | = | x3 + 1 |
[Left] | = | 1 |
[Sum_term_var(x1)] | = | 1 |
[Concat#(x1, x2)] | = | x1 + 0 |
[Case(x1, x2, x3)] | = | x1 + x2 + x3 + 2 |
[Term_inr(x1)] | = | x1 + 8856 |
[Sum_sub#(x1, x2)] | = | 0 |
[Sum_constant(x1)] | = | 1 |
[Sum_sub(x1, x2)] | = | 1 |
[Right] | = | 1 |
[Cons_usual(x1, x2, x3)] | = | x2 + x3 + 11798 |
[Term_var(x1)] | = | 9508 |
[Id] | = | 32286 |
[Term_sub(x1, x2)] | = | x1 + x2 + 1 |
[Frozen(x1,...,x4)] | = | 0 |
[Frozen#(x1,...,x4)] | = | x1 + x2 + x3 + 0 |
[Term_app(x1, x2)] | = | x1 + x2 + 10451 |
[Term_inl(x1)] | = | x1 + 30613 |
[Term_pair(x1, x2)] | = | x1 + x2 + 5854 |
[Term_sub#(x1, x2)] | = | x1 + 0 |
[Concat(x1, x2)] | = | x1 + x2 + 28102 |
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) |
Sum_sub(xi,Id) | → | Sum_term_var(xi) | (14) |
Term_sub#(Term_sub(m,s),t) | → | Term_sub#(m,Concat(s,t)) | (43) |
Concat#(Cons_usual(x,m,s),t) | → | Concat#(s,t) | (29) |
Concat#(Cons_sum(xi,k,s),t) | → | Concat#(s,t) | (41) |
Frozen#(m,Sum_constant(Left),n,s) | → | Term_sub#(m,s) | (40) |
Concat#(Concat(s,t),u) | → | Concat#(t,u) | (27) |
Term_sub#(Term_pair(m,n),s) | → | Term_sub#(n,s) | (39) |
Frozen#(m,Sum_constant(Right),n,s) | → | Term_sub#(n,s) | (38) |
Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(n,s) | (37) |
Term_sub#(Term_app(m,n),s) | → | Term_sub#(n,s) | (26) |
Term_sub#(Term_inl(m),s) | → | Term_sub#(m,s) | (25) |
Concat#(Cons_usual(x,m,s),t) | → | Term_sub#(m,t) | (24) |
Term_sub#(Term_inr(m),s) | → | Term_sub#(m,s) | (36) |
Term_sub#(Case(m,xi,n),s) | → | Frozen#(m,Sum_sub(xi,s),n,s) | (35) |
Concat#(Concat(s,t),u) | → | Concat#(s,Concat(t,u)) | (34) |
Term_sub#(Term_sub(m,s),t) | → | Concat#(s,t) | (33) |
Term_sub#(Term_app(m,n),s) | → | Term_sub#(m,s) | (32) |
Term_sub#(Term_pair(m,n),s) | → | Term_sub#(m,s) | (22) |
Frozen#(m,Sum_term_var(xi),n,s) | → | Term_sub#(m,s) | (30) |
The dependency pairs are split into 0 components.
Term_sub#(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub#(Term_var(x),s) | (23) |
Term_sub#(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub#(Term_var(x),s) | (31) |
[Cons_sum(x1, x2, x3)] | = | x3 + 1 |
[Left] | = | 1 |
[Sum_term_var(x1)] | = | 1 |
[Concat#(x1, x2)] | = | 0 |
[Case(x1, x2, x3)] | = | x1 + x2 + x3 + 13297 |
[Term_inr(x1)] | = | x1 + 31205 |
[Sum_sub#(x1, x2)] | = | 0 |
[Sum_constant(x1)] | = | 1 |
[Sum_sub(x1, x2)] | = | 1 |
[Right] | = | 1 |
[Cons_usual(x1, x2, x3)] | = | x3 + 11798 |
[Term_var(x1)] | = | 46441 |
[Id] | = | 1 |
[Term_sub(x1, x2)] | = | x1 + x2 + 2 |
[Frozen(x1,...,x4)] | = | x2 + 0 |
[Frozen#(x1,...,x4)] | = | x2 + 0 |
[Term_app(x1, x2)] | = | x2 + 22105 |
[Term_inl(x1)] | = | x1 + 1 |
[Term_pair(x1, x2)] | = | x1 + x2 + 30490 |
[Term_sub#(x1, x2)] | = | x2 + 0 |
[Concat(x1, x2)] | = | x1 + x2 + 3 |
Concat(Concat(s,t),u) | → | Concat(s,Concat(t,u)) | (18) |
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) |
Concat(Id,s) | → | s | (21) |
Concat(Cons_usual(x,m,s),t) | → | Cons_usual(x,Term_sub(m,t),Concat(s,t)) | (19) |
Sum_sub(xi,Cons_usual(y,m,s)) | → | Sum_sub(xi,s) | (17) |
Concat(Cons_sum(xi,k,s),t) | → | Cons_sum(xi,k,Concat(s,t)) | (20) |
Sum_sub(xi,Id) | → | Sum_term_var(xi) | (14) |
Term_sub#(Term_var(x),Cons_usual(y,m,s)) | → | Term_sub#(Term_var(x),s) | (23) |
Term_sub#(Term_var(x),Cons_sum(xi,k,s)) | → | Term_sub#(Term_var(x),s) | (31) |
The dependency pairs are split into 0 components.
Sum_sub#(xi,Cons_sum(psi,k,s)) | → | Sum_sub#(xi,s) | (42) |
Sum_sub#(xi,Cons_usual(y,m,s)) | → | Sum_sub#(xi,s) | (28) |
[Cons_sum(x1, x2, x3)] | = | x3 + 1 |
[Left] | = | 1 |
[Sum_term_var(x1)] | = | 1 |
[Concat#(x1, x2)] | = | 0 |
[Case(x1, x2, x3)] | = | x1 + x2 + x3 + 48178 |
[Term_inr(x1)] | = | x1 + 31205 |
[Sum_sub#(x1, x2)] | = | x2 + 0 |
[Sum_constant(x1)] | = | 1 |
[Sum_sub(x1, x2)] | = | 1 |
[Right] | = | 1 |
[Cons_usual(x1, x2, x3)] | = | x3 + 11798 |
[Term_var(x1)] | = | 1 |
[Id] | = | 1 |
[Term_sub(x1, x2)] | = | x1 + x2 + 2 |
[Frozen(x1,...,x4)] | = | x2 + 0 |
[Frozen#(x1,...,x4)] | = | x2 + 0 |
[Term_app(x1, x2)] | = | x2 + 1 |
[Term_inl(x1)] | = | x1 + 1 |
[Term_pair(x1, x2)] | = | x1 + x2 + 15208 |
[Term_sub#(x1, x2)] | = | x2 + 0 |
[Concat(x1, x2)] | = | x1 + x2 + 3 |
Concat(Concat(s,t),u) | → | Concat(s,Concat(t,u)) | (18) |
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) |
Concat(Id,s) | → | s | (21) |
Concat(Cons_usual(x,m,s),t) | → | Cons_usual(x,Term_sub(m,t),Concat(s,t)) | (19) |
Sum_sub(xi,Cons_usual(y,m,s)) | → | Sum_sub(xi,s) | (17) |
Concat(Cons_sum(xi,k,s),t) | → | Cons_sum(xi,k,Concat(s,t)) | (20) |
Sum_sub(xi,Id) | → | Sum_term_var(xi) | (14) |
Sum_sub#(xi,Cons_sum(psi,k,s)) | → | Sum_sub#(xi,s) | (42) |
Sum_sub#(xi,Cons_usual(y,m,s)) | → | Sum_sub#(xi,s) | (28) |
The dependency pairs are split into 0 components.