Left Termination proof of /tmp/tmpnrDxIx/maximum-fbf.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 135 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 5 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 19 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

(0) Obligation:

Clauses:

max(X, Y, X) :- less(Y, X).
max(X, Y, Y) :- less(X, s(Y)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: max(a,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: max(T1, T2, T3)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: max(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | max(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: less(T7, T8) | max(T1, T7, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: max(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX4 is free\nX5 is free\nmax(T1, T2, T3) !=? max(X4, X5, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: less(T7, T8), SCOPE: 2, CLAUSE: 2 | less(T7, T8), SCOPE: 2, CLAUSE: 3 | ?_2 | max(T1, T7, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: less(T7, T8), SCOPE: 2, CLAUSE: 2\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: less(T7, T8), SCOPE: 2, CLAUSE: 3 | ?_2 | max(T1, T7, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: less(T7, T8), SCOPE: 2, CLAUSE: 3\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_2 | max(T1, T7, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="B: less(T22, T24)\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: less(T22, T24), SCOPE: 3, CLAUSE: 2 | less(T22, T24), SCOPE: 3, CLAUSE: 3\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: less(T22, T24), SCOPE: 3, CLAUSE: 2\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: less(T22, T24), SCOPE: 3, CLAUSE: 3\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: less(T36, T38)\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: max(T1, T7, T3), SCOPE: 1, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: less(T47, s(T46))\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: less(T47, s(T46)), SCOPE: 4, CLAUSE: 2 | less(T47, s(T46)), SCOPE: 4, CLAUSE: 3\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: less(T47, s(T46)), SCOPE: 4, CLAUSE: 2\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: less(T47, s(T46)), SCOPE: 4, CLAUSE: 3\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="C: less(T61, T60)\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: less(T61, T60), SCOPE: 5, CLAUSE: 2 | less(T61, T60), SCOPE: 5, CLAUSE: 3\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: less(T61, T60), SCOPE: 5, CLAUSE: 2\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: less(T61, T60), SCOPE: 5, CLAUSE: 3\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: less(T75, T74)\n\nT74 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: less(T82, s(T81))\n\nT81 is ground\nX4 is free\nX5 is free\nmax(T1, T81, T3) !=? max(X4, X5, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: less(T82, s(T81)), SCOPE: 6, CLAUSE: 2 | less(T82, s(T81)), SCOPE: 6, CLAUSE: 3\n\nT81 is ground\nX4 is free\nX5 is free\nmax(T1, T81, T3) !=? max(X4, X5, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: less(T82, s(T81)), SCOPE: 6, CLAUSE: 2\n\nT81 is ground\nX4 is free\nX5 is free\nmax(T1, T81, T3) !=? max(X4, X5, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: less(T82, s(T81)), SCOPE: 6, CLAUSE: 3\n\nT81 is ground\nX4 is free\nX5 is free\nmax(T1, T81, T3) !=? max(X4, X5, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: less(T94, T93)\n\nT93 is ground\nX4 is free\nX5 is free\nmax(T1, T93, T3) !=? max(X4, X5, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 120 [arrowhead = none ];
120 -> 3;

121 [label="EVAL with clause\nmax(X4, X5, X4) :- less(X5, X4).\nand substitutionT1 -> T8,\nX4 -> T8,\nT2 -> T7,\nX5 -> T7,\nT3 -> T8,\nT6 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 121 [arrowhead = none ];
121 -> 7;

122 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 122 [arrowhead = none ];
122 -> 9;

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

124 [label="EVAL with clause\nmax(X72, X73, X73) :- less(X72, s(X73)).\nand substitutionT1 -> T82,\nX72 -> T82,\nT2 -> T81,\nX73 -> T81,\nT3 -> T81,\nT80 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 124 [arrowhead = none ];
124 -> 105;

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

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

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

128 [label="EVAL with clause\nless(0, s(X10)).\nand substitutionT7 -> 0,\nX10 -> T13,\nT8 -> s(T13)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 128 [arrowhead = none ];
128 -> 19;

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

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

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

132 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 132 [arrowhead = none ];
132 -> 21;

133 [label="EVAL with clause\nless(s(X19), s(X20)) :- less(X19, X20).\nand substitutionX19 -> T22,\nT7 -> s(T22),\nX20 -> T24,\nT8 -> s(T24),\nT23 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 133 [arrowhead = none ];
133 -> 30;

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

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

136 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
30 -> 136 [arrowhead = none ];
136 -> 34;

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

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

139 [label="EVAL with clause\nless(0, s(X27)).\nand substitutionT22 -> 0,\nX27 -> T31,\nT24 -> s(T31)", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 139 [arrowhead = none ];
139 -> 45;

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

141 [label="EVAL with clause\nless(s(X32), s(X33)) :- less(X32, X33).\nand substitutionX32 -> T36,\nT22 -> s(T36),\nX33 -> T38,\nT24 -> s(T38),\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 141 [arrowhead = none ];
141 -> 53;

142 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 142 [arrowhead = none ];
142 -> 54;

143 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 143 [arrowhead = none ];
143 -> 49;

144 [label="INSTANCE with matching:\nT22 -> T36\nT24 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 144 [arrowhead = none , style=dashed];
144 -> 30[style=dashed];

145 [label="EVAL with clause\nmax(X40, X41, X41) :- less(X40, s(X41)).\nand substitutionT1 -> T47,\nX40 -> T47,\nT7 -> T46,\nX41 -> T46,\nT3 -> T46,\nT45 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 145 [arrowhead = none ];
145 -> 63;

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

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

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
70 -> 148 [arrowhead = none ];
148 -> 74;

149 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
70 -> 149 [arrowhead = none ];
149 -> 75;

150 [label="EVAL with clause\nless(0, s(X48)).\nand substitutionT47 -> 0,\nT46 -> T54,\nX48 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 150 [arrowhead = none ];
150 -> 76;

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

152 [label="EVAL with clause\nless(s(X53), s(X54)) :- less(X53, X54).\nand substitutionX53 -> T61,\nT47 -> s(T61),\nT46 -> T60,\nX54 -> T60,\nT59 -> T61", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 152 [arrowhead = none ];
152 -> 82;

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

154 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 154 [arrowhead = none ];
154 -> 78;

155 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
82 -> 155 [arrowhead = none ];
155 -> 89;

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

157 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
89 -> 157 [arrowhead = none ];
157 -> 94;

158 [label="EVAL with clause\nless(0, s(X61)).\nand substitutionT61 -> 0,\nX61 -> T68,\nT60 -> s(T68)", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 158 [arrowhead = none ];
158 -> 98;

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

160 [label="EVAL with clause\nless(s(X66), s(X67)) :- less(X66, X67).\nand substitutionX66 -> T75,\nT61 -> s(T75),\nX67 -> T74,\nT60 -> s(T74),\nT73 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 160 [arrowhead = none ];
160 -> 103;

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

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

163 [label="INSTANCE with matching:\nT61 -> T75\nT60 -> T74", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 163 [arrowhead = none , style=dashed];
163 -> 82[style=dashed];

164 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
105 -> 164 [arrowhead = none ];
164 -> 107;

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

166 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
107 -> 166 [arrowhead = none ];
166 -> 111;

167 [label="EVAL with clause\nless(0, s(X78)).\nand substitutionT82 -> 0,\nT81 -> T87,\nX78 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 167 [arrowhead = none ];
167 -> 113;

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

169 [label="EVAL with clause\nless(s(X83), s(X84)) :- less(X83, X84).\nand substitutionX83 -> T94,\nT82 -> s(T94),\nT81 -> T93,\nX84 -> T93,\nT92 -> T94", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 169 [arrowhead = none ];
169 -> 118;

170 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 170 [arrowhead = none ];
170 -> 119;

171 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 171 [arrowhead = none ];
171 -> 117;

172 [label="INSTANCE with matching:\nT61 -> T94\nT60 -> T93", fontsize=14, style = filled, fillcolor = lightgrey];
118 -> 172 [arrowhead = none , style=dashed];
172 -> 82[style=dashed];

}

(2) Obligation:

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

maxA_in_aga(s(T13), 0, s(T13)) → maxA_out_aga(s(T13), 0, s(T13))
maxA_in_aga(s(T24), s(T22), s(T24)) → U1_aga(T24, T22, lessB_in_ga(T22, T24))
lessB_in_ga(0, s(T31)) → lessB_out_ga(0, s(T31))
lessB_in_ga(s(T36), s(T38)) → U4_ga(T36, T38, lessB_in_ga(T36, T38))
U4_ga(T36, T38, lessB_out_ga(T36, T38)) → lessB_out_ga(s(T36), s(T38))
U1_aga(T24, T22, lessB_out_ga(T22, T24)) → maxA_out_aga(s(T24), s(T22), s(T24))
maxA_in_aga(0, T54, T54) → maxA_out_aga(0, T54, T54)
maxA_in_aga(s(T61), T60, T60) → U2_aga(T61, T60, lessC_in_ag(T61, T60))
lessC_in_ag(0, s(T68)) → lessC_out_ag(0, s(T68))
lessC_in_ag(s(T75), s(T74)) → U5_ag(T75, T74, lessC_in_ag(T75, T74))
U5_ag(T75, T74, lessC_out_ag(T75, T74)) → lessC_out_ag(s(T75), s(T74))
U2_aga(T61, T60, lessC_out_ag(T61, T60)) → maxA_out_aga(s(T61), T60, T60)
maxA_in_aga(s(T94), T93, T93) → U3_aga(T94, T93, lessC_in_ag(T94, T93))
U3_aga(T94, T93, lessC_out_ag(T94, T93)) → maxA_out_aga(s(T94), T93, T93)

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

MAXA_IN_AGA(s(T24), s(T22), s(T24)) → U1_AGA(T24, T22, lessB_in_ga(T22, T24))
MAXA_IN_AGA(s(T24), s(T22), s(T24)) → LESSB_IN_GA(T22, T24)
LESSB_IN_GA(s(T36), s(T38)) → U4_GA(T36, T38, lessB_in_ga(T36, T38))
LESSB_IN_GA(s(T36), s(T38)) → LESSB_IN_GA(T36, T38)
MAXA_IN_AGA(s(T61), T60, T60) → U2_AGA(T61, T60, lessC_in_ag(T61, T60))
MAXA_IN_AGA(s(T61), T60, T60) → LESSC_IN_AG(T61, T60)
LESSC_IN_AG(s(T75), s(T74)) → U5_AG(T75, T74, lessC_in_ag(T75, T74))
LESSC_IN_AG(s(T75), s(T74)) → LESSC_IN_AG(T75, T74)
MAXA_IN_AGA(s(T94), T93, T93) → U3_AGA(T94, T93, lessC_in_ag(T94, T93))

The TRS R consists of the following rules:

maxA_in_aga(s(T13), 0, s(T13)) → maxA_out_aga(s(T13), 0, s(T13))
maxA_in_aga(s(T24), s(T22), s(T24)) → U1_aga(T24, T22, lessB_in_ga(T22, T24))
lessB_in_ga(0, s(T31)) → lessB_out_ga(0, s(T31))
lessB_in_ga(s(T36), s(T38)) → U4_ga(T36, T38, lessB_in_ga(T36, T38))
U4_ga(T36, T38, lessB_out_ga(T36, T38)) → lessB_out_ga(s(T36), s(T38))
U1_aga(T24, T22, lessB_out_ga(T22, T24)) → maxA_out_aga(s(T24), s(T22), s(T24))
maxA_in_aga(0, T54, T54) → maxA_out_aga(0, T54, T54)
maxA_in_aga(s(T61), T60, T60) → U2_aga(T61, T60, lessC_in_ag(T61, T60))
lessC_in_ag(0, s(T68)) → lessC_out_ag(0, s(T68))
lessC_in_ag(s(T75), s(T74)) → U5_ag(T75, T74, lessC_in_ag(T75, T74))
U5_ag(T75, T74, lessC_out_ag(T75, T74)) → lessC_out_ag(s(T75), s(T74))
U2_aga(T61, T60, lessC_out_ag(T61, T60)) → maxA_out_aga(s(T61), T60, T60)
maxA_in_aga(s(T94), T93, T93) → U3_aga(T94, T93, lessC_in_ag(T94, T93))
U3_aga(T94, T93, lessC_out_ag(T94, T93)) → maxA_out_aga(s(T94), T93, T93)

The argument filtering Pi contains the following mapping:
maxA_in_aga(x1, x2, x3) = maxA_in_aga(x2)
0 = 0
maxA_out_aga(x1, x2, x3) = maxA_out_aga(x2)
s(x1) = s(x1)
U1_aga(x1, x2, x3) = U1_aga(x2, x3)
lessB_in_ga(x1, x2) = lessB_in_ga(x1)
lessB_out_ga(x1, x2) = lessB_out_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
U2_aga(x1, x2, x3) = U2_aga(x2, x3)
lessC_in_ag(x1, x2) = lessC_in_ag(x2)
lessC_out_ag(x1, x2) = lessC_out_ag(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x2, x3)
U3_aga(x1, x2, x3) = U3_aga(x2, x3)
MAXA_IN_AGA(x1, x2, x3) = MAXA_IN_AGA(x2)
U1_AGA(x1, x2, x3) = U1_AGA(x2, x3)
LESSB_IN_GA(x1, x2) = LESSB_IN_GA(x1)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
U2_AGA(x1, x2, x3) = U2_AGA(x2, x3)
LESSC_IN_AG(x1, x2) = LESSC_IN_AG(x2)
U5_AG(x1, x2, x3) = U5_AG(x2, x3)
U3_AGA(x1, x2, x3) = U3_AGA(x2, x3)

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

(4) Obligation:

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

MAXA_IN_AGA(s(T24), s(T22), s(T24)) → U1_AGA(T24, T22, lessB_in_ga(T22, T24))
MAXA_IN_AGA(s(T24), s(T22), s(T24)) → LESSB_IN_GA(T22, T24)
LESSB_IN_GA(s(T36), s(T38)) → U4_GA(T36, T38, lessB_in_ga(T36, T38))
LESSB_IN_GA(s(T36), s(T38)) → LESSB_IN_GA(T36, T38)
MAXA_IN_AGA(s(T61), T60, T60) → U2_AGA(T61, T60, lessC_in_ag(T61, T60))
MAXA_IN_AGA(s(T61), T60, T60) → LESSC_IN_AG(T61, T60)
LESSC_IN_AG(s(T75), s(T74)) → U5_AG(T75, T74, lessC_in_ag(T75, T74))
LESSC_IN_AG(s(T75), s(T74)) → LESSC_IN_AG(T75, T74)
MAXA_IN_AGA(s(T94), T93, T93) → U3_AGA(T94, T93, lessC_in_ag(T94, T93))

The TRS R consists of the following rules:

maxA_in_aga(s(T13), 0, s(T13)) → maxA_out_aga(s(T13), 0, s(T13))
maxA_in_aga(s(T24), s(T22), s(T24)) → U1_aga(T24, T22, lessB_in_ga(T22, T24))
lessB_in_ga(0, s(T31)) → lessB_out_ga(0, s(T31))
lessB_in_ga(s(T36), s(T38)) → U4_ga(T36, T38, lessB_in_ga(T36, T38))
U4_ga(T36, T38, lessB_out_ga(T36, T38)) → lessB_out_ga(s(T36), s(T38))
U1_aga(T24, T22, lessB_out_ga(T22, T24)) → maxA_out_aga(s(T24), s(T22), s(T24))
maxA_in_aga(0, T54, T54) → maxA_out_aga(0, T54, T54)
maxA_in_aga(s(T61), T60, T60) → U2_aga(T61, T60, lessC_in_ag(T61, T60))
lessC_in_ag(0, s(T68)) → lessC_out_ag(0, s(T68))
lessC_in_ag(s(T75), s(T74)) → U5_ag(T75, T74, lessC_in_ag(T75, T74))
U5_ag(T75, T74, lessC_out_ag(T75, T74)) → lessC_out_ag(s(T75), s(T74))
U2_aga(T61, T60, lessC_out_ag(T61, T60)) → maxA_out_aga(s(T61), T60, T60)
maxA_in_aga(s(T94), T93, T93) → U3_aga(T94, T93, lessC_in_ag(T94, T93))
U3_aga(T94, T93, lessC_out_ag(T94, T93)) → maxA_out_aga(s(T94), T93, T93)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSC_IN_AG(s(T75), s(T74)) → LESSC_IN_AG(T75, T74)

The TRS R consists of the following rules:

maxA_in_aga(s(T13), 0, s(T13)) → maxA_out_aga(s(T13), 0, s(T13))
maxA_in_aga(s(T24), s(T22), s(T24)) → U1_aga(T24, T22, lessB_in_ga(T22, T24))
lessB_in_ga(0, s(T31)) → lessB_out_ga(0, s(T31))
lessB_in_ga(s(T36), s(T38)) → U4_ga(T36, T38, lessB_in_ga(T36, T38))
U4_ga(T36, T38, lessB_out_ga(T36, T38)) → lessB_out_ga(s(T36), s(T38))
U1_aga(T24, T22, lessB_out_ga(T22, T24)) → maxA_out_aga(s(T24), s(T22), s(T24))
maxA_in_aga(0, T54, T54) → maxA_out_aga(0, T54, T54)
maxA_in_aga(s(T61), T60, T60) → U2_aga(T61, T60, lessC_in_ag(T61, T60))
lessC_in_ag(0, s(T68)) → lessC_out_ag(0, s(T68))
lessC_in_ag(s(T75), s(T74)) → U5_ag(T75, T74, lessC_in_ag(T75, T74))
U5_ag(T75, T74, lessC_out_ag(T75, T74)) → lessC_out_ag(s(T75), s(T74))
U2_aga(T61, T60, lessC_out_ag(T61, T60)) → maxA_out_aga(s(T61), T60, T60)
maxA_in_aga(s(T94), T93, T93) → U3_aga(T94, T93, lessC_in_ag(T94, T93))
U3_aga(T94, T93, lessC_out_ag(T94, T93)) → maxA_out_aga(s(T94), T93, T93)

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

LESSC_IN_AG(s(T75), s(T74)) → LESSC_IN_AG(T75, T74)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
LESSC_IN_AG(x1, x2) = LESSC_IN_AG(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:

LESSC_IN_AG(s(T74)) → LESSC_IN_AG(T74)

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:

LESSC_IN_AG(s(T74)) → LESSC_IN_AG(T74)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESSB_IN_GA(s(T36), s(T38)) → LESSB_IN_GA(T36, T38)

The TRS R consists of the following rules:

maxA_in_aga(s(T13), 0, s(T13)) → maxA_out_aga(s(T13), 0, s(T13))
maxA_in_aga(s(T24), s(T22), s(T24)) → U1_aga(T24, T22, lessB_in_ga(T22, T24))
lessB_in_ga(0, s(T31)) → lessB_out_ga(0, s(T31))
lessB_in_ga(s(T36), s(T38)) → U4_ga(T36, T38, lessB_in_ga(T36, T38))
U4_ga(T36, T38, lessB_out_ga(T36, T38)) → lessB_out_ga(s(T36), s(T38))
U1_aga(T24, T22, lessB_out_ga(T22, T24)) → maxA_out_aga(s(T24), s(T22), s(T24))
maxA_in_aga(0, T54, T54) → maxA_out_aga(0, T54, T54)
maxA_in_aga(s(T61), T60, T60) → U2_aga(T61, T60, lessC_in_ag(T61, T60))
lessC_in_ag(0, s(T68)) → lessC_out_ag(0, s(T68))
lessC_in_ag(s(T75), s(T74)) → U5_ag(T75, T74, lessC_in_ag(T75, T74))
U5_ag(T75, T74, lessC_out_ag(T75, T74)) → lessC_out_ag(s(T75), s(T74))
U2_aga(T61, T60, lessC_out_ag(T61, T60)) → maxA_out_aga(s(T61), T60, T60)
maxA_in_aga(s(T94), T93, T93) → U3_aga(T94, T93, lessC_in_ag(T94, T93))
U3_aga(T94, T93, lessC_out_ag(T94, T93)) → maxA_out_aga(s(T94), T93, T93)

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

LESSB_IN_GA(s(T36), s(T38)) → LESSB_IN_GA(T36, T38)

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

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:

LESSB_IN_GA(s(T36)) → LESSB_IN_GA(T36)

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:

LESSB_IN_GA(s(T36)) → LESSB_IN_GA(T36)
The graph contains the following edges 1 > 1

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