Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete_GM)

The rewrite relation of the following TRS is considered.

a__U11(tt,V1,V2) → a__U12(a__isNat(V1),V2) (1)
a__U12(tt,V2) → a__U13(a__isNat(V2)) (2)
a__U13(tt) → tt (3)
a__U21(tt,V1) → a__U22(a__isNat(V1)) (4)
a__U22(tt) → tt (5)
a__U31(tt,N) → mark(N) (6)
a__U41(tt,M,N) → s(a__plus(mark(N),mark(M))) (7)
a__and(tt,X) → mark(X) (8)
a__isNat(0) → tt (9)
a__isNat(plus(V1,V2)) → a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) (10)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1),V1) (11)
a__isNatKind(0) → tt (12)
a__isNatKind(plus(V1,V2)) → a__and(a__isNatKind(V1),isNatKind(V2)) (13)
a__isNatKind(s(V1)) → a__isNatKind(V1) (14)
a__plus(N,0) → a__U31(a__and(a__isNat(N),isNatKind(N)),N) (15)
a__plus(N,s(M)) → a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) (16)
mark(U11(X1,X2,X3)) → a__U11(mark(X1),X2,X3) (17)
mark(U12(X1,X2)) → a__U12(mark(X1),X2) (18)
mark(isNat(X)) → a__isNat(X) (19)
mark(U13(X)) → a__U13(mark(X)) (20)
mark(U21(X1,X2)) → a__U21(mark(X1),X2) (21)
mark(U22(X)) → a__U22(mark(X)) (22)
mark(U31(X1,X2)) → a__U31(mark(X1),X2) (23)
mark(U41(X1,X2,X3)) → a__U41(mark(X1),X2,X3) (24)
mark(plus(X1,X2)) → a__plus(mark(X1),mark(X2)) (25)
mark(and(X1,X2)) → a__and(mark(X1),X2) (26)
mark(isNatKind(X)) → a__isNatKind(X) (27)
mark(tt) → tt (28)
mark(s(X)) → s(mark(X)) (29)
mark(0) → 0 (30)
a__U11(X1,X2,X3) → U11(X1,X2,X3) (31)
a__U12(X1,X2) → U12(X1,X2) (32)
a__isNat(X) → isNat(X) (33)
a__U13(X) → U13(X) (34)
a__U21(X1,X2) → U21(X1,X2) (35)
a__U22(X) → U22(X) (36)
a__U31(X1,X2) → U31(X1,X2) (37)
a__U41(X1,X2,X3) → U41(X1,X2,X3) (38)
a__plus(X1,X2) → plus(X1,X2) (39)
a__and(X1,X2) → and(X1,X2) (40)
a__isNatKind(X) → isNatKind(X) (41)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(a__U11) = 1 stat(a__U11) = mul
prec(tt) = 2 stat(tt) = mul
prec(a__U12) = 0 stat(a__U12) = mul
prec(a__isNat) = 0 stat(a__isNat) = mul
prec(a__U21) = 3 stat(a__U21) = mul
prec(a__U31) = 4 stat(a__U31) = mul
prec(a__U41) = 7 stat(a__U41) = lex
prec(s) = 6 stat(s) = mul
prec(a__plus) = 7 stat(a__plus) = lex
prec(a__and) = 5 stat(a__and) = mul
prec(0) = 8 stat(0) = mul
prec(plus) = 7 stat(plus) = lex
prec(and) = 5 stat(and) = mul
prec(isNat) = 0 stat(isNat) = mul
prec(U11) = 1 stat(U11) = mul
prec(U12) = 0 stat(U12) = mul
prec(U21) = 3 stat(U21) = mul
prec(U31) = 4 stat(U31) = mul
prec(U41) = 7 stat(U41) = lex

π(a__U11) = [1,2,3]
π(tt) = []
π(a__U12) = [1,2]
π(a__isNat) = [1]
π(a__U13) = 1
π(a__U21) = [1,2]
π(a__U22) = 1
π(a__U31) = [1,2]
π(mark) = 1
π(a__U41) = [2,3,1]
π(s) = [1]
π(a__plus) = [2,1]
π(a__and) = [1,2]
π(0) = []
π(plus) = [2,1]
π(a__isNatKind) = 1
π(isNatKind) = 1
π(and) = [1,2]
π(isNat) = [1]
π(U11) = [1,2,3]
π(U12) = [1,2]
π(U13) = 1
π(U21) = [1,2]
π(U22) = 1
π(U31) = [1,2]
π(U41) = [2,3,1]

all of the following rules can be deleted.
a__U11(tt,V1,V2) → a__U12(a__isNat(V1),V2) (1)
a__U12(tt,V2) → a__U13(a__isNat(V2)) (2)
a__U21(tt,V1) → a__U22(a__isNat(V1)) (4)
a__U31(tt,N) → mark(N) (6)
a__U41(tt,M,N) → s(a__plus(mark(N),mark(M))) (7)
a__and(tt,X) → mark(X) (8)
a__isNat(0) → tt (9)
a__isNat(plus(V1,V2)) → a__U11(a__and(a__isNatKind(V1),isNatKind(V2)),V1,V2) (10)
a__isNat(s(V1)) → a__U21(a__isNatKind(V1),V1) (11)
a__isNatKind(0) → tt (12)
a__isNatKind(plus(V1,V2)) → a__and(a__isNatKind(V1),isNatKind(V2)) (13)
a__isNatKind(s(V1)) → a__isNatKind(V1) (14)
a__plus(N,0) → a__U31(a__and(a__isNat(N),isNatKind(N)),N) (15)
a__plus(N,s(M)) → a__U41(a__and(a__and(a__isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N) (16)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(tt) = 23 weight(tt) = 1
prec(0) = 22 weight(0) = 1
prec(a__U13) = 10 weight(a__U13) = 1
prec(a__U22) = 16 weight(a__U22) = 1
prec(mark) = 25 weight(mark) = 0
prec(isNat) = 0 weight(isNat) = 1
prec(a__isNat) = 12 weight(a__isNat) = 1
prec(U13) = 9 weight(U13) = 1
prec(U22) = 15 weight(U22) = 1
prec(isNatKind) = 13 weight(isNatKind) = 1
prec(a__isNatKind) = 20 weight(a__isNatKind) = 1
prec(s) = 21 weight(s) = 1
prec(U11) = 19 weight(U11) = 0
prec(a__U11) = 24 weight(a__U11) = 0
prec(U12) = 11 weight(U12) = 0
prec(a__U12) = 18 weight(a__U12) = 0
prec(U21) = 5 weight(U21) = 0
prec(a__U21) = 7 weight(a__U21) = 0
prec(U31) = 1 weight(U31) = 0
prec(a__U31) = 6 weight(a__U31) = 0
prec(U41) = 14 weight(U41) = 0
prec(a__U41) = 17 weight(a__U41) = 0
prec(plus) = 2 weight(plus) = 0
prec(a__plus) = 8 weight(a__plus) = 0
prec(and) = 3 weight(and) = 0
prec(a__and) = 4 weight(a__and) = 0
all of the following rules can be deleted.
a__U13(tt) → tt (3)
a__U22(tt) → tt (5)
mark(U11(X1,X2,X3)) → a__U11(mark(X1),X2,X3) (17)
mark(U12(X1,X2)) → a__U12(mark(X1),X2) (18)
mark(isNat(X)) → a__isNat(X) (19)
mark(U13(X)) → a__U13(mark(X)) (20)
mark(U21(X1,X2)) → a__U21(mark(X1),X2) (21)
mark(U22(X)) → a__U22(mark(X)) (22)
mark(U31(X1,X2)) → a__U31(mark(X1),X2) (23)
mark(U41(X1,X2,X3)) → a__U41(mark(X1),X2,X3) (24)
mark(plus(X1,X2)) → a__plus(mark(X1),mark(X2)) (25)
mark(and(X1,X2)) → a__and(mark(X1),X2) (26)
mark(isNatKind(X)) → a__isNatKind(X) (27)
mark(tt) → tt (28)
mark(s(X)) → s(mark(X)) (29)
mark(0) → 0 (30)
a__U11(X1,X2,X3) → U11(X1,X2,X3) (31)
a__U12(X1,X2) → U12(X1,X2) (32)
a__isNat(X) → isNat(X) (33)
a__U13(X) → U13(X) (34)
a__U21(X1,X2) → U21(X1,X2) (35)
a__U22(X) → U22(X) (36)
a__U31(X1,X2) → U31(X1,X2) (37)
a__U41(X1,X2,X3) → U41(X1,X2,X3) (38)
a__plus(X1,X2) → plus(X1,X2) (39)
a__and(X1,X2) → and(X1,X2) (40)
a__isNatKind(X) → isNatKind(X) (41)

1.1.1 R is empty

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