(0) Obligation:
Clauses:
gopher(nil, nil).
gopher(cons(nil, Y), cons(nil, Y)).
gopher(cons(cons(U, V), W), X) :- gopher(cons(U, cons(V, W)), X).
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(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
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)
cons(
x1,
x2) =
cons(
x1,
x2)
U1_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_ga(
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:
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → U1_GA(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
The TRS R consists of the following rules:
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
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)
cons(
x1,
x2) =
cons(
x1,
x2)
U1_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_ga(
x1,
x2,
x3,
x4,
x6)
GOPHERA_IN_GA(
x1,
x2) =
GOPHERA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_GA(
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:
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → U1_GA(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
The TRS R consists of the following rules:
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
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)
cons(
x1,
x2) =
cons(
x1,
x2)
U1_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_ga(
x1,
x2,
x3,
x4,
x6)
GOPHERA_IN_GA(
x1,
x2) =
GOPHERA_IN_GA(
x1)
U1_GA(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_GA(
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 1 less node.
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
The TRS R consists of the following rules:
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
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)
cons(
x1,
x2) =
cons(
x1,
x2)
U1_ga(
x1,
x2,
x3,
x4,
x5,
x6) =
U1_ga(
x1,
x2,
x3,
x4,
x6)
GOPHERA_IN_GA(
x1,
x2) =
GOPHERA_IN_GA(
x1)
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:
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
R is empty.
The argument filtering Pi contains the following mapping:
cons(
x1,
x2) =
cons(
x1,
x2)
GOPHERA_IN_GA(
x1,
x2) =
GOPHERA_IN_GA(
x1)
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:
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37)) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))))
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(11) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37)) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))))
Used ordering: Knuth-Bendix order [KBO] with precedence:
cons2 > GOPHERAINGA1
and weight map:
GOPHERA_IN_GA_1=1
cons_2=0
The variable weight is 1
(12) Obligation:
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(13) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(14) YES