Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/MYNAT_nokinds_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,N) → mark(N) (1)
a__U21(tt,M,N) → s(a__plus(mark(N),mark(M))) (2)
a__U31(tt) → 0 (3)
a__U41(tt,M,N) → a__plus(a__x(mark(N),mark(M)),mark(N)) (4)
a__and(tt,X) → mark(X) (5)
a__isNat(0) → tt (6)
a__isNat(plus(V1,V2)) → a__and(a__isNat(V1),isNat(V2)) (7)
a__isNat(s(V1)) → a__isNat(V1) (8)
a__isNat(x(V1,V2)) → a__and(a__isNat(V1),isNat(V2)) (9)
a__plus(N,0) → a__U11(a__isNat(N),N) (10)
a__plus(N,s(M)) → a__U21(a__and(a__isNat(M),isNat(N)),M,N) (11)
a__x(N,0) → a__U31(a__isNat(N)) (12)
a__x(N,s(M)) → a__U41(a__and(a__isNat(M),isNat(N)),M,N) (13)
mark(U11(X1,X2)) → a__U11(mark(X1),X2) (14)
mark(U21(X1,X2,X3)) → a__U21(mark(X1),X2,X3) (15)
mark(plus(X1,X2)) → a__plus(mark(X1),mark(X2)) (16)
mark(U31(X)) → a__U31(mark(X)) (17)
mark(U41(X1,X2,X3)) → a__U41(mark(X1),X2,X3) (18)
mark(x(X1,X2)) → a__x(mark(X1),mark(X2)) (19)
mark(and(X1,X2)) → a__and(mark(X1),X2) (20)
mark(isNat(X)) → a__isNat(X) (21)
mark(tt) → tt (22)
mark(s(X)) → s(mark(X)) (23)
mark(0) → 0 (24)
a__U11(X1,X2) → U11(X1,X2) (25)
a__U21(X1,X2,X3) → U21(X1,X2,X3) (26)
a__plus(X1,X2) → plus(X1,X2) (27)
a__U31(X) → U31(X) (28)
a__U41(X1,X2,X3) → U41(X1,X2,X3) (29)
a__x(X1,X2) → x(X1,X2) (30)
a__and(X1,X2) → and(X1,X2) (31)
a__isNat(X) → isNat(X) (32)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(a__U11) = 0 stat(a__U11) = mul
prec(tt) = 3 stat(tt) = mul
prec(a__U21) = 2 stat(a__U21) = lex
prec(s) = 1 stat(s) = mul
prec(a__plus) = 2 stat(a__plus) = lex
prec(0) = 3 stat(0) = mul
prec(a__U41) = 4 stat(a__U41) = lex
prec(a__x) = 4 stat(a__x) = lex
prec(a__and) = 1 stat(a__and) = mul
prec(plus) = 2 stat(plus) = lex
prec(x) = 4 stat(x) = lex
prec(U11) = 0 stat(U11) = mul
prec(U21) = 2 stat(U21) = lex
prec(U41) = 4 stat(U41) = lex
prec(and) = 1 stat(and) = mul

π(a__U11) = [1,2]
π(tt) = []
π(mark) = 1
π(a__U21) = [2,3,1]
π(s) = [1]
π(a__plus) = [2,1]
π(a__U31) = 1
π(0) = []
π(a__U41) = [2,3,1]
π(a__x) = [2,1]
π(a__and) = [1,2]
π(a__isNat) = 1
π(plus) = [2,1]
π(isNat) = 1
π(x) = [2,1]
π(U11) = [1,2]
π(U21) = [2,3,1]
π(U31) = 1
π(U41) = [2,3,1]
π(and) = [1,2]

all of the following rules can be deleted.
a__U11(tt,N) → mark(N) (1)
a__U21(tt,M,N) → s(a__plus(mark(N),mark(M))) (2)
a__U41(tt,M,N) → a__plus(a__x(mark(N),mark(M)),mark(N)) (4)
a__and(tt,X) → mark(X) (5)
a__isNat(plus(V1,V2)) → a__and(a__isNat(V1),isNat(V2)) (7)
a__isNat(s(V1)) → a__isNat(V1) (8)
a__isNat(x(V1,V2)) → a__and(a__isNat(V1),isNat(V2)) (9)
a__plus(N,0) → a__U11(a__isNat(N),N) (10)
a__plus(N,s(M)) → a__U21(a__and(a__isNat(M),isNat(N)),M,N) (11)
a__x(N,0) → a__U31(a__isNat(N)) (12)
a__x(N,s(M)) → a__U41(a__and(a__isNat(M),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) = 5 weight(tt) = 2
prec(0) = 0 weight(0) = 1
prec(a__U31) = 13 weight(a__U31) = 1
prec(a__isNat) = 10 weight(a__isNat) = 1
prec(mark) = 19 weight(mark) = 0
prec(U31) = 9 weight(U31) = 1
prec(isNat) = 8 weight(isNat) = 1
prec(s) = 18 weight(s) = 1
prec(U11) = 1 weight(U11) = 0
prec(a__U11) = 2 weight(a__U11) = 0
prec(U21) = 3 weight(U21) = 0
prec(a__U21) = 4 weight(a__U21) = 0
prec(plus) = 14 weight(plus) = 0
prec(a__plus) = 15 weight(a__plus) = 0
prec(U41) = 11 weight(U41) = 0
prec(a__U41) = 12 weight(a__U41) = 0
prec(x) = 6 weight(x) = 0
prec(a__x) = 7 weight(a__x) = 0
prec(and) = 16 weight(and) = 0
prec(a__and) = 17 weight(a__and) = 0
all of the following rules can be deleted.
a__U31(tt) → 0 (3)
a__isNat(0) → tt (6)
mark(U11(X1,X2)) → a__U11(mark(X1),X2) (14)
mark(U21(X1,X2,X3)) → a__U21(mark(X1),X2,X3) (15)
mark(plus(X1,X2)) → a__plus(mark(X1),mark(X2)) (16)
mark(U31(X)) → a__U31(mark(X)) (17)
mark(U41(X1,X2,X3)) → a__U41(mark(X1),X2,X3) (18)
mark(x(X1,X2)) → a__x(mark(X1),mark(X2)) (19)
mark(and(X1,X2)) → a__and(mark(X1),X2) (20)
mark(isNat(X)) → a__isNat(X) (21)
mark(tt) → tt (22)
mark(s(X)) → s(mark(X)) (23)
mark(0) → 0 (24)
a__U11(X1,X2) → U11(X1,X2) (25)
a__U21(X1,X2,X3) → U21(X1,X2,X3) (26)
a__plus(X1,X2) → plus(X1,X2) (27)
a__U31(X) → U31(X) (28)
a__U41(X1,X2,X3) → U41(X1,X2,X3) (29)
a__x(X1,X2) → x(X1,X2) (30)
a__and(X1,X2) → and(X1,X2) (31)
a__isNat(X) → isNat(X) (32)

1.1.1 R is empty

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