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

(0) Obligation:

Clauses:

div(X, 0, Z, R) :- ','(!, fail).
div(0, Y, Z, R) :- ','(!, ','(=(Z, 0), =(R, 0))).
div(X, Y, s(Z), R) :- ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))).
div(X, Y, 0, X).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).

Query: div(g,g,a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: div(T1, T2, T3, T4)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 0 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_1, fail) | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX4 is free\nX5 is free\nX6 is free\ndiv(T1, T2, T3, T4) !=? div(X4, 0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: fail\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(!_1, ','(=(T17, 0), =(T18, 0))) | div(0, T14, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T14, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT14 is ground\nX4 is free\nX5 is free\nX6 is free\ndiv(0, T14, T3, T4) !=? div(X4, 0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\ndiv(T1, T2, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T1, T2, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(=(T17, 0), =(T18, 0))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: =(T19, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(minus(T24, T25, X21), ','(!_1, div(X21, T25, T28, T29))) | div(T24, T25, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\nX21 is free\ndiv(T24, T25, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T24, T25, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\ndiv(T1, T2, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T1, T2, T3, T4) !=? div(0, X10, X11, X12)\ndiv(T1, T2, T3, T4) !=? div(X17, X18, s(X19), X20)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(minus(T24, T25, X21), ','(!_1, div(X21, T25, T28, T29))), SCOPE: 2, CLAUSE: 4 | ','(minus(T24, T25, X21), ','(!_1, div(X21, T25, T28, T29))), SCOPE: 2, CLAUSE: 5 | ?_2 | div(T24, T25, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\nX21 is free\ndiv(T24, T25, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T24, T25, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(minus(T24, T25, X21), ','(!_1, div(X21, T25, T28, T29))), SCOPE: 2, CLAUSE: 5 | ?_2 | div(T24, T25, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\nX21 is free\ndiv(T24, T25, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T24, T25, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(minus(T24, T25, X21), ','(!_1, div(X21, T25, T28, T29))), SCOPE: 2, CLAUSE: 5\n\nT24 is ground\nT25 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\nX21 is free\ndiv(T24, T25, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T24, T25, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ?_2 | div(T24, T25, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\ndiv(T24, T25, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T24, T25, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="B: ','(minus(T39, T40, X42), ','(!_1, div(X42, s(T40), T28, T29)))\n\nT39 is ground\nT40 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="C: minus(T39, T40, X42)\n\nT39 is ground\nT40 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="D: ','(!_1, div(T43, s(T40), T28, T29))\n\nT40 is ground\nT43 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: minus(T39, T40, X42), SCOPE: 3, CLAUSE: 4 | minus(T39, T40, X42), SCOPE: 3, CLAUSE: 5\n\nT39 is ground\nT40 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: minus(T39, T40, X42), SCOPE: 3, CLAUSE: 4\n\nT39 is ground\nT40 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: minus(T39, T40, X42), SCOPE: 3, CLAUSE: 5\n\nT39 is ground\nT40 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: minus(T55, T56, X63)\n\nT55 is ground\nT56 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: div(T43, s(T40), T28, T29)\n\nT40 is ground\nT43 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: div(T24, T25, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nX4 is free\nX5 is free\nX6 is free\nX10 is free\nX11 is free\nX12 is free\ndiv(T24, T25, T3, T4) !=? div(X4, 0, X5, X6)\ndiv(T24, T25, T3, T4) !=? div(0, X10, X11, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 112 [arrowhead = none ];
112 -> 5;

113 [label="EVAL with clause\ndiv(X4, 0, X5, X6) :- ','(!_1, fail).\nand substitutionT1 -> T8,\nX4 -> T8,\nT2 -> 0,\nT3 -> T9,\nX5 -> T9,\nT4 -> T10,\nX6 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 113 [arrowhead = none ];
113 -> 8;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 114 [arrowhead = none ];
114 -> 10;

115 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 115 [arrowhead = none ];
115 -> 13;

116 [label="EVAL with clause\ndiv(0, X10, X11, X12) :- ','(!_1, ','(=(X11, 0), =(X12, 0))).\nand substitutionT1 -> 0,\nT2 -> T14,\nX10 -> T14,\nT3 -> T17,\nX11 -> T17,\nT4 -> T18,\nX12 -> T18,\nT15 -> T17,\nT16 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 116 [arrowhead = none ];
116 -> 21;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 117 [arrowhead = none ];
117 -> 27;

118 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 118 [arrowhead = none ];
118 -> 17;

119 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 119 [arrowhead = none ];
119 -> 28;

120 [label="EVAL with clause\ndiv(X17, X18, s(X19), X20) :- ','(minus(X17, X18, X21), ','(!_1, div(X21, X18, X19, X20))).\nand substitutionT1 -> T24,\nX17 -> T24,\nT2 -> T25,\nX18 -> T25,\nX19 -> T28,\nT3 -> s(T28),\nT4 -> T29,\nX20 -> T29,\nT26 -> T28,\nT27 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 120 [arrowhead = none ];
120 -> 43;

121 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 121 [arrowhead = none ];
121 -> 47;

122 [label="UNIFY CASE with substitutionT17 -> 0,\nT18 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 122 [arrowhead = none ];
122 -> 30;

123 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 123 [arrowhead = none ];
123 -> 31;

124 [label="UNIFY CASE with substitutionT19 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 124 [arrowhead = none ];
124 -> 35;

125 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 125 [arrowhead = none ];
125 -> 37;

126 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 126 [arrowhead = none ];
126 -> 39;

127 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
43 -> 127 [arrowhead = none ];
127 -> 49;

128 [label="EVAL with clause\ndiv(X77, X78, 0, X77).\nand substitutionT1 -> T68,\nX77 -> T68,\nT2 -> T69,\nX78 -> T69,\nT3 -> 0,\nT4 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 128 [arrowhead = none ];
128 -> 108;

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

130 [label="BACKTRACK\nfor clause: minus(X, 0, X)\nwith clash: (div(T24, T25, T3, T4), div(X4, 0, X5, X6))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 130 [arrowhead = none ];
130 -> 53;

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

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

133 [label="EVAL with clause\nminus(s(X39), s(X40), X41) :- minus(X39, X40, X41).\nand substitutionX39 -> T39,\nT24 -> s(T39),\nX40 -> T40,\nT25 -> s(T40),\nX21 -> X42,\nX41 -> X42", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 133 [arrowhead = none ];
133 -> 65;

134 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 134 [arrowhead = none ];
134 -> 66;

135 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 135 [arrowhead = none ];
135 -> 98;

136 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
65 -> 136 [arrowhead = none ];
136 -> 70;

137 [label="SPLIT 2\nnew knowledge:\nT39 is ground\nT40 is ground\nT43 is ground\nreplacements:X42 -> T43", fontsize=14, style = filled, fillcolor = violet];
65 -> 137 [arrowhead = none ];
137 -> 71;

138 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
70 -> 138 [arrowhead = none ];
138 -> 73;

139 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 139 [arrowhead = none ];
139 -> 91;

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 140 [arrowhead = none ];
140 -> 78;

141 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 141 [arrowhead = none ];
141 -> 79;

142 [label="EVAL with clause\nminus(X51, 0, X51).\nand substitutionT39 -> T50,\nX51 -> T50,\nT40 -> 0,\nX42 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 142 [arrowhead = none ];
142 -> 80;

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

144 [label="EVAL with clause\nminus(s(X60), s(X61), X62) :- minus(X60, X61, X62).\nand substitutionX60 -> T55,\nT39 -> s(T55),\nX61 -> T56,\nT40 -> s(T56),\nX42 -> X63,\nX62 -> X63", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 144 [arrowhead = none ];
144 -> 87;

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

146 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 146 [arrowhead = none ];
146 -> 82;

147 [label="INSTANCE with matching:\nT39 -> T55\nT40 -> T56\nX42 -> X63", fontsize=14, style = filled, fillcolor = lightgrey];
87 -> 147 [arrowhead = none , style=dashed];
147 -> 70[style=dashed];

148 [label="INSTANCE with matching:\nT1 -> T43\nT2 -> s(T40)\nT3 -> T28\nT4 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 148 [arrowhead = none , style=dashed];
148 -> 3[style=dashed];

149 [label="EVAL with clause\ndiv(X73, X74, 0, X73).\nand substitutionT24 -> T64,\nX73 -> T64,\nT25 -> T65,\nX74 -> T65,\nT3 -> 0,\nT4 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 149 [arrowhead = none ];
149 -> 100;

150 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 150 [arrowhead = none ];
150 -> 103;

151 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 151 [arrowhead = none ];
151 -> 104;

152 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 152 [arrowhead = none ];
152 -> 111;

}

(2) Obligation:

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

divA_in_ggaa(0, T14, 0, 0) → divA_out_ggaa(0, T14, 0, 0)
divA_in_ggaa(s(T39), s(T40), s(T28), T29) → U1_ggaa(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
pB_in_ggaaa(T39, T40, T43, T28, T29) → U4_ggaaa(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
minusC_in_gga(T50, 0, T50) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56), X63) → U2_gga(T55, T56, X63, minusC_in_gga(T55, T56, X63))
U2_gga(T55, T56, X63, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)
U4_ggaaa(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_ggaaa(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
pD_in_ggaa(T43, T40, T28, T29) → U3_ggaa(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
divA_in_ggaa(T64, T65, 0, T64) → divA_out_ggaa(T64, T65, 0, T64)
U3_ggaa(T43, T40, T28, T29, divA_out_ggaa(T43, s(T40), T28, T29)) → pD_out_ggaa(T43, T40, T28, T29)
U5_ggaaa(T39, T40, T43, T28, T29, pD_out_ggaa(T43, T40, T28, T29)) → pB_out_ggaaa(T39, T40, T43, T28, T29)
U1_ggaa(T39, T40, T28, T29, pB_out_ggaaa(T39, T40, X42, T28, T29)) → divA_out_ggaa(s(T39), s(T40), s(T28), T29)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4)  =  divA_in_ggaa(x1, x2)
0  =  0
divA_out_ggaa(x1, x2, x3, x4)  =  divA_out_ggaa(x1, x2, x3, x4)
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4, x5)  =  U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U4_ggaaa(x1, x2, x3, x4, x5, x6)  =  U4_ggaaa(x1, x2, x6)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x3, x6)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)

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

DIVA_IN_GGAA(s(T39), s(T40), s(T28), T29) → U1_GGAA(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
DIVA_IN_GGAA(s(T39), s(T40), s(T28), T29) → PB_IN_GGAAA(T39, T40, X42, T28, T29)
PB_IN_GGAAA(T39, T40, T43, T28, T29) → U4_GGAAA(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
PB_IN_GGAAA(T39, T40, T43, T28, T29) → MINUSC_IN_GGA(T39, T40, T43)
MINUSC_IN_GGA(s(T55), s(T56), X63) → U2_GGA(T55, T56, X63, minusC_in_gga(T55, T56, X63))
MINUSC_IN_GGA(s(T55), s(T56), X63) → MINUSC_IN_GGA(T55, T56, X63)
U4_GGAAA(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_GGAAA(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
U4_GGAAA(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → PD_IN_GGAA(T43, T40, T28, T29)
PD_IN_GGAA(T43, T40, T28, T29) → U3_GGAA(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
PD_IN_GGAA(T43, T40, T28, T29) → DIVA_IN_GGAA(T43, s(T40), T28, T29)

The TRS R consists of the following rules:

divA_in_ggaa(0, T14, 0, 0) → divA_out_ggaa(0, T14, 0, 0)
divA_in_ggaa(s(T39), s(T40), s(T28), T29) → U1_ggaa(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
pB_in_ggaaa(T39, T40, T43, T28, T29) → U4_ggaaa(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
minusC_in_gga(T50, 0, T50) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56), X63) → U2_gga(T55, T56, X63, minusC_in_gga(T55, T56, X63))
U2_gga(T55, T56, X63, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)
U4_ggaaa(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_ggaaa(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
pD_in_ggaa(T43, T40, T28, T29) → U3_ggaa(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
divA_in_ggaa(T64, T65, 0, T64) → divA_out_ggaa(T64, T65, 0, T64)
U3_ggaa(T43, T40, T28, T29, divA_out_ggaa(T43, s(T40), T28, T29)) → pD_out_ggaa(T43, T40, T28, T29)
U5_ggaaa(T39, T40, T43, T28, T29, pD_out_ggaa(T43, T40, T28, T29)) → pB_out_ggaaa(T39, T40, T43, T28, T29)
U1_ggaa(T39, T40, T28, T29, pB_out_ggaaa(T39, T40, X42, T28, T29)) → divA_out_ggaa(s(T39), s(T40), s(T28), T29)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4)  =  divA_in_ggaa(x1, x2)
0  =  0
divA_out_ggaa(x1, x2, x3, x4)  =  divA_out_ggaa(x1, x2, x3, x4)
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4, x5)  =  U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U4_ggaaa(x1, x2, x3, x4, x5, x6)  =  U4_ggaaa(x1, x2, x6)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x3, x6)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
DIVA_IN_GGAA(x1, x2, x3, x4)  =  DIVA_IN_GGAA(x1, x2)
U1_GGAA(x1, x2, x3, x4, x5)  =  U1_GGAA(x1, x2, x5)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U4_GGAAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAAA(x1, x2, x6)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U5_GGAAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAAA(x1, x2, x3, x6)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)

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

(4) Obligation:

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

DIVA_IN_GGAA(s(T39), s(T40), s(T28), T29) → U1_GGAA(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
DIVA_IN_GGAA(s(T39), s(T40), s(T28), T29) → PB_IN_GGAAA(T39, T40, X42, T28, T29)
PB_IN_GGAAA(T39, T40, T43, T28, T29) → U4_GGAAA(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
PB_IN_GGAAA(T39, T40, T43, T28, T29) → MINUSC_IN_GGA(T39, T40, T43)
MINUSC_IN_GGA(s(T55), s(T56), X63) → U2_GGA(T55, T56, X63, minusC_in_gga(T55, T56, X63))
MINUSC_IN_GGA(s(T55), s(T56), X63) → MINUSC_IN_GGA(T55, T56, X63)
U4_GGAAA(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_GGAAA(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
U4_GGAAA(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → PD_IN_GGAA(T43, T40, T28, T29)
PD_IN_GGAA(T43, T40, T28, T29) → U3_GGAA(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
PD_IN_GGAA(T43, T40, T28, T29) → DIVA_IN_GGAA(T43, s(T40), T28, T29)

The TRS R consists of the following rules:

divA_in_ggaa(0, T14, 0, 0) → divA_out_ggaa(0, T14, 0, 0)
divA_in_ggaa(s(T39), s(T40), s(T28), T29) → U1_ggaa(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
pB_in_ggaaa(T39, T40, T43, T28, T29) → U4_ggaaa(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
minusC_in_gga(T50, 0, T50) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56), X63) → U2_gga(T55, T56, X63, minusC_in_gga(T55, T56, X63))
U2_gga(T55, T56, X63, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)
U4_ggaaa(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_ggaaa(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
pD_in_ggaa(T43, T40, T28, T29) → U3_ggaa(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
divA_in_ggaa(T64, T65, 0, T64) → divA_out_ggaa(T64, T65, 0, T64)
U3_ggaa(T43, T40, T28, T29, divA_out_ggaa(T43, s(T40), T28, T29)) → pD_out_ggaa(T43, T40, T28, T29)
U5_ggaaa(T39, T40, T43, T28, T29, pD_out_ggaa(T43, T40, T28, T29)) → pB_out_ggaaa(T39, T40, T43, T28, T29)
U1_ggaa(T39, T40, T28, T29, pB_out_ggaaa(T39, T40, X42, T28, T29)) → divA_out_ggaa(s(T39), s(T40), s(T28), T29)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4)  =  divA_in_ggaa(x1, x2)
0  =  0
divA_out_ggaa(x1, x2, x3, x4)  =  divA_out_ggaa(x1, x2, x3, x4)
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4, x5)  =  U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U4_ggaaa(x1, x2, x3, x4, x5, x6)  =  U4_ggaaa(x1, x2, x6)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x3, x6)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
DIVA_IN_GGAA(x1, x2, x3, x4)  =  DIVA_IN_GGAA(x1, x2)
U1_GGAA(x1, x2, x3, x4, x5)  =  U1_GGAA(x1, x2, x5)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U4_GGAAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAAA(x1, x2, x6)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U5_GGAAA(x1, x2, x3, x4, x5, x6)  =  U5_GGAAA(x1, x2, x3, x6)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)

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:

MINUSC_IN_GGA(s(T55), s(T56), X63) → MINUSC_IN_GGA(T55, T56, X63)

The TRS R consists of the following rules:

divA_in_ggaa(0, T14, 0, 0) → divA_out_ggaa(0, T14, 0, 0)
divA_in_ggaa(s(T39), s(T40), s(T28), T29) → U1_ggaa(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
pB_in_ggaaa(T39, T40, T43, T28, T29) → U4_ggaaa(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
minusC_in_gga(T50, 0, T50) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56), X63) → U2_gga(T55, T56, X63, minusC_in_gga(T55, T56, X63))
U2_gga(T55, T56, X63, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)
U4_ggaaa(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_ggaaa(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
pD_in_ggaa(T43, T40, T28, T29) → U3_ggaa(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
divA_in_ggaa(T64, T65, 0, T64) → divA_out_ggaa(T64, T65, 0, T64)
U3_ggaa(T43, T40, T28, T29, divA_out_ggaa(T43, s(T40), T28, T29)) → pD_out_ggaa(T43, T40, T28, T29)
U5_ggaaa(T39, T40, T43, T28, T29, pD_out_ggaa(T43, T40, T28, T29)) → pB_out_ggaaa(T39, T40, T43, T28, T29)
U1_ggaa(T39, T40, T28, T29, pB_out_ggaaa(T39, T40, X42, T28, T29)) → divA_out_ggaa(s(T39), s(T40), s(T28), T29)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4)  =  divA_in_ggaa(x1, x2)
0  =  0
divA_out_ggaa(x1, x2, x3, x4)  =  divA_out_ggaa(x1, x2, x3, x4)
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4, x5)  =  U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U4_ggaaa(x1, x2, x3, x4, x5, x6)  =  U4_ggaaa(x1, x2, x6)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x3, x6)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
MINUSC_IN_GGA(x1, x2, x3)  =  MINUSC_IN_GGA(x1, x2)

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:

MINUSC_IN_GGA(s(T55), s(T56), X63) → MINUSC_IN_GGA(T55, T56, X63)

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

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

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

MINUSC_IN_GGA(s(T55), s(T56)) → MINUSC_IN_GGA(T55, T56)

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:

• MINUSC_IN_GGA(s(T55), s(T56)) → MINUSC_IN_GGA(T55, T56)
  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:

DIVA_IN_GGAA(s(T39), s(T40), s(T28), T29) → PB_IN_GGAAA(T39, T40, X42, T28, T29)
PB_IN_GGAAA(T39, T40, T43, T28, T29) → U4_GGAAA(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
U4_GGAAA(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → PD_IN_GGAA(T43, T40, T28, T29)
PD_IN_GGAA(T43, T40, T28, T29) → DIVA_IN_GGAA(T43, s(T40), T28, T29)

The TRS R consists of the following rules:

divA_in_ggaa(0, T14, 0, 0) → divA_out_ggaa(0, T14, 0, 0)
divA_in_ggaa(s(T39), s(T40), s(T28), T29) → U1_ggaa(T39, T40, T28, T29, pB_in_ggaaa(T39, T40, X42, T28, T29))
pB_in_ggaaa(T39, T40, T43, T28, T29) → U4_ggaaa(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
minusC_in_gga(T50, 0, T50) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56), X63) → U2_gga(T55, T56, X63, minusC_in_gga(T55, T56, X63))
U2_gga(T55, T56, X63, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)
U4_ggaaa(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → U5_ggaaa(T39, T40, T43, T28, T29, pD_in_ggaa(T43, T40, T28, T29))
pD_in_ggaa(T43, T40, T28, T29) → U3_ggaa(T43, T40, T28, T29, divA_in_ggaa(T43, s(T40), T28, T29))
divA_in_ggaa(T64, T65, 0, T64) → divA_out_ggaa(T64, T65, 0, T64)
U3_ggaa(T43, T40, T28, T29, divA_out_ggaa(T43, s(T40), T28, T29)) → pD_out_ggaa(T43, T40, T28, T29)
U5_ggaaa(T39, T40, T43, T28, T29, pD_out_ggaa(T43, T40, T28, T29)) → pB_out_ggaaa(T39, T40, T43, T28, T29)
U1_ggaa(T39, T40, T28, T29, pB_out_ggaaa(T39, T40, X42, T28, T29)) → divA_out_ggaa(s(T39), s(T40), s(T28), T29)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4)  =  divA_in_ggaa(x1, x2)
0  =  0
divA_out_ggaa(x1, x2, x3, x4)  =  divA_out_ggaa(x1, x2, x3, x4)
s(x1)  =  s(x1)
U1_ggaa(x1, x2, x3, x4, x5)  =  U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5)  =  pB_in_ggaaa(x1, x2)
U4_ggaaa(x1, x2, x3, x4, x5, x6)  =  U4_ggaaa(x1, x2, x6)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
U5_ggaaa(x1, x2, x3, x4, x5, x6)  =  U5_ggaaa(x1, x2, x3, x6)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5)  =  pB_out_ggaaa(x1, x2, x3, x4, x5)
DIVA_IN_GGAA(x1, x2, x3, x4)  =  DIVA_IN_GGAA(x1, x2)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U4_GGAAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAAA(x1, x2, x6)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)

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:

DIVA_IN_GGAA(s(T39), s(T40), s(T28), T29) → PB_IN_GGAAA(T39, T40, X42, T28, T29)
PB_IN_GGAAA(T39, T40, T43, T28, T29) → U4_GGAAA(T39, T40, T43, T28, T29, minusC_in_gga(T39, T40, T43))
U4_GGAAA(T39, T40, T43, T28, T29, minusC_out_gga(T39, T40, T43)) → PD_IN_GGAA(T43, T40, T28, T29)
PD_IN_GGAA(T43, T40, T28, T29) → DIVA_IN_GGAA(T43, s(T40), T28, T29)

The TRS R consists of the following rules:

minusC_in_gga(T50, 0, T50) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56), X63) → U2_gga(T55, T56, X63, minusC_in_gga(T55, T56, X63))
U2_gga(T55, T56, X63, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
minusC_in_gga(x1, x2, x3)  =  minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3)  =  minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
DIVA_IN_GGAA(x1, x2, x3, x4)  =  DIVA_IN_GGAA(x1, x2)
PB_IN_GGAAA(x1, x2, x3, x4, x5)  =  PB_IN_GGAAA(x1, x2)
U4_GGAAA(x1, x2, x3, x4, x5, x6)  =  U4_GGAAA(x1, x2, x6)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(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:

DIVA_IN_GGAA(s(T39), s(T40)) → PB_IN_GGAAA(T39, T40)
PB_IN_GGAAA(T39, T40) → U4_GGAAA(T39, T40, minusC_in_gga(T39, T40))
U4_GGAAA(T39, T40, minusC_out_gga(T39, T40, T43)) → PD_IN_GGAA(T43, T40)
PD_IN_GGAA(T43, T40) → DIVA_IN_GGAA(T43, s(T40))

The TRS R consists of the following rules:

minusC_in_gga(T50, 0) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56)) → U2_gga(T55, T56, minusC_in_gga(T55, T56))
U2_gga(T55, T56, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)

The set Q consists of the following terms:

minusC_in_gga(x0, x1)
U2_gga(x0, x1, x2)

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

(19) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

DIVA_IN_GGAA(s(T39), s(T40)) → PB_IN_GGAAA(T39, T40)

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

POL(0) = 0   
POL(DIVA_IN_GGAA(x₁, x₂)) = 1 + x₁   
POL(PB_IN_GGAAA(x₁, x₂)) = 1 + x₁   
POL(PD_IN_GGAA(x₁, x₂)) = 1 + x₁   
POL(U2_gga(x₁, x₂, x₃)) = x₃   
POL(U4_GGAAA(x₁, x₂, x₃)) = x₃   
POL(minusC_in_gga(x₁, x₂)) = 1 + x₁   
POL(minusC_out_gga(x₁, x₂, x₃)) = 1 + x₃   
POL(s(x₁)) = 1 + x₁   

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

minusC_in_gga(T50, 0) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56)) → U2_gga(T55, T56, minusC_in_gga(T55, T56))
U2_gga(T55, T56, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)

(20) Obligation:

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

PB_IN_GGAAA(T39, T40) → U4_GGAAA(T39, T40, minusC_in_gga(T39, T40))
U4_GGAAA(T39, T40, minusC_out_gga(T39, T40, T43)) → PD_IN_GGAA(T43, T40)
PD_IN_GGAA(T43, T40) → DIVA_IN_GGAA(T43, s(T40))

The TRS R consists of the following rules:

minusC_in_gga(T50, 0) → minusC_out_gga(T50, 0, T50)
minusC_in_gga(s(T55), s(T56)) → U2_gga(T55, T56, minusC_in_gga(T55, T56))
U2_gga(T55, T56, minusC_out_gga(T55, T56, X63)) → minusC_out_gga(s(T55), s(T56), X63)

The set Q consists of the following terms:

minusC_in_gga(x0, x1)
U2_gga(x0, x1, x2)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE