Left Termination of the query pattern
subset(g,g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

member(X, .(Y, Xs)) :- member(X, Xs).
member(X, .(X, Xs)).
subset(.(X, Xs), Ys) :- ','(member(X, Ys), subset(Xs, Ys)).
subset([], Ys).

Query: subset(g,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: subset(T1, T2)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: subset(T1, T2), SCOPE: 1, CLAUSE: 2 | subset(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(member(T6, T8), subset(T7, T8)) | subset(.(T6, T7), T8), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: subset(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX4 is free\nX5 is free\nX6 is free\nsubset(T1, T2) !=? subset(.(X4, X5), X6)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(member(T6, T8), subset(T7, T8)), SCOPE: 2, CLAUSE: 0 | ','(member(T6, T8), subset(T7, T8)), SCOPE: 2, CLAUSE: 1 | ?_2 | subset(.(T6, T7), T8), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(member(T6, T8), subset(T7, T8)), SCOPE: 2, CLAUSE: 0\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(member(T6, T8), subset(T7, T8)), SCOPE: 2, CLAUSE: 1 | ?_2 | subset(.(T6, T7), T8), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="B: ','(member(T21, T23), subset(T7, .(T22, T23)))\n\nT7 is ground\nT21 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="C: member(T21, T23)\n\nT21 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: subset(T7, .(T22, T23))\n\nT7 is ground\nT22 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: member(T21, T23), SCOPE: 3, CLAUSE: 0 | member(T21, T23), SCOPE: 3, CLAUSE: 1\n\nT21 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: member(T21, T23), SCOPE: 3, CLAUSE: 0\n\nT21 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: member(T21, T23), SCOPE: 3, CLAUSE: 1\n\nT21 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: member(T42, T44)\n\nT42 is ground\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(member(T6, T8), subset(T7, T8)), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ?_2 | subset(.(T6, T7), T8), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: subset(T7, .(T66, T67))\n\nT7 is ground\nT66 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: subset(.(T6, T7), T8), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 76 [arrowhead = none ];
76 -> 6;

77 [label="EVAL with clause\nsubset(.(X4, X5), X6) :- ','(member(X4, X6), subset(X5, X6)).\nand substitutionX4 -> T6,\nX5 -> T7,\nT1 -> .(T6, T7),\nT2 -> T8,\nX6 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 77 [arrowhead = none ];
77 -> 10;

78 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 78 [arrowhead = none ];
78 -> 12;

79 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 79 [arrowhead = none ];
79 -> 16;

80 [label="EVAL with clause\nsubset([], X70).\nand substitutionT1 -> [],\nT2 -> T73,\nX70 -> T73", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 80 [arrowhead = none ];
80 -> 73;

81 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 81 [arrowhead = none ];
81 -> 74;

82 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 82 [arrowhead = none ];
82 -> 18;

83 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 83 [arrowhead = none ];
83 -> 20;

84 [label="EVAL with clause\nmember(X19, .(X20, X21)) :- member(X19, X21).\nand substitutionT6 -> T21,\nX19 -> T21,\nX20 -> T22,\nX21 -> T23,\nT8 -> .(T22, T23)", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 84 [arrowhead = none ];
84 -> 23;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 85 [arrowhead = none ];
85 -> 24;

86 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 86 [arrowhead = none ];
86 -> 62;

87 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 87 [arrowhead = none ];
87 -> 63;

88 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
23 -> 88 [arrowhead = none ];
88 -> 27;

89 [label="SPLIT 2\nnew knowledge:\nT21 is ground\nT23 is ground", fontsize=14, style = filled, fillcolor = violet];
23 -> 89 [arrowhead = none ];
89 -> 30;

90 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 90 [arrowhead = none ];
90 -> 33;

91 [label="INSTANCE with matching:\nT1 -> T7\nT2 -> .(T22, T23)", fontsize=14, style = filled, fillcolor = lightgrey];
30 -> 91 [arrowhead = none , style=dashed];
91 -> 3[style=dashed];

92 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
33 -> 92 [arrowhead = none ];
92 -> 38;

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
33 -> 93 [arrowhead = none ];
93 -> 39;

94 [label="EVAL with clause\nmember(X40, .(X41, X42)) :- member(X40, X42).\nand substitutionT21 -> T42,\nX40 -> T42,\nX41 -> T43,\nX42 -> T44,\nT23 -> .(T43, T44)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 94 [arrowhead = none ];
94 -> 43;

95 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 95 [arrowhead = none ];
95 -> 45;

96 [label="EVAL with clause\nmember(X50, .(X50, X51)).\nand substitutionT21 -> T52,\nX50 -> T52,\nX51 -> T53,\nT23 -> .(T52, T53)", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 96 [arrowhead = none ];
96 -> 47;

97 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 97 [arrowhead = none ];
97 -> 50;

98 [label="INSTANCE with matching:\nT21 -> T42\nT23 -> T44", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 98 [arrowhead = none , style=dashed];
98 -> 27[style=dashed];

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 99 [arrowhead = none ];
99 -> 51;

100 [label="EVAL with clause\nmember(X63, .(X63, X64)).\nand substitutionT6 -> T66,\nX63 -> T66,\nX64 -> T67,\nT8 -> .(T66, T67)", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 100 [arrowhead = none ];
100 -> 66;

101 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 101 [arrowhead = none ];
101 -> 67;

102 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 102 [arrowhead = none ];
102 -> 71;

103 [label="INSTANCE with matching:\nT1 -> T7\nT2 -> .(T66, T67)", fontsize=14, style = filled, fillcolor = lightgrey];
66 -> 103 [arrowhead = none , style=dashed];
103 -> 3[style=dashed];

104 [label="BACKTRACK\nfor clause: subset([], Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 104 [arrowhead = none ];
104 -> 72;

105 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 105 [arrowhead = none ];
105 -> 75;

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → U1_GG(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
PB_IN_GGGG(T21, T23, T7, T22) → MEMBERC_IN_GG(T21, T23)
MEMBERC_IN_GG(T42, .(T43, T44)) → U3_GG(T42, T43, T44, memberC_in_gg(T42, T44))
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_GGGG(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → U2_GG(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))

The TRS R consists of the following rules:

subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → U1_GG(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
PB_IN_GGGG(T21, T23, T7, T22) → MEMBERC_IN_GG(T21, T23)
MEMBERC_IN_GG(T42, .(T43, T44)) → U3_GG(T42, T43, T44, memberC_in_gg(T42, T44))
MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_GGGG(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → U2_GG(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))

The TRS R consists of the following rules:

subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 5 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)

The TRS R consists of the following rules:

subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MEMBERC_IN_GG(T42, .(T43, T44)) → MEMBERC_IN_GG(T42, T44)
  The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))

The TRS R consists of the following rules:

subsetA_in_gg(.(T21, T7), .(T22, T23)) → U1_gg(T21, T7, T22, T23, pB_in_gggg(T21, T23, T7, T22))
pB_in_gggg(T21, T23, T7, T22) → U4_gggg(T21, T23, T7, T22, memberC_in_gg(T21, T23))
memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))
U4_gggg(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → U5_gggg(T21, T23, T7, T22, subsetA_in_gg(T7, .(T22, T23)))
subsetA_in_gg(.(T66, T7), .(T66, T67)) → U2_gg(T66, T7, T67, subsetA_in_gg(T7, .(T66, T67)))
subsetA_in_gg([], T73) → subsetA_out_gg([], T73)
U2_gg(T66, T7, T67, subsetA_out_gg(T7, .(T66, T67))) → subsetA_out_gg(.(T66, T7), .(T66, T67))
U5_gggg(T21, T23, T7, T22, subsetA_out_gg(T7, .(T22, T23))) → pB_out_gggg(T21, T23, T7, T22)
U1_gg(T21, T7, T22, T23, pB_out_gggg(T21, T23, T7, T22)) → subsetA_out_gg(.(T21, T7), .(T22, T23))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))

The TRS R consists of the following rules:

memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))

Pi is empty.
We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))

The TRS R consists of the following rules:

memberC_in_gg(T42, .(T43, T44)) → U3_gg(T42, T43, T44, memberC_in_gg(T42, T44))
memberC_in_gg(T52, .(T52, T53)) → memberC_out_gg(T52, .(T52, T53))
U3_gg(T42, T43, T44, memberC_out_gg(T42, T44)) → memberC_out_gg(T42, .(T43, T44))

The set Q consists of the following terms:

memberC_in_gg(x0, x1)
U3_gg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• PB_IN_GGGG(T21, T23, T7, T22) → U4_GGGG(T21, T23, T7, T22, memberC_in_gg(T21, T23))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4

• SUBSETA_IN_GG(.(T21, T7), .(T22, T23)) → PB_IN_GGGG(T21, T23, T7, T22)
  The graph contains the following edges 1 > 1, 2 > 2, 1 > 3, 2 > 4

• U4_GGGG(T21, T23, T7, T22, memberC_out_gg(T21, T23)) → SUBSETA_IN_GG(T7, .(T22, T23))
  The graph contains the following edges 3 >= 1

• SUBSETA_IN_GG(.(T66, T7), .(T66, T67)) → SUBSETA_IN_GG(T7, .(T66, T67))
  The graph contains the following edges 1 > 1, 2 >= 2

(20) YES