(0) Obligation:

Clauses:

f(A, [], RES) :- g(A, [], RES).
f(.(A, As), .(B, Bs), RES) :- f(.(B, .(A, As)), Bs, RES).
g([], RES, RES).
g(.(C, Cs), D, RES) :- g(Cs, .(C, D), RES).

Queries:

f(g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

g71([], T404, T405, .(T404, T405)).
g71(.(T416, T417), T418, T419, T421) :- g71(T417, T416, .(T418, T419), T421).
g13([], T31, .(T31, [])).
g13(.(T57, []), T58, .(T57, .(T58, []))).
g13(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))).
g13(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))).
g13(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))).
g13(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))).
g13(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))).
g13(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) :- g71(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374).
f1([], [], []).
f1(.(T21, T22), [], T24) :- g13(T22, T21, T24).
f1(.(T480, T481), .(T479, []), T483) :- g13(.(T480, T481), T479, T483).
f1(.(T501, T502), .(T500, .(T503, T504)), T506) :- f1(.(T503, .(T500, .(T501, T502))), T504, T506).

Queries:

f1(g,g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
f1_in: (b,b,f)
g13_in: (b,b,f)
g71_in: (b,b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

f1_in_gga([], [], []) → f1_out_gga([], [], [])
f1_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, g13_in_gga(T22, T21, T24))
g13_in_gga([], T31, .(T31, [])) → g13_out_gga([], T31, .(T31, []))
g13_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → g13_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
g13_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → g13_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
g13_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → g13_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
g13_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → g13_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
g13_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → g13_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
g13_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → g13_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
g13_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
g71_in_ggga([], T404, T405, .(T404, T405)) → g71_out_ggga([], T404, T405, .(T404, T405))
g71_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, g71_out_ggga(T417, T416, .(T418, T419), T421)) → g71_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → g13_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, g13_out_gga(T22, T21, T24)) → f1_out_gga(.(T21, T22), [], T24)
f1_in_gga(.(T480, T481), .(T479, []), T483) → U4_gga(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
U4_gga(T480, T481, T479, T483, g13_out_gga(.(T480, T481), T479, T483)) → f1_out_gga(.(T480, T481), .(T479, []), T483)
f1_in_gga(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_gga(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
U5_gga(T501, T502, T500, T503, T504, T506, f1_out_gga(.(T503, .(T500, .(T501, T502))), T504, T506)) → f1_out_gga(.(T501, T502), .(T500, .(T503, T504)), T506)

The argument filtering Pi contains the following mapping:
f1_in_gga(x1, x2, x3)  =  f1_in_gga(x1, x2)
[]  =  []
f1_out_gga(x1, x2, x3)  =  f1_out_gga(x3)
.(x1, x2)  =  .(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
g13_in_gga(x1, x2, x3)  =  g13_in_gga(x1, x2)
g13_out_gga(x1, x2, x3)  =  g13_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_gga(x11)
g71_in_ggga(x1, x2, x3, x4)  =  g71_in_ggga(x1, x2, x3)
g71_out_ggga(x1, x2, x3, x4)  =  g71_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6)  =  U1_ggga(x6)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x5)
U5_gga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gga(x7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

f1_in_gga([], [], []) → f1_out_gga([], [], [])
f1_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, g13_in_gga(T22, T21, T24))
g13_in_gga([], T31, .(T31, [])) → g13_out_gga([], T31, .(T31, []))
g13_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → g13_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
g13_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → g13_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
g13_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → g13_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
g13_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → g13_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
g13_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → g13_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
g13_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → g13_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
g13_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
g71_in_ggga([], T404, T405, .(T404, T405)) → g71_out_ggga([], T404, T405, .(T404, T405))
g71_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, g71_out_ggga(T417, T416, .(T418, T419), T421)) → g71_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → g13_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, g13_out_gga(T22, T21, T24)) → f1_out_gga(.(T21, T22), [], T24)
f1_in_gga(.(T480, T481), .(T479, []), T483) → U4_gga(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
U4_gga(T480, T481, T479, T483, g13_out_gga(.(T480, T481), T479, T483)) → f1_out_gga(.(T480, T481), .(T479, []), T483)
f1_in_gga(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_gga(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
U5_gga(T501, T502, T500, T503, T504, T506, f1_out_gga(.(T503, .(T500, .(T501, T502))), T504, T506)) → f1_out_gga(.(T501, T502), .(T500, .(T503, T504)), T506)

The argument filtering Pi contains the following mapping:
f1_in_gga(x1, x2, x3)  =  f1_in_gga(x1, x2)
[]  =  []
f1_out_gga(x1, x2, x3)  =  f1_out_gga(x3)
.(x1, x2)  =  .(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
g13_in_gga(x1, x2, x3)  =  g13_in_gga(x1, x2)
g13_out_gga(x1, x2, x3)  =  g13_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_gga(x11)
g71_in_ggga(x1, x2, x3, x4)  =  g71_in_ggga(x1, x2, x3)
g71_out_ggga(x1, x2, x3, x4)  =  g71_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6)  =  U1_ggga(x6)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x5)
U5_gga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gga(x7)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

F1_IN_GGA(.(T21, T22), [], T24) → U3_GGA(T21, T22, T24, g13_in_gga(T22, T21, T24))
F1_IN_GGA(.(T21, T22), [], T24) → G13_IN_GGA(T22, T21, T24)
G13_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_GGA(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
G13_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → G71_IN_GGGA(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)
G71_IN_GGGA(.(T416, T417), T418, T419, T421) → U1_GGGA(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
G71_IN_GGGA(.(T416, T417), T418, T419, T421) → G71_IN_GGGA(T417, T416, .(T418, T419), T421)
F1_IN_GGA(.(T480, T481), .(T479, []), T483) → U4_GGA(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
F1_IN_GGA(.(T480, T481), .(T479, []), T483) → G13_IN_GGA(.(T480, T481), T479, T483)
F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_GGA(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504)), T506) → F1_IN_GGA(.(T503, .(T500, .(T501, T502))), T504, T506)

The TRS R consists of the following rules:

f1_in_gga([], [], []) → f1_out_gga([], [], [])
f1_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, g13_in_gga(T22, T21, T24))
g13_in_gga([], T31, .(T31, [])) → g13_out_gga([], T31, .(T31, []))
g13_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → g13_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
g13_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → g13_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
g13_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → g13_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
g13_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → g13_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
g13_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → g13_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
g13_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → g13_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
g13_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
g71_in_ggga([], T404, T405, .(T404, T405)) → g71_out_ggga([], T404, T405, .(T404, T405))
g71_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, g71_out_ggga(T417, T416, .(T418, T419), T421)) → g71_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → g13_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, g13_out_gga(T22, T21, T24)) → f1_out_gga(.(T21, T22), [], T24)
f1_in_gga(.(T480, T481), .(T479, []), T483) → U4_gga(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
U4_gga(T480, T481, T479, T483, g13_out_gga(.(T480, T481), T479, T483)) → f1_out_gga(.(T480, T481), .(T479, []), T483)
f1_in_gga(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_gga(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
U5_gga(T501, T502, T500, T503, T504, T506, f1_out_gga(.(T503, .(T500, .(T501, T502))), T504, T506)) → f1_out_gga(.(T501, T502), .(T500, .(T503, T504)), T506)

The argument filtering Pi contains the following mapping:
f1_in_gga(x1, x2, x3)  =  f1_in_gga(x1, x2)
[]  =  []
f1_out_gga(x1, x2, x3)  =  f1_out_gga(x3)
.(x1, x2)  =  .(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
g13_in_gga(x1, x2, x3)  =  g13_in_gga(x1, x2)
g13_out_gga(x1, x2, x3)  =  g13_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_gga(x11)
g71_in_ggga(x1, x2, x3, x4)  =  g71_in_ggga(x1, x2, x3)
g71_out_ggga(x1, x2, x3, x4)  =  g71_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6)  =  U1_ggga(x6)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x5)
U5_gga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gga(x7)
F1_IN_GGA(x1, x2, x3)  =  F1_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
G13_IN_GGA(x1, x2, x3)  =  G13_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_GGA(x11)
G71_IN_GGGA(x1, x2, x3, x4)  =  G71_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5, x6)  =  U1_GGGA(x6)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x5)
U5_GGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GGA(x7)

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

(6) Obligation:

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

F1_IN_GGA(.(T21, T22), [], T24) → U3_GGA(T21, T22, T24, g13_in_gga(T22, T21, T24))
F1_IN_GGA(.(T21, T22), [], T24) → G13_IN_GGA(T22, T21, T24)
G13_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_GGA(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
G13_IN_GGA(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → G71_IN_GGGA(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)
G71_IN_GGGA(.(T416, T417), T418, T419, T421) → U1_GGGA(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
G71_IN_GGGA(.(T416, T417), T418, T419, T421) → G71_IN_GGGA(T417, T416, .(T418, T419), T421)
F1_IN_GGA(.(T480, T481), .(T479, []), T483) → U4_GGA(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
F1_IN_GGA(.(T480, T481), .(T479, []), T483) → G13_IN_GGA(.(T480, T481), T479, T483)
F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_GGA(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504)), T506) → F1_IN_GGA(.(T503, .(T500, .(T501, T502))), T504, T506)

The TRS R consists of the following rules:

f1_in_gga([], [], []) → f1_out_gga([], [], [])
f1_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, g13_in_gga(T22, T21, T24))
g13_in_gga([], T31, .(T31, [])) → g13_out_gga([], T31, .(T31, []))
g13_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → g13_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
g13_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → g13_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
g13_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → g13_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
g13_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → g13_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
g13_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → g13_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
g13_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → g13_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
g13_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
g71_in_ggga([], T404, T405, .(T404, T405)) → g71_out_ggga([], T404, T405, .(T404, T405))
g71_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, g71_out_ggga(T417, T416, .(T418, T419), T421)) → g71_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → g13_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, g13_out_gga(T22, T21, T24)) → f1_out_gga(.(T21, T22), [], T24)
f1_in_gga(.(T480, T481), .(T479, []), T483) → U4_gga(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
U4_gga(T480, T481, T479, T483, g13_out_gga(.(T480, T481), T479, T483)) → f1_out_gga(.(T480, T481), .(T479, []), T483)
f1_in_gga(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_gga(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
U5_gga(T501, T502, T500, T503, T504, T506, f1_out_gga(.(T503, .(T500, .(T501, T502))), T504, T506)) → f1_out_gga(.(T501, T502), .(T500, .(T503, T504)), T506)

The argument filtering Pi contains the following mapping:
f1_in_gga(x1, x2, x3)  =  f1_in_gga(x1, x2)
[]  =  []
f1_out_gga(x1, x2, x3)  =  f1_out_gga(x3)
.(x1, x2)  =  .(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
g13_in_gga(x1, x2, x3)  =  g13_in_gga(x1, x2)
g13_out_gga(x1, x2, x3)  =  g13_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_gga(x11)
g71_in_ggga(x1, x2, x3, x4)  =  g71_in_ggga(x1, x2, x3)
g71_out_ggga(x1, x2, x3, x4)  =  g71_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6)  =  U1_ggga(x6)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x5)
U5_gga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gga(x7)
F1_IN_GGA(x1, x2, x3)  =  F1_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
G13_IN_GGA(x1, x2, x3)  =  G13_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_GGA(x11)
G71_IN_GGGA(x1, x2, x3, x4)  =  G71_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5, x6)  =  U1_GGGA(x6)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x5)
U5_GGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GGA(x7)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

G71_IN_GGGA(.(T416, T417), T418, T419, T421) → G71_IN_GGGA(T417, T416, .(T418, T419), T421)

The TRS R consists of the following rules:

f1_in_gga([], [], []) → f1_out_gga([], [], [])
f1_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, g13_in_gga(T22, T21, T24))
g13_in_gga([], T31, .(T31, [])) → g13_out_gga([], T31, .(T31, []))
g13_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → g13_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
g13_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → g13_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
g13_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → g13_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
g13_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → g13_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
g13_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → g13_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
g13_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → g13_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
g13_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
g71_in_ggga([], T404, T405, .(T404, T405)) → g71_out_ggga([], T404, T405, .(T404, T405))
g71_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, g71_out_ggga(T417, T416, .(T418, T419), T421)) → g71_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → g13_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, g13_out_gga(T22, T21, T24)) → f1_out_gga(.(T21, T22), [], T24)
f1_in_gga(.(T480, T481), .(T479, []), T483) → U4_gga(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
U4_gga(T480, T481, T479, T483, g13_out_gga(.(T480, T481), T479, T483)) → f1_out_gga(.(T480, T481), .(T479, []), T483)
f1_in_gga(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_gga(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
U5_gga(T501, T502, T500, T503, T504, T506, f1_out_gga(.(T503, .(T500, .(T501, T502))), T504, T506)) → f1_out_gga(.(T501, T502), .(T500, .(T503, T504)), T506)

The argument filtering Pi contains the following mapping:
f1_in_gga(x1, x2, x3)  =  f1_in_gga(x1, x2)
[]  =  []
f1_out_gga(x1, x2, x3)  =  f1_out_gga(x3)
.(x1, x2)  =  .(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
g13_in_gga(x1, x2, x3)  =  g13_in_gga(x1, x2)
g13_out_gga(x1, x2, x3)  =  g13_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_gga(x11)
g71_in_ggga(x1, x2, x3, x4)  =  g71_in_ggga(x1, x2, x3)
g71_out_ggga(x1, x2, x3, x4)  =  g71_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6)  =  U1_ggga(x6)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x5)
U5_gga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gga(x7)
G71_IN_GGGA(x1, x2, x3, x4)  =  G71_IN_GGGA(x1, x2, x3)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

G71_IN_GGGA(.(T416, T417), T418, T419, T421) → G71_IN_GGGA(T417, T416, .(T418, T419), T421)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

G71_IN_GGGA(.(T416, T417), T418, T419) → G71_IN_GGGA(T417, T416, .(T418, T419))

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

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

  • G71_IN_GGGA(.(T416, T417), T418, T419) → G71_IN_GGGA(T417, T416, .(T418, T419))
    The graph contains the following edges 1 > 1, 1 > 2

(15) YES

(16) Obligation:

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

F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504)), T506) → F1_IN_GGA(.(T503, .(T500, .(T501, T502))), T504, T506)

The TRS R consists of the following rules:

f1_in_gga([], [], []) → f1_out_gga([], [], [])
f1_in_gga(.(T21, T22), [], T24) → U3_gga(T21, T22, T24, g13_in_gga(T22, T21, T24))
g13_in_gga([], T31, .(T31, [])) → g13_out_gga([], T31, .(T31, []))
g13_in_gga(.(T57, []), T58, .(T57, .(T58, []))) → g13_out_gga(.(T57, []), T58, .(T57, .(T58, [])))
g13_in_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, [])))) → g13_out_gga(.(T94, .(T93, [])), T95, .(T93, .(T94, .(T95, []))))
g13_in_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, []))))) → g13_out_gga(.(T141, .(T140, .(T139, []))), T142, .(T139, .(T140, .(T141, .(T142, [])))))
g13_in_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, [])))))) → g13_out_gga(.(T198, .(T197, .(T196, .(T195, [])))), T199, .(T195, .(T196, .(T197, .(T198, .(T199, []))))))
g13_in_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, []))))))) → g13_out_gga(.(T265, .(T264, .(T263, .(T262, .(T261, []))))), T266, .(T261, .(T262, .(T263, .(T264, .(T265, .(T266, [])))))))
g13_in_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, [])))))))) → g13_out_gga(.(T342, .(T341, .(T340, .(T339, .(T338, .(T337, [])))))), T343, .(T337, .(T338, .(T339, .(T340, .(T341, .(T342, .(T343, []))))))))
g13_in_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374) → U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_in_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374))
g71_in_ggga([], T404, T405, .(T404, T405)) → g71_out_ggga([], T404, T405, .(T404, T405))
g71_in_ggga(.(T416, T417), T418, T419, T421) → U1_ggga(T416, T417, T418, T419, T421, g71_in_ggga(T417, T416, .(T418, T419), T421))
U1_ggga(T416, T417, T418, T419, T421, g71_out_ggga(T417, T416, .(T418, T419), T421)) → g71_out_ggga(.(T416, T417), T418, T419, T421)
U2_gga(T371, T370, T369, T368, T367, T366, T364, T365, T372, T374, g71_out_ggga(T365, T364, .(T366, .(T367, .(T368, .(T369, .(T370, .(T371, .(T372, []))))))), T374)) → g13_out_gga(.(T371, .(T370, .(T369, .(T368, .(T367, .(T366, .(T364, T365))))))), T372, T374)
U3_gga(T21, T22, T24, g13_out_gga(T22, T21, T24)) → f1_out_gga(.(T21, T22), [], T24)
f1_in_gga(.(T480, T481), .(T479, []), T483) → U4_gga(T480, T481, T479, T483, g13_in_gga(.(T480, T481), T479, T483))
U4_gga(T480, T481, T479, T483, g13_out_gga(.(T480, T481), T479, T483)) → f1_out_gga(.(T480, T481), .(T479, []), T483)
f1_in_gga(.(T501, T502), .(T500, .(T503, T504)), T506) → U5_gga(T501, T502, T500, T503, T504, T506, f1_in_gga(.(T503, .(T500, .(T501, T502))), T504, T506))
U5_gga(T501, T502, T500, T503, T504, T506, f1_out_gga(.(T503, .(T500, .(T501, T502))), T504, T506)) → f1_out_gga(.(T501, T502), .(T500, .(T503, T504)), T506)

The argument filtering Pi contains the following mapping:
f1_in_gga(x1, x2, x3)  =  f1_in_gga(x1, x2)
[]  =  []
f1_out_gga(x1, x2, x3)  =  f1_out_gga(x3)
.(x1, x2)  =  .(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
g13_in_gga(x1, x2, x3)  =  g13_in_gga(x1, x2)
g13_out_gga(x1, x2, x3)  =  g13_out_gga(x3)
U2_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U2_gga(x11)
g71_in_ggga(x1, x2, x3, x4)  =  g71_in_ggga(x1, x2, x3)
g71_out_ggga(x1, x2, x3, x4)  =  g71_out_ggga(x4)
U1_ggga(x1, x2, x3, x4, x5, x6)  =  U1_ggga(x6)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x5)
U5_gga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gga(x7)
F1_IN_GGA(x1, x2, x3)  =  F1_IN_GGA(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504)), T506) → F1_IN_GGA(.(T503, .(T500, .(T501, T502))), T504, T506)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504))) → F1_IN_GGA(.(T503, .(T500, .(T501, T502))), T504)

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

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

  • F1_IN_GGA(.(T501, T502), .(T500, .(T503, T504))) → F1_IN_GGA(.(T503, .(T500, .(T501, T502))), T504)
    The graph contains the following edges 2 > 2

(22) YES