Left Termination proof of /tmp/tmpCJy5Jf/overlap1.pl

Left Termination of the query pattern overlap_in_2(g, g) w.r.t. the given Prolog program could not be shown:

0 Prolog

↳1 CutEliminatorProof (⇐)

↳2 Prolog

  ↳3 PrologToPiTRSProof (⇐)

    ↳4 PiTRS

    ↳5 DependencyPairsProof (⇔)

    ↳6 PiDP

    ↳7 DependencyGraphProof (⇔)

    ↳8 PiDP

    ↳9 UsableRulesProof (⇔)

    ↳10 PiDP

    ↳11 PiDPToQDPProof (⇐)

    ↳12 QDP

    ↳13 UsableRulesReductionPairsProof (⇔)

    ↳14 QDP

    ↳15 Narrowing (⇐)

    ↳16 QDP

    ↳17 UsableRulesProof (⇔)

    ↳18 QDP

    ↳19 QReductionProof (⇔)

    ↳20 QDP

    ↳21 Instantiation (⇔)

    ↳22 QDP

    ↳23 NonTerminationProof (⇔)

    ↳24 FALSE

  ↳25 PrologToPiTRSProof (⇐)

    ↳26 PiTRS

    ↳27 DependencyPairsProof (⇔)

    ↳28 PiDP

    ↳29 DependencyGraphProof (⇔)

    ↳30 PiDP

    ↳31 UsableRulesProof (⇔)

    ↳32 PiDP

    ↳33 PiDPToQDPProof (⇐)

    ↳34 QDP

    ↳35 Narrowing (⇐)

    ↳36 QDP

    ↳37 UsableRulesProof (⇔)

    ↳38 QDP

    ↳39 QReductionProof (⇔)

    ↳40 QDP

      ↳41 QDPOrderProof (⇔)

        ↳42 QDP

          ↳43 Instantiation (⇔)

            ↳44 QDP

          ↳45 Instantiation (⇔)

            ↳46 QDP

            ↳47 NonTerminationProof (⇔)

            ↳48 FALSE

      ↳49 QDPOrderProof (⇔)

        ↳50 QDP

(0) Obligation:

Clauses:

overlap(Xs, Ys) :- ','(member(X, Xs), member(X, Ys)).
member(X1, []) :- ','(!, failure(a)).
member(X, Y) :- head(Y, X).
member(X, Y) :- ','(tail(Y, T), member(X, T)).
head([], X2).
head(.(H, X3), H).
tail([], []).
tail(.(X4, T), T).
failure(b).

Queries:

overlap(g,g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

overlap(Xs, Ys) :- ','(member(X, Xs), member(X, Ys)).
member(X1, []) :- failure(a).
member(X, Y) :- head(Y, X).
member(X, Y) :- ','(tail(Y, T), member(X, T)).
head([], X2).
head(.(H, X3), H).
tail([], []).
tail(.(X4, T), T).
failure(b).

Queries:

overlap(g,g).

(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:
overlap_in: (b,b)
member_in: (f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

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

OVERLAP_IN_GG(Xs, Ys) → U1_GG(Xs, Ys, member_in_ag(X, Xs))
OVERLAP_IN_GG(Xs, Ys) → MEMBER_IN_AG(X, Xs)
MEMBER_IN_AG(X1, []) → U3_AG(X1, failure_in_g(a))
MEMBER_IN_AG(X1, []) → FAILURE_IN_G(a)
MEMBER_IN_AG(X, Y) → U4_AG(X, Y, head_in_ga(Y, X))
MEMBER_IN_AG(X, Y) → HEAD_IN_GA(Y, X)
MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
MEMBER_IN_AG(X, Y) → TAIL_IN_GA(Y, T)
U5_AG(X, Y, tail_out_ga(Y, T)) → U6_AG(X, Y, member_in_ag(X, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → U2_GG(Xs, Ys, member_in_ag(X, Ys))
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → MEMBER_IN_AG(X, Ys)

The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

The argument filtering Pi contains the following mapping:
overlap_in_gg(x1, x2) = overlap_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x2, x3)
member_in_ag(x1, x2) = member_in_ag(x2)
[] = []
U3_ag(x1, x2) = U3_ag(x2)
failure_in_g(x1) = failure_in_g(x1)
b = b
failure_out_g(x1) = failure_out_g
a = a
member_out_ag(x1, x2) = member_out_ag
U4_ag(x1, x2, x3) = U4_ag(x3)
head_in_ga(x1, x2) = head_in_ga(x1)
head_out_ga(x1, x2) = head_out_ga
.(x1, x2) = .(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x3)
tail_in_ga(x1, x2) = tail_in_ga(x1)
tail_out_ga(x1, x2) = tail_out_ga(x2)
U6_ag(x1, x2, x3) = U6_ag(x3)
U2_gg(x1, x2, x3) = U2_gg(x3)
overlap_out_gg(x1, x2) = overlap_out_gg
OVERLAP_IN_GG(x1, x2) = OVERLAP_IN_GG(x1, x2)
U1_GG(x1, x2, x3) = U1_GG(x2, x3)
MEMBER_IN_AG(x1, x2) = MEMBER_IN_AG(x2)
U3_AG(x1, x2) = U3_AG(x2)
FAILURE_IN_G(x1) = FAILURE_IN_G(x1)
U4_AG(x1, x2, x3) = U4_AG(x3)
HEAD_IN_GA(x1, x2) = HEAD_IN_GA(x1)
U5_AG(x1, x2, x3) = U5_AG(x3)
TAIL_IN_GA(x1, x2) = TAIL_IN_GA(x1)
U6_AG(x1, x2, x3) = U6_AG(x3)
U2_GG(x1, x2, x3) = U2_GG(x3)

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

(6) Obligation:

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

OVERLAP_IN_GG(Xs, Ys) → U1_GG(Xs, Ys, member_in_ag(X, Xs))
OVERLAP_IN_GG(Xs, Ys) → MEMBER_IN_AG(X, Xs)
MEMBER_IN_AG(X1, []) → U3_AG(X1, failure_in_g(a))
MEMBER_IN_AG(X1, []) → FAILURE_IN_G(a)
MEMBER_IN_AG(X, Y) → U4_AG(X, Y, head_in_ga(Y, X))
MEMBER_IN_AG(X, Y) → HEAD_IN_GA(Y, X)
MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
MEMBER_IN_AG(X, Y) → TAIL_IN_GA(Y, T)
U5_AG(X, Y, tail_out_ga(Y, T)) → U6_AG(X, Y, member_in_ag(X, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → U2_GG(Xs, Ys, member_in_ag(X, Ys))
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → MEMBER_IN_AG(X, Ys)

The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)

The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

The argument filtering Pi contains the following mapping:
overlap_in_gg(x1, x2) = overlap_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x2, x3)
member_in_ag(x1, x2) = member_in_ag(x2)
[] = []
U3_ag(x1, x2) = U3_ag(x2)
failure_in_g(x1) = failure_in_g(x1)
b = b
failure_out_g(x1) = failure_out_g
a = a
member_out_ag(x1, x2) = member_out_ag
U4_ag(x1, x2, x3) = U4_ag(x3)
head_in_ga(x1, x2) = head_in_ga(x1)
head_out_ga(x1, x2) = head_out_ga
.(x1, x2) = .(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x3)
tail_in_ga(x1, x2) = tail_in_ga(x1)
tail_out_ga(x1, x2) = tail_out_ga(x2)
U6_ag(x1, x2, x3) = U6_ag(x3)
U2_gg(x1, x2, x3) = U2_gg(x3)
overlap_out_gg(x1, x2) = overlap_out_gg
MEMBER_IN_AG(x1, x2) = MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3) = U5_AG(x3)

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

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)

The TRS R consists of the following rules:

tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
tail_in_ga(x1, x2) = tail_in_ga(x1)
tail_out_ga(x1, x2) = tail_out_ga(x2)
MEMBER_IN_AG(x1, x2) = MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3) = U5_AG(x3)

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

MEMBER_IN_AG(Y) → U5_AG(tail_in_ga(Y))
U5_AG(tail_out_ga(T)) → MEMBER_IN_AG(T)

The TRS R consists of the following rules:

tail_in_ga([]) → tail_out_ga([])
tail_in_ga(.(X4, T)) → tail_out_ga(T)

The set Q consists of the following terms:

tail_in_ga(x0)

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

(13) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

tail_in_ga(.(X4, T)) → tail_out_ga(T)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + 2·x₂
POL(MEMBER_IN_AG(x₁)) = x₁
POL(U5_AG(x₁)) = x₁
POL([]) = 0
POL(tail_in_ga(x₁)) = x₁
POL(tail_out_ga(x₁)) = 2·x₁

(14) Obligation:

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

MEMBER_IN_AG(Y) → U5_AG(tail_in_ga(Y))
U5_AG(tail_out_ga(T)) → MEMBER_IN_AG(T)

The TRS R consists of the following rules:

tail_in_ga([]) → tail_out_ga([])

The set Q consists of the following terms:

tail_in_ga(x0)

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

(15) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule MEMBER_IN_AG(Y) → U5_AG(tail_in_ga(Y)) at position [0] we obtained the following new rules [LPAR04]:

MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))

(16) Obligation:

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

U5_AG(tail_out_ga(T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))

The TRS R consists of the following rules:

tail_in_ga([]) → tail_out_ga([])

The set Q consists of the following terms:

tail_in_ga(x0)

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

(17) 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.

(18) Obligation:

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

U5_AG(tail_out_ga(T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))

R is empty.
The set Q consists of the following terms:

tail_in_ga(x0)

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

(19) 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].

tail_in_ga(x0)

(20) Obligation:

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

U5_AG(tail_out_ga(T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))

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

(21) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AG(tail_out_ga(T)) → MEMBER_IN_AG(T) we obtained the following new rules [LPAR04]:

U5_AG(tail_out_ga([])) → MEMBER_IN_AG([])

(22) Obligation:

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

MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))
U5_AG(tail_out_ga([])) → MEMBER_IN_AG([])

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

(23) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U5_AG(tail_out_ga([])) evaluates to t =U5_AG(tail_out_ga([]))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U5_AG(tail_out_ga([])) → MEMBER_IN_AG([])
with rule U5_AG(tail_out_ga([])) → MEMBER_IN_AG([]) at position [] and matcher [ ]

MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))
with rule MEMBER_IN_AG([]) → U5_AG(tail_out_ga([]))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(24) FALSE

(25) PrologToPiTRSProof (SOUND transformation)

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(26) Obligation:

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

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

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

OVERLAP_IN_GG(Xs, Ys) → U1_GG(Xs, Ys, member_in_ag(X, Xs))
OVERLAP_IN_GG(Xs, Ys) → MEMBER_IN_AG(X, Xs)
MEMBER_IN_AG(X1, []) → U3_AG(X1, failure_in_g(a))
MEMBER_IN_AG(X1, []) → FAILURE_IN_G(a)
MEMBER_IN_AG(X, Y) → U4_AG(X, Y, head_in_ga(Y, X))
MEMBER_IN_AG(X, Y) → HEAD_IN_GA(Y, X)
MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
MEMBER_IN_AG(X, Y) → TAIL_IN_GA(Y, T)
U5_AG(X, Y, tail_out_ga(Y, T)) → U6_AG(X, Y, member_in_ag(X, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → U2_GG(Xs, Ys, member_in_ag(X, Ys))
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → MEMBER_IN_AG(X, Ys)

The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

The argument filtering Pi contains the following mapping:
overlap_in_gg(x1, x2) = overlap_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
member_in_ag(x1, x2) = member_in_ag(x2)
[] = []
U3_ag(x1, x2) = U3_ag(x2)
failure_in_g(x1) = failure_in_g(x1)
b = b
failure_out_g(x1) = failure_out_g(x1)
a = a
member_out_ag(x1, x2) = member_out_ag(x2)
U4_ag(x1, x2, x3) = U4_ag(x2, x3)
head_in_ga(x1, x2) = head_in_ga(x1)
head_out_ga(x1, x2) = head_out_ga(x1)
.(x1, x2) = .(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x2, x3)
tail_in_ga(x1, x2) = tail_in_ga(x1)
tail_out_ga(x1, x2) = tail_out_ga(x1, x2)
U6_ag(x1, x2, x3) = U6_ag(x2, x3)
U2_gg(x1, x2, x3) = U2_gg(x1, x2, x3)
overlap_out_gg(x1, x2) = overlap_out_gg(x1, x2)
OVERLAP_IN_GG(x1, x2) = OVERLAP_IN_GG(x1, x2)
U1_GG(x1, x2, x3) = U1_GG(x1, x2, x3)
MEMBER_IN_AG(x1, x2) = MEMBER_IN_AG(x2)
U3_AG(x1, x2) = U3_AG(x2)
FAILURE_IN_G(x1) = FAILURE_IN_G(x1)
U4_AG(x1, x2, x3) = U4_AG(x2, x3)
HEAD_IN_GA(x1, x2) = HEAD_IN_GA(x1)
U5_AG(x1, x2, x3) = U5_AG(x2, x3)
TAIL_IN_GA(x1, x2) = TAIL_IN_GA(x1)
U6_AG(x1, x2, x3) = U6_AG(x2, x3)
U2_GG(x1, x2, x3) = U2_GG(x1, x2, x3)

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

(28) Obligation:

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

OVERLAP_IN_GG(Xs, Ys) → U1_GG(Xs, Ys, member_in_ag(X, Xs))
OVERLAP_IN_GG(Xs, Ys) → MEMBER_IN_AG(X, Xs)
MEMBER_IN_AG(X1, []) → U3_AG(X1, failure_in_g(a))
MEMBER_IN_AG(X1, []) → FAILURE_IN_G(a)
MEMBER_IN_AG(X, Y) → U4_AG(X, Y, head_in_ga(Y, X))
MEMBER_IN_AG(X, Y) → HEAD_IN_GA(Y, X)
MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
MEMBER_IN_AG(X, Y) → TAIL_IN_GA(Y, T)
U5_AG(X, Y, tail_out_ga(Y, T)) → U6_AG(X, Y, member_in_ag(X, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → U2_GG(Xs, Ys, member_in_ag(X, Ys))
U1_GG(Xs, Ys, member_out_ag(X, Xs)) → MEMBER_IN_AG(X, Ys)

The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(30) Obligation:

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

MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)

The TRS R consists of the following rules:

overlap_in_gg(Xs, Ys) → U1_gg(Xs, Ys, member_in_ag(X, Xs))
member_in_ag(X1, []) → U3_ag(X1, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U3_ag(X1, failure_out_g(a)) → member_out_ag(X1, [])
member_in_ag(X, Y) → U4_ag(X, Y, head_in_ga(Y, X))
head_in_ga([], X2) → head_out_ga([], X2)
head_in_ga(.(H, X3), H) → head_out_ga(.(H, X3), H)
U4_ag(X, Y, head_out_ga(Y, X)) → member_out_ag(X, Y)
member_in_ag(X, Y) → U5_ag(X, Y, tail_in_ga(Y, T))
tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)
U5_ag(X, Y, tail_out_ga(Y, T)) → U6_ag(X, Y, member_in_ag(X, T))
U6_ag(X, Y, member_out_ag(X, T)) → member_out_ag(X, Y)
U1_gg(Xs, Ys, member_out_ag(X, Xs)) → U2_gg(Xs, Ys, member_in_ag(X, Ys))
U2_gg(Xs, Ys, member_out_ag(X, Ys)) → overlap_out_gg(Xs, Ys)

The argument filtering Pi contains the following mapping:
overlap_in_gg(x1, x2) = overlap_in_gg(x1, x2)
U1_gg(x1, x2, x3) = U1_gg(x1, x2, x3)
member_in_ag(x1, x2) = member_in_ag(x2)
[] = []
U3_ag(x1, x2) = U3_ag(x2)
failure_in_g(x1) = failure_in_g(x1)
b = b
failure_out_g(x1) = failure_out_g(x1)
a = a
member_out_ag(x1, x2) = member_out_ag(x2)
U4_ag(x1, x2, x3) = U4_ag(x2, x3)
head_in_ga(x1, x2) = head_in_ga(x1)
head_out_ga(x1, x2) = head_out_ga(x1)
.(x1, x2) = .(x1, x2)
U5_ag(x1, x2, x3) = U5_ag(x2, x3)
tail_in_ga(x1, x2) = tail_in_ga(x1)
tail_out_ga(x1, x2) = tail_out_ga(x1, x2)
U6_ag(x1, x2, x3) = U6_ag(x2, x3)
U2_gg(x1, x2, x3) = U2_gg(x1, x2, x3)
overlap_out_gg(x1, x2) = overlap_out_gg(x1, x2)
MEMBER_IN_AG(x1, x2) = MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3) = U5_AG(x2, x3)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

MEMBER_IN_AG(X, Y) → U5_AG(X, Y, tail_in_ga(Y, T))
U5_AG(X, Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(X, T)

The TRS R consists of the following rules:

tail_in_ga([], []) → tail_out_ga([], [])
tail_in_ga(.(X4, T), T) → tail_out_ga(.(X4, T), T)

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
tail_in_ga(x1, x2) = tail_in_ga(x1)
tail_out_ga(x1, x2) = tail_out_ga(x1, x2)
MEMBER_IN_AG(x1, x2) = MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3) = U5_AG(x2, x3)

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

MEMBER_IN_AG(Y) → U5_AG(Y, tail_in_ga(Y))
U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T)

The TRS R consists of the following rules:

tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, T)) → tail_out_ga(.(X4, T), T)

The set Q consists of the following terms:

tail_in_ga(x0)

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

(35) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule MEMBER_IN_AG(Y) → U5_AG(Y, tail_in_ga(Y)) at position [1] we obtained the following new rules [LPAR04]:

MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
MEMBER_IN_AG(.(x0, x1)) → U5_AG(.(x0, x1), tail_out_ga(.(x0, x1), x1))

(36) Obligation:

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

U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
MEMBER_IN_AG(.(x0, x1)) → U5_AG(.(x0, x1), tail_out_ga(.(x0, x1), x1))

The TRS R consists of the following rules:

tail_in_ga([]) → tail_out_ga([], [])
tail_in_ga(.(X4, T)) → tail_out_ga(.(X4, T), T)

The set Q consists of the following terms:

tail_in_ga(x0)

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

(37) 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.

(38) Obligation:

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

U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
MEMBER_IN_AG(.(x0, x1)) → U5_AG(.(x0, x1), tail_out_ga(.(x0, x1), x1))

R is empty.
The set Q consists of the following terms:

tail_in_ga(x0)

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

(39) 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].

tail_in_ga(x0)

(40) Obligation:

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

U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
MEMBER_IN_AG(.(x0, x1)) → U5_AG(.(x0, x1), tail_out_ga(.(x0, x1), x1))

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

(41) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MEMBER_IN_AG(.(x0, x1)) → U5_AG(.(x0, x1), tail_out_ga(.(x0, x1), x1))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U5_AG(x₁, x₂)) = 0 +
[ 0, 0 ]

· x₁ +
[ 1, 0 ]

· x₂

POL(tail_out_ga(x₁, x₂)) =
/ 0 \

\ 0 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 1 \

\ 0 0 /

· x₂

POL(MEMBER_IN_AG(x₁)) = 0 +
[ 0, 1 ]

· x₁

POL([]) =
/ 0 \

\ 0 /

POL(.(x₁, x₂)) =
/ 0 \

\ 1 /

+
/ 0 0 \

\ 0 0 /

· x₁ +
/ 0 0 \

\ 0 1 /

· x₂

The following usable rules [FROCOS05] were oriented: none

(42) Obligation:

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

U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))

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

(43) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T) we obtained the following new rules [LPAR04]:

U5_AG([], tail_out_ga([], [])) → MEMBER_IN_AG([])

(44) Obligation:

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

MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
U5_AG([], tail_out_ga([], [])) → MEMBER_IN_AG([])

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

(45) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T) we obtained the following new rules [LPAR04]:

U5_AG([], tail_out_ga([], [])) → MEMBER_IN_AG([])

(46) Obligation:

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

MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
U5_AG([], tail_out_ga([], [])) → MEMBER_IN_AG([])

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

(47) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U5_AG([], tail_out_ga([], [])) evaluates to t =U5_AG([], tail_out_ga([], []))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U5_AG([], tail_out_ga([], [])) → MEMBER_IN_AG([])
with rule U5_AG([], tail_out_ga([], [])) → MEMBER_IN_AG([]) at position [] and matcher [ ]

MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))
with rule MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

(48) FALSE

(49) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MEMBER_IN_AG(.(x0, x1)) → U5_AG(.(x0, x1), tail_out_ga(.(x0, x1), x1))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(MEMBER_IN_AG(x₁)) = x₁
POL(U5_AG(x₁, x₂)) = x₂
POL([]) = 0
POL(tail_out_ga(x₁, x₂)) = x₂

The following usable rules [FROCOS05] were oriented: none

(50) Obligation:

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

U5_AG(Y, tail_out_ga(Y, T)) → MEMBER_IN_AG(T)
MEMBER_IN_AG([]) → U5_AG([], tail_out_ga([], []))

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