Left Termination proof of /tmp/tmpGAHAaY/reminder.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 130 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 47 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 23 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 41 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 TRUE

(0) Obligation:

Clauses:

rem(X, Y, R) :- ','(notZero(Y), ','(sub(X, Y, Z), rem(Z, Y, R))).
rem(X, Y, X) :- ','(notZero(Y), geq(X, Y)).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
notZero(s(X)).
geq(s(X), s(Y)) :- geq(X, Y).
geq(X, 0).

Query: rem(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: rem(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: rem(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | rem(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(notZero(T8), ','(sub(T7, T8, X7), rem(X7, T8, T10))) | rem(T7, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(notZero(T8), ','(sub(T7, T8, X7), rem(X7, T8, T10))), SCOPE: 2, CLAUSE: 4 | ?_2 | rem(T7, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(notZero(T8), ','(sub(T7, T8, X7), rem(X7, T8, T10))), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nT8 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ?_2 | rem(T7, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="B: ','(sub(T7, s(T15), X7), rem(X7, s(T15), T10))\n\nT7 is ground\nT15 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="E: sub(T7, s(T15), X7)\n\nT7 is ground\nT15 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: rem(T18, s(T15), T10)\n\nT15 is ground\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: sub(T7, s(T15), X7), SCOPE: 3, CLAUSE: 2 | sub(T7, s(T15), X7), SCOPE: 3, CLAUSE: 3\n\nT7 is ground\nT15 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: sub(T7, s(T15), X7), SCOPE: 3, CLAUSE: 2\n\nT7 is ground\nT15 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: sub(T7, s(T15), X7), SCOPE: 3, CLAUSE: 3\n\nT7 is ground\nT15 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="D: sub(T29, T30, X40)\n\nT29 is ground\nT30 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: sub(T29, T30, X40), SCOPE: 4, CLAUSE: 2 | sub(T29, T30, X40), SCOPE: 4, CLAUSE: 3\n\nT29 is ground\nT30 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: sub(T29, T30, X40), SCOPE: 4, CLAUSE: 2\n\nT29 is ground\nT30 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: sub(T29, T30, X40), SCOPE: 4, CLAUSE: 3\n\nT29 is ground\nT30 is ground\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: sub(T41, T42, X64)\n\nT41 is ground\nT42 is ground\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: rem(T7, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(notZero(T57), geq(T56, T57))\n\nT56 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(notZero(T57), geq(T56, T57)), SCOPE: 5, CLAUSE: 4\n\nT56 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: geq(T56, s(T62))\n\nT56 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: geq(T56, s(T62)), SCOPE: 6, CLAUSE: 5 | geq(T56, s(T62)), SCOPE: 6, CLAUSE: 6\n\nT56 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: geq(T56, s(T62)), SCOPE: 6, CLAUSE: 5\n\nT56 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: geq(T56, s(T62)), SCOPE: 6, CLAUSE: 6\n\nT56 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="C: geq(T73, T74)\n\nT73 is ground\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: geq(T73, T74), SCOPE: 7, CLAUSE: 5 | geq(T73, T74), SCOPE: 7, CLAUSE: 6\n\nT73 is ground\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: geq(T73, T74), SCOPE: 7, CLAUSE: 5\n\nT73 is ground\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: geq(T73, T74), SCOPE: 7, CLAUSE: 6\n\nT73 is ground\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: geq(T85, T86)\n\nT85 is ground\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 132 [arrowhead = none ];
132 -> 4;

133 [label="ONLY EVAL with clause\nrem(X4, X5, X6) :- ','(notZero(X5), ','(sub(X4, X5, X7), rem(X7, X5, X6))).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T8,\nX5 -> T8,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 133 [arrowhead = none ];
133 -> 13;

134 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 134 [arrowhead = none ];
134 -> 14;

135 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 135 [arrowhead = none ];
135 -> 15;

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

137 [label="EVAL with clause\nnotZero(s(X12)).\nand substitutionX12 -> T15,\nT8 -> s(T15)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 137 [arrowhead = none ];
137 -> 17;

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

139 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 139 [arrowhead = none ];
139 -> 69;

140 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 140 [arrowhead = none ];
140 -> 26;

141 [label="SPLIT 2\nnew knowledge:\nT7 is ground\nT15 is ground\nT18 is ground\nreplacements:X7 -> T18", fontsize=14, style = filled, fillcolor = violet];
17 -> 141 [arrowhead = none ];
141 -> 28;

142 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
26 -> 142 [arrowhead = none ];
142 -> 31;

143 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> s(T15)\nT3 -> T10", fontsize=14, style = filled, fillcolor = lightgrey];
28 -> 143 [arrowhead = none , style=dashed];
143 -> 1[style=dashed];

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 144 [arrowhead = none ];
144 -> 34;

145 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 145 [arrowhead = none ];
145 -> 35;

146 [label="EVAL with clause\nsub(s(X37), s(X38), X39) :- sub(X37, X38, X39).\nand substitutionX37 -> T29,\nT7 -> s(T29),\nT15 -> T30,\nX38 -> T30,\nX7 -> X40,\nX39 -> X40", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 146 [arrowhead = none ];
146 -> 42;

147 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 147 [arrowhead = none ];
147 -> 43;

148 [label="BACKTRACK\nfor clause: sub(X, 0, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 148 [arrowhead = none ];
148 -> 68;

149 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
42 -> 149 [arrowhead = none ];
149 -> 50;

150 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 150 [arrowhead = none ];
150 -> 52;

151 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 151 [arrowhead = none ];
151 -> 53;

152 [label="EVAL with clause\nsub(s(X61), s(X62), X63) :- sub(X61, X62, X63).\nand substitutionX61 -> T41,\nT29 -> s(T41),\nX62 -> T42,\nT30 -> s(T42),\nX40 -> X64,\nX63 -> X64", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 152 [arrowhead = none ];
152 -> 55;

153 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 153 [arrowhead = none ];
153 -> 56;

154 [label="EVAL with clause\nsub(X71, 0, X71).\nand substitutionT29 -> T47,\nX71 -> T47,\nT30 -> 0,\nX40 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 154 [arrowhead = none ];
154 -> 63;

155 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 155 [arrowhead = none ];
155 -> 65;

156 [label="INSTANCE with matching:\nT29 -> T41\nT30 -> T42\nX40 -> X64", fontsize=14, style = filled, fillcolor = lightgrey];
55 -> 156 [arrowhead = none , style=dashed];
156 -> 42[style=dashed];

157 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 157 [arrowhead = none ];
157 -> 66;

158 [label="EVAL with clause\nrem(X81, X82, X81) :- ','(notZero(X82), geq(X81, X82)).\nand substitutionT7 -> T56,\nX81 -> T56,\nT8 -> T57,\nX82 -> T57,\nT3 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 158 [arrowhead = none ];
158 -> 72;

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

160 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 160 [arrowhead = none ];
160 -> 75;

161 [label="EVAL with clause\nnotZero(s(X87)).\nand substitutionX87 -> T62,\nT57 -> s(T62)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 161 [arrowhead = none ];
161 -> 78;

162 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 162 [arrowhead = none ];
162 -> 79;

163 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 163 [arrowhead = none ];
163 -> 81;

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

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

166 [label="EVAL with clause\ngeq(s(X98), s(X99)) :- geq(X98, X99).\nand substitutionX98 -> T73,\nT56 -> s(T73),\nT62 -> T74,\nX99 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 166 [arrowhead = none ];
166 -> 94;

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

168 [label="BACKTRACK\nfor clause: geq(X, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 168 [arrowhead = none ];
168 -> 131;

169 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
94 -> 169 [arrowhead = none ];
169 -> 101;

170 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
101 -> 170 [arrowhead = none ];
170 -> 104;

171 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
101 -> 171 [arrowhead = none ];
171 -> 106;

172 [label="EVAL with clause\ngeq(s(X110), s(X111)) :- geq(X110, X111).\nand substitutionX110 -> T85,\nT73 -> s(T85),\nX111 -> T86,\nT74 -> s(T86)", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 172 [arrowhead = none ];
172 -> 109;

173 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 173 [arrowhead = none ];
173 -> 112;

174 [label="EVAL with clause\ngeq(X116, 0).\nand substitutionT73 -> T91,\nX116 -> T91,\nT74 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 174 [arrowhead = none ];
174 -> 128;

175 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 175 [arrowhead = none ];
175 -> 129;

176 [label="INSTANCE with matching:\nT73 -> T85\nT74 -> T86", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 176 [arrowhead = none , style=dashed];
176 -> 94[style=dashed];

177 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 177 [arrowhead = none ];
177 -> 130;

}

(2) Obligation:

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

remA_in_gga(T7, s(T15), T10) → U1_gga(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
pB_in_ggaa(T7, T15, T18, T10) → U6_ggaa(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U6_ggaa(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_ggaa(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
remA_in_gga(s(T73), s(T74), s(T73)) → U2_gga(T73, T74, geqC_in_gg(T73, T74))
geqC_in_gg(s(T85), s(T86)) → U4_gg(T85, T86, geqC_in_gg(T85, T86))
geqC_in_gg(T91, 0) → geqC_out_gg(T91, 0)
U4_gg(T85, T86, geqC_out_gg(T85, T86)) → geqC_out_gg(s(T85), s(T86))
U2_gga(T73, T74, geqC_out_gg(T73, T74)) → remA_out_gga(s(T73), s(T74), s(T73))
U7_ggaa(T7, T15, T18, T10, remA_out_gga(T18, s(T15), T10)) → pB_out_ggaa(T7, T15, T18, T10)
U1_gga(T7, T15, T10, pB_out_ggaa(T7, T15, X7, T10)) → remA_out_gga(T7, s(T15), T10)

(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:

REMA_IN_GGA(T7, s(T15), T10) → U1_GGA(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
REMA_IN_GGA(T7, s(T15), T10) → PB_IN_GGAA(T7, T15, X7, T10)
PB_IN_GGAA(T7, T15, T18, T10) → U6_GGAA(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
PB_IN_GGAA(T7, T15, T18, T10) → SUBE_IN_GGA(T7, T15, T18)
SUBE_IN_GGA(s(T29), T30, X40) → U5_GGA(T29, T30, X40, subD_in_gga(T29, T30, X40))
SUBE_IN_GGA(s(T29), T30, X40) → SUBD_IN_GGA(T29, T30, X40)
SUBD_IN_GGA(s(T41), s(T42), X64) → U3_GGA(T41, T42, X64, subD_in_gga(T41, T42, X64))
SUBD_IN_GGA(s(T41), s(T42), X64) → SUBD_IN_GGA(T41, T42, X64)
U6_GGAA(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_GGAA(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
U6_GGAA(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → REMA_IN_GGA(T18, s(T15), T10)
REMA_IN_GGA(s(T73), s(T74), s(T73)) → U2_GGA(T73, T74, geqC_in_gg(T73, T74))
REMA_IN_GGA(s(T73), s(T74), s(T73)) → GEQC_IN_GG(T73, T74)
GEQC_IN_GG(s(T85), s(T86)) → U4_GG(T85, T86, geqC_in_gg(T85, T86))
GEQC_IN_GG(s(T85), s(T86)) → GEQC_IN_GG(T85, T86)

The TRS R consists of the following rules:

remA_in_gga(T7, s(T15), T10) → U1_gga(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
pB_in_ggaa(T7, T15, T18, T10) → U6_ggaa(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U6_ggaa(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_ggaa(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
remA_in_gga(s(T73), s(T74), s(T73)) → U2_gga(T73, T74, geqC_in_gg(T73, T74))
geqC_in_gg(s(T85), s(T86)) → U4_gg(T85, T86, geqC_in_gg(T85, T86))
geqC_in_gg(T91, 0) → geqC_out_gg(T91, 0)
U4_gg(T85, T86, geqC_out_gg(T85, T86)) → geqC_out_gg(s(T85), s(T86))
U2_gga(T73, T74, geqC_out_gg(T73, T74)) → remA_out_gga(s(T73), s(T74), s(T73))
U7_ggaa(T7, T15, T18, T10, remA_out_gga(T18, s(T15), T10)) → pB_out_ggaa(T7, T15, T18, T10)
U1_gga(T7, T15, T10, pB_out_ggaa(T7, T15, X7, T10)) → remA_out_gga(T7, s(T15), T10)

The argument filtering Pi contains the following mapping:
remA_in_gga(x1, x2, x3) = remA_in_gga(x1, x2)
s(x1) = s(x1)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4) = pB_in_ggaa(x1, x2)
U6_ggaa(x1, x2, x3, x4, x5) = U6_ggaa(x1, x2, x5)
subE_in_gga(x1, x2, x3) = subE_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
subD_in_gga(x1, x2, x3) = subD_in_gga(x1, x2)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
0 = 0
subD_out_gga(x1, x2, x3) = subD_out_gga(x1, x2, x3)
subE_out_gga(x1, x2, x3) = subE_out_gga(x1, x2, x3)
U7_ggaa(x1, x2, x3, x4, x5) = U7_ggaa(x1, x2, x3, x5)
U2_gga(x1, x2, x3) = U2_gga(x1, x2, x3)
geqC_in_gg(x1, x2) = geqC_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
geqC_out_gg(x1, x2) = geqC_out_gg(x1, x2)
remA_out_gga(x1, x2, x3) = remA_out_gga(x1, x2, x3)
pB_out_ggaa(x1, x2, x3, x4) = pB_out_ggaa(x1, x2, x3, x4)
REMA_IN_GGA(x1, x2, x3) = REMA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4) = U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4) = PB_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5) = U6_GGAA(x1, x2, x5)
SUBE_IN_GGA(x1, x2, x3) = SUBE_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4) = U5_GGA(x1, x2, x4)
SUBD_IN_GGA(x1, x2, x3) = SUBD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
U7_GGAA(x1, x2, x3, x4, x5) = U7_GGAA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3) = U2_GGA(x1, x2, x3)
GEQC_IN_GG(x1, x2) = GEQC_IN_GG(x1, x2)
U4_GG(x1, x2, x3) = U4_GG(x1, x2, x3)

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

(4) Obligation:

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

REMA_IN_GGA(T7, s(T15), T10) → U1_GGA(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
REMA_IN_GGA(T7, s(T15), T10) → PB_IN_GGAA(T7, T15, X7, T10)
PB_IN_GGAA(T7, T15, T18, T10) → U6_GGAA(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
PB_IN_GGAA(T7, T15, T18, T10) → SUBE_IN_GGA(T7, T15, T18)
SUBE_IN_GGA(s(T29), T30, X40) → U5_GGA(T29, T30, X40, subD_in_gga(T29, T30, X40))
SUBE_IN_GGA(s(T29), T30, X40) → SUBD_IN_GGA(T29, T30, X40)
SUBD_IN_GGA(s(T41), s(T42), X64) → U3_GGA(T41, T42, X64, subD_in_gga(T41, T42, X64))
SUBD_IN_GGA(s(T41), s(T42), X64) → SUBD_IN_GGA(T41, T42, X64)
U6_GGAA(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_GGAA(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
U6_GGAA(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → REMA_IN_GGA(T18, s(T15), T10)
REMA_IN_GGA(s(T73), s(T74), s(T73)) → U2_GGA(T73, T74, geqC_in_gg(T73, T74))
REMA_IN_GGA(s(T73), s(T74), s(T73)) → GEQC_IN_GG(T73, T74)
GEQC_IN_GG(s(T85), s(T86)) → U4_GG(T85, T86, geqC_in_gg(T85, T86))
GEQC_IN_GG(s(T85), s(T86)) → GEQC_IN_GG(T85, T86)

The TRS R consists of the following rules:

remA_in_gga(T7, s(T15), T10) → U1_gga(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
pB_in_ggaa(T7, T15, T18, T10) → U6_ggaa(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U6_ggaa(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_ggaa(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
remA_in_gga(s(T73), s(T74), s(T73)) → U2_gga(T73, T74, geqC_in_gg(T73, T74))
geqC_in_gg(s(T85), s(T86)) → U4_gg(T85, T86, geqC_in_gg(T85, T86))
geqC_in_gg(T91, 0) → geqC_out_gg(T91, 0)
U4_gg(T85, T86, geqC_out_gg(T85, T86)) → geqC_out_gg(s(T85), s(T86))
U2_gga(T73, T74, geqC_out_gg(T73, T74)) → remA_out_gga(s(T73), s(T74), s(T73))
U7_ggaa(T7, T15, T18, T10, remA_out_gga(T18, s(T15), T10)) → pB_out_ggaa(T7, T15, T18, T10)
U1_gga(T7, T15, T10, pB_out_ggaa(T7, T15, X7, T10)) → remA_out_gga(T7, s(T15), T10)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 9 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

GEQC_IN_GG(s(T85), s(T86)) → GEQC_IN_GG(T85, T86)

The TRS R consists of the following rules:

remA_in_gga(T7, s(T15), T10) → U1_gga(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
pB_in_ggaa(T7, T15, T18, T10) → U6_ggaa(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U6_ggaa(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_ggaa(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
remA_in_gga(s(T73), s(T74), s(T73)) → U2_gga(T73, T74, geqC_in_gg(T73, T74))
geqC_in_gg(s(T85), s(T86)) → U4_gg(T85, T86, geqC_in_gg(T85, T86))
geqC_in_gg(T91, 0) → geqC_out_gg(T91, 0)
U4_gg(T85, T86, geqC_out_gg(T85, T86)) → geqC_out_gg(s(T85), s(T86))
U2_gga(T73, T74, geqC_out_gg(T73, T74)) → remA_out_gga(s(T73), s(T74), s(T73))
U7_ggaa(T7, T15, T18, T10, remA_out_gga(T18, s(T15), T10)) → pB_out_ggaa(T7, T15, T18, T10)
U1_gga(T7, T15, T10, pB_out_ggaa(T7, T15, X7, T10)) → remA_out_gga(T7, s(T15), T10)

(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:

GEQC_IN_GG(s(T85), s(T86)) → GEQC_IN_GG(T85, T86)

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:

GEQC_IN_GG(s(T85), s(T86)) → GEQC_IN_GG(T85, T86)

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:

GEQC_IN_GG(s(T85), s(T86)) → GEQC_IN_GG(T85, T86)
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:

SUBD_IN_GGA(s(T41), s(T42), X64) → SUBD_IN_GGA(T41, T42, X64)

The TRS R consists of the following rules:

remA_in_gga(T7, s(T15), T10) → U1_gga(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
pB_in_ggaa(T7, T15, T18, T10) → U6_ggaa(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U6_ggaa(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_ggaa(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
remA_in_gga(s(T73), s(T74), s(T73)) → U2_gga(T73, T74, geqC_in_gg(T73, T74))
geqC_in_gg(s(T85), s(T86)) → U4_gg(T85, T86, geqC_in_gg(T85, T86))
geqC_in_gg(T91, 0) → geqC_out_gg(T91, 0)
U4_gg(T85, T86, geqC_out_gg(T85, T86)) → geqC_out_gg(s(T85), s(T86))
U2_gga(T73, T74, geqC_out_gg(T73, T74)) → remA_out_gga(s(T73), s(T74), s(T73))
U7_ggaa(T7, T15, T18, T10, remA_out_gga(T18, s(T15), T10)) → pB_out_ggaa(T7, T15, T18, T10)
U1_gga(T7, T15, T10, pB_out_ggaa(T7, T15, X7, T10)) → remA_out_gga(T7, s(T15), T10)

(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:

SUBD_IN_GGA(s(T41), s(T42), X64) → SUBD_IN_GGA(T41, T42, X64)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
SUBD_IN_GGA(x1, x2, x3) = SUBD_IN_GGA(x1, x2)

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

(17) PiDPToQDPProof (SOUND 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:

SUBD_IN_GGA(s(T41), s(T42)) → SUBD_IN_GGA(T41, T42)

R is empty.
Q is empty.
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:

SUBD_IN_GGA(s(T41), s(T42)) → SUBD_IN_GGA(T41, T42)
The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

REMA_IN_GGA(T7, s(T15), T10) → PB_IN_GGAA(T7, T15, X7, T10)
PB_IN_GGAA(T7, T15, T18, T10) → U6_GGAA(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
U6_GGAA(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → REMA_IN_GGA(T18, s(T15), T10)

The TRS R consists of the following rules:

remA_in_gga(T7, s(T15), T10) → U1_gga(T7, T15, T10, pB_in_ggaa(T7, T15, X7, T10))
pB_in_ggaa(T7, T15, T18, T10) → U6_ggaa(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U6_ggaa(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → U7_ggaa(T7, T15, T18, T10, remA_in_gga(T18, s(T15), T10))
remA_in_gga(s(T73), s(T74), s(T73)) → U2_gga(T73, T74, geqC_in_gg(T73, T74))
geqC_in_gg(s(T85), s(T86)) → U4_gg(T85, T86, geqC_in_gg(T85, T86))
geqC_in_gg(T91, 0) → geqC_out_gg(T91, 0)
U4_gg(T85, T86, geqC_out_gg(T85, T86)) → geqC_out_gg(s(T85), s(T86))
U2_gga(T73, T74, geqC_out_gg(T73, T74)) → remA_out_gga(s(T73), s(T74), s(T73))
U7_ggaa(T7, T15, T18, T10, remA_out_gga(T18, s(T15), T10)) → pB_out_ggaa(T7, T15, T18, T10)
U1_gga(T7, T15, T10, pB_out_ggaa(T7, T15, X7, T10)) → remA_out_gga(T7, s(T15), T10)

The argument filtering Pi contains the following mapping:
remA_in_gga(x1, x2, x3) = remA_in_gga(x1, x2)
s(x1) = s(x1)
U1_gga(x1, x2, x3, x4) = U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4) = pB_in_ggaa(x1, x2)
U6_ggaa(x1, x2, x3, x4, x5) = U6_ggaa(x1, x2, x5)
subE_in_gga(x1, x2, x3) = subE_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
subD_in_gga(x1, x2, x3) = subD_in_gga(x1, x2)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
0 = 0
subD_out_gga(x1, x2, x3) = subD_out_gga(x1, x2, x3)
subE_out_gga(x1, x2, x3) = subE_out_gga(x1, x2, x3)
U7_ggaa(x1, x2, x3, x4, x5) = U7_ggaa(x1, x2, x3, x5)
U2_gga(x1, x2, x3) = U2_gga(x1, x2, x3)
geqC_in_gg(x1, x2) = geqC_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
geqC_out_gg(x1, x2) = geqC_out_gg(x1, x2)
remA_out_gga(x1, x2, x3) = remA_out_gga(x1, x2, x3)
pB_out_ggaa(x1, x2, x3, x4) = pB_out_ggaa(x1, x2, x3, x4)
REMA_IN_GGA(x1, x2, x3) = REMA_IN_GGA(x1, x2)
PB_IN_GGAA(x1, x2, x3, x4) = PB_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5) = U6_GGAA(x1, x2, x5)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

REMA_IN_GGA(T7, s(T15), T10) → PB_IN_GGAA(T7, T15, X7, T10)
PB_IN_GGAA(T7, T15, T18, T10) → U6_GGAA(T7, T15, T18, T10, subE_in_gga(T7, T15, T18))
U6_GGAA(T7, T15, T18, T10, subE_out_gga(T7, T15, T18)) → REMA_IN_GGA(T18, s(T15), T10)

The TRS R consists of the following rules:

subE_in_gga(s(T29), T30, X40) → U5_gga(T29, T30, X40, subD_in_gga(T29, T30, X40))
U5_gga(T29, T30, X40, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
subD_in_gga(s(T41), s(T42), X64) → U3_gga(T41, T42, X64, subD_in_gga(T41, T42, X64))
subD_in_gga(T47, 0, T47) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, X64, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
subE_in_gga(x1, x2, x3) = subE_in_gga(x1, x2)
U5_gga(x1, x2, x3, x4) = U5_gga(x1, x2, x4)
subD_in_gga(x1, x2, x3) = subD_in_gga(x1, x2)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
0 = 0
subD_out_gga(x1, x2, x3) = subD_out_gga(x1, x2, x3)
subE_out_gga(x1, x2, x3) = subE_out_gga(x1, x2, x3)
REMA_IN_GGA(x1, x2, x3) = REMA_IN_GGA(x1, x2)
PB_IN_GGAA(x1, x2, x3, x4) = PB_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5) = U6_GGAA(x1, x2, x5)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

REMA_IN_GGA(T7, s(T15)) → PB_IN_GGAA(T7, T15)
PB_IN_GGAA(T7, T15) → U6_GGAA(T7, T15, subE_in_gga(T7, T15))
U6_GGAA(T7, T15, subE_out_gga(T7, T15, T18)) → REMA_IN_GGA(T18, s(T15))

The TRS R consists of the following rules:

subE_in_gga(s(T29), T30) → U5_gga(T29, T30, subD_in_gga(T29, T30))
U5_gga(T29, T30, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
subD_in_gga(s(T41), s(T42)) → U3_gga(T41, T42, subD_in_gga(T41, T42))
subD_in_gga(T47, 0) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)

The set Q consists of the following terms:

subE_in_gga(x0, x1)
U5_gga(x0, x1, x2)
subD_in_gga(x0, x1)
U3_gga(x0, x1, x2)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U6_GGAA(T7, T15, subE_out_gga(T7, T15, T18)) → REMA_IN_GGA(T18, s(T15))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(PB_IN_GGAA(x₁, x₂)) = x₁
POL(REMA_IN_GGA(x₁, x₂)) = x₁
POL(U3_gga(x₁, x₂, x₃)) = x₃
POL(U5_gga(x₁, x₂, x₃)) = 1 + x₃
POL(U6_GGAA(x₁, x₂, x₃)) = x₃
POL(s(x₁)) = 1 + x₁
POL(subD_in_gga(x₁, x₂)) = x₁
POL(subD_out_gga(x₁, x₂, x₃)) = x₃
POL(subE_in_gga(x₁, x₂)) = x₁
POL(subE_out_gga(x₁, x₂, x₃)) = 1 + x₃

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

subE_in_gga(s(T29), T30) → U5_gga(T29, T30, subD_in_gga(T29, T30))
subD_in_gga(s(T41), s(T42)) → U3_gga(T41, T42, subD_in_gga(T41, T42))
subD_in_gga(T47, 0) → subD_out_gga(T47, 0, T47)
U5_gga(T29, T30, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
U3_gga(T41, T42, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)

(27) Obligation:

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

REMA_IN_GGA(T7, s(T15)) → PB_IN_GGAA(T7, T15)
PB_IN_GGAA(T7, T15) → U6_GGAA(T7, T15, subE_in_gga(T7, T15))

The TRS R consists of the following rules:

subE_in_gga(s(T29), T30) → U5_gga(T29, T30, subD_in_gga(T29, T30))
U5_gga(T29, T30, subD_out_gga(T29, T30, X40)) → subE_out_gga(s(T29), T30, X40)
subD_in_gga(s(T41), s(T42)) → U3_gga(T41, T42, subD_in_gga(T41, T42))
subD_in_gga(T47, 0) → subD_out_gga(T47, 0, T47)
U3_gga(T41, T42, subD_out_gga(T41, T42, X64)) → subD_out_gga(s(T41), s(T42), X64)

The set Q consists of the following terms:

subE_in_gga(x0, x1)
U5_gga(x0, x1, x2)
subD_in_gga(x0, x1)
U3_gga(x0, x1, x2)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE