YES
(VAR x n h t m pid store)
(RULES 
fstsplit(0,x) -> nil
fstsplit(s(n),nil) -> nil
fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
sndsplit(0,x) -> x
sndsplit(s(n),nil) -> nil
sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
empty(nil) -> true
empty(cons(h,t)) -> false
leq(0,m) -> true
leq(s(n),0) -> false
leq(s(n),s(m)) -> leq(n,m)
length(nil) -> 0
length(cons(h,t)) -> s(length(t))
app(nil,x) -> x
app(cons(h,t),x) -> cons(h,app(t,x))
map_f(pid,nil) -> nil
map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t))
process(store,m) -> if1(store,m,leq(m,length(store)))
if1(store,m,true) -> if2(store,m,empty(fstsplit(m,store)))
if1(store,m,false) -> if3(store,m,empty(fstsplit(m,app(map_f(self,nil),store))))
if2(store,m,false) -> process(app(map_f(self,nil),sndsplit(m,store)),m)
if3(store,m,false) -> process(sndsplit(m,app(map_f(self,nil),store)),m)
)

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 AAECC:

-> Dependency pairs:
nF_fstsplit(s(n),cons(h,t)) -> nF_fstsplit(n,t)
nF_sndsplit(s(n),cons(h,t)) -> nF_sndsplit(n,t)
nF_leq(s(n),s(m)) -> nF_leq(n,m)
nF_length(cons(h,t)) -> nF_length(t)
nF_app(cons(h,t),x) -> nF_app(t,x)
nF_map_f(pid,cons(h,t)) -> nF_app(f(pid,h),map_f(pid,t))
nF_map_f(pid,cons(h,t)) -> nF_map_f(pid,t)
nF_process(store,m) -> nF_if1(store,m,leq(m,length(store)))
nF_process(store,m) -> nF_leq(m,length(store))
nF_process(store,m) -> nF_length(store)
nF_if1(store,m,true) -> nF_if2(store,m,empty(fstsplit(m,store)))
nF_if1(store,m,true) -> nF_empty(fstsplit(m,store))
nF_if1(store,m,true) -> nF_fstsplit(m,store)
nF_if1(store,m,false) -> nF_if3(store,m,empty(fstsplit(m,app(map_f(self,nil),store))))
nF_if1(store,m,false) -> nF_empty(fstsplit(m,app(map_f(self,nil),store)))
nF_if1(store,m,false) -> nF_fstsplit(m,app(map_f(self,nil),store))
nF_if1(store,m,false) -> nF_app(map_f(self,nil),store)
nF_if1(store,m,false) -> nF_map_f(self,nil)
nF_if2(store,m,false) -> nF_process(app(map_f(self,nil),sndsplit(m,store)),m)
nF_if2(store,m,false) -> nF_app(map_f(self,nil),sndsplit(m,store))
nF_if2(store,m,false) -> nF_map_f(self,nil)
nF_if2(store,m,false) -> nF_sndsplit(m,store)
nF_if3(store,m,false) -> nF_process(sndsplit(m,app(map_f(self,nil),store)),m)
nF_if3(store,m,false) -> nF_sndsplit(m,app(map_f(self,nil),store))
nF_if3(store,m,false) -> nF_app(map_f(self,nil),store)
nF_if3(store,m,false) -> nF_map_f(self,nil)

-> Proof of termination for AAECC_1_1:
-> -> Dependency pairs in cycle:
nF_if1(store,m,true) -> nF_if2(store,m,empty(fstsplit(m,store)))
nF_process(store,0) -> nF_if1(store,0,true)
nF_if2(store,m,false) -> nF_process(app(map_f(self,nil),sndsplit(m,store)),m)

UsableRules:
fstsplit(0,x) -> nil
fstsplit(s(n),nil) -> nil
fstsplit(s(n),cons(h,t)) -> cons(h,fstsplit(n,t))
sndsplit(0,x) -> x
sndsplit(s(n),nil) -> nil
sndsplit(s(n),cons(h,t)) -> sndsplit(n,t)
empty(nil) -> true
empty(cons(h,t)) -> false
app(nil,x) -> x
app(cons(h,t),x) -> cons(h,app(t,x))
map_f(pid,nil) -> nil
map_f(pid,cons(h,t)) -> app(f(pid,h),map_f(pid,t))

Polynomial Interpretation:

[fstsplit](X1,X2) = X1
[0] = 0
[nil] = 0
[s](X) = X + 1
[cons](X1,X2) = X2 + 1
[sndsplit](X1,X2) = X1 + X2
[empty](X) = X
[true] = 0
[false] = 1
[leq](X1,X2) = 0
[length](X) = 0
[app](X1,X2) = X1 + X2
[map_f](X1,X2) = 1
[f](X1,X2) = 0
[process](X1,X2) = 0
[if1](X1,X2,X3) = 0
[if2](X1,X2,X3) = 0
[if3](X1,X2,X3) = 0
[self] = 0
[nF_if1](X1,X2,X3) = X2
[nF_process](X1,X2) = 0
[nF_if2](X1,X2,X3) = X3

TIME: 7.1168e-2


-> Proof of termination for AAECC_1_2:
-> -> Dependency pairs in cycle:
nF_map_f(pid,cons(h,t)) -> nF_map_f(pid,t)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for AAECC_1_3:
-> -> Dependency pairs in cycle:
nF_app(cons(h,t),x) -> nF_app(t,x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for AAECC_1_4:
-> -> Dependency pairs in cycle:
nF_length(cons(h,t)) -> nF_length(t)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for AAECC_1_5:
-> -> Dependency pairs in cycle:
nF_leq(s(n),s(m)) -> nF_leq(n,m)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for AAECC_1_6:
-> -> Dependency pairs in cycle:
nF_sndsplit(s(n),cons(h,t)) -> nF_sndsplit(n,t)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for AAECC_1_7:
-> -> Dependency pairs in cycle:
nF_fstsplit(s(n),cons(h,t)) -> nF_fstsplit(n,t)

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.