Certification Problem

Input (TPDB TRS_Standard/Rubio_04/wst99)

The rewrite relation of the following TRS is considered.

din(der(plus(X,Y)))	→	u21(din(der(X)),X,Y)	(1)
u21(dout(DX),X,Y)	→	u22(din(der(Y)),X,Y,DX)	(2)
u22(dout(DY),X,Y,DX)	→	dout(plus(DX,DY))	(3)
din(der(times(X,Y)))	→	u31(din(der(X)),X,Y)	(4)
u31(dout(DX),X,Y)	→	u32(din(der(Y)),X,Y,DX)	(5)
u32(dout(DY),X,Y,DX)	→	dout(plus(times(X,DY),times(Y,DX)))	(6)
din(der(der(X)))	→	u41(din(der(X)),X)	(7)
u41(dout(DX),X)	→	u42(din(der(DX)),X,DX)	(8)
u42(dout(DDX),X,DX)	→	dout(DDX)	(9)

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.

u21^#(dout(DX),X,Y)	→	din^#(der(Y))	(10)
u31^#(dout(DX),X,Y)	→	din^#(der(Y))	(11)
u41^#(dout(DX),X)	→	u42^#(din(der(DX)),X,DX)	(12)
din^#(der(times(X,Y)))	→	u31^#(din(der(X)),X,Y)	(13)
din^#(der(times(X,Y)))	→	din^#(der(X))	(14)
din^#(der(plus(X,Y)))	→	u21^#(din(der(X)),X,Y)	(15)
u41^#(dout(DX),X)	→	din^#(der(DX))	(16)
u31^#(dout(DX),X,Y)	→	u32^#(din(der(Y)),X,Y,DX)	(17)
din^#(der(der(X)))	→	u41^#(din(der(X)),X)	(18)
u21^#(dout(DX),X,Y)	→	u22^#(din(der(Y)),X,Y,DX)	(19)
din^#(der(plus(X,Y)))	→	din^#(der(X))	(20)
din^#(der(der(X)))	→	din^#(der(X))	(21)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

din^#(der(der(X)))	→	din^#(der(X))	(21)
din^#(der(times(X,Y)))	→	din^#(der(X))	(14)
din^#(der(plus(X,Y)))	→	din^#(der(X))	(20)
din^#(der(der(X)))	→	u41^#(din(der(X)),X)	(18)
din^#(der(times(X,Y)))	→	u31^#(din(der(X)),X,Y)	(13)
u31^#(dout(DX),X,Y)	→	din^#(der(Y))	(11)
u41^#(dout(DX),X)	→	din^#(der(DX))	(16)
din^#(der(plus(X,Y)))	→	u21^#(din(der(X)),X,Y)	(15)
u21^#(dout(DX),X,Y)	→	din^#(der(Y))	(10)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[din(x₁)]	=	x₁ + 0
[u22^#(x₁,...,x₄)]	=	0
[der(x₁)]	=	1
[u21^#(x₁, x₂, x₃)]	=	x₁ + 0
[din^#(x₁)]	=	2
[u41(x₁, x₂)]	=	1
[times(x₁, x₂)]	=	20819
[u32(x₁,...,x₄)]	=	3
[u21(x₁, x₂, x₃)]	=	x₁ + 0
[u41^#(x₁, x₂)]	=	x₁ + 0
[plus(x₁, x₂)]	=	x₂ + 1
[u42^#(x₁, x₂, x₃)]	=	0
[u31^#(x₁, x₂, x₃)]	=	x₁ + 0
[u22(x₁,...,x₄)]	=	3
[u42(x₁, x₂, x₃)]	=	x₁ + 0
[u32^#(x₁,...,x₄)]	=	0
[dout(x₁)]	=	3
[u31(x₁, x₂, x₃)]	=	x₁ + 0

together with the usable rules

din(der(times(X,Y)))	→	u31(din(der(X)),X,Y)	(4)
u41(dout(DX),X)	→	u42(din(der(DX)),X,DX)	(8)
din(der(plus(X,Y)))	→	u21(din(der(X)),X,Y)	(1)
u22(dout(DY),X,Y,DX)	→	dout(plus(DX,DY))	(3)
u31(dout(DX),X,Y)	→	u32(din(der(Y)),X,Y,DX)	(5)
din(der(der(X)))	→	u41(din(der(X)),X)	(7)
u42(dout(DDX),X,DX)	→	dout(DDX)	(9)
u32(dout(DY),X,Y,DX)	→	dout(plus(times(X,DY),times(Y,DX)))	(6)
u21(dout(DX),X,Y)	→	u22(din(der(Y)),X,Y,DX)	(2)

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

din^#(der(der(X)))	→	u41^#(din(der(X)),X)	(18)
din^#(der(times(X,Y)))	→	u31^#(din(der(X)),X,Y)	(13)
u31^#(dout(DX),X,Y)	→	din^#(der(Y))	(11)
u41^#(dout(DX),X)	→	din^#(der(DX))	(16)
din^#(der(plus(X,Y)))	→	u21^#(din(der(X)),X,Y)	(15)
u21^#(dout(DX),X,Y)	→	din^#(der(Y))	(10)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

din^#(der(times(X,Y)))	→	din^#(der(X))	(14)
din^#(der(plus(X,Y)))	→	din^#(der(X))	(20)
din^#(der(der(X)))	→	din^#(der(X))	(21)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[din(x₁)]	=	x₁ + 0
[u22^#(x₁,...,x₄)]	=	0
[der(x₁)]	=	x₁ + 2998
[u21^#(x₁, x₂, x₃)]	=	x₁ + 0
[din^#(x₁)]	=	x₁ + 2
[u41(x₁, x₂)]	=	5996
[times(x₁, x₂)]	=	x₁ + x₂ + 1
[u32(x₁,...,x₄)]	=	5996
[u21(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[u41^#(x₁, x₂)]	=	x₁ + 0
[plus(x₁, x₂)]	=	x₁ + x₂ + 1
[u42^#(x₁, x₂, x₃)]	=	0
[u31^#(x₁, x₂, x₃)]	=	x₁ + 0
[u22(x₁,...,x₄)]	=	5996
[u42(x₁, x₂, x₃)]	=	5996
[u32^#(x₁,...,x₄)]	=	0
[dout(x₁)]	=	5996
[u31(x₁, x₂, x₃)]	=	x₁ + 0

together with the usable rules

din(der(times(X,Y)))	→	u31(din(der(X)),X,Y)	(4)
u41(dout(DX),X)	→	u42(din(der(DX)),X,DX)	(8)
din(der(plus(X,Y)))	→	u21(din(der(X)),X,Y)	(1)
u22(dout(DY),X,Y,DX)	→	dout(plus(DX,DY))	(3)
u31(dout(DX),X,Y)	→	u32(din(der(Y)),X,Y,DX)	(5)
din(der(der(X)))	→	u41(din(der(X)),X)	(7)
u42(dout(DDX),X,DX)	→	dout(DDX)	(9)
u32(dout(DY),X,Y,DX)	→	dout(plus(times(X,DY),times(Y,DX)))	(6)
u21(dout(DX),X,Y)	→	u22(din(der(Y)),X,Y,DX)	(2)

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

din^#(der(times(X,Y)))	→	din^#(der(X))	(14)
din^#(der(plus(X,Y)))	→	din^#(der(X))	(20)
din^#(der(der(X)))	→	din^#(der(X))	(21)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.