Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_2_AEL03_Z)

The rewrite relation of the following TRS is considered.

from(X) → cons(X,n__from(s(X))) (1)
2ndspos(0,Z) → rnil (2)
2ndspos(s(N),cons(X,n__cons(Y,Z))) → rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z))) (3)
2ndsneg(0,Z) → rnil (4)
2ndsneg(s(N),cons(X,n__cons(Y,Z))) → rcons(negrecip(activate(Y)),2ndspos(N,activate(Z))) (5)
pi(X) → 2ndspos(X,from(0)) (6)
plus(0,Y) → Y (7)
plus(s(X),Y) → s(plus(X,Y)) (8)
times(0,Y) → 0 (9)
times(s(X),Y) → plus(Y,times(X,Y)) (10)
square(X) → times(X,X) (11)
from(X) → n__from(X) (12)
cons(X1,X2) → n__cons(X1,X2) (13)
activate(n__from(X)) → from(X) (14)
activate(n__cons(X1,X2)) → cons(X1,X2) (15)
activate(X) → X (16)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(from) = 3 stat(from) = mul
prec(cons) = 1 stat(cons) = mul
prec(s) = 2 stat(s) = mul
prec(2ndspos) = 5 stat(2ndspos) = lex
prec(0) = 8 stat(0) = mul
prec(rnil) = 6 stat(rnil) = mul
prec(n__cons) = 0 stat(n__cons) = mul
prec(rcons) = 4 stat(rcons) = mul
prec(activate) = 3 stat(activate) = mul
prec(2ndsneg) = 5 stat(2ndsneg) = lex
prec(pi) = 9 stat(pi) = mul
prec(plus) = 7 stat(plus) = mul
prec(times) = 8 stat(times) = mul
prec(square) = 10 stat(square) = lex

π(from) = [1]
π(cons) = [1,2]
π(n__from) = 1
π(s) = [1]
π(2ndspos) = [1,2]
π(0) = []
π(rnil) = []
π(n__cons) = [1,2]
π(rcons) = [1,2]
π(posrecip) = 1
π(activate) = [1]
π(2ndsneg) = [1,2]
π(negrecip) = 1
π(pi) = [1]
π(plus) = [1,2]
π(times) = [1,2]
π(square) = [1]

all of the following rules can be deleted.
from(X) → cons(X,n__from(s(X))) (1)
2ndspos(0,Z) → rnil (2)
2ndspos(s(N),cons(X,n__cons(Y,Z))) → rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z))) (3)
2ndsneg(0,Z) → rnil (4)
2ndsneg(s(N),cons(X,n__cons(Y,Z))) → rcons(negrecip(activate(Y)),2ndspos(N,activate(Z))) (5)
pi(X) → 2ndspos(X,from(0)) (6)
plus(0,Y) → Y (7)
plus(s(X),Y) → s(plus(X,Y)) (8)
times(0,Y) → 0 (9)
times(s(X),Y) → plus(Y,times(X,Y)) (10)
square(X) → times(X,X) (11)
from(X) → n__from(X) (12)
cons(X1,X2) → n__cons(X1,X2) (13)
activate(n__cons(X1,X2)) → cons(X1,X2) (15)
activate(X) → X (16)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(activate) = 2 weight(activate) = 1
prec(n__from) = 0 weight(n__from) = 1
prec(from) = 1 weight(from) = 2
all of the following rules can be deleted.
activate(n__from(X)) → from(X) (14)

1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.