(0) Obligation:

Clauses:

gopher(nil, nil).
gopher(X, cons(nil, T)) :- ','(no(empty(X)), ','(head(X, nil), tail(X, T))).
gopher(X, Y) :- ','(no(empty(X)), ','(head(X, H), ','(no(empty(H)), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

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

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2)  =  gopherA_in_ga(x1)
nil  =  nil
gopherA_out_ga(x1, x2)  =  gopherA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
cons(x1, x2)  =  cons(x1, x2)

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

GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → U1_GA(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → GOPHERA_IN_GA(cons(T85, cons(T86, T87)), T48)
GOPHERA_IN_GA(.(.(T129, T130), T131), T92) → U2_GA(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))

The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2)  =  gopherA_in_ga(x1)
nil  =  nil
gopherA_out_ga(x1, x2)  =  gopherA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
cons(x1, x2)  =  cons(x1, x2)
GOPHERA_IN_GA(x1, x2)  =  GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)

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

(4) Obligation:

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

GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → U1_GA(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → GOPHERA_IN_GA(cons(T85, cons(T86, T87)), T48)
GOPHERA_IN_GA(.(.(T129, T130), T131), T92) → U2_GA(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))

The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2)  =  gopherA_in_ga(x1)
nil  =  nil
gopherA_out_ga(x1, x2)  =  gopherA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
cons(x1, x2)  =  cons(x1, x2)
GOPHERA_IN_GA(x1, x2)  =  GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 3 less nodes.

(6) TRUE