YES Termination proof of AG_#3.17a_mset.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRSRRRProof (⇔, 0 ms)
↳2 RelTRS
↳3 RelTRSRRRProof (⇔, 0 ms)
↳4 RelTRS
↳5 RelTRSRRRProof (⇔, 28 ms)
↳6 RelTRS
↳7 RelTRSRRRProof (⇔, 0 ms)
↳8 RelTRS
↳9 RelTRSRRRProof (⇔, 12 ms)
↳10 RelTRS
↳11 RelTRSRRRProof (⇔, 0 ms)
↳12 RelTRS
↳13 RIsEmptyProof (⇔, 0 ms)
↳14 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(1) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(0) = 1   
POL(app(x1, x2)) = 1 + x1 + x2   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(nil) = 1   
POL(plus(x1, x2)) = 1 + x1 + x2   
POL(pred(x1)) = x1   
POL(s(x1)) = x1   
POL(sum(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

app(nil, k) → k
app(l, nil) → l
plus(0, y) → y
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
Rules from S:
none


(2) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))
pred(cons(s(x), nil)) → cons(x, nil)

The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(3) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(nil) = 0   
POL(plus(x1, x2)) = x1 + x2   
POL(pred(x1)) = 1 + x1   
POL(s(x1)) = 1 + x1   
POL(sum(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
pred(cons(s(x), nil)) → cons(x, nil)
Rules from S:
none


(4) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))

The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(5) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(app(x1, x2)) =
/0\
\0/
 +
/11\
\01/
·x1 +
/10\
\01/
·x2

POL(cons(x1, x2)) =
/0\
\1/
 +
/10\
\11/
·x1 +
/10\
\01/
·x2

POL(sum(x1)) =
/0\
\0/
 +
/10\
\01/
·x1

POL(nil) =
/0\
\1/

POL(plus(x1, x2)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/10\
\00/
·x2

POL(s(x1)) =
/0\
\0/
 +
/10\
\00/
·x1
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

app(cons(x, l), k) → cons(x, app(l, k))
Rules from S:
none


(6) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))

The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(7) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(sum(x1)) =
/0\
\0/
 +
/10\
\11/
·x1

POL(cons(x1, x2)) =
/0\
\0/
 +
/11\
\00/
·x1 +
/11\
\00/
·x2

POL(nil) =
/0\
\0/

POL(app(x1, x2)) =
/0\
\1/
 +
/10\
\00/
·x1 +
/10\
\10/
·x2

POL(plus(x1, x2)) =
/1\
\0/
 +
/11\
\11/
·x1 +
/10\
\00/
·x2

POL(s(x1)) =
/1\
\1/
 +
/10\
\01/
·x1
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

plus(s(x), y) → s(plus(x, y))
Rules from S:
none


(8) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))

The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(9) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(sum(x1)) =
/1\
\1/
 +
/10\
\00/
·x1

POL(cons(x1, x2)) =
/0\
\1/
 +
/11\
\00/
·x1 +
/11\
\01/
·x2

POL(nil) =
/1\
\0/

POL(app(x1, x2)) =
/0\
\1/
 +
/10\
\00/
·x1 +
/11\
\01/
·x2
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

sum(cons(x, nil)) → cons(x, nil)
Rules from S:
none


(10) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))

The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(11) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(sum(x1)) =
/1\
\0/
 +
/11\
\00/
·x1

POL(app(x1, x2)) =
/1\
\1/
 +
/10\
\00/
·x1 +
/11\
\01/
·x2

POL(cons(x1, x2)) =
/0\
\1/
 +
/11\
\00/
·x1 +
/10\
\01/
·x2
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
Rules from S:
none


(12) Obligation:

Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:

cons(x, cons(y, l)) → cons(y, cons(x, l))

(13) RIsEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(14) YES