YES
(VAR x y n u v w z)
(RULES 
minus(x,0) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0,s(y)) -> 0
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
app(nil,y) -> y
app(add(n,x),y) -> add(n,app(x,y))
reverse(nil) -> nil
reverse(add(n,x)) -> app(reverse(x),add(n,nil))
shuffle(nil) -> nil
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
concat(leaf,y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))
less_leaves(x,leaf) -> false
less_leaves(leaf,cons(w,z)) -> true
less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z))
)

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for _3_53:

-> Dependency pairs:
nF_minus(s(x),s(y)) -> nF_minus(x,y)
nF_quot(s(x),s(y)) -> nF_quot(minus(x,y),s(y))
nF_quot(s(x),s(y)) -> nF_minus(x,y)
nF_app(add(n,x),y) -> nF_app(x,y)
nF_reverse(add(n,x)) -> nF_app(reverse(x),add(n,nil))
nF_reverse(add(n,x)) -> nF_reverse(x)
nF_shuffle(add(n,x)) -> nF_shuffle(reverse(x))
nF_shuffle(add(n,x)) -> nF_reverse(x)
nF_concat(cons(u,v),y) -> nF_concat(v,y)
nF_less_leaves(cons(u,v),cons(w,z)) -> nF_less_leaves(concat(u,v),concat(w,z))
nF_less_leaves(cons(u,v),cons(w,z)) -> nF_concat(u,v)
nF_less_leaves(cons(u,v),cons(w,z)) -> nF_concat(w,z)

-> Proof of termination for _3_53_1_1:
-> -> Dependency pairs in cycle:
nF_less_leaves(cons(u,v),cons(w,z)) -> nF_less_leaves(concat(u,v),concat(w,z))

UsableRules:
concat(leaf,y) -> y
concat(cons(u,v),y) -> cons(u,concat(v,y))

Polynomial Interpretation:

[minus](X1,X2) = 0
[0] = 0
[s](X) = 0
[quot](X1,X2) = 0
[app](X1,X2) = 0
[nil] = 0
[add](X1,X2) = 0
[reverse](X) = 0
[shuffle](X) = 0
[concat](X1,X2) = X1 + X2
[leaf] = 0
[cons](X1,X2) = X1 + X2 + 1
[less_leaves](X1,X2) = 0
[false] = 0
[true] = 0
[nF_less_leaves](X1,X2) = X1

TIME: 4.1607e-2


-> Proof of termination for _3_53_1_2:
-> -> Dependency pairs in cycle:
nF_concat(cons(u,v),y) -> nF_concat(v,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for _3_53_1_3:
-> -> Dependency pairs in cycle:
nF_shuffle(add(n,x)) -> nF_shuffle(reverse(x))

UsableRules:
app(nil,y) -> y
app(add(n,x),y) -> add(n,app(x,y))
reverse(nil) -> nil
reverse(add(n,x)) -> app(reverse(x),add(n,nil))

Polynomial Interpretation:

[minus](X1,X2) = 0
[0] = 0
[s](X) = 0
[quot](X1,X2) = 0
[app](X1,X2) = X1 + X2
[nil] = 0
[add](X1,X2) = X2 + 1
[reverse](X) = X
[shuffle](X) = 0
[concat](X1,X2) = 0
[leaf] = 0
[cons](X1,X2) = 0
[less_leaves](X1,X2) = 0
[false] = 0
[true] = 0
[nF_shuffle](X) = X

TIME: 4.0781e-2


-> Proof of termination for _3_53_1_4:
-> -> Dependency pairs in cycle:
nF_reverse(add(n,x)) -> nF_reverse(x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for _3_53_1_5:
-> -> Dependency pairs in cycle:
nF_app(add(n,x),y) -> nF_app(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for _3_53_1_6:
-> -> Dependency pairs in cycle:
nF_quot(s(x),s(y)) -> nF_quot(minus(x,y),s(y))

UsableRules:
minus(x,0) -> x
minus(s(x),s(y)) -> minus(x,y)

Polynomial Interpretation:

[minus](X1,X2) = X1
[0] = 0
[s](X) = X + 1
[quot](X1,X2) = 0
[app](X1,X2) = 0
[nil] = 0
[add](X1,X2) = 0
[reverse](X) = 0
[shuffle](X) = 0
[concat](X1,X2) = 0
[leaf] = 0
[cons](X1,X2) = 0
[less_leaves](X1,X2) = 0
[false] = 0
[true] = 0
[nF_quot](X1,X2) = X1

TIME: 3.9842e-2


-> Proof of termination for _3_53_1_7:
-> -> Dependency pairs in cycle:
nF_minus(s(x),s(y)) -> nF_minus(x,y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.