(0) Obligation:

Clauses:

parse(Xs, T) :- ','(app(As, cons(a, cons(s(A, B, C), cons(b, Bs))), Xs), ','(app(As, cons(s(a, s(A, B, C), b), Bs), Ys), parse(Ys, T))).
parse(Xs, T) :- ','(app(As, cons(a, cons(s(A, B), cons(b, Bs))), Xs), ','(app(As, cons(s(a, s(A, B), b), Bs), Ys), parse(Ys, T))).
parse(Xs, T) :- ','(app(As, cons(a, cons(b, Bs)), Xs), ','(app(As, cons(s(a, b), Bs), Ys), parse(Ys, T))).
parse(cons(s(A, B), nil), s(A, B)).
parse(cons(s(A, B, C), nil), s(A, B, C)).
app(nil, X, X).
app(cons(X, Xs), Ys, cons(X, Zs)) :- app(Xs, Ys, Zs).

Queries:

parse(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

app21(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) :- app21(X212, X213, X214, X215, X216, T41).
parse10(T30, T31) :- app21(X135, X136, X137, X138, X139, T30).
parse10(T30, T37) :- ','(appc21(T32, T33, T34, T35, T36, T30), p22(T32, T33, T34, T35, T36, X140, T37)).
parse10(T127, T128) :- p43(X306, X307, X308, X309, T127, X310, T128).
parse10(T208, T209) :- p66(X450, X451, T208, X452, T209).
app31(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) :- app31(T98, T100, T101, T102, T99, X255).
app44(cons(X370, X371), X372, X373, X374, cons(X370, T137)) :- app44(X371, X372, X373, X374, T137).
app54(cons(T177, T182), T184, T185, T183, cons(T177, X411)) :- app54(T182, T184, T185, T183, X411).
app67(cons(X490, X491), X492, cons(X490, T216)) :- app67(X491, X492, T216).
app77(cons(T234, T237), T238, cons(T234, X525)) :- app77(T237, T238, X525).
p22(T32, T33, T34, T35, T36, X140, T37) :- app31(T32, T33, T34, T35, T36, X140).
p22(T32, T33, T34, T35, T36, T50, T51) :- ','(appc31(T32, T33, T34, T35, T36, T50), parse10(T50, T51)).
p43(X306, X307, X308, X309, T127, X310, T128) :- app44(X306, X307, X308, X309, T127).
p43(T129, T130, T131, T132, T127, X310, T133) :- ','(appc44(T129, T130, T131, T132, T127), app54(T129, T130, T131, T132, X310)).
p43(T129, T130, T131, T132, T127, T144, T145) :- ','(appc44(T129, T130, T131, T132, T127), ','(appc54(T129, T130, T131, T132, T144), parse10(T144, T145))).
p66(X450, X451, T208, X452, T209) :- app67(X450, X451, T208).
p66(T210, T211, T208, X452, T212) :- ','(appc67(T210, T211, T208), app77(T210, T211, X452)).
p66(T210, T211, T208, T219, T220) :- ','(appc67(T210, T211, T208), ','(appc77(T210, T211, T219), parse10(T219, T220))).
parse1(cons(a, cons(s(T9, T10, T11), cons(b, T12))), T7) :- ','(appc9(T9, T10, T11, T12, T13), parse10(T13, T7)).
parse1(cons(X608, T266), T7) :- app21(X609, X610, X611, X612, X613, T266).
parse1(cons(X608, T266), T7) :- ','(appc21(T267, T268, T269, T270, T271, T266), p22(cons(X608, T267), T268, T269, T270, T271, X10, T7)).
parse1(T287, T289) :- p43(X682, X683, X684, X685, T287, X686, T289).
parse1(T300, T302) :- p66(X719, X720, T300, X721, T302).

Clauses:

appc21(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))).
appc21(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) :- appc21(X212, X213, X214, X215, X216, T41).
parsec10(T30, T37) :- ','(appc21(T32, T33, T34, T35, T36, T30), qc22(T32, T33, T34, T35, T36, X140, T37)).
parsec10(T127, T128) :- qc43(X306, X307, X308, X309, T127, X310, T128).
parsec10(T208, T209) :- qc66(X450, X451, T208, X452, T209).
parsec10(cons(s(T251, T252), nil), s(T251, T252)).
parsec10(cons(s(T259, T260, T261), nil), s(T259, T260, T261)).
appc31(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)).
appc31(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) :- appc31(T98, T100, T101, T102, T99, X255).
appc44(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))).
appc44(cons(X370, X371), X372, X373, X374, cons(X370, T137)) :- appc44(X371, X372, X373, X374, T137).
appc54(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)).
appc54(cons(T177, T182), T184, T185, T183, cons(T177, X411)) :- appc54(T182, T184, T185, T183, X411).
appc67(nil, X470, cons(a, cons(b, X470))).
appc67(cons(X490, X491), X492, cons(X490, T216)) :- appc67(X491, X492, T216).
appc77(nil, T227, cons(s(a, b), T227)).
appc77(cons(T234, T237), T238, cons(T234, X525)) :- appc77(T237, T238, X525).
qc22(T32, T33, T34, T35, T36, T50, T51) :- ','(appc31(T32, T33, T34, T35, T36, T50), parsec10(T50, T51)).
qc43(T129, T130, T131, T132, T127, T144, T145) :- ','(appc44(T129, T130, T131, T132, T127), ','(appc54(T129, T130, T131, T132, T144), parsec10(T144, T145))).
qc66(T210, T211, T208, T219, T220) :- ','(appc67(T210, T211, T208), ','(appc77(T210, T211, T219), parsec10(T219, T220))).
appc9(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)).

Afs:

parse1(x1, x2)  =  parse1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
parse1_in: (b,f)
parse10_in: (b,f)
app21_in: (f,f,f,f,f,b)
appc21_in: (f,f,f,f,f,b)
p22_in: (b,b,b,b,b,f,f)
app31_in: (b,b,b,b,b,f)
appc31_in: (b,b,b,b,b,f)
p43_in: (f,f,f,f,b,f,f)
app44_in: (f,f,f,f,b)
appc44_in: (f,f,f,f,b)
app54_in: (b,b,b,b,f)
appc54_in: (b,b,b,b,f)
p66_in: (f,f,b,f,f)
app67_in: (f,f,b)
appc67_in: (f,f,b)
app77_in: (b,b,f)
appc77_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PARSE1_IN_GA(cons(a, cons(s(T9, T10, T11), cons(b, T12))), T7) → U27_GA(T9, T10, T11, T12, T7, appc9_in_gggga(T9, T10, T11, T12, T13))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → U28_GA(T9, T10, T11, T12, T7, parse10_in_ga(T13, T7))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → PARSE10_IN_GA(T13, T7)
PARSE10_IN_GA(T30, T31) → U2_GA(T30, T31, app21_in_aaaaag(X135, X136, X137, X138, X139, T30))
PARSE10_IN_GA(T30, T31) → APP21_IN_AAAAAG(X135, X136, X137, X138, X139, T30)
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U1_AAAAAG(X211, X212, X213, X214, X215, X216, T41, app21_in_aaaaag(X212, X213, X214, X215, X216, T41))
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)
PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → U4_GA(T30, T37, p22_in_gggggaa(T32, T33, T34, T35, T36, X140, T37))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → U12_GGGGGAA(T32, T33, T34, T35, T36, X140, T37, app31_in_ggggga(T32, T33, T34, T35, T36, X140))
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → APP31_IN_GGGGGA(T32, T33, T34, T35, T36, X140)
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U7_GGGGGA(T92, T98, T100, T101, T102, T99, X255, app31_in_ggggga(T98, T100, T101, T102, T99, X255))
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → U14_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, parse10_in_ga(T50, T51))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → U5_GA(T127, T128, p43_in_aaaagaa(X306, X307, X308, X309, T127, X310, T128))
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → U15_AAAAGAA(X306, X307, X308, X309, T127, X310, T128, app44_in_aaaag(X306, X307, X308, X309, T127))
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → APP44_IN_AAAAG(X306, X307, X308, X309, T127)
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U8_AAAAG(X370, X371, X372, X373, X374, T137, app44_in_aaaag(X371, X372, X373, X374, T137))
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, X310, T133) → U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_in_aaaag(T129, T130, T131, T132, T127))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U17_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, app54_in_gggga(T129, T130, T131, T132, X310))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → APP54_IN_GGGGA(T129, T130, T131, T132, X310)
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U9_GGGGA(T177, T182, T184, T185, T183, X411, app54_in_gggga(T182, T184, T185, T183, X411))
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → U20_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, parse10_in_ga(T144, T145))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → U6_GA(T208, T209, p66_in_aagaa(X450, X451, T208, X452, T209))
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(X450, X451, T208, X452, T209) → U21_AAGAA(X450, X451, T208, X452, T209, app67_in_aag(X450, X451, T208))
P66_IN_AAGAA(X450, X451, T208, X452, T209) → APP67_IN_AAG(X450, X451, T208)
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → U10_AAG(X490, X491, X492, T216, app67_in_aag(X491, X492, T216))
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)
P66_IN_AAGAA(T210, T211, T208, X452, T212) → U22_AAGAA(T210, T211, T208, X452, T212, appc67_in_aag(T210, T211, T208))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → U23_AAGAA(T210, T211, T208, X452, T212, app77_in_gga(T210, T211, X452))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → APP77_IN_GGA(T210, T211, X452)
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → U11_GGA(T234, T237, T238, X525, app77_in_gga(T237, T238, X525))
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → U26_AAGAA(T210, T211, T208, T219, T220, parse10_in_ga(T219, T220))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)
PARSE1_IN_GA(cons(X608, T266), T7) → U29_GA(X608, T266, T7, app21_in_aaaaag(X609, X610, X611, X612, X613, T266))
PARSE1_IN_GA(cons(X608, T266), T7) → APP21_IN_AAAAAG(X609, X610, X611, X612, X613, T266)
PARSE1_IN_GA(cons(X608, T266), T7) → U30_GA(X608, T266, T7, appc21_in_aaaaag(T267, T268, T269, T270, T271, T266))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → U31_GA(X608, T266, T7, p22_in_gggggaa(cons(X608, T267), T268, T269, T270, T271, X10, T7))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → P22_IN_GGGGGAA(cons(X608, T267), T268, T269, T270, T271, X10, T7)
PARSE1_IN_GA(T287, T289) → U32_GA(T287, T289, p43_in_aaaagaa(X682, X683, X684, X685, T287, X686, T289))
PARSE1_IN_GA(T287, T289) → P43_IN_AAAAGAA(X682, X683, X684, X685, T287, X686, T289)
PARSE1_IN_GA(T300, T302) → U33_GA(T300, T302, p66_in_aagaa(X719, X720, T300, X721, T302))
PARSE1_IN_GA(T300, T302) → P66_IN_AAGAA(X719, X720, T300, X721, T302)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
parse10_in_ga(x1, x2)  =  parse10_in_ga(x1)
app21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  app21_in_aaaaag(x6)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
p22_in_gggggaa(x1, x2, x3, x4, x5, x6, x7)  =  p22_in_gggggaa(x1, x2, x3, x4, x5)
app31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  app31_in_ggggga(x1, x2, x3, x4, x5)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
p43_in_aaaagaa(x1, x2, x3, x4, x5, x6, x7)  =  p43_in_aaaagaa(x5)
app44_in_aaaag(x1, x2, x3, x4, x5)  =  app44_in_aaaag(x5)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
app54_in_gggga(x1, x2, x3, x4, x5)  =  app54_in_gggga(x1, x2, x3, x4)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
p66_in_aagaa(x1, x2, x3, x4, x5)  =  p66_in_aagaa(x3)
app67_in_aag(x1, x2, x3)  =  app67_in_aag(x3)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
app77_in_gga(x1, x2, x3)  =  app77_in_gga(x1, x2)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
PARSE1_IN_GA(x1, x2)  =  PARSE1_IN_GA(x1)
U27_GA(x1, x2, x3, x4, x5, x6)  =  U27_GA(x1, x2, x3, x4, x6)
U28_GA(x1, x2, x3, x4, x5, x6)  =  U28_GA(x1, x2, x3, x4, x6)
PARSE10_IN_GA(x1, x2)  =  PARSE10_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
APP21_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APP21_IN_AAAAAG(x6)
U1_AAAAAG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_AAAAAG(x1, x7, x8)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
P22_IN_GGGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  P22_IN_GGGGGAA(x1, x2, x3, x4, x5)
U12_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GGGGGAA(x1, x2, x3, x4, x5, x8)
APP31_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APP31_IN_GGGGGA(x1, x2, x3, x4, x5)
U7_GGGGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U7_GGGGGA(x1, x2, x3, x4, x5, x6, x8)
U13_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGGGGAA(x1, x2, x3, x4, x5, x8)
U14_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GGGGGAA(x1, x2, x3, x4, x5, x6, x8)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
P43_IN_AAAAGAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAGAA(x5)
U15_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_AAAAGAA(x5, x8)
APP44_IN_AAAAG(x1, x2, x3, x4, x5)  =  APP44_IN_AAAAG(x5)
U8_AAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U8_AAAAG(x1, x6, x7)
U16_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_AAAAGAA(x5, x8)
U17_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_AAAAGAA(x1, x2, x3, x4, x5, x8)
APP54_IN_GGGGA(x1, x2, x3, x4, x5)  =  APP54_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGGGA(x1, x2, x3, x4, x5, x7)
U18_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_AAAAGAA(x5, x8)
U19_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAGAA(x1, x2, x3, x4, x5, x8)
U20_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U20_AAAAGAA(x1, x2, x3, x4, x5, x8)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
P66_IN_AAGAA(x1, x2, x3, x4, x5)  =  P66_IN_AAGAA(x3)
U21_AAGAA(x1, x2, x3, x4, x5, x6)  =  U21_AAGAA(x3, x6)
APP67_IN_AAG(x1, x2, x3)  =  APP67_IN_AAG(x3)
U10_AAG(x1, x2, x3, x4, x5)  =  U10_AAG(x1, x4, x5)
U22_AAGAA(x1, x2, x3, x4, x5, x6)  =  U22_AAGAA(x3, x6)
U23_AAGAA(x1, x2, x3, x4, x5, x6)  =  U23_AAGAA(x1, x2, x3, x6)
APP77_IN_GGA(x1, x2, x3)  =  APP77_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4, x5)  =  U11_GGA(x1, x2, x3, x5)
U24_AAGAA(x1, x2, x3, x4, x5, x6)  =  U24_AAGAA(x3, x6)
U25_AAGAA(x1, x2, x3, x4, x5, x6)  =  U25_AAGAA(x1, x2, x3, x6)
U26_AAGAA(x1, x2, x3, x4, x5, x6)  =  U26_AAGAA(x1, x2, x3, x6)
U29_GA(x1, x2, x3, x4)  =  U29_GA(x1, x2, x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x2, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x2, x4)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
U33_GA(x1, x2, x3)  =  U33_GA(x1, x3)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

PARSE1_IN_GA(cons(a, cons(s(T9, T10, T11), cons(b, T12))), T7) → U27_GA(T9, T10, T11, T12, T7, appc9_in_gggga(T9, T10, T11, T12, T13))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → U28_GA(T9, T10, T11, T12, T7, parse10_in_ga(T13, T7))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → PARSE10_IN_GA(T13, T7)
PARSE10_IN_GA(T30, T31) → U2_GA(T30, T31, app21_in_aaaaag(X135, X136, X137, X138, X139, T30))
PARSE10_IN_GA(T30, T31) → APP21_IN_AAAAAG(X135, X136, X137, X138, X139, T30)
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U1_AAAAAG(X211, X212, X213, X214, X215, X216, T41, app21_in_aaaaag(X212, X213, X214, X215, X216, T41))
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)
PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → U4_GA(T30, T37, p22_in_gggggaa(T32, T33, T34, T35, T36, X140, T37))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → U12_GGGGGAA(T32, T33, T34, T35, T36, X140, T37, app31_in_ggggga(T32, T33, T34, T35, T36, X140))
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → APP31_IN_GGGGGA(T32, T33, T34, T35, T36, X140)
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U7_GGGGGA(T92, T98, T100, T101, T102, T99, X255, app31_in_ggggga(T98, T100, T101, T102, T99, X255))
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → U14_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, parse10_in_ga(T50, T51))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → U5_GA(T127, T128, p43_in_aaaagaa(X306, X307, X308, X309, T127, X310, T128))
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → U15_AAAAGAA(X306, X307, X308, X309, T127, X310, T128, app44_in_aaaag(X306, X307, X308, X309, T127))
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → APP44_IN_AAAAG(X306, X307, X308, X309, T127)
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U8_AAAAG(X370, X371, X372, X373, X374, T137, app44_in_aaaag(X371, X372, X373, X374, T137))
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, X310, T133) → U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_in_aaaag(T129, T130, T131, T132, T127))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U17_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, app54_in_gggga(T129, T130, T131, T132, X310))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → APP54_IN_GGGGA(T129, T130, T131, T132, X310)
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U9_GGGGA(T177, T182, T184, T185, T183, X411, app54_in_gggga(T182, T184, T185, T183, X411))
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → U20_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, parse10_in_ga(T144, T145))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → U6_GA(T208, T209, p66_in_aagaa(X450, X451, T208, X452, T209))
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(X450, X451, T208, X452, T209) → U21_AAGAA(X450, X451, T208, X452, T209, app67_in_aag(X450, X451, T208))
P66_IN_AAGAA(X450, X451, T208, X452, T209) → APP67_IN_AAG(X450, X451, T208)
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → U10_AAG(X490, X491, X492, T216, app67_in_aag(X491, X492, T216))
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)
P66_IN_AAGAA(T210, T211, T208, X452, T212) → U22_AAGAA(T210, T211, T208, X452, T212, appc67_in_aag(T210, T211, T208))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → U23_AAGAA(T210, T211, T208, X452, T212, app77_in_gga(T210, T211, X452))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → APP77_IN_GGA(T210, T211, X452)
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → U11_GGA(T234, T237, T238, X525, app77_in_gga(T237, T238, X525))
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → U26_AAGAA(T210, T211, T208, T219, T220, parse10_in_ga(T219, T220))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)
PARSE1_IN_GA(cons(X608, T266), T7) → U29_GA(X608, T266, T7, app21_in_aaaaag(X609, X610, X611, X612, X613, T266))
PARSE1_IN_GA(cons(X608, T266), T7) → APP21_IN_AAAAAG(X609, X610, X611, X612, X613, T266)
PARSE1_IN_GA(cons(X608, T266), T7) → U30_GA(X608, T266, T7, appc21_in_aaaaag(T267, T268, T269, T270, T271, T266))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → U31_GA(X608, T266, T7, p22_in_gggggaa(cons(X608, T267), T268, T269, T270, T271, X10, T7))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → P22_IN_GGGGGAA(cons(X608, T267), T268, T269, T270, T271, X10, T7)
PARSE1_IN_GA(T287, T289) → U32_GA(T287, T289, p43_in_aaaagaa(X682, X683, X684, X685, T287, X686, T289))
PARSE1_IN_GA(T287, T289) → P43_IN_AAAAGAA(X682, X683, X684, X685, T287, X686, T289)
PARSE1_IN_GA(T300, T302) → U33_GA(T300, T302, p66_in_aagaa(X719, X720, T300, X721, T302))
PARSE1_IN_GA(T300, T302) → P66_IN_AAGAA(X719, X720, T300, X721, T302)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
parse10_in_ga(x1, x2)  =  parse10_in_ga(x1)
app21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  app21_in_aaaaag(x6)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
p22_in_gggggaa(x1, x2, x3, x4, x5, x6, x7)  =  p22_in_gggggaa(x1, x2, x3, x4, x5)
app31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  app31_in_ggggga(x1, x2, x3, x4, x5)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
p43_in_aaaagaa(x1, x2, x3, x4, x5, x6, x7)  =  p43_in_aaaagaa(x5)
app44_in_aaaag(x1, x2, x3, x4, x5)  =  app44_in_aaaag(x5)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
app54_in_gggga(x1, x2, x3, x4, x5)  =  app54_in_gggga(x1, x2, x3, x4)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
p66_in_aagaa(x1, x2, x3, x4, x5)  =  p66_in_aagaa(x3)
app67_in_aag(x1, x2, x3)  =  app67_in_aag(x3)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
app77_in_gga(x1, x2, x3)  =  app77_in_gga(x1, x2)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
PARSE1_IN_GA(x1, x2)  =  PARSE1_IN_GA(x1)
U27_GA(x1, x2, x3, x4, x5, x6)  =  U27_GA(x1, x2, x3, x4, x6)
U28_GA(x1, x2, x3, x4, x5, x6)  =  U28_GA(x1, x2, x3, x4, x6)
PARSE10_IN_GA(x1, x2)  =  PARSE10_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
APP21_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APP21_IN_AAAAAG(x6)
U1_AAAAAG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U1_AAAAAG(x1, x7, x8)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
P22_IN_GGGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  P22_IN_GGGGGAA(x1, x2, x3, x4, x5)
U12_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GGGGGAA(x1, x2, x3, x4, x5, x8)
APP31_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APP31_IN_GGGGGA(x1, x2, x3, x4, x5)
U7_GGGGGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U7_GGGGGA(x1, x2, x3, x4, x5, x6, x8)
U13_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGGGGAA(x1, x2, x3, x4, x5, x8)
U14_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GGGGGAA(x1, x2, x3, x4, x5, x6, x8)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
P43_IN_AAAAGAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAGAA(x5)
U15_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_AAAAGAA(x5, x8)
APP44_IN_AAAAG(x1, x2, x3, x4, x5)  =  APP44_IN_AAAAG(x5)
U8_AAAAG(x1, x2, x3, x4, x5, x6, x7)  =  U8_AAAAG(x1, x6, x7)
U16_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_AAAAGAA(x5, x8)
U17_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_AAAAGAA(x1, x2, x3, x4, x5, x8)
APP54_IN_GGGGA(x1, x2, x3, x4, x5)  =  APP54_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGGGA(x1, x2, x3, x4, x5, x7)
U18_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_AAAAGAA(x5, x8)
U19_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAGAA(x1, x2, x3, x4, x5, x8)
U20_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U20_AAAAGAA(x1, x2, x3, x4, x5, x8)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
P66_IN_AAGAA(x1, x2, x3, x4, x5)  =  P66_IN_AAGAA(x3)
U21_AAGAA(x1, x2, x3, x4, x5, x6)  =  U21_AAGAA(x3, x6)
APP67_IN_AAG(x1, x2, x3)  =  APP67_IN_AAG(x3)
U10_AAG(x1, x2, x3, x4, x5)  =  U10_AAG(x1, x4, x5)
U22_AAGAA(x1, x2, x3, x4, x5, x6)  =  U22_AAGAA(x3, x6)
U23_AAGAA(x1, x2, x3, x4, x5, x6)  =  U23_AAGAA(x1, x2, x3, x6)
APP77_IN_GGA(x1, x2, x3)  =  APP77_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4, x5)  =  U11_GGA(x1, x2, x3, x5)
U24_AAGAA(x1, x2, x3, x4, x5, x6)  =  U24_AAGAA(x3, x6)
U25_AAGAA(x1, x2, x3, x4, x5, x6)  =  U25_AAGAA(x1, x2, x3, x6)
U26_AAGAA(x1, x2, x3, x4, x5, x6)  =  U26_AAGAA(x1, x2, x3, x6)
U29_GA(x1, x2, x3, x4)  =  U29_GA(x1, x2, x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x2, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x2, x4)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
U33_GA(x1, x2, x3)  =  U33_GA(x1, x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
APP77_IN_GGA(x1, x2, x3)  =  APP77_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:

APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)

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

APP77_IN_GGA(cons(T234, T237), T238) → APP77_IN_GGA(T237, T238)

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:

  • APP77_IN_GGA(cons(T234, T237), T238) → APP77_IN_GGA(T237, T238)
    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:

APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
APP67_IN_AAG(x1, x2, x3)  =  APP67_IN_AAG(x3)

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:

APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)

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

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:

APP67_IN_AAG(cons(X490, T216)) → APP67_IN_AAG(T216)

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:

  • APP67_IN_AAG(cons(X490, T216)) → APP67_IN_AAG(T216)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
APP54_IN_GGGGA(x1, x2, x3, x4, x5)  =  APP54_IN_GGGGA(x1, x2, x3, x4)

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:

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APP54_IN_GGGGA(x1, x2, x3, x4, x5)  =  APP54_IN_GGGGA(x1, x2, x3, x4)

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:

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183) → APP54_IN_GGGGA(T182, T184, T185, T183)

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

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

  • APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183) → APP54_IN_GGGGA(T182, T184, T185, T183)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4

(27) YES

(28) Obligation:

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

APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
APP44_IN_AAAAG(x1, x2, x3, x4, x5)  =  APP44_IN_AAAAG(x5)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APP44_IN_AAAAG(x1, x2, x3, x4, x5)  =  APP44_IN_AAAAG(x5)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

APP44_IN_AAAAG(cons(X370, T137)) → APP44_IN_AAAAG(T137)

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

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

  • APP44_IN_AAAAG(cons(X370, T137)) → APP44_IN_AAAAG(T137)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
APP31_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APP31_IN_GGGGGA(x1, x2, x3, x4, x5)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APP31_IN_GGGGGA(x1, x2, x3, x4, x5, x6)  =  APP31_IN_GGGGGA(x1, x2, x3, x4, x5)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99)

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

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

  • APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5

(41) YES

(42) Obligation:

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

APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
APP21_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APP21_IN_AAAAAG(x6)

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

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
APP21_IN_AAAAAG(x1, x2, x3, x4, x5, x6)  =  APP21_IN_AAAAAG(x6)

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

APP21_IN_AAAAAG(cons(X211, T41)) → APP21_IN_AAAAAG(T41)

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

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

  • APP21_IN_AAAAAG(cons(X211, T41)) → APP21_IN_AAAAAG(T41)
    The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

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

PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc9_in_gggga(x1, x2, x3, x4, x5)  =  appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5)  =  appc9_out_gggga(x1, x2, x3, x4, x5)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
PARSE10_IN_GA(x1, x2)  =  PARSE10_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
P22_IN_GGGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  P22_IN_GGGGGAA(x1, x2, x3, x4, x5)
U13_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGGGGAA(x1, x2, x3, x4, x5, x8)
P43_IN_AAAAGAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAGAA(x5)
U18_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_AAAAGAA(x5, x8)
U19_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAGAA(x1, x2, x3, x4, x5, x8)
P66_IN_AAGAA(x1, x2, x3, x4, x5)  =  P66_IN_AAGAA(x3)
U24_AAGAA(x1, x2, x3, x4, x5, x6)  =  U24_AAGAA(x3, x6)
U25_AAGAA(x1, x2, x3, x4, x5, x6)  =  U25_AAGAA(x1, x2, x3, x6)

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

(50) UsableRulesProof (EQUIVALENT transformation)

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

(51) Obligation:

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

PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)

The TRS R consists of the following rules:

appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
a  =  a
s(x1, x2, x3)  =  s(x1, x2, x3)
b  =  b
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)  =  appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8)  =  U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_in_ggggga(x1, x2, x3, x4, x5)
nil  =  nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6)  =  appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5)  =  appc44_in_aaaag(x5)
s(x1, x2)  =  s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5)  =  appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7)  =  U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5)  =  appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5)  =  appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7)  =  U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3)  =  appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3)  =  appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5)  =  U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3)  =  appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3)  =  appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5)  =  U44_gga(x1, x2, x3, x5)
PARSE10_IN_GA(x1, x2)  =  PARSE10_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
P22_IN_GGGGGAA(x1, x2, x3, x4, x5, x6, x7)  =  P22_IN_GGGGGAA(x1, x2, x3, x4, x5)
U13_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGGGGAA(x1, x2, x3, x4, x5, x8)
P43_IN_AAAAGAA(x1, x2, x3, x4, x5, x6, x7)  =  P43_IN_AAAAGAA(x5)
U18_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_AAAAGAA(x5, x8)
U19_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_AAAAGAA(x1, x2, x3, x4, x5, x8)
P66_IN_AAGAA(x1, x2, x3, x4, x5)  =  P66_IN_AAGAA(x3)
U24_AAGAA(x1, x2, x3, x4, x5, x6)  =  U24_AAGAA(x3, x6)
U25_AAGAA(x1, x2, x3, x4, x5, x6)  =  U25_AAGAA(x1, x2, x3, x6)

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

(52) PiDPToQDPProof (SOUND transformation)

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

(53) Obligation:

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

PARSE10_IN_GA(T30) → U3_GA(T30, appc21_in_aaaaag(T30))
U3_GA(T30, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36) → U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_in_ggggga(T32, T33, T34, T35, T36))
U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50)
PARSE10_IN_GA(T127) → P43_IN_AAAAGAA(T127)
P43_IN_AAAAGAA(T127) → U18_AAAAGAA(T127, appc44_in_aaaag(T127))
U18_AAAAGAA(T127, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_in_gggga(T129, T130, T131, T132))
U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144)
PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


P22_IN_GGGGGAA(T32, T33, T34, T35, T36) → U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_in_ggggga(T32, T33, T34, T35, T36))
U18_AAAAGAA(T127, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_in_gggga(T129, T130, T131, T132))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P22_IN_GGGGGAA(x1, x2, x3, x4, x5)) = 1 + x1 + x5   
POL(P43_IN_AAAAGAA(x1)) = x1   
POL(P66_IN_AAGAA(x1)) = x1   
POL(PARSE10_IN_GA(x1)) = x1   
POL(U13_GGGGGAA(x1, x2, x3, x4, x5, x6)) = x6   
POL(U18_AAAAGAA(x1, x2)) = x2   
POL(U19_AAAAGAA(x1, x2, x3, x4, x5, x6)) = x6   
POL(U24_AAGAA(x1, x2)) = x2   
POL(U25_AAGAA(x1, x2, x3, x4)) = x4   
POL(U35_aaaaag(x1, x2, x3)) = 1 + x3   
POL(U3_GA(x1, x2)) = x2   
POL(U40_ggggga(x1, x2, x3, x4, x5, x6, x7)) = 1 + x7   
POL(U41_aaaag(x1, x2, x3)) = 1 + x3   
POL(U42_gggga(x1, x2, x3, x4, x5, x6)) = 1 + x6   
POL(U43_aag(x1, x2, x3)) = 1 + x3   
POL(U44_gga(x1, x2, x3, x4)) = 1 + x4   
POL(a) = 0   
POL(appc21_in_aaaaag(x1)) = x1   
POL(appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)) = 1 + x1 + x5   
POL(appc31_in_ggggga(x1, x2, x3, x4, x5)) = x1 + x5   
POL(appc31_out_ggggga(x1, x2, x3, x4, x5, x6)) = x6   
POL(appc44_in_aaaag(x1)) = x1   
POL(appc44_out_aaaag(x1, x2, x3, x4, x5)) = 1 + x1 + x4   
POL(appc54_in_gggga(x1, x2, x3, x4)) = x1 + x4   
POL(appc54_out_gggga(x1, x2, x3, x4, x5)) = x5   
POL(appc67_in_aag(x1)) = x1   
POL(appc67_out_aag(x1, x2, x3)) = x1 + x2   
POL(appc77_in_gga(x1, x2)) = x1 + x2   
POL(appc77_out_gga(x1, x2, x3)) = x3   
POL(b) = 0   
POL(cons(x1, x2)) = 1 + x2   
POL(nil) = 1   
POL(s(x1, x2)) = 0   
POL(s(x1, x2, x3)) = 0   

The following usable rules [FROCOS05] were oriented:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(55) Obligation:

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

PARSE10_IN_GA(T30) → U3_GA(T30, appc21_in_aaaaag(T30))
U3_GA(T30, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36)
U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50)
PARSE10_IN_GA(T127) → P43_IN_AAAAGAA(T127)
P43_IN_AAAAGAA(T127) → U18_AAAAGAA(T127, appc44_in_aaaag(T127))
U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144)
PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(56) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes.

(57) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(58) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(59) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(60) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)

(61) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

The set Q consists of the following terms:

appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(62) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P66_IN_AAGAA(x1)) = x1   
POL(PARSE10_IN_GA(x1)) = x1   
POL(U24_AAGAA(x1, x2)) = x2   
POL(U25_AAGAA(x1, x2, x3, x4)) = x4   
POL(U43_aag(x1, x2, x3)) = 1 + x3   
POL(U44_gga(x1, x2, x3, x4)) = 1 + x4   
POL(a) = 0   
POL(appc67_in_aag(x1)) = x1   
POL(appc67_out_aag(x1, x2, x3)) = 1 + x1 + x2   
POL(appc77_in_gga(x1, x2)) = x1 + x2   
POL(appc77_out_gga(x1, x2, x3)) = x3   
POL(b) = 0   
POL(cons(x1, x2)) = 1 + x2   
POL(nil) = 1   
POL(s(x1, x2)) = 0   

The following usable rules [FROCOS05] were oriented:

appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

(63) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

The set Q consists of the following terms:

appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(64) DependencyGraphProof (EQUIVALENT transformation)

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

(65) TRUE