Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/LengthOfFiniteLists_complete_GM)

The rewrite relation of the following TRS is considered.

a__zeros	→	cons(0,zeros)	(1)
a__U11(tt,V1)	→	a__U12(a__isNatList(V1))	(2)
a__U12(tt)	→	tt	(3)
a__U21(tt,V1)	→	a__U22(a__isNat(V1))	(4)
a__U22(tt)	→	tt	(5)
a__U31(tt,V)	→	a__U32(a__isNatList(V))	(6)
a__U32(tt)	→	tt	(7)
a__U41(tt,V1,V2)	→	a__U42(a__isNat(V1),V2)	(8)
a__U42(tt,V2)	→	a__U43(a__isNatIList(V2))	(9)
a__U43(tt)	→	tt	(10)
a__U51(tt,V1,V2)	→	a__U52(a__isNat(V1),V2)	(11)
a__U52(tt,V2)	→	a__U53(a__isNatList(V2))	(12)
a__U53(tt)	→	tt	(13)
a__U61(tt,L)	→	s(a__length(mark(L)))	(14)
a__and(tt,X)	→	mark(X)	(15)
a__isNat(0)	→	tt	(16)
a__isNat(length(V1))	→	a__U11(a__isNatIListKind(V1),V1)	(17)
a__isNat(s(V1))	→	a__U21(a__isNatKind(V1),V1)	(18)
a__isNatIList(V)	→	a__U31(a__isNatIListKind(V),V)	(19)
a__isNatIList(zeros)	→	tt	(20)
a__isNatIList(cons(V1,V2))	→	a__U41(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(21)
a__isNatIListKind(nil)	→	tt	(22)
a__isNatIListKind(zeros)	→	tt	(23)
a__isNatIListKind(cons(V1,V2))	→	a__and(a__isNatKind(V1),isNatIListKind(V2))	(24)
a__isNatKind(0)	→	tt	(25)
a__isNatKind(length(V1))	→	a__isNatIListKind(V1)	(26)
a__isNatKind(s(V1))	→	a__isNatKind(V1)	(27)
a__isNatList(nil)	→	tt	(28)
a__isNatList(cons(V1,V2))	→	a__U51(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(29)
a__length(nil)	→	0	(30)
a__length(cons(N,L))	→	a__U61(a__and(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),L)	(31)
mark(zeros)	→	a__zeros	(32)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(33)
mark(U12(X))	→	a__U12(mark(X))	(34)
mark(isNatList(X))	→	a__isNatList(X)	(35)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(36)
mark(U22(X))	→	a__U22(mark(X))	(37)
mark(isNat(X))	→	a__isNat(X)	(38)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(39)
mark(U32(X))	→	a__U32(mark(X))	(40)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(41)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(42)
mark(U43(X))	→	a__U43(mark(X))	(43)
mark(isNatIList(X))	→	a__isNatIList(X)	(44)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(45)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(46)
mark(U53(X))	→	a__U53(mark(X))	(47)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(48)
mark(length(X))	→	a__length(mark(X))	(49)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(50)
mark(isNatIListKind(X))	→	a__isNatIListKind(X)	(51)
mark(isNatKind(X))	→	a__isNatKind(X)	(52)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(53)
mark(0)	→	0	(54)
mark(tt)	→	tt	(55)
mark(s(X))	→	s(mark(X))	(56)
mark(nil)	→	nil	(57)
a__zeros	→	zeros	(58)
a__U11(X1,X2)	→	U11(X1,X2)	(59)
a__U12(X)	→	U12(X)	(60)
a__isNatList(X)	→	isNatList(X)	(61)
a__U21(X1,X2)	→	U21(X1,X2)	(62)
a__U22(X)	→	U22(X)	(63)
a__isNat(X)	→	isNat(X)	(64)
a__U31(X1,X2)	→	U31(X1,X2)	(65)
a__U32(X)	→	U32(X)	(66)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(67)
a__U42(X1,X2)	→	U42(X1,X2)	(68)
a__U43(X)	→	U43(X)	(69)
a__isNatIList(X)	→	isNatIList(X)	(70)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(71)
a__U52(X1,X2)	→	U52(X1,X2)	(72)
a__U53(X)	→	U53(X)	(73)
a__U61(X1,X2)	→	U61(X1,X2)	(74)
a__length(X)	→	length(X)	(75)
a__and(X1,X2)	→	and(X1,X2)	(76)
a__isNatIListKind(X)	→	isNatIListKind(X)	(77)
a__isNatKind(X)	→	isNatKind(X)	(78)

The evaluation strategy is innermost.

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.

a__U11^#(tt,V1)	→	a__U12^#(a__isNatList(V1))	(79)
a__U11^#(tt,V1)	→	a__isNatList^#(V1)	(80)
a__U21^#(tt,V1)	→	a__U22^#(a__isNat(V1))	(81)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(82)
a__U31^#(tt,V)	→	a__U32^#(a__isNatList(V))	(83)
a__U31^#(tt,V)	→	a__isNatList^#(V)	(84)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isNat(V1),V2)	(85)
a__U41^#(tt,V1,V2)	→	a__isNat^#(V1)	(86)
a__U42^#(tt,V2)	→	a__U43^#(a__isNatIList(V2))	(87)
a__U42^#(tt,V2)	→	a__isNatIList^#(V2)	(88)
a__U51^#(tt,V1,V2)	→	a__U52^#(a__isNat(V1),V2)	(89)
a__U51^#(tt,V1,V2)	→	a__isNat^#(V1)	(90)
a__U52^#(tt,V2)	→	a__U53^#(a__isNatList(V2))	(91)
a__U52^#(tt,V2)	→	a__isNatList^#(V2)	(92)
a__U61^#(tt,L)	→	a__length^#(mark(L))	(93)
a__U61^#(tt,L)	→	mark^#(L)	(94)
a__and^#(tt,X)	→	mark^#(X)	(95)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(96)
a__isNat^#(length(V1))	→	a__isNatIListKind^#(V1)	(97)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(98)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(99)
a__isNatIList^#(V)	→	a__U31^#(a__isNatIListKind(V),V)	(100)
a__isNatIList^#(V)	→	a__isNatIListKind^#(V)	(101)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(102)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(103)
a__isNatIList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(104)
a__isNatIListKind^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(105)
a__isNatIListKind^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(106)
a__isNatKind^#(length(V1))	→	a__isNatIListKind^#(V1)	(107)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(108)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(109)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(110)
a__isNatList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(111)
a__length^#(cons(N,L))	→	a__U61^#(a__and(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),L)	(112)
a__length^#(cons(N,L))	→	a__and^#(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N)))	(113)
a__length^#(cons(N,L))	→	a__and^#(a__isNatList(L),isNatIListKind(L))	(114)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(115)
mark^#(zeros)	→	a__zeros^#	(116)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(117)
mark^#(U11(X1,X2))	→	mark^#(X1)	(118)
mark^#(U12(X))	→	a__U12^#(mark(X))	(119)
mark^#(U12(X))	→	mark^#(X)	(120)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(121)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(122)
mark^#(U21(X1,X2))	→	mark^#(X1)	(123)
mark^#(U22(X))	→	a__U22^#(mark(X))	(124)
mark^#(U22(X))	→	mark^#(X)	(125)
mark^#(isNat(X))	→	a__isNat^#(X)	(126)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(127)
mark^#(U31(X1,X2))	→	mark^#(X1)	(128)
mark^#(U32(X))	→	a__U32^#(mark(X))	(129)
mark^#(U32(X))	→	mark^#(X)	(130)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(131)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(132)
mark^#(U42(X1,X2))	→	a__U42^#(mark(X1),X2)	(133)
mark^#(U42(X1,X2))	→	mark^#(X1)	(134)
mark^#(U43(X))	→	a__U43^#(mark(X))	(135)
mark^#(U43(X))	→	mark^#(X)	(136)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(137)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(138)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(139)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(140)
mark^#(U52(X1,X2))	→	mark^#(X1)	(141)
mark^#(U53(X))	→	a__U53^#(mark(X))	(142)
mark^#(U53(X))	→	mark^#(X)	(143)
mark^#(U61(X1,X2))	→	a__U61^#(mark(X1),X2)	(144)
mark^#(U61(X1,X2))	→	mark^#(X1)	(145)
mark^#(length(X))	→	a__length^#(mark(X))	(146)
mark^#(length(X))	→	mark^#(X)	(147)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(148)
mark^#(and(X1,X2))	→	mark^#(X1)	(149)
mark^#(isNatIListKind(X))	→	a__isNatIListKind^#(X)	(150)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(151)
mark^#(cons(X1,X2))	→	mark^#(X1)	(152)
mark^#(s(X))	→	mark^#(X)	(153)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__U11^#(tt,V1)	→	a__isNatList^#(V1)	(80)
a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(109)
a__U51^#(tt,V1,V2)	→	a__U52^#(a__isNat(V1),V2)	(89)
a__U52^#(tt,V2)	→	a__isNatList^#(V2)	(92)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(110)
a__and^#(tt,X)	→	mark^#(X)	(95)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(117)
mark^#(U11(X1,X2))	→	mark^#(X1)	(118)
mark^#(U12(X))	→	mark^#(X)	(120)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(121)
a__isNatList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(111)
a__isNatKind^#(length(V1))	→	a__isNatIListKind^#(V1)	(107)
a__isNatIListKind^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(105)
a__isNatIListKind^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(106)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(108)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(122)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(82)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(96)
a__isNat^#(length(V1))	→	a__isNatIListKind^#(V1)	(97)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(98)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(99)
mark^#(U21(X1,X2))	→	mark^#(X1)	(123)
mark^#(U22(X))	→	mark^#(X)	(125)
mark^#(isNat(X))	→	a__isNat^#(X)	(126)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(127)
a__U31^#(tt,V)	→	a__isNatList^#(V)	(84)
mark^#(U31(X1,X2))	→	mark^#(X1)	(128)
mark^#(U32(X))	→	mark^#(X)	(130)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(131)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isNat(V1),V2)	(85)
a__U42^#(tt,V2)	→	a__isNatIList^#(V2)	(88)
a__isNatIList^#(V)	→	a__U31^#(a__isNatIListKind(V),V)	(100)
a__isNatIList^#(V)	→	a__isNatIListKind^#(V)	(101)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(102)
a__U41^#(tt,V1,V2)	→	a__isNat^#(V1)	(86)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(103)
a__isNatIList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(104)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(132)
mark^#(U42(X1,X2))	→	a__U42^#(mark(X1),X2)	(133)
mark^#(U42(X1,X2))	→	mark^#(X1)	(134)
mark^#(U43(X))	→	mark^#(X)	(136)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(137)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(138)
a__U51^#(tt,V1,V2)	→	a__isNat^#(V1)	(90)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(139)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(140)
mark^#(U52(X1,X2))	→	mark^#(X1)	(141)
mark^#(U53(X))	→	mark^#(X)	(143)
mark^#(U61(X1,X2))	→	a__U61^#(mark(X1),X2)	(144)
a__U61^#(tt,L)	→	a__length^#(mark(L))	(93)
a__length^#(cons(N,L))	→	a__U61^#(a__and(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),L)	(112)
a__U61^#(tt,L)	→	mark^#(L)	(94)
mark^#(U61(X1,X2))	→	mark^#(X1)	(145)
mark^#(length(X))	→	a__length^#(mark(X))	(146)
a__length^#(cons(N,L))	→	a__and^#(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N)))	(113)
a__length^#(cons(N,L))	→	a__and^#(a__isNatList(L),isNatIListKind(L))	(114)
a__length^#(cons(N,L))	→	a__isNatList^#(L)	(115)
mark^#(length(X))	→	mark^#(X)	(147)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(148)
mark^#(and(X1,X2))	→	mark^#(X1)	(149)
mark^#(isNatIListKind(X))	→	a__isNatIListKind^#(X)	(150)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(151)
mark^#(cons(X1,X2))	→	mark^#(X1)	(152)
mark^#(s(X))	→	mark^#(X)	(153)

1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[a__and^#(x₁, x₂)]	=	x₂
[a__length^#(x₁)]	=	x₁
[a__U11^#(x₁, x₂)]	=	-2
[a__U21^#(x₁, x₂)]	=	-2
[a__U31^#(x₁, x₂)]	=	-2
[a__U41^#(x₁, x₂, x₃)]	=	-2
[a__U42^#(x₁, x₂)]	=	-2
[a__U51^#(x₁, x₂, x₃)]	=	-2
[a__U52^#(x₁, x₂)]	=	-2
[a__U61^#(x₁, x₂)]	=	x₂
[a__isNatKind(x₁)]	=	0
[0]	=	0
[tt]	=	0
[mark(x₁)]	=	x₁
[and(x₁, x₂)]	=	x₁ + x₂
[a__and(x₁, x₂)]	=	x₁ + x₂
[isNatIListKind(x₁)]	=	0
[a__isNatIListKind(x₁)]	=	0
[cons(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[isNatKind(x₁)]	=	0
[length(x₁)]	=	1 + x₁
[s(x₁)]	=	x₁
[a__isNat(x₁)]	=	0
[a__U11(x₁, x₂)]	=	x₁
[a__U21(x₁, x₂)]	=	2 · x₁
[isNat(x₁)]	=	0
[zeros]	=	0
[a__zeros]	=	0
[U11(x₁, x₂)]	=	x₁
[U12(x₁)]	=	x₁
[a__U12(x₁)]	=	x₁
[isNatList(x₁)]	=	0
[a__isNatList(x₁)]	=	0
[U21(x₁, x₂)]	=	2 · x₁
[U22(x₁)]	=	2 · x₁
[a__U22(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	x₁
[a__U31(x₁, x₂)]	=	x₁
[U32(x₁)]	=	2 · x₁
[a__U32(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	x₁
[a__U41(x₁, x₂, x₃)]	=	x₁
[U42(x₁, x₂)]	=	x₁
[a__U42(x₁, x₂)]	=	x₁
[U43(x₁)]	=	2 · x₁
[a__U43(x₁)]	=	2 · x₁
[isNatIList(x₁)]	=	0
[a__isNatIList(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	2 · x₁
[a__U51(x₁, x₂, x₃)]	=	2 · x₁
[U52(x₁, x₂)]	=	2 · x₁
[a__U52(x₁, x₂)]	=	2 · x₁
[U53(x₁)]	=	2 · x₁
[a__U53(x₁)]	=	2 · x₁
[U61(x₁, x₂)]	=	1 + 2 · x₁ + x₂
[a__U61(x₁, x₂)]	=	1 + 2 · x₁ + x₂
[a__length(x₁)]	=	1 + x₁
[nil]	=	0
[a__isNatList^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁
[a__isNatKind^#(x₁)]	=	0
[a__isNatIListKind^#(x₁)]	=	0
[a__isNat^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0

the pairs

mark^#(U61(X1,X2))	→	a__U61^#(mark(X1),X2)	(144)
mark^#(U61(X1,X2))	→	mark^#(X1)	(145)
mark^#(length(X))	→	a__length^#(mark(X))	(146)
mark^#(length(X))	→	mark^#(X)	(147)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a__U61^#(tt,L)	→	a__length^#(mark(L))	(93)
a__length^#(cons(N,L))	→	a__U61^#(a__and(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),L)	(112)

1.1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[a__length^#(x₁)]	=	-2 + 2 · x₁
[a__U61^#(x₁, x₂)]	=	1 + x₁ + 2 · x₂
[mark(x₁)]	=	2 + x₁
[zeros]	=	0
[a__zeros]	=	2
[U11(x₁, x₂)]	=	0
[a__U11(x₁, x₂)]	=	2
[U12(x₁)]	=	0
[a__U12(x₁)]	=	2
[isNatList(x₁)]	=	x₁
[a__isNatList(x₁)]	=	x₁
[U21(x₁, x₂)]	=	x₁
[a__U21(x₁, x₂)]	=	x₁
[U22(x₁)]	=	x₁
[a__U22(x₁)]	=	x₁
[isNat(x₁)]	=	1
[a__isNat(x₁)]	=	2
[U31(x₁, x₂)]	=	x₁ + 2 · x₂
[a__U31(x₁, x₂)]	=	x₁ + 2 · x₂
[U32(x₁)]	=	0
[a__U32(x₁)]	=	2
[U41(x₁, x₂, x₃)]	=	2 + 2 · x₃
[a__U41(x₁, x₂, x₃)]	=	2 + 2 · x₃
[U42(x₁, x₂)]	=	x₁ + 2 · x₂
[a__U42(x₁, x₂)]	=	x₁ + 2 · x₂
[U43(x₁)]	=	x₁
[a__U43(x₁)]	=	x₁
[isNatIList(x₁)]	=	2 · x₁
[a__isNatIList(x₁)]	=	2 + 2 · x₁
[U51(x₁, x₂, x₃)]	=	x₃
[a__U51(x₁, x₂, x₃)]	=	2 + x₃
[U52(x₁, x₂)]	=	x₂
[a__U52(x₁, x₂)]	=	2 + x₂
[U53(x₁)]	=	x₁
[a__U53(x₁)]	=	x₁
[U61(x₁, x₂)]	=	2
[a__U61(x₁, x₂)]	=	2
[length(x₁)]	=	1
[a__length(x₁)]	=	2
[and(x₁, x₂)]	=	x₁ + x₂
[a__and(x₁, x₂)]	=	x₁ + x₂
[tt]	=	2
[isNatIListKind(x₁)]	=	0
[a__isNatIListKind(x₁)]	=	2
[cons(x₁, x₂)]	=	2 + 2 · x₂
[a__isNatKind(x₁)]	=	2
[isNatKind(x₁)]	=	0
[s(x₁)]	=	2
[0]	=	0
[nil]	=	2

the pair

a__U61^#(tt,L)

→

a__length^#(mark(L))

(93)

could be deleted.

1.1.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.

a__length^#(cons(N,L))	→	a__U61^#(a__and(a__and(a__isNatList(L),isNatIListKind(L)),and(isNat(N),isNatKind(N))),L)	(112)

1	>	2

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

The 2^nd component contains the pair

a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(109)
a__U51^#(tt,V1,V2)	→	a__U52^#(a__isNat(V1),V2)	(89)
a__U52^#(tt,V2)	→	a__isNatList^#(V2)	(92)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(110)
a__and^#(tt,X)	→	mark^#(X)	(95)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(117)
a__U11^#(tt,V1)	→	a__isNatList^#(V1)	(80)
a__isNatList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(111)
a__isNatKind^#(length(V1))	→	a__isNatIListKind^#(V1)	(107)
a__isNatIListKind^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(105)
a__isNatIListKind^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(106)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(108)
mark^#(U11(X1,X2))	→	mark^#(X1)	(118)
mark^#(U12(X))	→	mark^#(X)	(120)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(121)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(122)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(82)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(96)
a__isNat^#(length(V1))	→	a__isNatIListKind^#(V1)	(97)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(98)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(99)
mark^#(U21(X1,X2))	→	mark^#(X1)	(123)
mark^#(U22(X))	→	mark^#(X)	(125)
mark^#(isNat(X))	→	a__isNat^#(X)	(126)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(127)
a__U31^#(tt,V)	→	a__isNatList^#(V)	(84)
mark^#(U31(X1,X2))	→	mark^#(X1)	(128)
mark^#(U32(X))	→	mark^#(X)	(130)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(131)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isNat(V1),V2)	(85)
a__U42^#(tt,V2)	→	a__isNatIList^#(V2)	(88)
a__isNatIList^#(V)	→	a__U31^#(a__isNatIListKind(V),V)	(100)
a__isNatIList^#(V)	→	a__isNatIListKind^#(V)	(101)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(102)
a__U41^#(tt,V1,V2)	→	a__isNat^#(V1)	(86)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(103)
a__isNatIList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(104)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(132)
mark^#(U42(X1,X2))	→	a__U42^#(mark(X1),X2)	(133)
mark^#(U42(X1,X2))	→	mark^#(X1)	(134)
mark^#(U43(X))	→	mark^#(X)	(136)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(137)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(138)
a__U51^#(tt,V1,V2)	→	a__isNat^#(V1)	(90)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(139)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(140)
mark^#(U52(X1,X2))	→	mark^#(X1)	(141)
mark^#(U53(X))	→	mark^#(X)	(143)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(148)
mark^#(and(X1,X2))	→	mark^#(X1)	(149)
mark^#(isNatIListKind(X))	→	a__isNatIListKind^#(X)	(150)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(151)
mark^#(cons(X1,X2))	→	mark^#(X1)	(152)
mark^#(s(X))	→	mark^#(X)	(153)

1.1.1.1.2 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

[a__and^#(x₁, x₂)]	=	2 · x₂
[a__U11^#(x₁, x₂)]	=	-2
[a__U21^#(x₁, x₂)]	=	-2
[a__U31^#(x₁, x₂)]	=	-2
[a__U41^#(x₁, x₂, x₃)]	=	-2 + x₁
[a__U42^#(x₁, x₂)]	=	-2
[a__U51^#(x₁, x₂, x₃)]	=	-2
[a__U52^#(x₁, x₂)]	=	-2
[a__isNatKind(x₁)]	=	0
[0]	=	0
[tt]	=	0
[mark(x₁)]	=	2 · x₁
[and(x₁, x₂)]	=	2 · x₁ + x₂
[a__and(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[isNatIListKind(x₁)]	=	0
[a__isNatIListKind(x₁)]	=	0
[cons(x₁, x₂)]	=	x₁ + 2 · x₂
[isNatKind(x₁)]	=	0
[length(x₁)]	=	1 + x₁
[s(x₁)]	=	x₁
[a__isNat(x₁)]	=	2 · x₁
[a__U11(x₁, x₂)]	=	2 + x₁ + 2 · x₂
[a__U21(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[isNat(x₁)]	=	2 · x₁
[zeros]	=	0
[a__zeros]	=	0
[U11(x₁, x₂)]	=	1 + x₁ + 2 · x₂
[U12(x₁)]	=	2 + x₁
[a__U12(x₁)]	=	2 + x₁
[isNatList(x₁)]	=	2 · x₁
[a__isNatList(x₁)]	=	2 · x₁
[U21(x₁, x₂)]	=	2 · x₁ + x₂
[U22(x₁)]	=	x₁
[a__U22(x₁)]	=	x₁
[U31(x₁, x₂)]	=	x₁ + 2 · x₂
[a__U31(x₁, x₂)]	=	x₁ + 2 · x₂
[U32(x₁)]	=	x₁
[a__U32(x₁)]	=	x₁
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + 2 · x₃
[a__U41(x₁, x₂, x₃)]	=	x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	x₁ + 2 · x₂
[a__U42(x₁, x₂)]	=	x₁ + 2 · x₂
[U43(x₁)]	=	x₁
[a__U43(x₁)]	=	x₁
[isNatIList(x₁)]	=	2 · x₁
[a__isNatIList(x₁)]	=	2 · x₁
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃
[a__U51(x₁, x₂, x₃)]	=	x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	x₁ + 2 · x₂
[a__U52(x₁, x₂)]	=	x₁ + 2 · x₂
[U53(x₁)]	=	x₁
[a__U53(x₁)]	=	x₁
[U61(x₁, x₂)]	=	1 + x₂
[a__U61(x₁, x₂)]	=	2 + 2 · x₂
[a__length(x₁)]	=	2 + x₁
[nil]	=	0
[a__isNatList^#(x₁)]	=	0
[mark^#(x₁)]	=	2 · x₁
[a__isNatKind^#(x₁)]	=	0
[a__isNatIListKind^#(x₁)]	=	0
[a__isNat^#(x₁)]	=	0
[a__isNatIList^#(x₁)]	=	0

the pairs

mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(117)
mark^#(U11(X1,X2))	→	mark^#(X1)	(118)
mark^#(U12(X))	→	mark^#(X)	(120)

could be deleted.

1.1.1.1.2.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

[a__and^#(x₁, x₂)]	=	2 + 2 · x₂
[a__U11^#(x₁, x₂)]	=	1 + 2 · x₂
[a__U21^#(x₁, x₂)]	=	1 + 2 · x₂
[a__U31^#(x₁, x₂)]	=	2 + 2 · x₂
[a__U41^#(x₁, x₂, x₃)]	=	2 + 2 · x₂ + 2 · x₃
[a__U42^#(x₁, x₂)]	=	2 + 2 · x₂
[a__U51^#(x₁, x₂, x₃)]	=	2 + 2 · x₂ + 2 · x₃
[a__U52^#(x₁, x₂)]	=	2 + 2 · x₂
[a__isNatKind(x₁)]	=	0
[0]	=	2
[tt]	=	0
[mark(x₁)]	=	0
[and(x₁, x₂)]	=	2 + x₁ + x₂
[a__and(x₁, x₂)]	=	-2
[isNatIListKind(x₁)]	=	2 · x₁
[a__isNatIListKind(x₁)]	=	0
[cons(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[isNatKind(x₁)]	=	1 + x₁
[length(x₁)]	=	1 + x₁
[s(x₁)]	=	2 + 2 · x₁
[a__isNat(x₁)]	=	0
[a__U11(x₁, x₂)]	=	-2 + x₂
[a__U21(x₁, x₂)]	=	1
[isNat(x₁)]	=	1 + 2 · x₁
[zeros]	=	0
[a__zeros]	=	0
[U11(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[U12(x₁)]	=	2 + 2 · x₁
[a__U12(x₁)]	=	-2
[isNatList(x₁)]	=	1 + 2 · x₁
[a__isNatList(x₁)]	=	0
[U21(x₁, x₂)]	=	1 + 2 · x₁ + x₂
[U22(x₁)]	=	x₁
[a__U22(x₁)]	=	-2
[U31(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U31(x₁, x₂)]	=	2
[U32(x₁)]	=	1 + 2 · x₁
[a__U32(x₁)]	=	0
[U41(x₁, x₂, x₃)]	=	2 + x₁ + 2 · x₂ + 2 · x₃
[a__U41(x₁, x₂, x₃)]	=	-2 + x₃
[U42(x₁, x₂)]	=	2 + x₁ + 2 · x₂
[a__U42(x₁, x₂)]	=	-2 + x₂
[U43(x₁)]	=	x₁
[a__U43(x₁)]	=	2
[isNatIList(x₁)]	=	2 + 2 · x₁
[a__isNatIList(x₁)]	=	0
[U51(x₁, x₂, x₃)]	=	2 + x₁ + 2 · x₂ + 2 · x₃
[a__U51(x₁, x₂, x₃)]	=	1 + x₂ + 2 · x₃
[U52(x₁, x₂)]	=	2 + x₁ + 2 · x₂
[a__U52(x₁, x₂)]	=	-2 + 2 · x₂
[U53(x₁)]	=	2 · x₁
[a__U53(x₁)]	=	-2
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[a__U61(x₁, x₂)]	=	-2 + x₂
[a__length(x₁)]	=	-2 + x₁
[nil]	=	2
[a__isNatList^#(x₁)]	=	2 · x₁
[mark^#(x₁)]	=	1 + 2 · x₁
[a__isNatKind^#(x₁)]	=	2 · x₁
[a__isNatIListKind^#(x₁)]	=	1 + 2 · x₁
[a__isNat^#(x₁)]	=	2 · x₁
[a__isNatIList^#(x₁)]	=	2 + 2 · x₁

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

a__isNatList^#(cons(V1,V2))	→	a__U51^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(109)
a__U52^#(tt,V2)	→	a__isNatList^#(V2)	(92)
a__isNatList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(110)
a__and^#(tt,X)	→	mark^#(X)	(95)
a__U11^#(tt,V1)	→	a__isNatList^#(V1)	(80)
a__isNatList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(111)
a__isNatKind^#(length(V1))	→	a__isNatIListKind^#(V1)	(107)
a__isNatIListKind^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(105)
a__isNatIListKind^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(106)
a__isNatKind^#(s(V1))	→	a__isNatKind^#(V1)	(108)
mark^#(isNatList(X))	→	a__isNatList^#(X)	(121)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(122)
a__U21^#(tt,V1)	→	a__isNat^#(V1)	(82)
a__isNat^#(length(V1))	→	a__U11^#(a__isNatIListKind(V1),V1)	(96)
a__isNat^#(length(V1))	→	a__isNatIListKind^#(V1)	(97)
a__isNat^#(s(V1))	→	a__U21^#(a__isNatKind(V1),V1)	(98)
a__isNat^#(s(V1))	→	a__isNatKind^#(V1)	(99)
mark^#(U21(X1,X2))	→	mark^#(X1)	(123)
mark^#(isNat(X))	→	a__isNat^#(X)	(126)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(127)
a__U31^#(tt,V)	→	a__isNatList^#(V)	(84)
mark^#(U31(X1,X2))	→	mark^#(X1)	(128)
mark^#(U32(X))	→	mark^#(X)	(130)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(131)
a__isNatIList^#(V)	→	a__isNatIListKind^#(V)	(101)
a__isNatIList^#(cons(V1,V2))	→	a__U41^#(a__and(a__isNatKind(V1),isNatIListKind(V2)),V1,V2)	(102)
a__U41^#(tt,V1,V2)	→	a__isNat^#(V1)	(86)
a__isNatIList^#(cons(V1,V2))	→	a__and^#(a__isNatKind(V1),isNatIListKind(V2))	(103)
a__isNatIList^#(cons(V1,V2))	→	a__isNatKind^#(V1)	(104)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(132)
mark^#(U42(X1,X2))	→	a__U42^#(mark(X1),X2)	(133)
mark^#(U42(X1,X2))	→	mark^#(X1)	(134)
mark^#(isNatIList(X))	→	a__isNatIList^#(X)	(137)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(138)
a__U51^#(tt,V1,V2)	→	a__isNat^#(V1)	(90)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(139)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(140)
mark^#(U52(X1,X2))	→	mark^#(X1)	(141)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(148)
mark^#(and(X1,X2))	→	mark^#(X1)	(149)
mark^#(isNatKind(X))	→	a__isNatKind^#(X)	(151)
mark^#(cons(X1,X2))	→	mark^#(X1)	(152)
mark^#(s(X))	→	mark^#(X)	(153)

could be deleted.

1.1.1.1.2.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(U43(X)) → mark^#(X) (136)

mark^#(U22(X)) → mark^#(X) (125)

mark^#(U53(X)) → mark^#(X) (143)

1.1.1.1.2.1.1.1 Usable Rules Processor

We restrict the rewrite rules to the following usable rules of the DP problem.

There are no rules.

1.1.1.1.2.1.1.1.1 Innermost Lhss Removal Processor

We restrict the innermost strategy to the following left hand sides.

There are no lhss.

1.1.1.1.2.1.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.

mark^#(U43(X)) → mark^#(X) (136)

1 > 1

mark^#(U22(X)) → mark^#(X) (125)

1 > 1

mark^#(U53(X)) → mark^#(X) (143)

1 > 1

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

Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/LengthOfFiniteLists_complete_GM)

Property / Task

Answer / Result

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

1.1 Dependency Graph Processor

1.1.1 Reduction Pair Processor

1.1.1.1 Dependency Graph Processor

1.1.1.1.1 Reduction Pair Processor

1.1.1.1.1.1 Size-Change Termination

1.1.1.1.2 Reduction Pair Processor

1.1.1.1.2.1 Reduction Pair Processor with Usable Rules

1.1.1.1.2.1.1 Dependency Graph Processor

1.1.1.1.2.1.1.1 Usable Rules Processor

1.1.1.1.2.1.1.1.1 Innermost Lhss Removal Processor

1.1.1.1.2.1.1.1.1.1 Size-Change Termination