Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/MYNAT_complete_C)

The rewrite relation of the following TRS is considered.

There are 101 ruless (increase limit for explicit display).

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(U11) = 1 stat(U11) = lex
prec(tt) = 5 stat(tt) = mul
prec(U12) = 0 stat(U12) = mul
prec(isNat) = 0 stat(isNat) = mul
prec(U21) = 0 stat(U21) = mul
prec(U31) = 6 stat(U31) = lex
prec(U32) = 5 stat(U32) = mul
prec(U41) = 2 stat(U41) = mul
prec(U51) = 4 stat(U51) = lex
prec(s) = 0 stat(s) = mul
prec(plus) = 4 stat(plus) = lex
prec(U61) = 8 stat(U61) = mul
prec(0) = 7 stat(0) = mul
prec(U71) = 9 stat(U71) = lex
prec(x) = 9 stat(x) = lex
prec(and) = 3 stat(and) = mul
prec(top) = 10 stat(top) = mul

π(active) = 1
π(U11) = [3,2,1]
π(tt) = []
π(mark) = 1
π(U12) = [1,2]
π(isNat) = [1]
π(U13) = 1
π(U21) = [1,2]
π(U22) = 1
π(U31) = [3,1,2]
π(U32) = [1,2]
π(U33) = 1
π(U41) = [1,2]
π(U51) = [3,2,1]
π(s) = [1]
π(plus) = [1,2]
π(U61) = [1]
π(0) = []
π(U71) = [3,2,1]
π(x) = [1,2]
π(and) = [1,2]
π(isNatKind) = 1
π(proper) = 1
π(ok) = 1
π(top) = [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,V1,V2)) → mark(U32(isNat(V1),V2)) (6)
active(U32(tt,V2)) → mark(U33(isNat(V2))) (7)
active(U41(tt,N)) → mark(N) (9)
active(U51(tt,M,N)) → mark(s(plus(N,M))) (10)
active(U61(tt)) → mark(0) (11)
active(U71(tt,M,N)) → mark(plus(x(N,M),N)) (12)
active(and(tt,X)) → mark(X) (13)
active(isNat(0)) → mark(tt) (14)
active(isNat(plus(V1,V2))) → mark(U11(and(isNatKind(V1),isNatKind(V2)),V1,V2)) (15)
active(isNat(s(V1))) → mark(U21(isNatKind(V1),V1)) (16)
active(isNat(x(V1,V2))) → mark(U31(and(isNatKind(V1),isNatKind(V2)),V1,V2)) (17)
active(isNatKind(0)) → mark(tt) (18)
active(isNatKind(plus(V1,V2))) → mark(and(isNatKind(V1),isNatKind(V2))) (19)
active(isNatKind(s(V1))) → mark(isNatKind(V1)) (20)
active(isNatKind(x(V1,V2))) → mark(and(isNatKind(V1),isNatKind(V2))) (21)
active(plus(N,0)) → mark(U41(and(isNat(N),isNatKind(N)),N)) (22)
active(plus(N,s(M))) → mark(U51(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) (23)
active(x(N,0)) → mark(U61(and(isNat(N),isNatKind(N)))) (24)
active(x(N,s(M))) → mark(U71(and(and(isNat(M),isNatKind(M)),and(isNat(N),isNatKind(N))),M,N)) (25)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U13(x1)] = 2 · x1
[tt] = 2
[mark(x1)] = 1 · x1
[U22(x1)] = 1 · x1
[U33(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[U12(x1, x2)] = 2 · x1 + 2 · x2
[U21(x1, x2)] = 2 · x1 + 2 · x2
[U31(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[U32(x1, x2)] = 1 · x1 + 2 · x2
[U41(x1, x2)] = 2 · x1 + 2 · x2
[U51(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[s(x1)] = 1 · x1
[plus(x1, x2)] = 2 · x1 + 2 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 1 · x1 + 1 · x2 + 2 · x3
[x(x1, x2)] = 1 · x1 + 2 · x2
[and(x1, x2)] = 2 · x1 + 2 · x2
[proper(x1)] = 1 · x1
[ok(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
[0] = 0
[isNatKind(x1)] = 1 · x1
[top(x1)] = 2 · x1
all of the following rules can be deleted.
active(U13(tt)) → mark(tt) (3)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U22(x1)] = 1 · x1
[tt] = 0
[mark(x1)] = 1 · x1
[U33(x1)] = 1 + 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 1 · x2 + 2 · x3
[U12(x1, x2)] = 1 · x1 + 2 · x2
[U13(x1)] = 1 · x1
[U21(x1, x2)] = 1 · x1 + 2 · x2
[U31(x1, x2, x3)] = 1 · x1 + 2 · x2 + 1 · x3
[U32(x1, x2)] = 2 · x1 + 2 · x2
[U41(x1, x2)] = 2 · x1 + 2 · x2
[U51(x1, x2, x3)] = 1 · x1 + 2 · x2 + 1 · x3
[s(x1)] = 2 · x1
[plus(x1, x2)] = 2 · x1 + 1 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 1 · x1 + 2 · x2 + 1 · x3
[x(x1, x2)] = 1 · x1 + 2 · x2
[and(x1, x2)] = 2 · x1 + 2 · x2
[proper(x1)] = 1 · x1
[ok(x1)] = 1 · x1
[isNat(x1)] = 2 · x1
[0] = 0
[isNatKind(x1)] = 2 · x1
[top(x1)] = 2 · x1
all of the following rules can be deleted.
active(U33(tt)) → mark(tt) (8)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U22(x1)] = 1 + 2 · x1
[tt] = 2
[mark(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[U12(x1, x2)] = 2 · x1 + 2 · x2
[U13(x1)] = 1 · x1
[U21(x1, x2)] = 1 · x1 + 1 · x2
[U31(x1, x2, x3)] = 2 · x1 + 2 · x2 + 1 · x3
[U32(x1, x2)] = 2 · x1 + 2 · x2
[U33(x1)] = 2 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U51(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[s(x1)] = 2 · x1
[plus(x1, x2)] = 2 · x1 + 2 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 · x1 + 1 · x2 + 2 · x3
[x(x1, x2)] = 2 · x1 + 2 · x2
[and(x1, x2)] = 1 · x1 + 2 · x2
[proper(x1)] = 1 · x1
[ok(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
[0] = 0
[isNatKind(x1)] = 2 · x1
[top(x1)] = 2 · x1
all of the following rules can be deleted.
active(U22(tt)) → mark(tt) (5)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 2 · x2 + 1 · x3
[U12(x1, x2)] = 2 · x1 + 2 · x2
[U13(x1)] = 2 · x1
[U21(x1, x2)] = 1 · x1 + 1 · x2
[U22(x1)] = 1 · x1
[U31(x1, x2, x3)] = 2 · x1 + 1 · x2 + 2 · x3
[U32(x1, x2)] = 2 · x1 + 2 · x2
[U33(x1)] = 2 · x1
[U41(x1, x2)] = 2 · x1 + 1 · x2
[U51(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[s(x1)] = 2 · x1
[plus(x1, x2)] = 1 · x1 + 2 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 · x1 + 2 · x2 + 1 · x3
[x(x1, x2)] = 2 · x1 + 2 · x2
[and(x1, x2)] = 1 · x1 + 2 · x2
[mark(x1)] = 1 + 1 · x1
[proper(x1)] = 1 · x1
[tt] = 0
[ok(x1)] = 1 · x1
[isNat(x1)] = 2 · x1
[0] = 0
[isNatKind(x1)] = 2 · x1
[top(x1)] = 1 · x1
all of the following rules can be deleted.
U11(mark(X1),X2,X3) → mark(U11(X1,X2,X3)) (44)
U12(mark(X1),X2) → mark(U12(X1,X2)) (45)
U13(mark(X)) → mark(U13(X)) (46)
U31(mark(X1),X2,X3) → mark(U31(X1,X2,X3)) (49)
U32(mark(X1),X2) → mark(U32(X1,X2)) (50)
U33(mark(X)) → mark(U33(X)) (51)
U41(mark(X1),X2) → mark(U41(X1,X2)) (52)
U51(mark(X1),X2,X3) → mark(U51(X1,X2,X3)) (53)
s(mark(X)) → mark(s(X)) (54)
plus(X1,mark(X2)) → mark(plus(X1,X2)) (56)
U71(mark(X1),X2,X3) → mark(U71(X1,X2,X3)) (58)
x(mark(X1),X2) → mark(x(X1,X2)) (59)
x(X1,mark(X2)) → mark(x(X1,X2)) (60)
top(mark(X)) → top(proper(X)) (100)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 1 · x2 + 2 · x3
[U12(x1, x2)] = 2 · x1 + 2 · x2
[U13(x1)] = 2 · x1
[U21(x1, x2)] = 2 · x1 + 2 · x2
[U22(x1)] = 2 · x1
[U31(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[U32(x1, x2)] = 2 · x1 + 2 · x2
[U33(x1)] = 1 + 2 · x1
[U41(x1, x2)] = 2 · x1 + 2 · x2
[U51(x1, x2, x3)] = 1 + 2 · x1 + 1 · x2 + 1 · x3
[s(x1)] = 2 · x1
[plus(x1, x2)] = 2 · x1 + 2 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[x(x1, x2)] = 2 · x1 + 2 · x2
[and(x1, x2)] = 2 · x1 + 1 · x2
[mark(x1)] = 1 · x1
[proper(x1)] = 2 · x1
[tt] = 2
[ok(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
[0] = 0
[isNatKind(x1)] = 1 + 1 · x1
[top(x1)] = 1 · x1
all of the following rules can be deleted.
proper(tt) → ok(tt) (63)
proper(U33(X)) → U33(proper(X)) (71)
proper(U51(X1,X2,X3)) → U51(proper(X1),proper(X2),proper(X3)) (73)
proper(isNatKind(X)) → isNatKind(proper(X)) (81)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[U12(x1, x2)] = 1 · x1 + 2 · x2
[U13(x1)] = 1 · x1
[U21(x1, x2)] = 2 · x1 + 1 · x2
[U22(x1)] = 1 · x1
[U31(x1, x2, x3)] = 1 · x1 + 2 · x2 + 1 · x3
[U32(x1, x2)] = 1 · x1 + 2 · x2
[U33(x1)] = 1 · x1
[U41(x1, x2)] = 1 · x1 + 1 · x2
[U51(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[s(x1)] = 2 + 2 · x1
[plus(x1, x2)] = 1 · x1 + 2 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[x(x1, x2)] = 2 · x1 + 1 · x2
[and(x1, x2)] = 1 · x1 + 1 · x2
[mark(x1)] = 1 · x1
[proper(x1)] = 2 · x1
[isNat(x1)] = 1 + 1 · x1
[0] = 0
[ok(x1)] = 1 · x1
[isNatKind(x1)] = 1 · x1
[top(x1)] = 1 · x1
all of the following rules can be deleted.
proper(isNat(X)) → isNat(proper(X)) (65)
proper(s(X)) → s(proper(X)) (74)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 2 · x2 + 1 · x3
[U12(x1, x2)] = 1 · x1 + 2 · x2
[U13(x1)] = 1 · x1
[U21(x1, x2)] = 1 · x1 + 1 · x2
[U22(x1)] = 1 · x1
[U31(x1, x2, x3)] = 2 · x1 + 2 · x2 + 1 · x3
[U32(x1, x2)] = 2 · x1 + 1 · x2
[U33(x1)] = 2 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U51(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[s(x1)] = 2 · x1
[plus(x1, x2)] = 1 · x1 + 2 · x2
[U61(x1)] = 2 + 1 · x1
[U71(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[x(x1, x2)] = 1 · x1 + 1 · x2
[and(x1, x2)] = 1 · x1 + 1 · x2
[mark(x1)] = 1 · x1
[proper(x1)] = 2 · x1
[0] = 0
[ok(x1)] = 1 · x1
[isNat(x1)] = 2 · x1
[isNatKind(x1)] = 2 · x1
[top(x1)] = 2 · x1
all of the following rules can be deleted.
proper(U61(X)) → U61(proper(X)) (76)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[U12(x1, x2)] = 2 · x1 + 1 · x2
[U13(x1)] = 1 · x1
[U21(x1, x2)] = 2 · x1 + 2 · x2
[U22(x1)] = 1 · x1
[U31(x1, x2, x3)] = 1 + 2 · x1 + 1 · x2 + 2 · x3
[U32(x1, x2)] = 2 · x1 + 2 · x2
[U33(x1)] = 2 · x1
[U41(x1, x2)] = 2 · x1 + 2 · x2
[U51(x1, x2, x3)] = 1 · x1 + 2 · x2 + 1 · x3
[s(x1)] = 1 · x1
[plus(x1, x2)] = 2 · x1 + 1 · x2
[U61(x1)] = 2 · x1
[U71(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[x(x1, x2)] = 2 · x1 + 2 · x2
[and(x1, x2)] = 1 · x1 + 2 · x2
[mark(x1)] = 1 + 1 · x1
[proper(x1)] = 2 · x1
[0] = 0
[ok(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
[isNatKind(x1)] = 1 · x1
[top(x1)] = 2 · x1
all of the following rules can be deleted.
U21(mark(X1),X2) → mark(U21(X1,X2)) (47)
plus(mark(X1),X2) → mark(plus(X1,X2)) (55)
U61(mark(X)) → mark(U61(X)) (57)
proper(U31(X1,X2,X3)) → U31(proper(X1),proper(X2),proper(X3)) (69)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[active(x1)] = 1 · x1
[U11(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[U12(x1, x2)] = 1 · x1 + 1 · x2
[U13(x1)] = 1 · x1
[U21(x1, x2)] = 1 · x1 + 1 · x2
[U22(x1)] = 1 · x1
[U31(x1, x2, x3)] = 1 · x1 + 2 · x2 + 2 · x3
[U32(x1, x2)] = 2 · x1 + 2 · x2
[U33(x1)] = 2 · x1
[U41(x1, x2)] = 1 · x1 + 2 · x2
[U51(x1, x2, x3)] = 2 · x1 + 2 · x2 + 2 · x3
[s(x1)] = 2 · x1
[plus(x1, x2)] = 2 · x1 + 2 · x2
[U61(x1)] = 1 · x1
[U71(x1, x2, x3)] = 2 · x1 + 1 · x2 + 2 · x3
[x(x1, x2)] = 2 · x1 + 2 · x2
[and(x1, x2)] = 2 · x1 + 2 · x2
[mark(x1)] = 2 + 1 · x1
[proper(x1)] = 2 · x1
[0] = 1
[ok(x1)] = 1 · x1
[isNat(x1)] = 1 · x1
[isNatKind(x1)] = 2 · x1
[top(x1)] = 1 · x1
all of the following rules can be deleted.
and(mark(X1),X2) → mark(and(X1,X2)) (61)
proper(0) → ok(0) (77)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(active) = 21 weight(active) = 3
prec(U13) = 10 weight(U13) = 5
prec(U22) = 11 weight(U22) = 5
prec(U33) = 14 weight(U33) = 5
prec(s) = 17 weight(s) = 5
prec(U61) = 16 weight(U61) = 5
prec(mark) = 8 weight(mark) = 1
prec(proper) = 22 weight(proper) = 0
prec(ok) = 9 weight(ok) = 4
prec(isNat) = 15 weight(isNat) = 5
prec(isNatKind) = 18 weight(isNatKind) = 5
prec(top) = 19 weight(top) = 1
prec(U11) = 5 weight(U11) = 0
prec(U12) = 0 weight(U12) = 0
prec(U21) = 12 weight(U21) = 0
prec(U31) = 20 weight(U31) = 0
prec(U32) = 1 weight(U32) = 0
prec(U41) = 2 weight(U41) = 0
prec(U51) = 3 weight(U51) = 0
prec(plus) = 13 weight(plus) = 0
prec(U71) = 4 weight(U71) = 0
prec(x) = 6 weight(x) = 0
prec(and) = 7 weight(and) = 0
all of the following rules can be deleted.
active(U11(X1,X2,X3)) → U11(active(X1),X2,X3) (26)
active(U12(X1,X2)) → U12(active(X1),X2) (27)
active(U13(X)) → U13(active(X)) (28)
active(U21(X1,X2)) → U21(active(X1),X2) (29)
active(U22(X)) → U22(active(X)) (30)
active(U31(X1,X2,X3)) → U31(active(X1),X2,X3) (31)
active(U32(X1,X2)) → U32(active(X1),X2) (32)
active(U33(X)) → U33(active(X)) (33)
active(U41(X1,X2)) → U41(active(X1),X2) (34)
active(U51(X1,X2,X3)) → U51(active(X1),X2,X3) (35)
active(s(X)) → s(active(X)) (36)
active(plus(X1,X2)) → plus(active(X1),X2) (37)
active(plus(X1,X2)) → plus(X1,active(X2)) (38)
active(U61(X)) → U61(active(X)) (39)
active(U71(X1,X2,X3)) → U71(active(X1),X2,X3) (40)
active(x(X1,X2)) → x(active(X1),X2) (41)
active(x(X1,X2)) → x(X1,active(X2)) (42)
active(and(X1,X2)) → and(active(X1),X2) (43)
U22(mark(X)) → mark(U22(X)) (48)
proper(U11(X1,X2,X3)) → U11(proper(X1),proper(X2),proper(X3)) (62)
proper(U12(X1,X2)) → U12(proper(X1),proper(X2)) (64)
proper(U13(X)) → U13(proper(X)) (66)
proper(U21(X1,X2)) → U21(proper(X1),proper(X2)) (67)
proper(U22(X)) → U22(proper(X)) (68)
proper(U32(X1,X2)) → U32(proper(X1),proper(X2)) (70)
proper(U41(X1,X2)) → U41(proper(X1),proper(X2)) (72)
proper(plus(X1,X2)) → plus(proper(X1),proper(X2)) (75)
proper(U71(X1,X2,X3)) → U71(proper(X1),proper(X2),proper(X3)) (78)
proper(x(X1,X2)) → x(proper(X1),proper(X2)) (79)
proper(and(X1,X2)) → and(proper(X1),proper(X2)) (80)
U11(ok(X1),ok(X2),ok(X3)) → ok(U11(X1,X2,X3)) (82)
U12(ok(X1),ok(X2)) → ok(U12(X1,X2)) (83)
isNat(ok(X)) → ok(isNat(X)) (84)
U13(ok(X)) → ok(U13(X)) (85)
U21(ok(X1),ok(X2)) → ok(U21(X1,X2)) (86)
U22(ok(X)) → ok(U22(X)) (87)
U31(ok(X1),ok(X2),ok(X3)) → ok(U31(X1,X2,X3)) (88)
U32(ok(X1),ok(X2)) → ok(U32(X1,X2)) (89)
U33(ok(X)) → ok(U33(X)) (90)
U41(ok(X1),ok(X2)) → ok(U41(X1,X2)) (91)
U51(ok(X1),ok(X2),ok(X3)) → ok(U51(X1,X2,X3)) (92)
s(ok(X)) → ok(s(X)) (93)
plus(ok(X1),ok(X2)) → ok(plus(X1,X2)) (94)
U61(ok(X)) → ok(U61(X)) (95)
U71(ok(X1),ok(X2),ok(X3)) → ok(U71(X1,X2,X3)) (96)
x(ok(X1),ok(X2)) → ok(x(X1,X2)) (97)
and(ok(X1),ok(X2)) → ok(and(X1,X2)) (98)
isNatKind(ok(X)) → ok(isNatKind(X)) (99)
top(ok(X)) → top(active(X)) (101)

1.1.1.1.1.1.1.1.1.1.1.1 R is empty

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