Certification Problem

Input (TPDB TRS_Standard/CiME_04/intersect)

The rewrite relation of the following TRS is considered.

if(true,x,y)	→	x	(1)
if(false,x,y)	→	y	(2)
eq(0,0)	→	true	(3)
eq(0,s(x))	→	false	(4)
eq(s(x),0)	→	false	(5)
eq(s(x),s(y))	→	eq(x,y)	(6)
app(nil,l)	→	l	(7)
app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(8)
app(app(l1,l2),l3)	→	app(l1,app(l2,l3))	(9)
mem(x,nil)	→	false	(10)
mem(x,cons(y,l))	→	ifmem(eq(x,y),x,l)	(11)
ifmem(true,x,l)	→	true	(12)
ifmem(false,x,l)	→	mem(x,l)	(13)
inter(x,nil)	→	nil	(14)
inter(nil,x)	→	nil	(15)
inter(app(l1,l2),l3)	→	app(inter(l1,l3),inter(l2,l3))	(16)
inter(l1,app(l2,l3))	→	app(inter(l1,l2),inter(l1,l3))	(17)
inter(cons(x,l1),l2)	→	ifinter(mem(x,l2),x,l1,l2)	(18)
inter(l1,cons(x,l2))	→	ifinter(mem(x,l1),x,l2,l1)	(19)
ifinter(true,x,l1,l2)	→	cons(x,inter(l1,l2))	(20)
ifinter(false,x,l1,l2)	→	inter(l1,l2)	(21)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

ifmem^#(false,x,l)	→	mem^#(x,l)	(22)
mem^#(x,cons(y,l))	→	eq^#(x,y)	(23)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(24)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(25)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(26)
inter^#(l1,cons(x,l2))	→	mem^#(x,l1)	(27)
inter^#(app(l1,l2),l3)	→	app^#(inter(l1,l3),inter(l2,l3))	(28)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(29)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(30)
mem^#(x,cons(y,l))	→	ifmem^#(eq(x,y),x,l)	(31)
app^#(cons(x,l1),l2)	→	app^#(l1,l2)	(32)
inter^#(cons(x,l1),l2)	→	mem^#(x,l2)	(33)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(34)
app^#(app(l1,l2),l3)	→	app^#(l1,app(l2,l3))	(35)
eq^#(s(x),s(y))	→	eq^#(x,y)	(36)
inter^#(l1,app(l2,l3))	→	app^#(inter(l1,l2),inter(l1,l3))	(37)
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(38)
app^#(app(l1,l2),l3)	→	app^#(l2,l3)	(39)
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(40)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(40)
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(38)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(34)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(26)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(25)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(24)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(30)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(29)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[mem(x₁, x₂)]	=	x₂ + 2
[s(x₁)]	=	1
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	6
[false]	=	1
[mem^#(x₁, x₂)]	=	0
[ifmem(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[ifinter^#(x₁,...,x₄)]	=	x₃ + x₄ + 1
[true]	=	7
[ifmem^#(x₁, x₂, x₃)]	=	0
[eq^#(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	1
[nil]	=	28958
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 2
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	x₁ + x₂ + 0
[app(x₁, x₂)]	=	x₁ + x₂ + 1

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(40)
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(38)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(34)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(26)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(25)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(24)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(30)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(29)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

app^#(app(l1,l2),l3)	→	app^#(l2,l3)	(39)
app^#(app(l1,l2),l3)	→	app^#(l1,app(l2,l3))	(35)
app^#(cons(x,l1),l2)	→	app^#(l1,l2)	(32)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[mem(x₁, x₂)]	=	x₂ + 2
[s(x₁)]	=	1
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	38554
[false]	=	1
[mem^#(x₁, x₂)]	=	0
[ifmem(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	38555
[ifmem^#(x₁, x₂, x₃)]	=	0
[eq^#(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	1
[nil]	=	38139
[app^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₂ + 38551
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 31755

together with the usable rules

app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(8)
app(nil,l)	→	l	(7)
app(app(l1,l2),l3)	→	app(l1,app(l2,l3))	(9)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

app^#(app(l1,l2),l3)	→	app^#(l2,l3)	(39)
app^#(app(l1,l2),l3)	→	app^#(l1,app(l2,l3))	(35)
app^#(cons(x,l1),l2)	→	app^#(l1,l2)	(32)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

mem^#(x,cons(y,l))	→	ifmem^#(eq(x,y),x,l)	(31)
ifmem^#(false,x,l)	→	mem^#(x,l)	(22)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[mem(x₁, x₂)]	=	x₂ + 2
[s(x₁)]	=	1
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	5
[false]	=	1
[mem^#(x₁, x₂)]	=	x₁ + x₂ + 0
[ifmem(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	6
[ifmem^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[eq^#(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	0
[0]	=	1
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 2
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 31755

together with the usable rules

app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(8)
app(nil,l)	→	l	(7)
app(app(l1,l2),l3)	→	app(l1,app(l2,l3))	(9)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

mem^#(x,cons(y,l))	→	ifmem^#(eq(x,y),x,l)	(31)
ifmem^#(false,x,l)	→	mem^#(x,l)	(22)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

eq^#(s(x),s(y))

→

eq^#(x,y)

(36)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[mem(x₁, x₂)]	=	x₂ + 2
[s(x₁)]	=	x₁ + 1
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	11946
[false]	=	1
[mem^#(x₁, x₂)]	=	0
[ifmem(x₁, x₂, x₃)]	=	x₁ + x₂ + 0
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	11947
[ifmem^#(x₁, x₂, x₃)]	=	1
[eq^#(x₁, x₂)]	=	x₁ + x₂ + 0
[if(x₁, x₂, x₃)]	=	0
[0]	=	1
[nil]	=	42207
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 11943
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 31755

together with the usable rules

app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(8)
app(nil,l)	→	l	(7)
app(app(l1,l2),l3)	→	app(l1,app(l2,l3))	(9)

(w.r.t. the implicit argument filter of the reduction pair), the pair

eq^#(s(x),s(y))

→

eq^#(x,y)

(36)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.