Certification Problem

Input (TPDB TRS_Standard/Secret_05_TRS/cime5)

The rewrite relation of the following TRS is considered.

intersect'ii'in(cons(X,X0),cons(X,X1))	→	intersect'ii'out	(1)
intersect'ii'in(Xs,cons(X0,Ys))	→	u'1'1(intersect'ii'in(Xs,Ys))	(2)
u'1'1(intersect'ii'out)	→	intersect'ii'out	(3)
intersect'ii'in(cons(X0,Xs),Ys)	→	u'2'1(intersect'ii'in(Xs,Ys))	(4)
u'2'1(intersect'ii'out)	→	intersect'ii'out	(5)
reduce'ii'in(sequent(cons(if(A,B),Fs),Gs),NF)	→	u'3'1(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs),NF))	(6)
u'3'1(reduce'ii'out)	→	reduce'ii'out	(7)
reduce'ii'in(sequent(cons(iff(A,B),Fs),Gs),NF)	→	u'4'1(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF))	(8)
u'4'1(reduce'ii'out)	→	reduce'ii'out	(9)
reduce'ii'in(sequent(cons(x'2a(F1,F2),Fs),Gs),NF)	→	u'5'1(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs),NF))	(10)
u'5'1(reduce'ii'out)	→	reduce'ii'out	(11)
reduce'ii'in(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	u'6'1(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF),F2,Fs,Gs,NF)	(12)
u'6'1(reduce'ii'out,F2,Fs,Gs,NF)	→	u'6'2(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF))	(13)
u'6'2(reduce'ii'out)	→	reduce'ii'out	(14)
reduce'ii'in(sequent(cons(x'2d(F1),Fs),Gs),NF)	→	u'7'1(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF))	(15)
u'7'1(reduce'ii'out)	→	reduce'ii'out	(16)
reduce'ii'in(sequent(Fs,cons(if(A,B),Gs)),NF)	→	u'8'1(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs)),NF))	(17)
u'8'1(reduce'ii'out)	→	reduce'ii'out	(18)
reduce'ii'in(sequent(Fs,cons(iff(A,B),Gs)),NF)	→	u'9'1(reduce'ii'in(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF))	(19)
u'9'1(reduce'ii'out)	→	reduce'ii'out	(20)
reduce'ii'in(sequent(cons(p(V),Fs),Gs),sequent(Left,Right))	→	u'10'1(reduce'ii'in(sequent(Fs,Gs),sequent(cons(p(V),Left),Right)))	(21)
u'10'1(reduce'ii'out)	→	reduce'ii'out	(22)
reduce'ii'in(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF)	→	u'11'1(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs))),NF))	(23)
u'11'1(reduce'ii'out)	→	reduce'ii'out	(24)
reduce'ii'in(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	u'12'1(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF),Fs,G2,Gs,NF)	(25)
u'12'1(reduce'ii'out,Fs,G2,Gs,NF)	→	u'12'2(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF))	(26)
u'12'2(reduce'ii'out)	→	reduce'ii'out	(27)
reduce'ii'in(sequent(Fs,cons(x'2d(G1),Gs)),NF)	→	u'13'1(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF))	(28)
u'13'1(reduce'ii'out)	→	reduce'ii'out	(29)
reduce'ii'in(sequent(nil,cons(p(V),Gs)),sequent(Left,Right))	→	u'14'1(reduce'ii'in(sequent(nil,Gs),sequent(Left,cons(p(V),Right))))	(30)
u'14'1(reduce'ii'out)	→	reduce'ii'out	(31)
reduce'ii'in(sequent(nil,nil),sequent(F1,F2))	→	u'15'1(intersect'ii'in(F1,F2))	(32)
u'15'1(intersect'ii'out)	→	reduce'ii'out	(33)
tautology'i'in(F)	→	u'16'1(reduce'ii'in(sequent(nil,cons(F,nil)),sequent(nil,nil)))	(34)
u'16'1(reduce'ii'out)	→	tautology'i'out	(35)

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.

intersect'ii'in^#(Xs,cons(X0,Ys))	→	intersect'ii'in^#(Xs,Ys)	(36)
intersect'ii'in^#(Xs,cons(X0,Ys))	→	u'1'1^#(intersect'ii'in(Xs,Ys))	(37)
intersect'ii'in^#(cons(X0,Xs),Ys)	→	intersect'ii'in^#(Xs,Ys)	(38)
intersect'ii'in^#(cons(X0,Xs),Ys)	→	u'2'1^#(intersect'ii'in(Xs,Ys))	(39)
reduce'ii'in^#(sequent(cons(if(A,B),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(x'2b(x'2d(B),A),Fs),Gs),NF)	(40)
reduce'ii'in^#(sequent(cons(if(A,B),Fs),Gs),NF)	→	u'3'1^#(reduce'ii'in(sequent(cons(x'2b(x'2d(B),A),Fs),Gs),NF))	(41)
reduce'ii'in^#(sequent(cons(iff(A,B),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF)	(42)
reduce'ii'in^#(sequent(cons(iff(A,B),Fs),Gs),NF)	→	u'4'1^#(reduce'ii'in(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF))	(43)
reduce'ii'in^#(sequent(cons(x'2a(F1,F2),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)	(44)
reduce'ii'in^#(sequent(cons(x'2a(F1,F2),Fs),Gs),NF)	→	u'5'1^#(reduce'ii'in(sequent(cons(F1,cons(F2,Fs)),Gs),NF))	(45)
reduce'ii'in^#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(F1,Fs),Gs),NF)	(46)
reduce'ii'in^#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	u'6'1^#(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF),F2,Fs,Gs,NF)	(47)
u'6'1^#(reduce'ii'out,F2,Fs,Gs,NF)	→	reduce'ii'in^#(sequent(cons(F2,Fs),Gs),NF)	(48)
u'6'1^#(reduce'ii'out,F2,Fs,Gs,NF)	→	u'6'2^#(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF))	(49)
reduce'ii'in^#(sequent(cons(x'2d(F1),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(Fs,cons(F1,Gs)),NF)	(50)
reduce'ii'in^#(sequent(cons(x'2d(F1),Fs),Gs),NF)	→	u'7'1^#(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF))	(51)
reduce'ii'in^#(sequent(Fs,cons(if(A,B),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(x'2b(x'2d(B),A),Gs)),NF)	(52)
reduce'ii'in^#(sequent(Fs,cons(if(A,B),Gs)),NF)	→	u'8'1^#(reduce'ii'in(sequent(Fs,cons(x'2b(x'2d(B),A),Gs)),NF))	(53)
reduce'ii'in^#(sequent(Fs,cons(iff(A,B),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF)	(54)
reduce'ii'in^#(sequent(Fs,cons(iff(A,B),Gs)),NF)	→	u'9'1^#(reduce'ii'in(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF))	(55)
reduce'ii'in^#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right))	→	reduce'ii'in^#(sequent(Fs,Gs),sequent(cons(p(V),Left),Right))	(56)
reduce'ii'in^#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right))	→	u'10'1^#(reduce'ii'in(sequent(Fs,Gs),sequent(cons(p(V),Left),Right)))	(57)
reduce'ii'in^#(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(G1,cons(G2,Gs))),NF)	(58)
reduce'ii'in^#(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF)	→	u'11'1^#(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs))),NF))	(59)
reduce'ii'in^#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(G1,Gs)),NF)	(60)
reduce'ii'in^#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	u'12'1^#(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF),Fs,G2,Gs,NF)	(61)
u'12'1^#(reduce'ii'out,Fs,G2,Gs,NF)	→	reduce'ii'in^#(sequent(Fs,cons(G2,Gs)),NF)	(62)
u'12'1^#(reduce'ii'out,Fs,G2,Gs,NF)	→	u'12'2^#(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF))	(63)
reduce'ii'in^#(sequent(Fs,cons(x'2d(G1),Gs)),NF)	→	reduce'ii'in^#(sequent(cons(G1,Fs),Gs),NF)	(64)
reduce'ii'in^#(sequent(Fs,cons(x'2d(G1),Gs)),NF)	→	u'13'1^#(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF))	(65)
reduce'ii'in^#(sequent(nil,cons(p(V),Gs)),sequent(Left,Right))	→	reduce'ii'in^#(sequent(nil,Gs),sequent(Left,cons(p(V),Right)))	(66)
reduce'ii'in^#(sequent(nil,cons(p(V),Gs)),sequent(Left,Right))	→	u'14'1^#(reduce'ii'in(sequent(nil,Gs),sequent(Left,cons(p(V),Right))))	(67)
reduce'ii'in^#(sequent(nil,nil),sequent(F1,F2))	→	intersect'ii'in^#(F1,F2)	(68)
reduce'ii'in^#(sequent(nil,nil),sequent(F1,F2))	→	u'15'1^#(intersect'ii'in(F1,F2))	(69)
tautology'i'in^#(F)	→	reduce'ii'in^#(sequent(nil,cons(F,nil)),sequent(nil,nil))	(70)
tautology'i'in^#(F)	→	u'16'1^#(reduce'ii'in(sequent(nil,cons(F,nil)),sequent(nil,nil)))	(71)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

reduce'ii'in^#(sequent(nil,cons(p(V),Gs)),sequent(Left,Right))	→	reduce'ii'in^#(sequent(nil,Gs),sequent(Left,cons(p(V),Right)))	(66)
reduce'ii'in^#(sequent(Fs,cons(x'2d(G1),Gs)),NF)	→	reduce'ii'in^#(sequent(cons(G1,Fs),Gs),NF)	(64)
reduce'ii'in^#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	u'12'1^#(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF),Fs,G2,Gs,NF)	(61)
u'12'1^#(reduce'ii'out,Fs,G2,Gs,NF)	→	reduce'ii'in^#(sequent(Fs,cons(G2,Gs)),NF)	(62)
reduce'ii'in^#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(G1,Gs)),NF)	(60)
reduce'ii'in^#(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(G1,cons(G2,Gs))),NF)	(58)
reduce'ii'in^#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right))	→	reduce'ii'in^#(sequent(Fs,Gs),sequent(cons(p(V),Left),Right))	(56)
reduce'ii'in^#(sequent(Fs,cons(iff(A,B),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF)	(54)
reduce'ii'in^#(sequent(cons(x'2d(F1),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(Fs,cons(F1,Gs)),NF)	(50)
reduce'ii'in^#(sequent(Fs,cons(if(A,B),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(x'2b(x'2d(B),A),Gs)),NF)	(52)
reduce'ii'in^#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	u'6'1^#(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF),F2,Fs,Gs,NF)	(47)
u'6'1^#(reduce'ii'out,F2,Fs,Gs,NF)	→	reduce'ii'in^#(sequent(cons(F2,Fs),Gs),NF)	(48)
reduce'ii'in^#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(F1,Fs),Gs),NF)	(46)
reduce'ii'in^#(sequent(cons(x'2a(F1,F2),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)	(44)
reduce'ii'in^#(sequent(cons(iff(A,B),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF)	(42)
reduce'ii'in^#(sequent(cons(if(A,B),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(x'2b(x'2d(B),A),Fs),Gs),NF)	(40)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(u'12'1^#)	=	{ 2, 2, 3, 3, 4 }
π(u'6'1^#)	=	{ 2, 2, 2, 3, 3, 4 }
π(reduce'ii'in^#)	=	{ 1 }
π(u'14'1)	=	{ 1, 1, 1 }
π(u'13'1)	=	{ 1, 1, 1 }
π(u'10'1)	=	{ 1, 1, 1 }
π(u'9'1)	=	{ 1 }
π(u'8'1)	=	{ 1, 1, 1 }
π(u'7'1)	=	{ 1, 1, 1 }
π(u'6'2)	=	{ 1, 1, 1 }
π(u'5'1)	=	{ 1, 1, 1 }
π(u'4'1)	=	{ 1, 1, 1 }
π(x'2a)	=	{ 1, 1, 2, 2 }
π(x'2b)	=	{ 1, 2, 2 }
π(x'2d)	=	{ 1, 1, 1 }
π(sequent)	=	{ 1, 1, 2 }
π(if)	=	{ 1, 1, 1, 2, 2, 2 }
π(cons)	=	{ 1, 2 }

to remove the pairs:

reduce'ii'in^#(sequent(nil,cons(p(V),Gs)),sequent(Left,Right))	→	reduce'ii'in^#(sequent(nil,Gs),sequent(Left,cons(p(V),Right)))	(66)
reduce'ii'in^#(sequent(Fs,cons(x'2d(G1),Gs)),NF)	→	reduce'ii'in^#(sequent(cons(G1,Fs),Gs),NF)	(64)
reduce'ii'in^#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	u'12'1^#(reduce'ii'in(sequent(Fs,cons(G1,Gs)),NF),Fs,G2,Gs,NF)	(61)
u'12'1^#(reduce'ii'out,Fs,G2,Gs,NF)	→	reduce'ii'in^#(sequent(Fs,cons(G2,Gs)),NF)	(62)
reduce'ii'in^#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(G1,Gs)),NF)	(60)
reduce'ii'in^#(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(G1,cons(G2,Gs))),NF)	(58)
reduce'ii'in^#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right))	→	reduce'ii'in^#(sequent(Fs,Gs),sequent(cons(p(V),Left),Right))	(56)
reduce'ii'in^#(sequent(Fs,cons(iff(A,B),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(x'2a(if(A,B),if(B,A)),Gs)),NF)	(54)
reduce'ii'in^#(sequent(cons(x'2d(F1),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(Fs,cons(F1,Gs)),NF)	(50)
reduce'ii'in^#(sequent(Fs,cons(if(A,B),Gs)),NF)	→	reduce'ii'in^#(sequent(Fs,cons(x'2b(x'2d(B),A),Gs)),NF)	(52)
reduce'ii'in^#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	u'6'1^#(reduce'ii'in(sequent(cons(F1,Fs),Gs),NF),F2,Fs,Gs,NF)	(47)
u'6'1^#(reduce'ii'out,F2,Fs,Gs,NF)	→	reduce'ii'in^#(sequent(cons(F2,Fs),Gs),NF)	(48)
reduce'ii'in^#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(F1,Fs),Gs),NF)	(46)
reduce'ii'in^#(sequent(cons(x'2a(F1,F2),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(F1,cons(F2,Fs)),Gs),NF)	(44)
reduce'ii'in^#(sequent(cons(iff(A,B),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(x'2a(if(A,B),if(B,A)),Fs),Gs),NF)	(42)
reduce'ii'in^#(sequent(cons(if(A,B),Fs),Gs),NF)	→	reduce'ii'in^#(sequent(cons(x'2b(x'2d(B),A),Fs),Gs),NF)	(40)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

intersect'ii'in^#(cons(X0,Xs),Ys) → intersect'ii'in^#(Xs,Ys) (38)

intersect'ii'in^#(Xs,cons(X0,Ys)) → intersect'ii'in^#(Xs,Ys) (36)

1.1.2 Subterm Criterion Processor
We use the projection
π(intersect'ii'in^#) = 1
and remove the pairs:
intersect'ii'in^#(cons(X0,Xs),Ys) → intersect'ii'in^#(Xs,Ys) (38)

1.1.2.1 Size-Change Termination

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

intersect'ii'in^#(Xs,cons(X0,Ys)) → intersect'ii'in^#(Xs,Ys) (36)

2 > 2

1 ≥ 1

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