Certification Problem

Input (TPDB TRS_Standard/CiME_04/tree)

The rewrite relation of the following TRS is considered.

0(#)	→	#	(1)
+(x,#)	→	x	(2)
+(#,x)	→	x	(3)
+(0(x),0(y))	→	0(+(x,y))	(4)
+(0(x),1(y))	→	1(+(x,y))	(5)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
+(x,+(y,z))	→	+(+(x,y),z)	(8)
-(x,#)	→	x	(9)
-(#,x)	→	#	(10)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(1(x),0(y))	→	1(-(x,y))	(13)
-(1(x),1(y))	→	0(-(x,y))	(14)
not(false)	→	true	(15)
not(true)	→	false	(16)
and(x,true)	→	x	(17)
and(x,false)	→	false	(18)
if(true,x,y)	→	x	(19)
if(false,x,y)	→	y	(20)
ge(0(x),0(y))	→	ge(x,y)	(21)
ge(0(x),1(y))	→	not(ge(y,x))	(22)
ge(1(x),0(y))	→	ge(x,y)	(23)
ge(1(x),1(y))	→	ge(x,y)	(24)
ge(x,#)	→	true	(25)
ge(#,1(x))	→	false	(26)
ge(#,0(x))	→	ge(#,x)	(27)
val(l(x))	→	x	(28)
val(n(x,y,z))	→	x	(29)
min(l(x))	→	x	(30)
min(n(x,y,z))	→	min(y)	(31)
max(l(x))	→	x	(32)
max(n(x,y,z))	→	max(z)	(33)
bs(l(x))	→	true	(34)
bs(n(x,y,z))	→	and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))	(35)
size(l(x))	→	1(#)	(36)
size(n(x,y,z))	→	+(+(size(x),size(y)),1(#))	(37)
wb(l(x))	→	true	(38)
wb(n(x,y,z))	→	and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z)))	(39)

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.

+^#(0(x),0(y))	→	0^#(+(x,y))	(40)
+^#(0(x),0(y))	→	+^#(x,y)	(41)
+^#(0(x),1(y))	→	+^#(x,y)	(42)
+^#(1(x),0(y))	→	+^#(x,y)	(43)
+^#(1(x),1(y))	→	0^#(+(+(x,y),1(#)))	(44)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(45)
+^#(1(x),1(y))	→	+^#(x,y)	(46)
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(47)
+^#(x,+(y,z))	→	+^#(x,y)	(48)
-^#(0(x),0(y))	→	0^#(-(x,y))	(49)
-^#(0(x),0(y))	→	-^#(x,y)	(50)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(51)
-^#(0(x),1(y))	→	-^#(x,y)	(52)
-^#(1(x),0(y))	→	-^#(x,y)	(53)
-^#(1(x),1(y))	→	0^#(-(x,y))	(54)
-^#(1(x),1(y))	→	-^#(x,y)	(55)
ge^#(0(x),0(y))	→	ge^#(x,y)	(56)
ge^#(0(x),1(y))	→	not^#(ge(y,x))	(57)
ge^#(0(x),1(y))	→	ge^#(y,x)	(58)
ge^#(1(x),0(y))	→	ge^#(x,y)	(59)
ge^#(1(x),1(y))	→	ge^#(x,y)	(60)
ge^#(#,0(x))	→	ge^#(#,x)	(61)
min^#(n(x,y,z))	→	min^#(y)	(62)
max^#(n(x,y,z))	→	max^#(z)	(63)
bs^#(n(x,y,z))	→	and^#(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z)))	(64)
bs^#(n(x,y,z))	→	and^#(ge(x,max(y)),ge(min(z),x))	(65)
bs^#(n(x,y,z))	→	ge^#(x,max(y))	(66)
bs^#(n(x,y,z))	→	max^#(y)	(67)
bs^#(n(x,y,z))	→	ge^#(min(z),x)	(68)
bs^#(n(x,y,z))	→	min^#(z)	(69)
bs^#(n(x,y,z))	→	and^#(bs(y),bs(z))	(70)
bs^#(n(x,y,z))	→	bs^#(y)	(71)
bs^#(n(x,y,z))	→	bs^#(z)	(72)
size^#(n(x,y,z))	→	+^#(+(size(x),size(y)),1(#))	(73)
size^#(n(x,y,z))	→	+^#(size(x),size(y))	(74)
size^#(n(x,y,z))	→	size^#(x)	(75)
size^#(n(x,y,z))	→	size^#(y)	(76)
wb^#(n(x,y,z))	→	and^#(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z)))	(77)
wb^#(n(x,y,z))	→	if^#(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y))))	(78)
wb^#(n(x,y,z))	→	ge^#(size(y),size(z))	(79)
wb^#(n(x,y,z))	→	size^#(y)	(80)
wb^#(n(x,y,z))	→	size^#(z)	(81)
wb^#(n(x,y,z))	→	ge^#(1(#),-(size(y),size(z)))	(82)
wb^#(n(x,y,z))	→	-^#(size(y),size(z))	(83)
wb^#(n(x,y,z))	→	ge^#(1(#),-(size(z),size(y)))	(84)
wb^#(n(x,y,z))	→	-^#(size(z),size(y))	(85)
wb^#(n(x,y,z))	→	and^#(wb(y),wb(z))	(86)
wb^#(n(x,y,z))	→	wb^#(y)	(87)
wb^#(n(x,y,z))	→	wb^#(z)	(88)

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.

The 1^st component contains the pair

wb^#(n(x,y,z)) → wb^#(z) (88)

wb^#(n(x,y,z)) → wb^#(y) (87)

1.1.1 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[n(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[wb^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
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.

wb^#(n(x,y,z)) → wb^#(z) (88)

1 > 1

wb^#(n(x,y,z)) → wb^#(y) (87)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair

bs^#(n(x,y,z)) → bs^#(z) (72)

bs^#(n(x,y,z)) → bs^#(y) (71)

1.1.2 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[n(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[bs^#(x₁)] = 1 · x₁

having no usable rules (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.

bs^#(n(x,y,z)) → bs^#(z) (72)

1 > 1

bs^#(n(x,y,z)) → bs^#(y) (71)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair

size^#(n(x,y,z)) → size^#(y) (76)

size^#(n(x,y,z)) → size^#(x) (75)

1.1.3 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[n(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[size^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.3.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

size^#(n(x,y,z)) → size^#(y) (76)

1 > 1

size^#(n(x,y,z)) → size^#(x) (75)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 4^th component contains the pair

ge^#(0(x),1(y))	→	ge^#(y,x)	(58)
ge^#(0(x),0(y))	→	ge^#(x,y)	(56)
ge^#(1(x),0(y))	→	ge^#(x,y)	(59)
ge^#(1(x),1(y))	→	ge^#(x,y)	(60)

1.1.4 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[0(x₁)]	=	1 · x₁
[1(x₁)]	=	1 · x₁
[ge^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.4.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

ge^#(0(x),1(y))	→	ge^#(y,x)	(58)

2	>	1
1	>	2
ge^#(0(x),0(y))	→	ge^#(x,y)	(56)

1	>	1
2	>	2
ge^#(1(x),0(y))	→	ge^#(x,y)	(59)

1	>	1
2	>	2
ge^#(1(x),1(y))	→	ge^#(x,y)	(60)

1	>	1
2	>	2

As there is no critical graph in the transitive closure, there are no infinite chains.

The 5^th component contains the pair

+^#(0(x),1(y))	→	+^#(x,y)	(42)
+^#(0(x),0(y))	→	+^#(x,y)	(41)
+^#(1(x),0(y))	→	+^#(x,y)	(43)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(45)
+^#(1(x),1(y))	→	+^#(x,y)	(46)
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(47)
+^#(x,+(y,z))	→	+^#(x,y)	(48)

1.1.5 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[+(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[#]	=	0
[0(x₁)]	=	1 · x₁
[1(x₁)]	=	1 · x₁
[+^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂

together with the usable rules

+(x,#)	→	x	(2)
+(#,x)	→	x	(3)
+(0(x),0(y))	→	0(+(x,y))	(4)
+(0(x),1(y))	→	1(+(x,y))	(5)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
+(x,+(y,z))	→	+(+(x,y),z)	(8)
0(#)	→	#	(1)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.5.1 Monotonic Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[+(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[#]	=	0
[0(x₁)]	=	2 · x₁
[1(x₁)]	=	1 + 2 · x₁
[+^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂

the pairs

+^#(0(x),1(y))	→	+^#(x,y)	(42)
+^#(1(x),0(y))	→	+^#(x,y)	(43)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(45)
+^#(1(x),1(y))	→	+^#(x,y)	(46)

and no rules could be deleted.

1.1.5.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

+^#(0(x),0(y))	→	+^#(x,y)	(41)

1	>	1
2	>	2
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(47)

2	>	2
+^#(x,+(y,z))	→	+^#(x,y)	(48)

1	≥	1
2	>	2

As there is no critical graph in the transitive closure, there are no infinite chains.

The 6^th component contains the pair

-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(51)
-^#(0(x),1(y))	→	-^#(x,y)	(52)
-^#(0(x),0(y))	→	-^#(x,y)	(50)
-^#(1(x),0(y))	→	-^#(x,y)	(53)
-^#(1(x),1(y))	→	-^#(x,y)	(55)

1.1.6 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[-(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[#]	=	0
[0(x₁)]	=	1 · x₁
[1(x₁)]	=	1 · x₁
[-^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂

together with the usable rules

-(x,#)	→	x	(9)
-(#,x)	→	#	(10)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(1(x),0(y))	→	1(-(x,y))	(13)
-(1(x),1(y))	→	0(-(x,y))	(14)
0(#)	→	#	(1)

(w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.

1.1.6.1 Monotonic Reduction Pair Processor

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(#)	=	0	weight(#)	=	2
prec(0)	=	2	weight(0)	=	5
prec(1)	=	1	weight(1)	=	3
prec(-)	=	4	weight(-)	=	0
prec(-^#)	=	3	weight(-^#)	=	0

the pairs

-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(51)
-^#(0(x),1(y))	→	-^#(x,y)	(52)
-^#(0(x),0(y))	→	-^#(x,y)	(50)
-^#(1(x),0(y))	→	-^#(x,y)	(53)
-^#(1(x),1(y))	→	-^#(x,y)	(55)

and the rules

-(x,#)	→	x	(9)
-(#,x)	→	#	(10)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(1(x),0(y))	→	1(-(x,y))	(13)
-(1(x),1(y))	→	0(-(x,y))	(14)
0(#)	→	#	(1)

could be deleted.

1.1.6.1.1 P is empty

There are no pairs anymore.

The 7^th component contains the pair
ge^#(#,0(x)) → ge^#(#,x) (61)

1.1.7 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[#] = 0

[0(x₁)] = 1 · x₁

[ge^#(x₁, x₂)] = 1 · x₁ + 1 · x₂

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.7.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

ge^#(#,0(x)) → ge^#(#,x) (61)

1 ≥ 1

2 > 2

As there is no critical graph in the transitive closure, there are no infinite chains.
The 8^th component contains the pair
min^#(n(x,y,z)) → min^#(y) (62)

1.1.8 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[n(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[min^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.8.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

min^#(n(x,y,z)) → min^#(y) (62)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 9^th component contains the pair
max^#(n(x,y,z)) → max^#(z) (63)

1.1.9 Monotonic Reduction Pair Processor with Usable Rules
Using the linear polynomial interpretation over the naturals

[n(x₁, x₂, x₃)] = 1 · x₁ + 1 · x₂ + 1 · x₃

[max^#(x₁)] = 1 · x₁

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the rule could be deleted.
1.1.9.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

max^#(n(x,y,z)) → max^#(z) (63)

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.

[n(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[wb^#(x₁)]	=	1 · x₁

[n(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[bs^#(x₁)]	=	1 · x₁

[n(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[size^#(x₁)]	=	1 · x₁

[n(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[min^#(x₁)]	=	1 · x₁

[n(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[max^#(x₁)]	=	1 · x₁

Certification Problem

Input (TPDB TRS_Standard/CiME_04/tree)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 Monotonic Reduction Pair Processor with Usable Rules

1.1.1.1 Size-Change Termination

1.1.2 Monotonic Reduction Pair Processor with Usable Rules

1.1.2.1 Size-Change Termination

1.1.3 Monotonic Reduction Pair Processor with Usable Rules

1.1.3.1 Size-Change Termination

1.1.4 Monotonic Reduction Pair Processor with Usable Rules

1.1.4.1 Size-Change Termination

1.1.5 Monotonic Reduction Pair Processor with Usable Rules

1.1.5.1 Monotonic Reduction Pair Processor

1.1.5.1.1 Size-Change Termination

1.1.6 Monotonic Reduction Pair Processor with Usable Rules

1.1.6.1 Monotonic Reduction Pair Processor

1.1.6.1.1 P is empty

1.1.7 Monotonic Reduction Pair Processor with Usable Rules

1.1.7.1 Size-Change Termination

1.1.8 Monotonic Reduction Pair Processor with Usable Rules

1.1.8.1 Size-Change Termination

1.1.9 Monotonic Reduction Pair Processor with Usable Rules

1.1.9.1 Size-Change Termination