Left Termination of the query pattern star_in_2(g, g) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 BuiltinConflictTransformerProof (⇐)
↳2 Prolog
↳3 PrologToDTProblemTransformerProof (⇐)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇐)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇐)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔)
        ↳15 YES
    ↳16 PiDP
        ↳17 PiDPToQDPProof (⇐)
        ↳18 QDP
        ↳19 QDPOrderProof (⇔)
        ↳20 QDP
        ↳21 DependencyGraphProof (⇔)
        ↳22 TRUE

(0) Obligation:

Clauses:

star(U, []) :- !.
star([], W) :- ','(!, =(W, [])).
star(U, W) :- ','(app(U, V, W), star(U, V)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).
=(X, X).

Queries:

star(g,g).

(1) BuiltinConflictTransformerProof (SOUND transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

star(U, []) :- !.
star([], W) :- ','(!, user_defined_=(W, [])).
star(U, W) :- ','(app(U, V, W), star(U, V)).
app([], L, L).
app(.(X, L), M, .(X, N)) :- app(L, M, N).
user_defined_=(X, X).

Queries:

star(g,g).

(3) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(4) Obligation:

Triples:

app17(.(T38, T39), X67, .(T38, T40)) :- app17(T39, X67, T40).
star1(.(T19, T20), .(T19, T21)) :- app17(T20, X29, T21).
star1(.(T19, T20), .(T19, T21)) :- ','(appc17(T20, T24, T21), star1(.(T19, T20), T24)).

Clauses:

starc1(T4, []).
starc1(.(T19, T20), .(T19, T21)) :- ','(appc17(T20, T24, T21), starc1(.(T19, T20), T24)).
appc17([], T31, T31).
appc17(.(T38, T39), X67, .(T38, T40)) :- appc17(T39, X67, T40).

Afs:

star1(x1, x2)  =  star1(x1, x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
star1_in: (b,b)
app17_in: (b,f,b)
appc17_in: (b,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U2_GG(T19, T20, T21, app17_in_gag(T20, X29, T21))
STAR1_IN_GG(.(T19, T20), .(T19, T21)) → APP17_IN_GAG(T20, X29, T21)
APP17_IN_GAG(.(T38, T39), X67, .(T38, T40)) → U1_GAG(T38, T39, X67, T40, app17_in_gag(T39, X67, T40))
APP17_IN_GAG(.(T38, T39), X67, .(T38, T40)) → APP17_IN_GAG(T39, X67, T40)
STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U3_GG(T19, T20, T21, appc17_in_gag(T20, T24, T21))
U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → U4_GG(T19, T20, T21, star1_in_gg(.(T19, T20), T24))
U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → STAR1_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appc17_in_gag([], T31, T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), X67, .(T38, T40)) → U8_gag(T38, T39, X67, T40, appc17_in_gag(T39, X67, T40))
U8_gag(T38, T39, X67, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

The argument filtering Pi contains the following mapping:
star1_in_gg(x1, x2)  =  star1_in_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
app17_in_gag(x1, x2, x3)  =  app17_in_gag(x1, x3)
appc17_in_gag(x1, x2, x3)  =  appc17_in_gag(x1, x3)
[]  =  []
appc17_out_gag(x1, x2, x3)  =  appc17_out_gag(x1, x2, x3)
U8_gag(x1, x2, x3, x4, x5)  =  U8_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)
U2_GG(x1, x2, x3, x4)  =  U2_GG(x1, x2, x3, x4)
APP17_IN_GAG(x1, x2, x3)  =  APP17_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5)  =  U1_GAG(x1, x2, x4, x5)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U2_GG(T19, T20, T21, app17_in_gag(T20, X29, T21))
STAR1_IN_GG(.(T19, T20), .(T19, T21)) → APP17_IN_GAG(T20, X29, T21)
APP17_IN_GAG(.(T38, T39), X67, .(T38, T40)) → U1_GAG(T38, T39, X67, T40, app17_in_gag(T39, X67, T40))
APP17_IN_GAG(.(T38, T39), X67, .(T38, T40)) → APP17_IN_GAG(T39, X67, T40)
STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U3_GG(T19, T20, T21, appc17_in_gag(T20, T24, T21))
U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → U4_GG(T19, T20, T21, star1_in_gg(.(T19, T20), T24))
U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → STAR1_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appc17_in_gag([], T31, T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), X67, .(T38, T40)) → U8_gag(T38, T39, X67, T40, appc17_in_gag(T39, X67, T40))
U8_gag(T38, T39, X67, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

The argument filtering Pi contains the following mapping:
star1_in_gg(x1, x2)  =  star1_in_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
app17_in_gag(x1, x2, x3)  =  app17_in_gag(x1, x3)
appc17_in_gag(x1, x2, x3)  =  appc17_in_gag(x1, x3)
[]  =  []
appc17_out_gag(x1, x2, x3)  =  appc17_out_gag(x1, x2, x3)
U8_gag(x1, x2, x3, x4, x5)  =  U8_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)
U2_GG(x1, x2, x3, x4)  =  U2_GG(x1, x2, x3, x4)
APP17_IN_GAG(x1, x2, x3)  =  APP17_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5)  =  U1_GAG(x1, x2, x4, x5)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)
U4_GG(x1, x2, x3, x4)  =  U4_GG(x1, x2, x3, x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

APP17_IN_GAG(.(T38, T39), X67, .(T38, T40)) → APP17_IN_GAG(T39, X67, T40)

The TRS R consists of the following rules:

appc17_in_gag([], T31, T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), X67, .(T38, T40)) → U8_gag(T38, T39, X67, T40, appc17_in_gag(T39, X67, T40))
U8_gag(T38, T39, X67, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc17_in_gag(x1, x2, x3)  =  appc17_in_gag(x1, x3)
[]  =  []
appc17_out_gag(x1, x2, x3)  =  appc17_out_gag(x1, x2, x3)
U8_gag(x1, x2, x3, x4, x5)  =  U8_gag(x1, x2, x4, x5)
APP17_IN_GAG(x1, x2, x3)  =  APP17_IN_GAG(x1, 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:

APP17_IN_GAG(.(T38, T39), X67, .(T38, T40)) → APP17_IN_GAG(T39, X67, T40)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP17_IN_GAG(x1, x2, x3)  =  APP17_IN_GAG(x1, 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:

APP17_IN_GAG(.(T38, T39), .(T38, T40)) → APP17_IN_GAG(T39, T40)

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:

  • APP17_IN_GAG(.(T38, T39), .(T38, T40)) → APP17_IN_GAG(T39, T40)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U3_GG(T19, T20, T21, appc17_in_gag(T20, T24, T21))
U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → STAR1_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appc17_in_gag([], T31, T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), X67, .(T38, T40)) → U8_gag(T38, T39, X67, T40, appc17_in_gag(T39, X67, T40))
U8_gag(T38, T39, X67, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc17_in_gag(x1, x2, x3)  =  appc17_in_gag(x1, x3)
[]  =  []
appc17_out_gag(x1, x2, x3)  =  appc17_out_gag(x1, x2, x3)
U8_gag(x1, x2, x3, x4, x5)  =  U8_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x1, x2, x3, x4)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U3_GG(T19, T20, T21, appc17_in_gag(T20, T21))
U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → STAR1_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appc17_in_gag([], T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), .(T38, T40)) → U8_gag(T38, T39, T40, appc17_in_gag(T39, T40))
U8_gag(T38, T39, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

The set Q consists of the following terms:

appc17_in_gag(x0, x1)
U8_gag(x0, x1, x2, x3)

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


STAR1_IN_GG(.(T19, T20), .(T19, T21)) → U3_GG(T19, T20, T21, appc17_in_gag(T20, T21))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(STAR1_IN_GG(x1, x2)) = x1 + x2   
POL(U3_GG(x1, x2, x3, x4)) = 1 + x4   
POL(U8_gag(x1, x2, x3, x4)) = 1 + x4   
POL([]) = 0   
POL(appc17_in_gag(x1, x2)) = x2   
POL(appc17_out_gag(x1, x2, x3)) = x1 + x2   

The following usable rules [FROCOS05] were oriented:

appc17_in_gag([], T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), .(T38, T40)) → U8_gag(T38, T39, T40, appc17_in_gag(T39, T40))
U8_gag(T38, T39, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

(20) Obligation:

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

U3_GG(T19, T20, T21, appc17_out_gag(T20, T24, T21)) → STAR1_IN_GG(.(T19, T20), T24)

The TRS R consists of the following rules:

appc17_in_gag([], T31) → appc17_out_gag([], T31, T31)
appc17_in_gag(.(T38, T39), .(T38, T40)) → U8_gag(T38, T39, T40, appc17_in_gag(T39, T40))
U8_gag(T38, T39, T40, appc17_out_gag(T39, X67, T40)) → appc17_out_gag(.(T38, T39), X67, .(T38, T40))

The set Q consists of the following terms:

appc17_in_gag(x0, x1)
U8_gag(x0, x1, x2, x3)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(22) TRUE