Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PEANO_complete-noand_FR)

The rewrite relation of the following TRS is considered.

U11(tt,V1,V2)	→	U12(isNatKind(activate(V1)),activate(V1),activate(V2))	(1)
U12(tt,V1,V2)	→	U13(isNatKind(activate(V2)),activate(V1),activate(V2))	(2)
U13(tt,V1,V2)	→	U14(isNatKind(activate(V2)),activate(V1),activate(V2))	(3)
U14(tt,V1,V2)	→	U15(isNat(activate(V1)),activate(V2))	(4)
U15(tt,V2)	→	U16(isNat(activate(V2)))	(5)
U16(tt)	→	tt	(6)
U21(tt,V1)	→	U22(isNatKind(activate(V1)),activate(V1))	(7)
U22(tt,V1)	→	U23(isNat(activate(V1)))	(8)
U23(tt)	→	tt	(9)
U31(tt,V2)	→	U32(isNatKind(activate(V2)))	(10)
U32(tt)	→	tt	(11)
U41(tt)	→	tt	(12)
U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
U52(tt,N)	→	activate(N)	(14)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
isNat(n__0)	→	tt	(19)
isNat(n__plus(V1,V2))	→	U11(isNatKind(activate(V1)),activate(V1),activate(V2))	(20)
isNat(n__s(V1))	→	U21(isNatKind(activate(V1)),activate(V1))	(21)
isNatKind(n__0)	→	tt	(22)
isNatKind(n__plus(V1,V2))	→	U31(isNatKind(activate(V1)),activate(V2))	(23)
isNatKind(n__s(V1))	→	U41(isNatKind(activate(V1)))	(24)
plus(N,0)	→	U51(isNat(N),N)	(25)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
0	→	n__0	(27)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
s(X)	→	n__s(X)	(29)
activate(n__0)	→	0	(30)
activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(31)
activate(n__s(X))	→	s(activate(X))	(32)
activate(X)	→	X	(33)

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.

U11^#(tt,V1,V2)	→	activate^#(V2)	(34)
U11^#(tt,V1,V2)	→	activate^#(V1)	(35)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(36)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(37)
U12^#(tt,V1,V2)	→	activate^#(V1)	(38)
U12^#(tt,V1,V2)	→	activate^#(V2)	(39)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(40)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(41)
U13^#(tt,V1,V2)	→	activate^#(V1)	(42)
U13^#(tt,V1,V2)	→	activate^#(V2)	(43)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(44)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(45)
U14^#(tt,V1,V2)	→	activate^#(V2)	(46)
U14^#(tt,V1,V2)	→	activate^#(V1)	(47)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(48)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(49)
U15^#(tt,V2)	→	activate^#(V2)	(50)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(51)
U15^#(tt,V2)	→	U16^#(isNat(activate(V2)))	(52)
U21^#(tt,V1)	→	activate^#(V1)	(53)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(54)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(55)
U22^#(tt,V1)	→	activate^#(V1)	(56)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(57)
U22^#(tt,V1)	→	U23^#(isNat(activate(V1)))	(58)
U31^#(tt,V2)	→	activate^#(V2)	(59)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(60)
U31^#(tt,V2)	→	U32^#(isNatKind(activate(V2)))	(61)
U51^#(tt,N)	→	activate^#(N)	(62)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(63)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(64)
U52^#(tt,N)	→	activate^#(N)	(65)
U61^#(tt,M,N)	→	activate^#(N)	(66)
U61^#(tt,M,N)	→	activate^#(M)	(67)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(68)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(69)
U62^#(tt,M,N)	→	activate^#(M)	(70)
U62^#(tt,M,N)	→	activate^#(N)	(71)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(72)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(73)
U63^#(tt,M,N)	→	activate^#(M)	(74)
U63^#(tt,M,N)	→	activate^#(N)	(75)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(76)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(77)
U64^#(tt,M,N)	→	activate^#(M)	(78)
U64^#(tt,M,N)	→	activate^#(N)	(79)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(80)
U64^#(tt,M,N)	→	s^#(plus(activate(N),activate(M)))	(81)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(82)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(83)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(84)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(85)
isNat^#(n__s(V1))	→	activate^#(V1)	(86)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(88)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(89)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(90)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(91)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(92)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(93)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(94)
isNatKind^#(n__s(V1))	→	U41^#(isNatKind(activate(V1)))	(95)
plus^#(N,0)	→	isNat^#(N)	(96)
plus^#(N,0)	→	U51^#(isNat(N),N)	(97)
plus^#(N,s(M))	→	isNat^#(M)	(98)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(99)
activate^#(n__0)	→	0^#	(100)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(101)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(102)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(103)
activate^#(n__s(X))	→	activate^#(X)	(104)
activate^#(n__s(X))	→	s^#(activate(X))	(105)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

plus^#(N,0)	→	U51^#(isNat(N),N)	(97)
U51^#(tt,N)	→	activate^#(N)	(62)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(101)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(102)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(103)
plus^#(N,0)	→	isNat^#(N)	(96)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(82)
activate^#(n__s(X))	→	activate^#(X)	(104)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(83)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(84)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(89)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(90)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(91)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(92)
U31^#(tt,V2)	→	activate^#(V2)	(59)
U31^#(tt,V2)	→	isNatKind^#(activate(V2))	(60)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(93)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(94)
isNat^#(n__plus(V1,V2))	→	U11^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(85)
U11^#(tt,V1,V2)	→	activate^#(V2)	(34)
U11^#(tt,V1,V2)	→	activate^#(V1)	(35)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(36)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(37)
U12^#(tt,V1,V2)	→	activate^#(V1)	(38)
U12^#(tt,V1,V2)	→	activate^#(V2)	(39)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(40)
U12^#(tt,V1,V2)	→	U13^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(41)
U13^#(tt,V1,V2)	→	activate^#(V1)	(42)
U13^#(tt,V1,V2)	→	activate^#(V2)	(43)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(44)
U13^#(tt,V1,V2)	→	U14^#(isNatKind(activate(V2)),activate(V1),activate(V2))	(45)
U14^#(tt,V1,V2)	→	activate^#(V2)	(46)
U14^#(tt,V1,V2)	→	activate^#(V1)	(47)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(48)
isNat^#(n__s(V1))	→	activate^#(V1)	(86)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(88)
U21^#(tt,V1)	→	activate^#(V1)	(53)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(54)
U21^#(tt,V1)	→	U22^#(isNatKind(activate(V1)),activate(V1))	(55)
U22^#(tt,V1)	→	activate^#(V1)	(56)
U22^#(tt,V1)	→	isNat^#(activate(V1))	(57)
U14^#(tt,V1,V2)	→	U15^#(isNat(activate(V1)),activate(V2))	(49)
U15^#(tt,V2)	→	activate^#(V2)	(50)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(51)
plus^#(N,s(M))	→	isNat^#(M)	(98)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(99)
U61^#(tt,M,N)	→	activate^#(N)	(66)
U61^#(tt,M,N)	→	activate^#(M)	(67)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(68)
U61^#(tt,M,N)	→	U62^#(isNatKind(activate(M)),activate(M),activate(N))	(69)
U62^#(tt,M,N)	→	activate^#(M)	(70)
U62^#(tt,M,N)	→	activate^#(N)	(71)
U62^#(tt,M,N)	→	isNat^#(activate(N))	(72)
U62^#(tt,M,N)	→	U63^#(isNat(activate(N)),activate(M),activate(N))	(73)
U63^#(tt,M,N)	→	activate^#(M)	(74)
U63^#(tt,M,N)	→	activate^#(N)	(75)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(76)
U63^#(tt,M,N)	→	U64^#(isNatKind(activate(N)),activate(M),activate(N))	(77)
U64^#(tt,M,N)	→	activate^#(M)	(78)
U64^#(tt,M,N)	→	activate^#(N)	(79)
U64^#(tt,M,N)	→	plus^#(activate(N),activate(M))	(80)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(63)
U51^#(tt,N)	→	U52^#(isNatKind(activate(N)),activate(N))	(64)
U52^#(tt,N)	→	activate^#(N)	(65)

1.1.1 Reduction Pair Processor with Usable Rules

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

[U61(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 2 · x₃ + 3
[U12(x₁, x₂, x₃)]	=	2 · x₁ + 0 · x₂ + 1 · x₃ + 1
[U41(x₁)]	=	0 · x₁ + 0
[U15(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 7/2
[U11(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 2 · x₃ + 0
[isNatKind(x₁)]	=	1 · x₁ + 0
[U51(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 2
[U64(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 2 · x₃ + 5/2
[n__s(x₁)]	=	1 · x₁ + 1/2
[U62(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 2 · x₃ + 3
[U13^#(x₁, x₂, x₃)]	=	0 · x₁ + 1 · x₂ + 3/2 · x₃ + 2
[U52(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 1
[0]	=	1/2
[isNat^#(x₁)]	=	1 · x₁ + 1/2
[plus(x₁, x₂)]	=	2 · x₁ + 3 · x₂ + 2
[U11^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 2 · x₃ + 5/2
[U52^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 1/2
[U13(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 2 · x₃ + 1/2
[U14^#(x₁, x₂, x₃)]	=	0 · x₁ + 1 · x₂ + 1 · x₃ + 2
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[tt]	=	0
[isNat(x₁)]	=	0 · x₁ + 0
[U63(x₁, x₂, x₃)]	=	0 · x₁ + 3 · x₂ + 2 · x₃ + 5/2
[n__plus(x₁, x₂)]	=	2 · x₁ + 3 · x₂ + 2
[plus^#(x₁, x₂)]	=	1 · x₁ + 2 · x₂ + 1/2
[isNatKind^#(x₁)]	=	1 · x₁ + 0
[U32(x₁)]	=	2 · x₁ + 1/2
[U12^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 2 · x₃ + 2
[U23(x₁)]	=	0 · x₁ + 1
[U61^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[s(x₁)]	=	1 · x₁ + 1/2
[n__0]	=	1/2
[U22(x₁, x₂)]	=	0 · x₁ + 3 · x₂ + 0
[U16(x₁)]	=	0 · x₁ + 0
[U31(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[U31^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 0
[U14(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 2 · x₃ + 0
[U22^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 1/2
[U64^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[U63^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[U21^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 1/2
[U62^#(x₁, x₂, x₃)]	=	0 · x₁ + 2 · x₂ + 1 · x₃ + 1/2
[U15^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 2
[activate^#(x₁)]	=	1 · x₁ + 0
[U51^#(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 1/2
[activate(x₁)]	=	1 · x₁ + 0

together with the usable rules

U51(tt,N)	→	U52(isNatKind(activate(N)),activate(N))	(13)
U52(tt,N)	→	activate(N)	(14)
U61(tt,M,N)	→	U62(isNatKind(activate(M)),activate(M),activate(N))	(15)
U62(tt,M,N)	→	U63(isNat(activate(N)),activate(M),activate(N))	(16)
U63(tt,M,N)	→	U64(isNatKind(activate(N)),activate(M),activate(N))	(17)
U64(tt,M,N)	→	s(plus(activate(N),activate(M)))	(18)
plus(N,0)	→	U51(isNat(N),N)	(25)
plus(N,s(M))	→	U61(isNat(M),M,N)	(26)
0	→	n__0	(27)
plus(X1,X2)	→	n__plus(X1,X2)	(28)
s(X)	→	n__s(X)	(29)
activate(n__0)	→	0	(30)
activate(n__plus(X1,X2))	→	plus(activate(X1),activate(X2))	(31)
activate(n__s(X))	→	s(activate(X))	(32)
activate(X)	→	X	(33)

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

plus^#(N,0)	→	U51^#(isNat(N),N)	(97)
U51^#(tt,N)	→	activate^#(N)	(62)
activate^#(n__plus(X1,X2))	→	activate^#(X2)	(101)
activate^#(n__plus(X1,X2))	→	activate^#(X1)	(102)
activate^#(n__plus(X1,X2))	→	plus^#(activate(X1),activate(X2))	(103)
plus^#(N,0)	→	isNat^#(N)	(96)
isNat^#(n__plus(V1,V2))	→	activate^#(V2)	(82)
activate^#(n__s(X))	→	activate^#(X)	(104)
isNat^#(n__plus(V1,V2))	→	activate^#(V1)	(83)
isNat^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(84)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V2)	(89)
isNatKind^#(n__plus(V1,V2))	→	activate^#(V1)	(90)
isNatKind^#(n__plus(V1,V2))	→	isNatKind^#(activate(V1))	(91)
isNatKind^#(n__plus(V1,V2))	→	U31^#(isNatKind(activate(V1)),activate(V2))	(92)
isNatKind^#(n__s(V1))	→	activate^#(V1)	(93)
isNatKind^#(n__s(V1))	→	isNatKind^#(activate(V1))	(94)
U11^#(tt,V1,V2)	→	activate^#(V2)	(34)
U11^#(tt,V1,V2)	→	activate^#(V1)	(35)
U11^#(tt,V1,V2)	→	isNatKind^#(activate(V1))	(36)
U11^#(tt,V1,V2)	→	U12^#(isNatKind(activate(V1)),activate(V1),activate(V2))	(37)
U12^#(tt,V1,V2)	→	activate^#(V1)	(38)
U12^#(tt,V1,V2)	→	activate^#(V2)	(39)
U12^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(40)
U13^#(tt,V1,V2)	→	activate^#(V1)	(42)
U13^#(tt,V1,V2)	→	activate^#(V2)	(43)
U13^#(tt,V1,V2)	→	isNatKind^#(activate(V2))	(44)
U14^#(tt,V1,V2)	→	activate^#(V2)	(46)
U14^#(tt,V1,V2)	→	activate^#(V1)	(47)
U14^#(tt,V1,V2)	→	isNat^#(activate(V1))	(48)
isNat^#(n__s(V1))	→	activate^#(V1)	(86)
isNat^#(n__s(V1))	→	isNatKind^#(activate(V1))	(87)
isNat^#(n__s(V1))	→	U21^#(isNatKind(activate(V1)),activate(V1))	(88)
U21^#(tt,V1)	→	activate^#(V1)	(53)
U21^#(tt,V1)	→	isNatKind^#(activate(V1))	(54)
U22^#(tt,V1)	→	activate^#(V1)	(56)
U15^#(tt,V2)	→	activate^#(V2)	(50)
U15^#(tt,V2)	→	isNat^#(activate(V2))	(51)
plus^#(N,s(M))	→	isNat^#(M)	(98)
plus^#(N,s(M))	→	U61^#(isNat(M),M,N)	(99)
U61^#(tt,M,N)	→	activate^#(N)	(66)
U61^#(tt,M,N)	→	activate^#(M)	(67)
U61^#(tt,M,N)	→	isNatKind^#(activate(M))	(68)
U62^#(tt,M,N)	→	activate^#(M)	(70)
U62^#(tt,M,N)	→	activate^#(N)	(71)
U63^#(tt,M,N)	→	activate^#(M)	(74)
U63^#(tt,M,N)	→	activate^#(N)	(75)
U63^#(tt,M,N)	→	isNatKind^#(activate(N))	(76)
U64^#(tt,M,N)	→	activate^#(M)	(78)
U64^#(tt,M,N)	→	activate^#(N)	(79)
U51^#(tt,N)	→	isNatKind^#(activate(N))	(63)
U52^#(tt,N)	→	activate^#(N)	(65)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.