Certification Problem
Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_nokinds_noand_GM)
The rewrite relation of the following TRS is considered.
a__U11(tt,V2) |
→ |
a__U12(a__isNat(V2)) |
(1) |
a__U12(tt) |
→ |
tt |
(2) |
a__U21(tt) |
→ |
tt |
(3) |
a__U31(tt,N) |
→ |
mark(N) |
(4) |
a__U41(tt,M,N) |
→ |
a__U42(a__isNat(N),M,N) |
(5) |
a__U42(tt,M,N) |
→ |
s(a__plus(mark(N),mark(M))) |
(6) |
a__isNat(0) |
→ |
tt |
(7) |
a__isNat(plus(V1,V2)) |
→ |
a__U11(a__isNat(V1),V2) |
(8) |
a__isNat(s(V1)) |
→ |
a__U21(a__isNat(V1)) |
(9) |
a__plus(N,0) |
→ |
a__U31(a__isNat(N),N) |
(10) |
a__plus(N,s(M)) |
→ |
a__U41(a__isNat(M),M,N) |
(11) |
mark(U11(X1,X2)) |
→ |
a__U11(mark(X1),X2) |
(12) |
mark(U12(X)) |
→ |
a__U12(mark(X)) |
(13) |
mark(isNat(X)) |
→ |
a__isNat(X) |
(14) |
mark(U21(X)) |
→ |
a__U21(mark(X)) |
(15) |
mark(U31(X1,X2)) |
→ |
a__U31(mark(X1),X2) |
(16) |
mark(U41(X1,X2,X3)) |
→ |
a__U41(mark(X1),X2,X3) |
(17) |
mark(U42(X1,X2,X3)) |
→ |
a__U42(mark(X1),X2,X3) |
(18) |
mark(plus(X1,X2)) |
→ |
a__plus(mark(X1),mark(X2)) |
(19) |
mark(tt) |
→ |
tt |
(20) |
mark(s(X)) |
→ |
s(mark(X)) |
(21) |
mark(0) |
→ |
0 |
(22) |
a__U11(X1,X2) |
→ |
U11(X1,X2) |
(23) |
a__U12(X) |
→ |
U12(X) |
(24) |
a__isNat(X) |
→ |
isNat(X) |
(25) |
a__U21(X) |
→ |
U21(X) |
(26) |
a__U31(X1,X2) |
→ |
U31(X1,X2) |
(27) |
a__U41(X1,X2,X3) |
→ |
U41(X1,X2,X3) |
(28) |
a__U42(X1,X2,X3) |
→ |
U42(X1,X2,X3) |
(29) |
a__plus(X1,X2) |
→ |
plus(X1,X2) |
(30) |
Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by AProVE @ termCOMP 2023)
1 Dependency Pair Transformation
The following set of initial dependency pairs has been identified.
a__U11#(tt,V2) |
→ |
a__U12#(a__isNat(V2)) |
(31) |
a__U11#(tt,V2) |
→ |
a__isNat#(V2) |
(32) |
a__U31#(tt,N) |
→ |
mark#(N) |
(33) |
a__U41#(tt,M,N) |
→ |
a__U42#(a__isNat(N),M,N) |
(34) |
a__U41#(tt,M,N) |
→ |
a__isNat#(N) |
(35) |
a__U42#(tt,M,N) |
→ |
a__plus#(mark(N),mark(M)) |
(36) |
a__U42#(tt,M,N) |
→ |
mark#(N) |
(37) |
a__U42#(tt,M,N) |
→ |
mark#(M) |
(38) |
a__isNat#(plus(V1,V2)) |
→ |
a__U11#(a__isNat(V1),V2) |
(39) |
a__isNat#(plus(V1,V2)) |
→ |
a__isNat#(V1) |
(40) |
a__isNat#(s(V1)) |
→ |
a__U21#(a__isNat(V1)) |
(41) |
a__isNat#(s(V1)) |
→ |
a__isNat#(V1) |
(42) |
a__plus#(N,0) |
→ |
a__U31#(a__isNat(N),N) |
(43) |
a__plus#(N,0) |
→ |
a__isNat#(N) |
(44) |
a__plus#(N,s(M)) |
→ |
a__U41#(a__isNat(M),M,N) |
(45) |
a__plus#(N,s(M)) |
→ |
a__isNat#(M) |
(46) |
mark#(U11(X1,X2)) |
→ |
a__U11#(mark(X1),X2) |
(47) |
mark#(U11(X1,X2)) |
→ |
mark#(X1) |
(48) |
mark#(U12(X)) |
→ |
a__U12#(mark(X)) |
(49) |
mark#(U12(X)) |
→ |
mark#(X) |
(50) |
mark#(isNat(X)) |
→ |
a__isNat#(X) |
(51) |
mark#(U21(X)) |
→ |
a__U21#(mark(X)) |
(52) |
mark#(U21(X)) |
→ |
mark#(X) |
(53) |
mark#(U31(X1,X2)) |
→ |
a__U31#(mark(X1),X2) |
(54) |
mark#(U31(X1,X2)) |
→ |
mark#(X1) |
(55) |
mark#(U41(X1,X2,X3)) |
→ |
a__U41#(mark(X1),X2,X3) |
(56) |
mark#(U41(X1,X2,X3)) |
→ |
mark#(X1) |
(57) |
mark#(U42(X1,X2,X3)) |
→ |
a__U42#(mark(X1),X2,X3) |
(58) |
mark#(U42(X1,X2,X3)) |
→ |
mark#(X1) |
(59) |
mark#(plus(X1,X2)) |
→ |
a__plus#(mark(X1),mark(X2)) |
(60) |
mark#(plus(X1,X2)) |
→ |
mark#(X1) |
(61) |
mark#(plus(X1,X2)) |
→ |
mark#(X2) |
(62) |
mark#(s(X)) |
→ |
mark#(X) |
(63) |
1.1 Dependency Graph Processor
The dependency pairs are split into 2
components.
-
The
1st
component contains the
pair
mark#(U11(X1,X2)) |
→ |
mark#(X1) |
(48) |
mark#(U12(X)) |
→ |
mark#(X) |
(50) |
mark#(U21(X)) |
→ |
mark#(X) |
(53) |
mark#(U31(X1,X2)) |
→ |
a__U31#(mark(X1),X2) |
(54) |
a__U31#(tt,N) |
→ |
mark#(N) |
(33) |
mark#(U31(X1,X2)) |
→ |
mark#(X1) |
(55) |
mark#(U41(X1,X2,X3)) |
→ |
a__U41#(mark(X1),X2,X3) |
(56) |
a__U41#(tt,M,N) |
→ |
a__U42#(a__isNat(N),M,N) |
(34) |
a__U42#(tt,M,N) |
→ |
a__plus#(mark(N),mark(M)) |
(36) |
a__plus#(N,0) |
→ |
a__U31#(a__isNat(N),N) |
(43) |
a__plus#(N,s(M)) |
→ |
a__U41#(a__isNat(M),M,N) |
(45) |
a__U42#(tt,M,N) |
→ |
mark#(N) |
(37) |
mark#(U41(X1,X2,X3)) |
→ |
mark#(X1) |
(57) |
mark#(U42(X1,X2,X3)) |
→ |
a__U42#(mark(X1),X2,X3) |
(58) |
a__U42#(tt,M,N) |
→ |
mark#(M) |
(38) |
mark#(U42(X1,X2,X3)) |
→ |
mark#(X1) |
(59) |
mark#(plus(X1,X2)) |
→ |
a__plus#(mark(X1),mark(X2)) |
(60) |
mark#(plus(X1,X2)) |
→ |
mark#(X1) |
(61) |
mark#(plus(X1,X2)) |
→ |
mark#(X2) |
(62) |
mark#(s(X)) |
→ |
mark#(X) |
(63) |
1.1.1 Reduction Pair Processor
Using the linear polynomial interpretation over the naturals
[a__plus#(x1, x2)] |
= |
2 · x1 + 2 · x2
|
[a__U31#(x1, x2)] |
= |
2 + 2 · x2
|
[a__U41#(x1, x2, x3)] |
= |
2 · x2 + 2 · x3
|
[a__U42#(x1, x2, x3)] |
= |
2 · x2 + 2 · x3
|
[mark(x1)] |
= |
x1 |
[U11(x1, x2)] |
= |
2 · x1
|
[a__U11(x1, x2)] |
= |
2 · x1
|
[U12(x1)] |
= |
2 · x1
|
[a__U12(x1)] |
= |
2 · x1
|
[isNat(x1)] |
= |
0 |
[a__isNat(x1)] |
= |
0 |
[U21(x1)] |
= |
2 · x1
|
[a__U21(x1)] |
= |
2 · x1
|
[U31(x1, x2)] |
= |
2 + x1 + x2
|
[a__U31(x1, x2)] |
= |
2 + x1 + x2
|
[tt] |
= |
0 |
[plus(x1, x2)] |
= |
x1 + 2 · x2
|
[a__plus(x1, x2)] |
= |
x1 + 2 · x2
|
[0] |
= |
1 |
[U41(x1, x2, x3)] |
= |
2 + 2 · x1 + 2 · x2 + x3
|
[a__U41(x1, x2, x3)] |
= |
2 + 2 · x1 + 2 · x2 + x3
|
[U42(x1, x2, x3)] |
= |
2 + x1 + 2 · x2 + x3
|
[a__U42(x1, x2, x3)] |
= |
2 + x1 + 2 · x2 + x3
|
[s(x1)] |
= |
2 + x1
|
[mark#(x1)] |
= |
2 · x1
|
the
pairs
mark#(U31(X1,X2)) |
→ |
a__U31#(mark(X1),X2) |
(54) |
a__U31#(tt,N) |
→ |
mark#(N) |
(33) |
mark#(U31(X1,X2)) |
→ |
mark#(X1) |
(55) |
mark#(U41(X1,X2,X3)) |
→ |
a__U41#(mark(X1),X2,X3) |
(56) |
a__plus#(N,s(M)) |
→ |
a__U41#(a__isNat(M),M,N) |
(45) |
mark#(U41(X1,X2,X3)) |
→ |
mark#(X1) |
(57) |
mark#(U42(X1,X2,X3)) |
→ |
a__U42#(mark(X1),X2,X3) |
(58) |
mark#(U42(X1,X2,X3)) |
→ |
mark#(X1) |
(59) |
mark#(s(X)) |
→ |
mark#(X) |
(63) |
could be deleted.
1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
1st
component contains the
pair
mark#(U12(X)) |
→ |
mark#(X) |
(50) |
mark#(U11(X1,X2)) |
→ |
mark#(X1) |
(48) |
mark#(U21(X)) |
→ |
mark#(X) |
(53) |
mark#(plus(X1,X2)) |
→ |
mark#(X1) |
(61) |
mark#(plus(X1,X2)) |
→ |
mark#(X2) |
(62) |
1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[U12(x1)] |
= |
1 · x1
|
[U11(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[U21(x1)] |
= |
1 · x1
|
[plus(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[mark#(x1)] |
= |
1 · x1
|
having no usable rules (w.r.t. the implicit argument filter of the
reduction pair),
the
rule
could be deleted.
1.1.1.1.1.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
mark#(U12(X)) |
→ |
mark#(X) |
(50) |
|
1 |
> |
1 |
mark#(U11(X1,X2)) |
→ |
mark#(X1) |
(48) |
|
1 |
> |
1 |
mark#(U21(X)) |
→ |
mark#(X) |
(53) |
|
1 |
> |
1 |
mark#(plus(X1,X2)) |
→ |
mark#(X1) |
(61) |
|
1 |
> |
1 |
mark#(plus(X1,X2)) |
→ |
mark#(X2) |
(62) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
-
The
2nd
component contains the
pair
a__U11#(tt,V2) |
→ |
a__isNat#(V2) |
(32) |
a__isNat#(plus(V1,V2)) |
→ |
a__U11#(a__isNat(V1),V2) |
(39) |
a__isNat#(plus(V1,V2)) |
→ |
a__isNat#(V1) |
(40) |
a__isNat#(s(V1)) |
→ |
a__isNat#(V1) |
(42) |
1.1.2 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals
[a__isNat(x1)] |
= |
1 · x1
|
[0] |
= |
0 |
[tt] |
= |
0 |
[plus(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[a__U11(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[s(x1)] |
= |
1 · x1
|
[a__U21(x1)] |
= |
1 · x1
|
[isNat(x1)] |
= |
1 · x1
|
[U21(x1)] |
= |
1 · x1
|
[a__U12(x1)] |
= |
1 · x1
|
[U11(x1, x2)] |
= |
1 · x1 + 1 · x2
|
[U12(x1)] |
= |
1 · x1
|
[a__isNat#(x1)] |
= |
1 · x1
|
[a__U11#(x1, x2)] |
= |
1 · x1 + 1 · x2
|
together with the usable
rules
a__isNat(0) |
→ |
tt |
(7) |
a__isNat(plus(V1,V2)) |
→ |
a__U11(a__isNat(V1),V2) |
(8) |
a__isNat(s(V1)) |
→ |
a__U21(a__isNat(V1)) |
(9) |
a__isNat(X) |
→ |
isNat(X) |
(25) |
a__U21(tt) |
→ |
tt |
(3) |
a__U21(X) |
→ |
U21(X) |
(26) |
a__U11(tt,V2) |
→ |
a__U12(a__isNat(V2)) |
(1) |
a__U11(X1,X2) |
→ |
U11(X1,X2) |
(23) |
a__U12(tt) |
→ |
tt |
(2) |
a__U12(X) |
→ |
U12(X) |
(24) |
(w.r.t. the implicit argument filter of the reduction pair),
the
rule
could be deleted.
1.1.2.1 Size-Change Termination
Using size-change termination in combination with
the subterm criterion
one obtains the following initial size-change graphs.
a__isNat#(plus(V1,V2)) |
→ |
a__U11#(a__isNat(V1),V2) |
(39) |
|
1 |
> |
2 |
a__U11#(tt,V2) |
→ |
a__isNat#(V2) |
(32) |
|
2 |
≥ |
1 |
a__isNat#(plus(V1,V2)) |
→ |
a__isNat#(V1) |
(40) |
|
1 |
> |
1 |
a__isNat#(s(V1)) |
→ |
a__isNat#(V1) |
(42) |
|
1 |
> |
1 |
As there is no critical graph in the transitive closure, there are no infinite chains.