Term Rewriting System R:
[m, xi, n, s, x, y, k, t, psi, u]
Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)
TERMSUB(Case(m, xi, n), s) -> SUMSUB(xi, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termsub(m, s), t) -> TERMSUB(m, Concat(s, t))
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)
SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)
CONCAT(Concat(s, t), u) -> CONCAT(s, Concat(t, u))
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Polynomial Ordering
       →DP Problem 2
Polo
       →DP Problem 3
Polo


Dependency Pairs:

SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)
SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

SUMSUB(xi, Consusual(y, m, s)) -> SUMSUB(xi, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(SUM_SUB(x1, x2))=  x2  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  1 + x3  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
           →DP Problem 4
Polynomial Ordering
       →DP Problem 2
Polo
       →DP Problem 3
Polo


Dependency Pair:

SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

SUMSUB(xi, Conssum(psi, k, s)) -> SUMSUB(xi, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(SUM_SUB(x1, x2))=  x2  
  POL(Cons_sum(x1, x2, x3))=  1 + x3  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
           →DP Problem 4
Polo
             ...
               →DP Problem 5
Dependency Graph
       →DP Problem 2
Polo
       →DP Problem 3
Polo


Dependency Pair:


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polynomial Ordering
       →DP Problem 3
Polo


Dependency Pairs:

TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)
TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

TERMSUB(Termvar(x), Consusual(y, m, s)) -> TERMSUB(Termvar(x), s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x2  
  POL(Term_var(x1))=  0  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  1 + x3  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
           →DP Problem 6
Polynomial Ordering
       →DP Problem 3
Polo


Dependency Pair:

TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

TERMSUB(Termvar(x), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x2  
  POL(Term_var(x1))=  0  
  POL(Cons_sum(x1, x2, x3))=  1 + x3  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
           →DP Problem 6
Polo
             ...
               →DP Problem 7
Dependency Graph
       →DP Problem 3
Polo


Dependency Pair:


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

CONCAT(Concat(s, t), u) -> CONCAT(t, u)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(Term_inl(x1))=  x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Term_inr(x1))=  x1  
  POL(Term_app(x1, x2))=  x1 + x2  
  POL(Term_pair(x1, x2))=  x1 + x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Concat(x1, x2))=  1 + x2  
  POL(Id)=  0  
  POL(Left)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Terminr(m), s) -> TERMSUB(m, s)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

TERMSUB(Terminr(m), s) -> TERMSUB(m, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(Term_inl(x1))=  x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Term_inr(x1))=  1 + x1  
  POL(Term_app(x1, x2))=  x1 + x2  
  POL(Term_pair(x1, x2))=  x1 + x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Id)=  0  
  POL(Left)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 9
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Terminl(m), s) -> TERMSUB(m, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

TERMSUB(Terminl(m), s) -> TERMSUB(m, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(Term_inl(x1))=  1 + x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Term_app(x1, x2))=  x1 + x2  
  POL(Term_pair(x1, x2))=  x1 + x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Left)=  0  
  POL(Id)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 10
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pairs can be strictly oriented:

TERMSUB(Termpair(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termpair(m, n), s) -> TERMSUB(m, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Term_app(x1, x2))=  x1 + x2  
  POL(Term_pair(x1, x2))=  1 + x1 + x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Left)=  0  
  POL(Id)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 11
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pairs can be strictly oriented:

TERMSUB(Termapp(m, n), s) -> TERMSUB(n, s)
TERMSUB(Termapp(m, n), s) -> TERMSUB(m, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  x3  
  POL(Cons_usual(x1, x2, x3))=  x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Term_app(x1, x2))=  1 + x1 + x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Id)=  0  
  POL(Left)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 12
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  1 + x3  
  POL(Cons_usual(x1, x2, x3))=  x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Id)=  0  
  POL(Left)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 13
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pairs can be strictly oriented:

CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  0  
  POL(Cons_usual(x1, x2, x3))=  1 + x2 + x3  
  POL(Term_sub(x1, x2))=  x2  
  POL(Sum_sub(x1, x2))=  0  
  POL(CONCAT(x1, x2))=  x1  
  POL(Sum_term_var(x1))=  0  
  POL(Id)=  0  
  POL(Left)=  0  
  POL(Case(x1, x2, x3))=  x1 + x3  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 14
Dependency Graph


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




Using the Dependency Graph the DP problem was split into 1 DP problems.


   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 15
Polynomial Ordering


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




The following dependency pair can be strictly oriented:

TERMSUB(Case(m, xi, n), s) -> FROZEN(m, Sumsub(xi, s), n, s)


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(Sum_term_var(x1))=  0  
  POL(TERM_SUB(x1, x2))=  x1  
  POL(Id)=  0  
  POL(Left)=  0  
  POL(FROZEN(x1, x2, x3, x4))=  x1 + x3  
  POL(Case(x1, x2, x3))=  1 + x1 + x3  
  POL(Cons_sum(x1, x2, x3))=  0  
  POL(Cons_usual(x1, x2, x3))=  0  
  POL(Sum_constant(x1))=  0  
  POL(Right)=  0  
  POL(Sum_sub(x1, x2))=  0  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Polo
       →DP Problem 2
Polo
       →DP Problem 3
Polo
           →DP Problem 8
Polo
             ...
               →DP Problem 16
Dependency Graph


Dependency Pairs:

FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumconstant(Right), n, s) -> TERMSUB(n, s)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)
FROZEN(m, Sumtermvar(xi), n, s) -> TERMSUB(n, s)


Rules:


Termsub(Case(m, xi, n), s) -> Frozen(m, Sumsub(xi, s), n, s)
Termsub(Termapp(m, n), s) -> Termapp(Termsub(m, s), Termsub(n, s))
Termsub(Termpair(m, n), s) -> Termpair(Termsub(m, s), Termsub(n, s))
Termsub(Terminl(m), s) -> Terminl(Termsub(m, s))
Termsub(Terminr(m), s) -> Terminr(Termsub(m, s))
Termsub(Termvar(x), Id) -> Termvar(x)
Termsub(Termvar(x), Consusual(y, m, s)) -> m
Termsub(Termvar(x), Consusual(y, m, s)) -> Termsub(Termvar(x), s)
Termsub(Termvar(x), Conssum(xi, k, s)) -> Termsub(Termvar(x), s)
Termsub(Termsub(m, s), t) -> Termsub(m, Concat(s, t))
Frozen(m, Sumconstant(Left), n, s) -> Termsub(m, s)
Frozen(m, Sumconstant(Right), n, s) -> Termsub(n, s)
Frozen(m, Sumtermvar(xi), n, s) -> Case(Termsub(m, s), xi, Termsub(n, s))
Sumsub(xi, Id) -> Sumtermvar(xi)
Sumsub(xi, Conssum(psi, k, s)) -> Sumconstant(k)
Sumsub(xi, Conssum(psi, k, s)) -> Sumsub(xi, s)
Sumsub(xi, Consusual(y, m, s)) -> Sumsub(xi, s)
Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
Concat(Consusual(x, m, s), t) -> Consusual(x, Termsub(m, t), Concat(s, t))
Concat(Conssum(xi, k, s), t) -> Conssum(xi, k, Concat(s, t))
Concat(Id, s) -> s


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:03 minutes