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 AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
intersect'ii'in#(Xs,cons(X0,Ys)) u'1'1#(intersect'ii'in(Xs,Ys)) (36)
intersect'ii'in#(Xs,cons(X0,Ys)) intersect'ii'in#(Xs,Ys) (37)
intersect'ii'in#(cons(X0,Xs),Ys) u'2'1#(intersect'ii'in(Xs,Ys)) (38)
intersect'ii'in#(cons(X0,Xs),Ys) intersect'ii'in#(Xs,Ys) (39)
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)) (40)
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) (41)
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)) (42)
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) (43)
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)) (44)
reduce'ii'in#(sequent(cons(x'2a(F1,F2),Fs),Gs),NF) reduce'ii'in#(sequent(cons(F1,cons(F2,Fs)),Gs),NF) (45)
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) (46)
reduce'ii'in#(sequent(cons(x'2b(F1,F2),Fs),Gs),NF) reduce'ii'in#(sequent(cons(F1,Fs),Gs),NF) (47)
u'6'1#(reduce'ii'out,F2,Fs,Gs,NF) u'6'2#(reduce'ii'in(sequent(cons(F2,Fs),Gs),NF)) (48)
u'6'1#(reduce'ii'out,F2,Fs,Gs,NF) reduce'ii'in#(sequent(cons(F2,Fs),Gs),NF) (49)
reduce'ii'in#(sequent(cons(x'2d(F1),Fs),Gs),NF) u'7'1#(reduce'ii'in(sequent(Fs,cons(F1,Gs)),NF)) (50)
reduce'ii'in#(sequent(cons(x'2d(F1),Fs),Gs),NF) reduce'ii'in#(sequent(Fs,cons(F1,Gs)),NF) (51)
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)) (52)
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) (53)
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)) (54)
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) (55)
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))) (56)
reduce'ii'in#(sequent(cons(p(V),Fs),Gs),sequent(Left,Right)) 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) u'11'1#(reduce'ii'in(sequent(Fs,cons(G1,cons(G2,Gs))),NF)) (58)
reduce'ii'in#(sequent(Fs,cons(x'2b(G1,G2),Gs)),NF) reduce'ii'in#(sequent(Fs,cons(G1,cons(G2,Gs))),NF) (59)
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) (60)
reduce'ii'in#(sequent(Fs,cons(x'2a(G1,G2),Gs)),NF) reduce'ii'in#(sequent(Fs,cons(G1,Gs)),NF) (61)
u'12'1#(reduce'ii'out,Fs,G2,Gs,NF) u'12'2#(reduce'ii'in(sequent(Fs,cons(G2,Gs)),NF)) (62)
u'12'1#(reduce'ii'out,Fs,G2,Gs,NF) reduce'ii'in#(sequent(Fs,cons(G2,Gs)),NF) (63)
reduce'ii'in#(sequent(Fs,cons(x'2d(G1),Gs)),NF) u'13'1#(reduce'ii'in(sequent(cons(G1,Fs),Gs),NF)) (64)
reduce'ii'in#(sequent(Fs,cons(x'2d(G1),Gs)),NF) reduce'ii'in#(sequent(cons(G1,Fs),Gs),NF) (65)
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)))) (66)
reduce'ii'in#(sequent(nil,cons(p(V),Gs)),sequent(Left,Right)) reduce'ii'in#(sequent(nil,Gs),sequent(Left,cons(p(V),Right))) (67)
reduce'ii'in#(sequent(nil,nil),sequent(F1,F2)) u'15'1#(intersect'ii'in(F1,F2)) (68)
reduce'ii'in#(sequent(nil,nil),sequent(F1,F2)) intersect'ii'in#(F1,F2) (69)
tautology'i'in#(F) u'16'1#(reduce'ii'in(sequent(nil,cons(F,nil)),sequent(nil,nil))) (70)
tautology'i'in#(F) 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.