YES
(VAR x y)
(RULES 
plus(x,0) -> x
plus(x,s(y)) -> s(plus(x,y))
times(0,y) -> 0
times(x,0) -> 0
times(s(x),y) -> plus(times(x,y),y)
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0
fac(s(x)) -> times(fac(p(s(x))),s(x))
)

Proving termination of rewriting for fac:

-> Dependency pairs:
nF_plus(x,s(y)) -> nF_plus(x,y)
nF_times(s(x),y) -> nF_plus(times(x,y),y)
nF_times(s(x),y) -> nF_times(x,y)
nF_p(s(s(x))) -> nF_p(s(x))
nF_fac(s(x)) -> nF_times(fac(p(s(x))),s(x))
nF_fac(s(x)) -> nF_fac(p(s(x)))
nF_fac(s(x)) -> nF_p(s(x))

-> Proof of termination for fac_1_1:
-> -> Dependency pairs in cycle:
nF_fac(s(x)) -> nF_fac(p(s(x)))

UsableRules:
p(s(s(x))) -> s(p(s(x)))
p(s(0)) -> 0

Polynomial Interpretation:

[plus](X1,X2) = 0
[0] = 0
[s](X) = 2.X.X + 2
[times](X1,X2) = 0
[p](X) = 1/2.X
[fac](X) = 0
[nF_fac](X) = 2.X.X

TIME: 1.882e-3


-> Proof of termination for fac_1_2:
-> -> Dependency pairs in cycle:
nF_p(s(s(x))) -> nF_p(s(x))

Termination proved: Cycles verify subterm criterion.

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

Termination proved: Cycles verify subterm criterion.

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

Termination proved: Cycles verify subterm criterion.

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



Termination was proved succesfully.