(0) Obligation:

Clauses:

shuffle(A, [], A) :- !.
shuffle([], B, B) :- !.
shuffle(.(A, RestA), B, .(A, Shuffled)) :- shuffle(RestA, B, Shuffled).
shuffle(A, .(B, RestB), .(B, Shuffled)) :- shuffle(A, RestB, Shuffled).

Query: shuffle(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

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

shuffleA_in_gga(T5, [], T5) → shuffleA_out_gga(T5, [], T5)
shuffleA_in_gga([], T7, T7) → shuffleA_out_gga([], T7, T7)
shuffleA_in_gga(.(T12, T19), [], .(T12, T19)) → shuffleA_out_gga(.(T12, T19), [], .(T12, T19))
shuffleA_in_gga(.(T12, []), T24, .(T12, T24)) → shuffleA_out_gga(.(T12, []), T24, .(T12, T24))
shuffleA_in_gga(.(T33, []), .(T34, T35), .(T34, T37)) → U1_gga(T33, T34, T35, T37, shuffleA_in_gga(.(T33, []), T35, T37))
shuffleA_in_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → U2_gga(T12, T55, T56, T57, T59, shuffleA_in_gga(T56, T57, T59))
shuffleA_in_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → U3_gga(T12, T77, T78, T79, T81, shuffleA_in_gga(T77, T79, T81))
shuffleA_in_gga(.(T93, T94), .(T95, T96), .(T95, T98)) → U4_gga(T93, T94, T95, T96, T98, shuffleA_in_gga(.(T93, T94), T96, T98))
shuffleA_in_gga(T112, .(T106, []), .(T106, T112)) → shuffleA_out_gga(T112, .(T106, []), .(T106, T112))
shuffleA_in_gga([], .(T106, T115), .(T106, T115)) → shuffleA_out_gga([], .(T106, T115), .(T106, T115))
shuffleA_in_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → U5_gga(T132, T133, T106, T134, T136, shuffleA_in_gga(T133, T134, T136))
shuffleA_in_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → U6_gga(T146, T106, T147, T148, T150, shuffleA_in_gga(T146, T148, T150))
U6_gga(T146, T106, T147, T148, T150, shuffleA_out_gga(T146, T148, T150)) → shuffleA_out_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150)))
U5_gga(T132, T133, T106, T134, T136, shuffleA_out_gga(T133, T134, T136)) → shuffleA_out_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136)))
U4_gga(T93, T94, T95, T96, T98, shuffleA_out_gga(.(T93, T94), T96, T98)) → shuffleA_out_gga(.(T93, T94), .(T95, T96), .(T95, T98))
U3_gga(T12, T77, T78, T79, T81, shuffleA_out_gga(T77, T79, T81)) → shuffleA_out_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81)))
U2_gga(T12, T55, T56, T57, T59, shuffleA_out_gga(T56, T57, T59)) → shuffleA_out_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59)))
U1_gga(T33, T34, T35, T37, shuffleA_out_gga(.(T33, []), T35, T37)) → shuffleA_out_gga(.(T33, []), .(T34, T35), .(T34, T37))

The argument filtering Pi contains the following mapping:
shuffleA_in_gga(x1, x2, x3)  =  shuffleA_in_gga(x1, x2)
[]  =  []
shuffleA_out_gga(x1, x2, x3)  =  shuffleA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5, x6)  =  U2_gga(x1, x2, x3, x4, x6)
U3_gga(x1, x2, x3, x4, x5, x6)  =  U3_gga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35), .(T34, T37)) → U1_GGA(T33, T34, T35, T37, shuffleA_in_gga(.(T33, []), T35, T37))
SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35), .(T34, T37)) → SHUFFLEA_IN_GGA(.(T33, []), T35, T37)
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → U2_GGA(T12, T55, T56, T57, T59, shuffleA_in_gga(T56, T57, T59))
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → SHUFFLEA_IN_GGA(T56, T57, T59)
SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → U3_GGA(T12, T77, T78, T79, T81, shuffleA_in_gga(T77, T79, T81))
SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → SHUFFLEA_IN_GGA(T77, T79, T81)
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96), .(T95, T98)) → U4_GGA(T93, T94, T95, T96, T98, shuffleA_in_gga(.(T93, T94), T96, T98))
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96), .(T95, T98)) → SHUFFLEA_IN_GGA(.(T93, T94), T96, T98)
SHUFFLEA_IN_GGA(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → U5_GGA(T132, T133, T106, T134, T136, shuffleA_in_gga(T133, T134, T136))
SHUFFLEA_IN_GGA(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → SHUFFLEA_IN_GGA(T133, T134, T136)
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → U6_GGA(T146, T106, T147, T148, T150, shuffleA_in_gga(T146, T148, T150))
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → SHUFFLEA_IN_GGA(T146, T148, T150)

The TRS R consists of the following rules:

shuffleA_in_gga(T5, [], T5) → shuffleA_out_gga(T5, [], T5)
shuffleA_in_gga([], T7, T7) → shuffleA_out_gga([], T7, T7)
shuffleA_in_gga(.(T12, T19), [], .(T12, T19)) → shuffleA_out_gga(.(T12, T19), [], .(T12, T19))
shuffleA_in_gga(.(T12, []), T24, .(T12, T24)) → shuffleA_out_gga(.(T12, []), T24, .(T12, T24))
shuffleA_in_gga(.(T33, []), .(T34, T35), .(T34, T37)) → U1_gga(T33, T34, T35, T37, shuffleA_in_gga(.(T33, []), T35, T37))
shuffleA_in_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → U2_gga(T12, T55, T56, T57, T59, shuffleA_in_gga(T56, T57, T59))
shuffleA_in_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → U3_gga(T12, T77, T78, T79, T81, shuffleA_in_gga(T77, T79, T81))
shuffleA_in_gga(.(T93, T94), .(T95, T96), .(T95, T98)) → U4_gga(T93, T94, T95, T96, T98, shuffleA_in_gga(.(T93, T94), T96, T98))
shuffleA_in_gga(T112, .(T106, []), .(T106, T112)) → shuffleA_out_gga(T112, .(T106, []), .(T106, T112))
shuffleA_in_gga([], .(T106, T115), .(T106, T115)) → shuffleA_out_gga([], .(T106, T115), .(T106, T115))
shuffleA_in_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → U5_gga(T132, T133, T106, T134, T136, shuffleA_in_gga(T133, T134, T136))
shuffleA_in_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → U6_gga(T146, T106, T147, T148, T150, shuffleA_in_gga(T146, T148, T150))
U6_gga(T146, T106, T147, T148, T150, shuffleA_out_gga(T146, T148, T150)) → shuffleA_out_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150)))
U5_gga(T132, T133, T106, T134, T136, shuffleA_out_gga(T133, T134, T136)) → shuffleA_out_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136)))
U4_gga(T93, T94, T95, T96, T98, shuffleA_out_gga(.(T93, T94), T96, T98)) → shuffleA_out_gga(.(T93, T94), .(T95, T96), .(T95, T98))
U3_gga(T12, T77, T78, T79, T81, shuffleA_out_gga(T77, T79, T81)) → shuffleA_out_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81)))
U2_gga(T12, T55, T56, T57, T59, shuffleA_out_gga(T56, T57, T59)) → shuffleA_out_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59)))
U1_gga(T33, T34, T35, T37, shuffleA_out_gga(.(T33, []), T35, T37)) → shuffleA_out_gga(.(T33, []), .(T34, T35), .(T34, T37))

The argument filtering Pi contains the following mapping:
shuffleA_in_gga(x1, x2, x3)  =  shuffleA_in_gga(x1, x2)
[]  =  []
shuffleA_out_gga(x1, x2, x3)  =  shuffleA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5, x6)  =  U2_gga(x1, x2, x3, x4, x6)
U3_gga(x1, x2, x3, x4, x5, x6)  =  U3_gga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
SHUFFLEA_IN_GGA(x1, x2, x3)  =  SHUFFLEA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5)  =  U1_GGA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3, x4, x5, x6)  =  U2_GGA(x1, x2, x3, x4, x6)
U3_GGA(x1, x2, x3, x4, x5, x6)  =  U3_GGA(x1, x2, x3, x4, x6)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5, x6)  =  U6_GGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35), .(T34, T37)) → U1_GGA(T33, T34, T35, T37, shuffleA_in_gga(.(T33, []), T35, T37))
SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35), .(T34, T37)) → SHUFFLEA_IN_GGA(.(T33, []), T35, T37)
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → U2_GGA(T12, T55, T56, T57, T59, shuffleA_in_gga(T56, T57, T59))
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → SHUFFLEA_IN_GGA(T56, T57, T59)
SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → U3_GGA(T12, T77, T78, T79, T81, shuffleA_in_gga(T77, T79, T81))
SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → SHUFFLEA_IN_GGA(T77, T79, T81)
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96), .(T95, T98)) → U4_GGA(T93, T94, T95, T96, T98, shuffleA_in_gga(.(T93, T94), T96, T98))
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96), .(T95, T98)) → SHUFFLEA_IN_GGA(.(T93, T94), T96, T98)
SHUFFLEA_IN_GGA(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → U5_GGA(T132, T133, T106, T134, T136, shuffleA_in_gga(T133, T134, T136))
SHUFFLEA_IN_GGA(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → SHUFFLEA_IN_GGA(T133, T134, T136)
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → U6_GGA(T146, T106, T147, T148, T150, shuffleA_in_gga(T146, T148, T150))
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → SHUFFLEA_IN_GGA(T146, T148, T150)

The TRS R consists of the following rules:

shuffleA_in_gga(T5, [], T5) → shuffleA_out_gga(T5, [], T5)
shuffleA_in_gga([], T7, T7) → shuffleA_out_gga([], T7, T7)
shuffleA_in_gga(.(T12, T19), [], .(T12, T19)) → shuffleA_out_gga(.(T12, T19), [], .(T12, T19))
shuffleA_in_gga(.(T12, []), T24, .(T12, T24)) → shuffleA_out_gga(.(T12, []), T24, .(T12, T24))
shuffleA_in_gga(.(T33, []), .(T34, T35), .(T34, T37)) → U1_gga(T33, T34, T35, T37, shuffleA_in_gga(.(T33, []), T35, T37))
shuffleA_in_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → U2_gga(T12, T55, T56, T57, T59, shuffleA_in_gga(T56, T57, T59))
shuffleA_in_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → U3_gga(T12, T77, T78, T79, T81, shuffleA_in_gga(T77, T79, T81))
shuffleA_in_gga(.(T93, T94), .(T95, T96), .(T95, T98)) → U4_gga(T93, T94, T95, T96, T98, shuffleA_in_gga(.(T93, T94), T96, T98))
shuffleA_in_gga(T112, .(T106, []), .(T106, T112)) → shuffleA_out_gga(T112, .(T106, []), .(T106, T112))
shuffleA_in_gga([], .(T106, T115), .(T106, T115)) → shuffleA_out_gga([], .(T106, T115), .(T106, T115))
shuffleA_in_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → U5_gga(T132, T133, T106, T134, T136, shuffleA_in_gga(T133, T134, T136))
shuffleA_in_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → U6_gga(T146, T106, T147, T148, T150, shuffleA_in_gga(T146, T148, T150))
U6_gga(T146, T106, T147, T148, T150, shuffleA_out_gga(T146, T148, T150)) → shuffleA_out_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150)))
U5_gga(T132, T133, T106, T134, T136, shuffleA_out_gga(T133, T134, T136)) → shuffleA_out_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136)))
U4_gga(T93, T94, T95, T96, T98, shuffleA_out_gga(.(T93, T94), T96, T98)) → shuffleA_out_gga(.(T93, T94), .(T95, T96), .(T95, T98))
U3_gga(T12, T77, T78, T79, T81, shuffleA_out_gga(T77, T79, T81)) → shuffleA_out_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81)))
U2_gga(T12, T55, T56, T57, T59, shuffleA_out_gga(T56, T57, T59)) → shuffleA_out_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59)))
U1_gga(T33, T34, T35, T37, shuffleA_out_gga(.(T33, []), T35, T37)) → shuffleA_out_gga(.(T33, []), .(T34, T35), .(T34, T37))

The argument filtering Pi contains the following mapping:
shuffleA_in_gga(x1, x2, x3)  =  shuffleA_in_gga(x1, x2)
[]  =  []
shuffleA_out_gga(x1, x2, x3)  =  shuffleA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5, x6)  =  U2_gga(x1, x2, x3, x4, x6)
U3_gga(x1, x2, x3, x4, x5, x6)  =  U3_gga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
SHUFFLEA_IN_GGA(x1, x2, x3)  =  SHUFFLEA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5)  =  U1_GGA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3, x4, x5, x6)  =  U2_GGA(x1, x2, x3, x4, x6)
U3_GGA(x1, x2, x3, x4, x5, x6)  =  U3_GGA(x1, x2, x3, x4, x6)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5, x6)  =  U6_GGA(x1, x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 6 less nodes.

(6) Obligation:

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

SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → SHUFFLEA_IN_GGA(T77, T79, T81)
SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35), .(T34, T37)) → SHUFFLEA_IN_GGA(.(T33, []), T35, T37)
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96), .(T95, T98)) → SHUFFLEA_IN_GGA(.(T93, T94), T96, T98)
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → SHUFFLEA_IN_GGA(T56, T57, T59)
SHUFFLEA_IN_GGA(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → SHUFFLEA_IN_GGA(T133, T134, T136)
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → SHUFFLEA_IN_GGA(T146, T148, T150)

The TRS R consists of the following rules:

shuffleA_in_gga(T5, [], T5) → shuffleA_out_gga(T5, [], T5)
shuffleA_in_gga([], T7, T7) → shuffleA_out_gga([], T7, T7)
shuffleA_in_gga(.(T12, T19), [], .(T12, T19)) → shuffleA_out_gga(.(T12, T19), [], .(T12, T19))
shuffleA_in_gga(.(T12, []), T24, .(T12, T24)) → shuffleA_out_gga(.(T12, []), T24, .(T12, T24))
shuffleA_in_gga(.(T33, []), .(T34, T35), .(T34, T37)) → U1_gga(T33, T34, T35, T37, shuffleA_in_gga(.(T33, []), T35, T37))
shuffleA_in_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → U2_gga(T12, T55, T56, T57, T59, shuffleA_in_gga(T56, T57, T59))
shuffleA_in_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → U3_gga(T12, T77, T78, T79, T81, shuffleA_in_gga(T77, T79, T81))
shuffleA_in_gga(.(T93, T94), .(T95, T96), .(T95, T98)) → U4_gga(T93, T94, T95, T96, T98, shuffleA_in_gga(.(T93, T94), T96, T98))
shuffleA_in_gga(T112, .(T106, []), .(T106, T112)) → shuffleA_out_gga(T112, .(T106, []), .(T106, T112))
shuffleA_in_gga([], .(T106, T115), .(T106, T115)) → shuffleA_out_gga([], .(T106, T115), .(T106, T115))
shuffleA_in_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → U5_gga(T132, T133, T106, T134, T136, shuffleA_in_gga(T133, T134, T136))
shuffleA_in_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → U6_gga(T146, T106, T147, T148, T150, shuffleA_in_gga(T146, T148, T150))
U6_gga(T146, T106, T147, T148, T150, shuffleA_out_gga(T146, T148, T150)) → shuffleA_out_gga(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150)))
U5_gga(T132, T133, T106, T134, T136, shuffleA_out_gga(T133, T134, T136)) → shuffleA_out_gga(.(T132, T133), .(T106, T134), .(T106, .(T132, T136)))
U4_gga(T93, T94, T95, T96, T98, shuffleA_out_gga(.(T93, T94), T96, T98)) → shuffleA_out_gga(.(T93, T94), .(T95, T96), .(T95, T98))
U3_gga(T12, T77, T78, T79, T81, shuffleA_out_gga(T77, T79, T81)) → shuffleA_out_gga(.(T12, T77), .(T78, T79), .(T12, .(T78, T81)))
U2_gga(T12, T55, T56, T57, T59, shuffleA_out_gga(T56, T57, T59)) → shuffleA_out_gga(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59)))
U1_gga(T33, T34, T35, T37, shuffleA_out_gga(.(T33, []), T35, T37)) → shuffleA_out_gga(.(T33, []), .(T34, T35), .(T34, T37))

The argument filtering Pi contains the following mapping:
shuffleA_in_gga(x1, x2, x3)  =  shuffleA_in_gga(x1, x2)
[]  =  []
shuffleA_out_gga(x1, x2, x3)  =  shuffleA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5, x6)  =  U2_gga(x1, x2, x3, x4, x6)
U3_gga(x1, x2, x3, x4, x5, x6)  =  U3_gga(x1, x2, x3, x4, x6)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
SHUFFLEA_IN_GGA(x1, x2, x3)  =  SHUFFLEA_IN_GGA(x1, x2)

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79), .(T12, .(T78, T81))) → SHUFFLEA_IN_GGA(T77, T79, T81)
SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35), .(T34, T37)) → SHUFFLEA_IN_GGA(.(T33, []), T35, T37)
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96), .(T95, T98)) → SHUFFLEA_IN_GGA(.(T93, T94), T96, T98)
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57, .(T12, .(T55, T59))) → SHUFFLEA_IN_GGA(T56, T57, T59)
SHUFFLEA_IN_GGA(.(T132, T133), .(T106, T134), .(T106, .(T132, T136))) → SHUFFLEA_IN_GGA(T133, T134, T136)
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148)), .(T106, .(T147, T150))) → SHUFFLEA_IN_GGA(T146, T148, T150)

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

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79)) → SHUFFLEA_IN_GGA(T77, T79)
SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35)) → SHUFFLEA_IN_GGA(.(T33, []), T35)
SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96)) → SHUFFLEA_IN_GGA(.(T93, T94), T96)
SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57) → SHUFFLEA_IN_GGA(T56, T57)
SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148))) → SHUFFLEA_IN_GGA(T146, T148)

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

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

  • SHUFFLEA_IN_GGA(.(T12, .(T55, T56)), T57) → SHUFFLEA_IN_GGA(T56, T57)
    The graph contains the following edges 1 > 1, 2 >= 2

  • SHUFFLEA_IN_GGA(.(T33, []), .(T34, T35)) → SHUFFLEA_IN_GGA(.(T33, []), T35)
    The graph contains the following edges 1 >= 1, 2 > 2

  • SHUFFLEA_IN_GGA(.(T12, T77), .(T78, T79)) → SHUFFLEA_IN_GGA(T77, T79)
    The graph contains the following edges 1 > 1, 2 > 2

  • SHUFFLEA_IN_GGA(.(T93, T94), .(T95, T96)) → SHUFFLEA_IN_GGA(.(T93, T94), T96)
    The graph contains the following edges 1 >= 1, 2 > 2

  • SHUFFLEA_IN_GGA(T146, .(T106, .(T147, T148))) → SHUFFLEA_IN_GGA(T146, T148)
    The graph contains the following edges 1 >= 1, 2 > 2

(12) YES