Certification Problem

Input (TPDB TRS_Standard/CiME_04/big)

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)	→	#	(9)
-(x,#)	→	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(true)	→	false	(15)
not(false)	→	true	(16)
if(true,x,y)	→	x	(17)
if(false,x,y)	→	y	(18)
eq(#,#)	→	true	(19)
eq(#,1(y))	→	false	(20)
eq(1(x),#)	→	false	(21)
eq(#,0(y))	→	eq(#,y)	(22)
eq(0(x),#)	→	eq(x,#)	(23)
eq(1(x),1(y))	→	eq(x,y)	(24)
eq(0(x),1(y))	→	false	(25)
eq(1(x),0(y))	→	false	(26)
eq(0(x),0(y))	→	eq(x,y)	(27)
ge(0(x),0(y))	→	ge(x,y)	(28)
ge(0(x),1(y))	→	not(ge(y,x))	(29)
ge(1(x),0(y))	→	ge(x,y)	(30)
ge(1(x),1(y))	→	ge(x,y)	(31)
ge(x,#)	→	true	(32)
ge(#,0(x))	→	ge(#,x)	(33)
ge(#,1(x))	→	false	(34)
log(x)	→	-(log'(x),1(#))	(35)
log'(#)	→	#	(36)
log'(1(x))	→	+(log'(x),1(#))	(37)
log'(0(x))	→	if(ge(x,1(#)),+(log'(x),1(#)),#)	(38)
*(#,x)	→	#	(39)
*(0(x),y)	→	0(*(x,y))	(40)
*(1(x),y)	→	+(0(*(x,y)),y)	(41)
((x,y),z)	→	(x,(y,z))	(42)
*(x,+(y,z))	→	+((x,y),(x,z))	(43)
app(nil,l)	→	l	(44)
app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(45)
sum(nil)	→	0(#)	(46)
sum(cons(x,l))	→	+(x,sum(l))	(47)
sum(app(l1,l2))	→	+(sum(l1),sum(l2))	(48)
prod(nil)	→	1(#)	(49)
prod(cons(x,l))	→	*(x,prod(l))	(50)
prod(app(l1,l2))	→	*(prod(l1),prod(l2))	(51)
mem(x,nil)	→	false	(52)
mem(x,cons(y,l))	→	if(eq(x,y),true,mem(x,l))	(53)
inter(x,nil)	→	nil	(54)
inter(nil,x)	→	nil	(55)
inter(app(l1,l2),l3)	→	app(inter(l1,l3),inter(l2,l3))	(56)
inter(l1,app(l2,l3))	→	app(inter(l1,l2),inter(l1,l3))	(57)
inter(cons(x,l1),l2)	→	ifinter(mem(x,l2),x,l1,l2)	(58)
inter(l1,cons(x,l2))	→	ifinter(mem(x,l1),x,l2,l1)	(59)
ifinter(true,x,l1,l2)	→	cons(x,inter(l1,l2))	(60)
ifinter(false,x,l1,l2)	→	inter(l1,l2)	(61)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

+^#(0(x),0(y))	→	+^#(x,y)	(62)
+^#(0(x),0(y))	→	0^#(+(x,y))	(63)
+^#(0(x),1(y))	→	+^#(x,y)	(64)
+^#(1(x),0(y))	→	+^#(x,y)	(65)
+^#(1(x),1(y))	→	+^#(x,y)	(66)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(67)
+^#(1(x),1(y))	→	0^#(+(+(x,y),1(#)))	(68)
+^#(+(x,y),z)	→	+^#(y,z)	(69)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(70)
-^#(0(x),0(y))	→	-^#(x,y)	(71)
-^#(0(x),0(y))	→	0^#(-(x,y))	(72)
-^#(0(x),1(y))	→	-^#(x,y)	(73)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(74)
-^#(1(x),0(y))	→	-^#(x,y)	(75)
-^#(1(x),1(y))	→	-^#(x,y)	(76)
-^#(1(x),1(y))	→	0^#(-(x,y))	(77)
eq^#(#,0(y))	→	eq^#(#,y)	(78)
eq^#(0(x),#)	→	eq^#(x,#)	(79)
eq^#(1(x),1(y))	→	eq^#(x,y)	(80)
eq^#(0(x),0(y))	→	eq^#(x,y)	(81)
ge^#(0(x),0(y))	→	ge^#(x,y)	(82)
ge^#(0(x),1(y))	→	ge^#(y,x)	(83)
ge^#(0(x),1(y))	→	not^#(ge(y,x))	(84)
ge^#(1(x),0(y))	→	ge^#(x,y)	(85)
ge^#(1(x),1(y))	→	ge^#(x,y)	(86)
ge^#(#,0(x))	→	ge^#(#,x)	(87)
log^#(x)	→	log'^#(x)	(88)
log^#(x)	→	-^#(log'(x),1(#))	(89)
log'^#(1(x))	→	log'^#(x)	(90)
log'^#(1(x))	→	+^#(log'(x),1(#))	(91)
log'^#(0(x))	→	log'^#(x)	(92)
log'^#(0(x))	→	+^#(log'(x),1(#))	(93)
log'^#(0(x))	→	ge^#(x,1(#))	(94)
log'^#(0(x))	→	if^#(ge(x,1(#)),+(log'(x),1(#)),#)	(95)
*^#(0(x),y)	→	*^#(x,y)	(96)
*^#(0(x),y)	→	0^#(*(x,y))	(97)
*^#(1(x),y)	→	*^#(x,y)	(98)
*^#(1(x),y)	→	0^#(*(x,y))	(99)
*^#(1(x),y)	→	+^#(0(*(x,y)),y)	(100)
^#((x,y),z)	→	*^#(y,z)	(101)
^#((x,y),z)	→	^#(x,(y,z))	(102)
*^#(x,+(y,z))	→	*^#(x,z)	(103)
*^#(x,+(y,z))	→	*^#(x,y)	(104)
*^#(x,+(y,z))	→	+^#((x,y),(x,z))	(105)
app^#(cons(x,l1),l2)	→	app^#(l1,l2)	(106)
sum^#(nil)	→	0^#(#)	(107)
sum^#(cons(x,l))	→	sum^#(l)	(108)
sum^#(cons(x,l))	→	+^#(x,sum(l))	(109)
sum^#(app(l1,l2))	→	sum^#(l2)	(110)
sum^#(app(l1,l2))	→	sum^#(l1)	(111)
sum^#(app(l1,l2))	→	+^#(sum(l1),sum(l2))	(112)
prod^#(cons(x,l))	→	prod^#(l)	(113)
prod^#(cons(x,l))	→	*^#(x,prod(l))	(114)
prod^#(app(l1,l2))	→	prod^#(l2)	(115)
prod^#(app(l1,l2))	→	prod^#(l1)	(116)
prod^#(app(l1,l2))	→	*^#(prod(l1),prod(l2))	(117)
mem^#(x,cons(y,l))	→	mem^#(x,l)	(118)
mem^#(x,cons(y,l))	→	eq^#(x,y)	(119)
mem^#(x,cons(y,l))	→	if^#(eq(x,y),true,mem(x,l))	(120)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(121)
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(122)
inter^#(app(l1,l2),l3)	→	app^#(inter(l1,l3),inter(l2,l3))	(123)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(124)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(125)
inter^#(l1,app(l2,l3))	→	app^#(inter(l1,l2),inter(l1,l3))	(126)
inter^#(cons(x,l1),l2)	→	mem^#(x,l2)	(127)
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(128)
inter^#(l1,cons(x,l2))	→	mem^#(x,l1)	(129)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(130)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(131)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(132)

1.1 Dependency Graph Processor

The dependency pairs are split into 14 components.

The 1^st component contains the pair

-^#(1(x),1(y))	→	-^#(x,y)	(76)
-^#(1(x),0(y))	→	-^#(x,y)	(75)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(74)
-^#(0(x),1(y))	→	-^#(x,y)	(73)
-^#(0(x),0(y))	→	-^#(x,y)	(71)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(-^#)	=	{ 1, 1 }
π(cons)	=	{ 2, 2, 2 }
π(-)	=	{ 1 }
π(1)	=	{ 1, 1 }
π(0)	=	{ 1, 1 }

to remove the pairs:

-^#(1(x),1(y))	→	-^#(x,y)	(76)
-^#(1(x),0(y))	→	-^#(x,y)	(75)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(74)
-^#(0(x),1(y))	→	-^#(x,y)	(73)
-^#(0(x),0(y))	→	-^#(x,y)	(71)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

log'^#(1(x)) → log'^#(x) (90)

log'^#(0(x)) → log'^#(x) (92)

1.1.2 Size-Change Termination

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

log'^#(1(x)) → log'^#(x) (90)

1 > 1

log'^#(0(x)) → log'^#(x) (92)

1 > 1

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

The 3^rd component contains the pair

ge^#(1(x),1(y))	→	ge^#(x,y)	(86)
ge^#(1(x),0(y))	→	ge^#(x,y)	(85)
ge^#(0(x),1(y))	→	ge^#(y,x)	(83)
ge^#(0(x),0(y))	→	ge^#(x,y)	(82)

1.1.3 Size-Change Termination

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

ge^#(1(x),1(y))	→	ge^#(x,y)	(86)

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

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

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

2	>	2
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)) → ge^#(#,x) (87)

1.1.4 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) (87)

2 > 2

1 ≥ 1

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

sum^#(cons(x,l)) → sum^#(l) (108)

sum^#(app(l1,l2)) → sum^#(l1) (111)

sum^#(app(l1,l2)) → sum^#(l2) (110)

1.1.5 Size-Change Termination

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

sum^#(cons(x,l)) → sum^#(l) (108)

1 > 1

sum^#(app(l1,l2)) → sum^#(l1) (111)

1 > 1

sum^#(app(l1,l2)) → sum^#(l2) (110)

1 > 1

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

prod^#(cons(x,l)) → prod^#(l) (113)

prod^#(app(l1,l2)) → prod^#(l1) (116)

prod^#(app(l1,l2)) → prod^#(l2) (115)

1.1.6 Size-Change Termination

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

prod^#(cons(x,l)) → prod^#(l) (113)

1 > 1

prod^#(app(l1,l2)) → prod^#(l1) (116)

1 > 1

prod^#(app(l1,l2)) → prod^#(l2) (115)

1 > 1

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

The 7^th component contains the pair

*^#(x,+(y,z))	→	*^#(x,y)	(104)
*^#(x,+(y,z))	→	*^#(x,z)	(103)
^#((x,y),z)	→	^#(x,(y,z))	(102)
^#((x,y),z)	→	*^#(y,z)	(101)
*^#(1(x),y)	→	*^#(x,y)	(98)
*^#(0(x),y)	→	*^#(x,y)	(96)

1.1.7 Size-Change Termination

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

*^#(x,+(y,z))	→	*^#(x,y)	(104)

2	>	2
1	≥	1
*^#(x,+(y,z))	→	*^#(x,z)	(103)

2	>	2
1	≥	1
^#((x,y),z)	→	^#(x,(y,z))	(102)

1	>	1
^#((x,y),z)	→	*^#(y,z)	(101)

2	≥	2
1	>	1
*^#(1(x),y)	→	*^#(x,y)	(98)

2	≥	2
1	>	1
*^#(0(x),y)	→	*^#(x,y)	(96)

2	≥	2
1	>	1

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

The 8^th component contains the pair

+^#(+(x,y),z)	→	+^#(x,+(y,z))	(70)
+^#(+(x,y),z)	→	+^#(y,z)	(69)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(67)
+^#(1(x),1(y))	→	+^#(x,y)	(66)
+^#(1(x),0(y))	→	+^#(x,y)	(65)
+^#(0(x),1(y))	→	+^#(x,y)	(64)
+^#(0(x),0(y))	→	+^#(x,y)	(62)

1.1.8 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the rationals with delta = 1/64

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

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 pairs

+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(67)
+^#(1(x),1(y))	→	+^#(x,y)	(66)
+^#(1(x),0(y))	→	+^#(x,y)	(65)
+^#(0(x),1(y))	→	+^#(x,y)	(64)

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.

+^#(+(x,y),z)	→	+^#(x,+(y,z))	(70)

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

2	≥	2
1	>	1
+^#(0(x),0(y))	→	+^#(x,y)	(62)

2	>	2
1	>	1

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

The 9^th component contains the pair

ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(132)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(130)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(131)
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(128)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(125)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(124)
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(122)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(121)

1.1.9 Size-Change Termination

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

ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(132)

4	≥	2
3	≥	1
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(130)

2	>	3
2	>	2
1	≥	4
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(131)

4	≥	2
3	≥	1
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(128)

2	≥	4
1	>	3
1	>	2
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(125)

2	>	2
1	≥	1
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(124)

2	>	2
1	≥	1
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(122)

2	≥	2
1	>	1
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(121)

2	≥	2
1	>	1

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

The 10^th component contains the pair
app^#(cons(x,l1),l2) → app^#(l1,l2) (106)

1.1.10 Size-Change Termination

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

app^#(cons(x,l1),l2) → app^#(l1,l2) (106)

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 11^th component contains the pair
mem^#(x,cons(y,l)) → mem^#(x,l) (118)

1.1.11 Size-Change Termination

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

mem^#(x,cons(y,l)) → mem^#(x,l) (118)

2 > 2

1 ≥ 1

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

eq^#(0(x),0(y)) → eq^#(x,y) (81)

eq^#(1(x),1(y)) → eq^#(x,y) (80)

1.1.12 Size-Change Termination

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

eq^#(0(x),0(y)) → eq^#(x,y) (81)

2 > 2

1 > 1

eq^#(1(x),1(y)) → eq^#(x,y) (80)

2 > 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 13^th component contains the pair
eq^#(#,0(y)) → eq^#(#,y) (78)

1.1.13 Size-Change Termination

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

eq^#(#,0(y)) → eq^#(#,y) (78)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 14^th component contains the pair
eq^#(0(x),#) → eq^#(x,#) (79)

1.1.14 Size-Change Termination

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

eq^#(0(x),#) → eq^#(x,#) (79)

2 ≥ 2

1 > 1

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

Certification Problem

Input (TPDB TRS_Standard/CiME_04/big)

Property / Task

Answer / Result

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 Subterm Criterion Processor

1.1.1.1 P is empty

1.1.2 Size-Change Termination

1.1.3 Size-Change Termination

1.1.4 Size-Change Termination

1.1.5 Size-Change Termination

1.1.6 Size-Change Termination

1.1.7 Size-Change Termination

1.1.8 Reduction Pair Processor with Usable Rules

1.1.8.1 Size-Change Termination

1.1.9 Size-Change Termination

1.1.10 Size-Change Termination

1.1.11 Size-Change Termination

1.1.12 Size-Change Termination

1.1.13 Size-Change Termination

1.1.14 Size-Change Termination