Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete_iGM)

The rewrite relation of the following TRS is considered.

active(U11(tt,V1,V2)) → mark(U12(isNat(V1),V2)) (1)
active(U12(tt,V2)) → mark(U13(isNat(V2))) (2)
active(U13(tt)) → mark(tt) (3)
active(U21(tt,V1)) → mark(U22(isNat(V1))) (4)
active(U22(tt)) → mark(tt) (5)
active(U31(tt,N)) → mark(N) (6)
active(U41(tt,M,N)) → mark(s(plus(N,M))) (7)
active(and(tt,X)) → mark(X) (8)
active(isNat(0)) → mark(tt) (9)
active(isNat(plus(V1,V2))) → mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) (10)
active(isNat(s(V1))) → mark(U21(isNatKind(V1),V1)) (11)
active(isNatKind(0)) → mark(tt) (12)
active(isNatKind(plus(V1,V2))) → mark(and(isNatKind(V1),isNatKind(V2))) (13)
active(isNatKind(s(V1))) → mark(isNatKind(V1)) (14)
active(plus(N,0)) → mark(U31(and(isNat(N),isNatKind(N)),N)) (15)
active(plus(N,s(M))) → mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) (16)
mark(U11(X1,X2,X3)) → active(U11(mark(X1),X2,X3)) (17)
mark(tt) → active(tt) (18)
mark(U12(X1,X2)) → active(U12(mark(X1),X2)) (19)
mark(isNat(X)) → active(isNat(X)) (20)
mark(U13(X)) → active(U13(mark(X))) (21)
mark(U21(X1,X2)) → active(U21(mark(X1),X2)) (22)
mark(U22(X)) → active(U22(mark(X))) (23)
mark(U31(X1,X2)) → active(U31(mark(X1),X2)) (24)
mark(U41(X1,X2,X3)) → active(U41(mark(X1),X2,X3)) (25)
mark(s(X)) → active(s(mark(X))) (26)
mark(plus(X1,X2)) → active(plus(mark(X1),mark(X2))) (27)
mark(and(X1,X2)) → active(and(mark(X1),X2)) (28)
mark(0) → active(0) (29)
mark(isNatKind(X)) → active(isNatKind(X)) (30)
U11(mark(X1),X2,X3) → U11(X1,X2,X3) (31)
U11(X1,mark(X2),X3) → U11(X1,X2,X3) (32)
U11(X1,X2,mark(X3)) → U11(X1,X2,X3) (33)
U11(active(X1),X2,X3) → U11(X1,X2,X3) (34)
U11(X1,active(X2),X3) → U11(X1,X2,X3) (35)
U11(X1,X2,active(X3)) → U11(X1,X2,X3) (36)
U12(mark(X1),X2) → U12(X1,X2) (37)
U12(X1,mark(X2)) → U12(X1,X2) (38)
U12(active(X1),X2) → U12(X1,X2) (39)
U12(X1,active(X2)) → U12(X1,X2) (40)
isNat(mark(X)) → isNat(X) (41)
isNat(active(X)) → isNat(X) (42)
U13(mark(X)) → U13(X) (43)
U13(active(X)) → U13(X) (44)
U21(mark(X1),X2) → U21(X1,X2) (45)
U21(X1,mark(X2)) → U21(X1,X2) (46)
U21(active(X1),X2) → U21(X1,X2) (47)
U21(X1,active(X2)) → U21(X1,X2) (48)
U22(mark(X)) → U22(X) (49)
U22(active(X)) → U22(X) (50)
U31(mark(X1),X2) → U31(X1,X2) (51)
U31(X1,mark(X2)) → U31(X1,X2) (52)
U31(active(X1),X2) → U31(X1,X2) (53)
U31(X1,active(X2)) → U31(X1,X2) (54)
U41(mark(X1),X2,X3) → U41(X1,X2,X3) (55)
U41(X1,mark(X2),X3) → U41(X1,X2,X3) (56)
U41(X1,X2,mark(X3)) → U41(X1,X2,X3) (57)
U41(active(X1),X2,X3) → U41(X1,X2,X3) (58)
U41(X1,active(X2),X3) → U41(X1,X2,X3) (59)
U41(X1,X2,active(X3)) → U41(X1,X2,X3) (60)
s(mark(X)) → s(X) (61)
s(active(X)) → s(X) (62)
plus(mark(X1),X2) → plus(X1,X2) (63)
plus(X1,mark(X2)) → plus(X1,X2) (64)
plus(active(X1),X2) → plus(X1,X2) (65)
plus(X1,active(X2)) → plus(X1,X2) (66)
and(mark(X1),X2) → and(X1,X2) (67)
and(X1,mark(X2)) → and(X1,X2) (68)
and(active(X1),X2) → and(X1,X2) (69)
and(X1,active(X2)) → and(X1,X2) (70)
isNatKind(mark(X)) → isNatKind(X) (71)
isNatKind(active(X)) → isNatKind(X) (72)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(U11) = 3 stat(U11) = mul
prec(tt) = 0 stat(tt) = mul
prec(U12) = 2 stat(U12) = mul
prec(isNat) = 2 stat(isNat) = mul
prec(U21) = 2 stat(U21) = mul
prec(U31) = 4 stat(U31) = mul
prec(U41) = 6 stat(U41) = lex
prec(s) = 2 stat(s) = mul
prec(plus) = 6 stat(plus) = lex
prec(and) = 5 stat(and) = lex
prec(0) = 0 stat(0) = mul
prec(isNatKind) = 1 stat(isNatKind) = mul

π(active) = 1
π(U11) = [1,2,3]
π(tt) = []
π(mark) = 1
π(U12) = [1,2]
π(isNat) = [1]
π(U13) = 1
π(U21) = [1,2]
π(U22) = 1
π(U31) = [1,2]
π(U41) = [3,2,1]
π(s) = [1]
π(plus) = [1,2]
π(and) = [2,1]
π(0) = []
π(isNatKind) = [1]

all of the following rules can be deleted.
active(U11(tt,V1,V2)) → mark(U12(isNat(V1),V2)) (1)
active(U12(tt,V2)) → mark(U13(isNat(V2))) (2)
active(U21(tt,V1)) → mark(U22(isNat(V1))) (4)
active(U31(tt,N)) → mark(N) (6)
active(U41(tt,M,N)) → mark(s(plus(N,M))) (7)
active(and(tt,X)) → mark(X) (8)
active(isNat(0)) → mark(tt) (9)
active(isNat(plus(V1,V2))) → mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) (10)
active(isNat(s(V1))) → mark(U21(isNatKind(V1),V1)) (11)
active(isNatKind(0)) → mark(tt) (12)
active(isNatKind(plus(V1,V2))) → mark(and(isNatKind(V1),isNatKind(V2))) (13)
active(isNatKind(s(V1))) → mark(isNatKind(V1)) (14)
active(plus(N,0)) → mark(U31(and(isNat(N),isNatKind(N)),N)) (15)
active(plus(N,s(M))) → mark(U41(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) (16)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 + 1 · x1
[U13(x1)] = 2 + 1 · x1
[tt] = 2
[mark(x1)] = 2 · x1
[U22(x1)] = 2 + 1 · x1
[U11(x1, x2, x3)] = 2 + 2 · x1 + 1 · x2 + 2 · x3
[U12(x1, x2)] = 2 + 1 · x1 + 1 · x2
[isNat(x1)] = 2 + 1 · x1
[U21(x1, x2)] = 2 + 1 · x1 + 2 · x2
[U31(x1, x2)] = 2 + 1 · x1 + 1 · x2
[U41(x1, x2, x3)] = 2 + 1 · x1 + 1 · x2 + 1 · x3
[s(x1)] = 2 + 1 · x1
[plus(x1, x2)] = 2 + 2 · x1 + 1 · x2
[and(x1, x2)] = 2 + 1 · x1 + 1 · x2
[0] = 2
[isNatKind(x1)] = 2 + 1 · x1
all of the following rules can be deleted.
active(U13(tt)) → mark(tt) (3)
active(U22(tt)) → mark(tt) (5)
mark(U11(X1,X2,X3)) → active(U11(mark(X1),X2,X3)) (17)
mark(tt) → active(tt) (18)
mark(U12(X1,X2)) → active(U12(mark(X1),X2)) (19)
mark(isNat(X)) → active(isNat(X)) (20)
mark(U13(X)) → active(U13(mark(X))) (21)
mark(U21(X1,X2)) → active(U21(mark(X1),X2)) (22)
mark(U22(X)) → active(U22(mark(X))) (23)
mark(U31(X1,X2)) → active(U31(mark(X1),X2)) (24)
mark(U41(X1,X2,X3)) → active(U41(mark(X1),X2,X3)) (25)
mark(s(X)) → active(s(mark(X))) (26)
mark(plus(X1,X2)) → active(plus(mark(X1),mark(X2))) (27)
mark(and(X1,X2)) → active(and(mark(X1),X2)) (28)
mark(0) → active(0) (29)
mark(isNatKind(X)) → active(isNatKind(X)) (30)
U11(active(X1),X2,X3) → U11(X1,X2,X3) (34)
U11(X1,active(X2),X3) → U11(X1,X2,X3) (35)
U11(X1,X2,active(X3)) → U11(X1,X2,X3) (36)
U12(active(X1),X2) → U12(X1,X2) (39)
U12(X1,active(X2)) → U12(X1,X2) (40)
isNat(active(X)) → isNat(X) (42)
U13(active(X)) → U13(X) (44)
U21(active(X1),X2) → U21(X1,X2) (47)
U21(X1,active(X2)) → U21(X1,X2) (48)
U22(active(X)) → U22(X) (50)
U31(active(X1),X2) → U31(X1,X2) (53)
U31(X1,active(X2)) → U31(X1,X2) (54)
U41(active(X1),X2,X3) → U41(X1,X2,X3) (58)
U41(X1,active(X2),X3) → U41(X1,X2,X3) (59)
U41(X1,X2,active(X3)) → U41(X1,X2,X3) (60)
s(active(X)) → s(X) (62)
plus(active(X1),X2) → plus(X1,X2) (65)
plus(X1,active(X2)) → plus(X1,X2) (66)
and(active(X1),X2) → and(X1,X2) (69)
and(X1,active(X2)) → and(X1,X2) (70)
isNatKind(active(X)) → isNatKind(X) (72)

1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(mark) = 12 weight(mark) = 0
prec(isNat) = 2 weight(isNat) = 1
prec(U13) = 3 weight(U13) = 1
prec(U22) = 5 weight(U22) = 1
prec(s) = 8 weight(s) = 1
prec(isNatKind) = 11 weight(isNatKind) = 1
prec(U11) = 1 weight(U11) = 0
prec(U12) = 0 weight(U12) = 0
prec(U21) = 4 weight(U21) = 0
prec(U31) = 6 weight(U31) = 0
prec(U41) = 7 weight(U41) = 0
prec(plus) = 9 weight(plus) = 0
prec(and) = 10 weight(and) = 0
all of the following rules can be deleted.
U11(mark(X1),X2,X3) → U11(X1,X2,X3) (31)
U11(X1,mark(X2),X3) → U11(X1,X2,X3) (32)
U11(X1,X2,mark(X3)) → U11(X1,X2,X3) (33)
U12(mark(X1),X2) → U12(X1,X2) (37)
U12(X1,mark(X2)) → U12(X1,X2) (38)
isNat(mark(X)) → isNat(X) (41)
U13(mark(X)) → U13(X) (43)
U21(mark(X1),X2) → U21(X1,X2) (45)
U21(X1,mark(X2)) → U21(X1,X2) (46)
U22(mark(X)) → U22(X) (49)
U31(mark(X1),X2) → U31(X1,X2) (51)
U31(X1,mark(X2)) → U31(X1,X2) (52)
U41(mark(X1),X2,X3) → U41(X1,X2,X3) (55)
U41(X1,mark(X2),X3) → U41(X1,X2,X3) (56)
U41(X1,X2,mark(X3)) → U41(X1,X2,X3) (57)
s(mark(X)) → s(X) (61)
plus(mark(X1),X2) → plus(X1,X2) (63)
plus(X1,mark(X2)) → plus(X1,X2) (64)
and(mark(X1),X2) → and(X1,X2) (67)
and(X1,mark(X2)) → and(X1,X2) (68)
isNatKind(mark(X)) → isNatKind(X) (71)

1.1.1.1 R is empty

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