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
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
AFS


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 that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(SUM_SUB(x1, x2))=  x1 + x2  
  POL(Cons_sum(x1, x2, x3))=  x1 + x2 + x3  
  POL(Cons_usual(x1, x2, x3))=  1 + x1 + x2 + x3  

resulting in one new DP problem.
Used Argument Filtering System:
SUMSUB(x1, x2) -> SUMSUB(x1, x2)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 4
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
AFS


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 that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(SUM_SUB(x1, x2))=  x1 + x2  
  POL(Cons_sum(x1, x2, x3))=  1 + x1 + x2 + x3  

resulting in one new DP problem.
Used Argument Filtering System:
SUMSUB(x1, x2) -> SUMSUB(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)


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


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
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →DP Problem 3
AFS


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), Conssum(xi, k, s)) -> TERMSUB(Termvar(x), s)


There are no usable rules for innermost that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1 + x2  
  POL(Term_var(x1))=  x1  
  POL(Cons_sum(x1, x2, x3))=  1 + x1 + x2 + x3  
  POL(Cons_usual(x1, x2, x3))=  x1 + x2 + x3  

resulting in one new DP problem.
Used Argument Filtering System:
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Termvar(x1) -> Termvar(x1)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 6
Argument Filtering and Ordering
       →DP Problem 3
AFS


Dependency Pair:

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 that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1 + x2  
  POL(Term_var(x1))=  x1  
  POL(Cons_usual(x1, x2, x3))=  1 + x1 + x2 + x3  

resulting in one new DP problem.
Used Argument Filtering System:
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Termvar(x1) -> Termvar(x1)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)


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


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
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Argument Filtering and 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:

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


The following usable rules for innermost can be oriented:

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)


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

resulting in one new DP problem.
Used Argument Filtering System:
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Terminl(x1) -> Terminl(x1)
Termapp(x1, x2) -> Termapp(x1, x2)
Termpair(x1, x2) -> Termpair(x1, x2)
CONCAT(x1, x2) -> CONCAT(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
FROZEN(x1, x2, x3, x4) -> FROZEN(x1, x2, x3, x4)
Sumconstant(x1) -> Sumconstant
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)
Sumtermvar(x1) -> Sumtermvar(x1)
Terminr(x1) -> Terminr(x1)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumsub(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
Argument Filtering and 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(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)


The following usable rules for innermost can be oriented:

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)


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

resulting in one new DP problem.
Used Argument Filtering System:
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Termpair(x1, x2) -> Termpair(x1, x2)
Termapp(x1, x2) -> Termapp(x1, x2)
CONCAT(x1, x2) -> CONCAT(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
FROZEN(x1, x2, x3, x4) -> FROZEN(x1, x2, x3, x4)
Sumconstant(x1) -> Sumconstant
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)
Sumtermvar(x1) -> Sumtermvar(x1)
Terminr(x1) -> Terminr(x1)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumsub(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 9
Argument Filtering and 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(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)


The following usable rules for innermost can be oriented:

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)


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

resulting in one new DP problem.
Used Argument Filtering System:
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Termapp(x1, x2) -> Termapp(x1, x2)
CONCAT(x1, x2) -> CONCAT(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
FROZEN(x1, x2, x3, x4) -> FROZEN(x1, x2, x3, x4)
Sumconstant(x1) -> Sumconstant
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)
Sumtermvar(x1) -> Sumtermvar(x1)
Terminr(x1) -> Terminr(x1)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumsub(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 10
Argument Filtering and 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)
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)


The following usable rules for innermost can be oriented:

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)


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

resulting in one new DP problem.
Used Argument Filtering System:
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Terminr(x1) -> Terminr(x1)
FROZEN(x1, x2, x3, x4) -> FROZEN(x1, x2, x3, x4)
Sumtermvar(x1) -> Sumtermvar(x1)
CONCAT(x1, x2) -> CONCAT(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumsub(x1, x2) -> x1
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
Sumconstant(x1) -> Sumconstant
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 11
Argument Filtering and 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)
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:

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)
FROZEN(m, Sumconstant(Left), n, s) -> TERMSUB(m, s)


The following usable rules for innermost can be oriented:

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)


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

resulting in one new DP problem.
Used Argument Filtering System:
FROZEN(x1, x2, x3, x4) -> FROZEN(x1, x2, x3, x4)
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Sumtermvar(x1) -> Sumtermvar(x1)
CONCAT(x1, x2) -> CONCAT(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Case(x1, x2, x3) -> Case(x1, x2, x3)
Sumsub(x1, x2) -> x1
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
Sumconstant(x1) -> Sumconstant
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 12
Dependency Graph


Dependency Pairs:

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(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
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 13
Argument Filtering and Ordering


Dependency Pairs:

CONCAT(Consusual(x, m, s), t) -> CONCAT(s, t)
TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
CONCAT(Consusual(x, m, s), t) -> TERMSUB(m, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)
CONCAT(Conssum(xi, k, s), t) -> CONCAT(s, t)


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 that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1 + x2  
  POL(Concat(x1, x2))=  x1 + x2  
  POL(Cons_sum(x1, x2, x3))=  1 + x1 + x2 + x3  
  POL(Cons_usual(x1, x2, x3))=  x1 + x2 + x3  
  POL(Term_sub(x1, x2))=  x1 + x2  
  POL(CONCAT(x1, x2))=  x1 + x2  

resulting in one new DP problem.
Used Argument Filtering System:
CONCAT(x1, x2) -> CONCAT(x1, x2)
Conssum(x1, x2, x3) -> Conssum(x1, x2, x3)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 14
Argument Filtering and Ordering


Dependency Pairs:

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


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 that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(TERM_SUB(x1, x2))=  x1 + x2  
  POL(Concat(x1, x2))=  x1 + x2  
  POL(Cons_usual(x1, x2, x3))=  1 + x1 + x2 + x3  
  POL(Term_sub(x1, x2))=  x1 + x2  
  POL(CONCAT(x1, x2))=  x1 + x2  

resulting in one new DP problem.
Used Argument Filtering System:
CONCAT(x1, x2) -> CONCAT(x1, x2)
Consusual(x1, x2, x3) -> Consusual(x1, x2, x3)
TERMSUB(x1, x2) -> TERMSUB(x1, x2)
Termsub(x1, x2) -> Termsub(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 15
Dependency Graph


Dependency Pairs:

TERMSUB(Termsub(m, s), t) -> CONCAT(s, t)
CONCAT(Concat(s, t), u) -> CONCAT(t, u)


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
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 16
Argument Filtering and Ordering


Dependency Pair:

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


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 that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(Concat(x1, x2))=  1 + x1 + x2  
  POL(CONCAT(x1, x2))=  x1 + x2  

resulting in one new DP problem.
Used Argument Filtering System:
CONCAT(x1, x2) -> CONCAT(x1, x2)
Concat(x1, x2) -> Concat(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 8
AFS
             ...
               →DP Problem 17
Dependency Graph


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.

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