Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_FR)

The rewrite relation of the following TRS is considered.

U11(tt,N) → activate(N) (1)
U21(tt,M,N) → s(plus(activate(N),activate(M))) (2)
and(tt,X) → activate(X) (3)
isNat(n__0) → tt (4)
isNat(n__plus(V1,V2)) → and(isNat(activate(V1)),n__isNat(activate(V2))) (5)
isNat(n__s(V1)) → isNat(activate(V1)) (6)
plus(N,0) → U11(isNat(N),N) (7)
plus(N,s(M)) → U21(and(isNat(M),n__isNat(N)),M,N) (8)
0 → n__0 (9)
plus(X1,X2) → n__plus(X1,X2) (10)
isNat(X) → n__isNat(X) (11)
s(X) → n__s(X) (12)
activate(n__0) → 0 (13)
activate(n__plus(X1,X2)) → plus(activate(X1),activate(X2)) (14)
activate(n__isNat(X)) → isNat(X) (15)
activate(n__s(X)) → s(activate(X)) (16)
activate(X) → X (17)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(U11) = 0 stat(U11) = mul
prec(tt) = 1 stat(tt) = mul
prec(U21) = 4 stat(U21) = lex
prec(s) = 3 stat(s) = mul
prec(plus) = 4 stat(plus) = lex
prec(and) = 2 stat(and) = mul
prec(n__0) = 5 stat(n__0) = mul
prec(n__plus) = 4 stat(n__plus) = lex
prec(n__s) = 3 stat(n__s) = mul
prec(0) = 5 stat(0) = mul

π(U11) = [1,2]
π(tt) = []
π(activate) = 1
π(U21) = [3,2,1]
π(s) = [1]
π(plus) = [1,2]
π(and) = [1,2]
π(isNat) = 1
π(n__0) = []
π(n__plus) = [1,2]
π(n__isNat) = 1
π(n__s) = [1]
π(0) = []

all of the following rules can be deleted.
U11(tt,N) → activate(N) (1)
U21(tt,M,N) → s(plus(activate(N),activate(M))) (2)
and(tt,X) → activate(X) (3)
isNat(n__0) → tt (4)
isNat(n__plus(V1,V2)) → and(isNat(activate(V1)),n__isNat(activate(V2))) (5)
isNat(n__s(V1)) → isNat(activate(V1)) (6)
plus(N,0) → U11(isNat(N),N) (7)
plus(N,s(M)) → U21(and(isNat(M),n__isNat(N)),M,N) (8)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(0) = 6 weight(0) = 1
prec(n__0) = 5 weight(n__0) = 1
prec(isNat) = 1 weight(isNat) = 1
prec(n__isNat) = 0 weight(n__isNat) = 1
prec(s) = 4 weight(s) = 1
prec(n__s) = 3 weight(n__s) = 1
prec(activate) = 8 weight(activate) = 0
prec(plus) = 7 weight(plus) = 0
prec(n__plus) = 2 weight(n__plus) = 0
all of the following rules can be deleted.
0 → n__0 (9)
plus(X1,X2) → n__plus(X1,X2) (10)
isNat(X) → n__isNat(X) (11)
s(X) → n__s(X) (12)
activate(n__0) → 0 (13)
activate(n__plus(X1,X2)) → plus(activate(X1),activate(X2)) (14)
activate(n__isNat(X)) → isNat(X) (15)
activate(n__s(X)) → s(activate(X)) (16)
activate(X) → X (17)

1.1.1 R is empty

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