Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_nokinds_Z)

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)
U31(tt) → 0 (3)
U41(tt,M,N) → plus(x(activate(N),activate(M)),activate(N)) (4)
and(tt,X) → activate(X) (5)
isNat(n__0) → tt (6)
isNat(n__plus(V1,V2)) → and(isNat(activate(V1)),n__isNat(activate(V2))) (7)
isNat(n__s(V1)) → isNat(activate(V1)) (8)
isNat(n__x(V1,V2)) → and(isNat(activate(V1)),n__isNat(activate(V2))) (9)
plus(N,0) → U11(isNat(N),N) (10)
plus(N,s(M)) → U21(and(isNat(M),n__isNat(N)),M,N) (11)
x(N,0) → U31(isNat(N)) (12)
x(N,s(M)) → U41(and(isNat(M),n__isNat(N)),M,N) (13)
0 → n__0 (14)
plus(X1,X2) → n__plus(X1,X2) (15)
isNat(X) → n__isNat(X) (16)
s(X) → n__s(X) (17)
x(X1,X2) → n__x(X1,X2) (18)
activate(n__0) → 0 (19)
activate(n__plus(X1,X2)) → plus(X1,X2) (20)
activate(n__isNat(X)) → isNat(X) (21)
activate(n__s(X)) → s(X) (22)
activate(n__x(X1,X2)) → x(X1,X2) (23)
activate(X) → X (24)

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) = 3 stat(tt) = mul
prec(U21) = 1 stat(U21) = lex
prec(s) = 0 stat(s) = mul
prec(plus) = 1 stat(plus) = lex
prec(0) = 3 stat(0) = mul
prec(U41) = 2 stat(U41) = lex
prec(x) = 2 stat(x) = lex
prec(and) = 0 stat(and) = lex
prec(n__0) = 3 stat(n__0) = mul
prec(n__plus) = 1 stat(n__plus) = lex
prec(n__s) = 0 stat(n__s) = mul
prec(n__x) = 2 stat(n__x) = lex

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

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)
U41(tt,M,N) → plus(x(activate(N),activate(M)),activate(N)) (4)
and(tt,X) → activate(X) (5)
isNat(n__plus(V1,V2)) → and(isNat(activate(V1)),n__isNat(activate(V2))) (7)
isNat(n__s(V1)) → isNat(activate(V1)) (8)
isNat(n__x(V1,V2)) → and(isNat(activate(V1)),n__isNat(activate(V2))) (9)
plus(N,0) → U11(isNat(N),N) (10)
plus(N,s(M)) → U21(and(isNat(M),n__isNat(N)),M,N) (11)
x(N,0) → U31(isNat(N)) (12)
x(N,s(M)) → U41(and(isNat(M),n__isNat(N)),M,N) (13)

1.1 Rule Removal

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

1.1.1 R is empty

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