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 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 PiDP
        ↳15 PiDPToQDPProof (⇐)
        ↳16 QDP
        ↳17 Instantiation (⇔)
        ↳18 QDP
        ↳19 Instantiation (⇔)
        ↳20 QDP
        ↳21 QDPOrderProof (⇔)
        ↳22 QDP
        ↳23 DependencyGraphProof (⇔)
        ↳24 TRUE
    ↳25 PiDP
        ↳26 UsableRulesProof (⇔)
        ↳27 PiDP
        ↳28 PiDPToQDPProof (⇔)
        ↳29 QDP
        ↳30 QDPSizeChangeProof (⇔)
        ↳31 YES

(0) Obligation:

Clauses:

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

Queries:

star(g,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

app16(.(T45, T46), X83, .(T45, T47)) :- app16(T46, X83, T47).
star1(.(T10, []), .(T10, T17)) :- star1(.(T10, []), T17).
star1(.(T10, .(T26, T27)), .(T10, .(T26, T28))) :- app16(T27, X45, T28).
star1(.(T10, .(T26, T27)), .(T10, .(T26, T28))) :- ','(appc16(T27, T31, T28), star1(.(T10, .(T26, T27)), .(T26, T28))).

Clauses:

starc1(T4, []).
starc1(.(T10, []), .(T10, T17)) :- starc1(.(T10, []), T17).
starc1(.(T10, .(T26, T27)), .(T10, .(T26, T28))) :- ','(appc16(T27, T31, T28), starc1(.(T10, .(T26, T27)), .(T26, T28))).
appc16([], T38, T38).
appc16(.(T45, T46), X83, .(T45, T47)) :- appc16(T46, X83, T47).

Afs:

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

(3) 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)
app16_in: (b,f,b)
appc16_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(.(T10, []), .(T10, T17)) → U2_GG(T10, T17, star1_in_gg(.(T10, []), T17))
STAR1_IN_GG(.(T10, []), .(T10, T17)) → STAR1_IN_GG(.(T10, []), T17)
STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U3_GG(T10, T26, T27, T28, app16_in_gag(T27, X45, T28))
STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → APP16_IN_GAG(T27, X45, T28)
APP16_IN_GAG(.(T45, T46), X83, .(T45, T47)) → U1_GAG(T45, T46, X83, T47, app16_in_gag(T46, X83, T47))
APP16_IN_GAG(.(T45, T46), X83, .(T45, T47)) → APP16_IN_GAG(T46, X83, T47)
STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U4_GG(T10, T26, T27, T28, appc16_in_gag(T27, T31, T28))
U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → U5_GG(T10, T26, T27, T28, star1_in_gg(.(T10, .(T26, T27)), .(T26, T28)))
U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → STAR1_IN_GG(.(T10, .(T26, T27)), .(T26, T28))

The TRS R consists of the following rules:

appc16_in_gag([], T38, T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), X83, .(T45, T47)) → U10_gag(T45, T46, X83, T47, appc16_in_gag(T46, X83, T47))
U10_gag(T45, T46, X83, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The argument filtering Pi contains the following mapping:
star1_in_gg(x1, x2)  =  star1_in_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
app16_in_gag(x1, x2, x3)  =  app16_in_gag(x1, x3)
appc16_in_gag(x1, x2, x3)  =  appc16_in_gag(x1, x3)
appc16_out_gag(x1, x2, x3)  =  appc16_out_gag(x1, x2, x3)
U10_gag(x1, x2, x3, x4, x5)  =  U10_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U3_GG(x1, x2, x3, x4, x5)  =  U3_GG(x1, x2, x3, x4, x5)
APP16_IN_GAG(x1, x2, x3)  =  APP16_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5)  =  U1_GAG(x1, x2, x4, x5)
U4_GG(x1, x2, x3, x4, x5)  =  U4_GG(x1, x2, x3, x4, x5)
U5_GG(x1, x2, x3, x4, x5)  =  U5_GG(x1, x2, x3, x4, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

STAR1_IN_GG(.(T10, []), .(T10, T17)) → U2_GG(T10, T17, star1_in_gg(.(T10, []), T17))
STAR1_IN_GG(.(T10, []), .(T10, T17)) → STAR1_IN_GG(.(T10, []), T17)
STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U3_GG(T10, T26, T27, T28, app16_in_gag(T27, X45, T28))
STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → APP16_IN_GAG(T27, X45, T28)
APP16_IN_GAG(.(T45, T46), X83, .(T45, T47)) → U1_GAG(T45, T46, X83, T47, app16_in_gag(T46, X83, T47))
APP16_IN_GAG(.(T45, T46), X83, .(T45, T47)) → APP16_IN_GAG(T46, X83, T47)
STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U4_GG(T10, T26, T27, T28, appc16_in_gag(T27, T31, T28))
U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → U5_GG(T10, T26, T27, T28, star1_in_gg(.(T10, .(T26, T27)), .(T26, T28)))
U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → STAR1_IN_GG(.(T10, .(T26, T27)), .(T26, T28))

The TRS R consists of the following rules:

appc16_in_gag([], T38, T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), X83, .(T45, T47)) → U10_gag(T45, T46, X83, T47, appc16_in_gag(T46, X83, T47))
U10_gag(T45, T46, X83, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The argument filtering Pi contains the following mapping:
star1_in_gg(x1, x2)  =  star1_in_gg(x1, x2)
.(x1, x2)  =  .(x1, x2)
[]  =  []
app16_in_gag(x1, x2, x3)  =  app16_in_gag(x1, x3)
appc16_in_gag(x1, x2, x3)  =  appc16_in_gag(x1, x3)
appc16_out_gag(x1, x2, x3)  =  appc16_out_gag(x1, x2, x3)
U10_gag(x1, x2, x3, x4, x5)  =  U10_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U3_GG(x1, x2, x3, x4, x5)  =  U3_GG(x1, x2, x3, x4, x5)
APP16_IN_GAG(x1, x2, x3)  =  APP16_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5)  =  U1_GAG(x1, x2, x4, x5)
U4_GG(x1, x2, x3, x4, x5)  =  U4_GG(x1, x2, x3, x4, x5)
U5_GG(x1, x2, x3, x4, x5)  =  U5_GG(x1, x2, x3, x4, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APP16_IN_GAG(.(T45, T46), X83, .(T45, T47)) → APP16_IN_GAG(T46, X83, T47)

The TRS R consists of the following rules:

appc16_in_gag([], T38, T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), X83, .(T45, T47)) → U10_gag(T45, T46, X83, T47, appc16_in_gag(T46, X83, T47))
U10_gag(T45, T46, X83, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
appc16_in_gag(x1, x2, x3)  =  appc16_in_gag(x1, x3)
appc16_out_gag(x1, x2, x3)  =  appc16_out_gag(x1, x2, x3)
U10_gag(x1, x2, x3, x4, x5)  =  U10_gag(x1, x2, x4, x5)
APP16_IN_GAG(x1, x2, x3)  =  APP16_IN_GAG(x1, x3)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APP16_IN_GAG(.(T45, T46), X83, .(T45, T47)) → APP16_IN_GAG(T46, X83, T47)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APP16_IN_GAG(.(T45, T46), .(T45, T47)) → APP16_IN_GAG(T46, T47)

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

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

  • APP16_IN_GAG(.(T45, T46), .(T45, T47)) → APP16_IN_GAG(T46, T47)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U4_GG(T10, T26, T27, T28, appc16_in_gag(T27, T31, T28))
U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → STAR1_IN_GG(.(T10, .(T26, T27)), .(T26, T28))

The TRS R consists of the following rules:

appc16_in_gag([], T38, T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), X83, .(T45, T47)) → U10_gag(T45, T46, X83, T47, appc16_in_gag(T46, X83, T47))
U10_gag(T45, T46, X83, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
appc16_in_gag(x1, x2, x3)  =  appc16_in_gag(x1, x3)
appc16_out_gag(x1, x2, x3)  =  appc16_out_gag(x1, x2, x3)
U10_gag(x1, x2, x3, x4, x5)  =  U10_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)
U4_GG(x1, x2, x3, x4, x5)  =  U4_GG(x1, x2, x3, x4, x5)

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

(15) PiDPToQDPProof (SOUND transformation)

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

(16) Obligation:

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

STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U4_GG(T10, T26, T27, T28, appc16_in_gag(T27, T28))
U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → STAR1_IN_GG(.(T10, .(T26, T27)), .(T26, T28))

The TRS R consists of the following rules:

appc16_in_gag([], T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), .(T45, T47)) → U10_gag(T45, T46, T47, appc16_in_gag(T46, T47))
U10_gag(T45, T46, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The set Q consists of the following terms:

appc16_in_gag(x0, x1)
U10_gag(x0, x1, x2, x3)

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

(17) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule STAR1_IN_GG(.(T10, .(T26, T27)), .(T10, .(T26, T28))) → U4_GG(T10, T26, T27, T28, appc16_in_gag(T27, T28)) we obtained the following new rules [LPAR04]:

STAR1_IN_GG(.(z0, .(z0, z2)), .(z0, .(z0, x3))) → U4_GG(z0, z0, z2, x3, appc16_in_gag(z2, x3))

(18) Obligation:

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

U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → STAR1_IN_GG(.(T10, .(T26, T27)), .(T26, T28))
STAR1_IN_GG(.(z0, .(z0, z2)), .(z0, .(z0, x3))) → U4_GG(z0, z0, z2, x3, appc16_in_gag(z2, x3))

The TRS R consists of the following rules:

appc16_in_gag([], T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), .(T45, T47)) → U10_gag(T45, T46, T47, appc16_in_gag(T46, T47))
U10_gag(T45, T46, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The set Q consists of the following terms:

appc16_in_gag(x0, x1)
U10_gag(x0, x1, x2, x3)

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

(19) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_GG(T10, T26, T27, T28, appc16_out_gag(T27, T31, T28)) → STAR1_IN_GG(.(T10, .(T26, T27)), .(T26, T28)) we obtained the following new rules [LPAR04]:

U4_GG(z0, z0, z1, z2, appc16_out_gag(z1, x4, z2)) → STAR1_IN_GG(.(z0, .(z0, z1)), .(z0, z2))

(20) Obligation:

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

STAR1_IN_GG(.(z0, .(z0, z2)), .(z0, .(z0, x3))) → U4_GG(z0, z0, z2, x3, appc16_in_gag(z2, x3))
U4_GG(z0, z0, z1, z2, appc16_out_gag(z1, x4, z2)) → STAR1_IN_GG(.(z0, .(z0, z1)), .(z0, z2))

The TRS R consists of the following rules:

appc16_in_gag([], T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), .(T45, T47)) → U10_gag(T45, T46, T47, appc16_in_gag(T46, T47))
U10_gag(T45, T46, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The set Q consists of the following terms:

appc16_in_gag(x0, x1)
U10_gag(x0, x1, x2, x3)

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

(21) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


STAR1_IN_GG(.(z0, .(z0, z2)), .(z0, .(z0, x3))) → U4_GG(z0, z0, z2, x3, appc16_in_gag(z2, x3))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U4_GG(x1, ..., x5) ) = x4 + 2


POL( appc16_in_gag(x1, x2) ) = 2x1 + 2


POL( [] ) = 2


POL( appc16_out_gag(x1, ..., x3) ) = max{0, x2 + x3 - 2}


POL( .(x1, x2) ) = x2 + 1


POL( U10_gag(x1, ..., x4) ) = max{0, 2x2 + x3 - 1}


POL( STAR1_IN_GG(x1, x2) ) = x2 + 1



The following usable rules [FROCOS05] were oriented: none

(22) Obligation:

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

U4_GG(z0, z0, z1, z2, appc16_out_gag(z1, x4, z2)) → STAR1_IN_GG(.(z0, .(z0, z1)), .(z0, z2))

The TRS R consists of the following rules:

appc16_in_gag([], T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), .(T45, T47)) → U10_gag(T45, T46, T47, appc16_in_gag(T46, T47))
U10_gag(T45, T46, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The set Q consists of the following terms:

appc16_in_gag(x0, x1)
U10_gag(x0, x1, x2, x3)

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

(23) DependencyGraphProof (EQUIVALENT transformation)

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

(24) TRUE

(25) Obligation:

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

STAR1_IN_GG(.(T10, []), .(T10, T17)) → STAR1_IN_GG(.(T10, []), T17)

The TRS R consists of the following rules:

appc16_in_gag([], T38, T38) → appc16_out_gag([], T38, T38)
appc16_in_gag(.(T45, T46), X83, .(T45, T47)) → U10_gag(T45, T46, X83, T47, appc16_in_gag(T46, X83, T47))
U10_gag(T45, T46, X83, T47, appc16_out_gag(T46, X83, T47)) → appc16_out_gag(.(T45, T46), X83, .(T45, T47))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
appc16_in_gag(x1, x2, x3)  =  appc16_in_gag(x1, x3)
appc16_out_gag(x1, x2, x3)  =  appc16_out_gag(x1, x2, x3)
U10_gag(x1, x2, x3, x4, x5)  =  U10_gag(x1, x2, x4, x5)
STAR1_IN_GG(x1, x2)  =  STAR1_IN_GG(x1, x2)

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

(26) UsableRulesProof (EQUIVALENT transformation)

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

(27) Obligation:

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

STAR1_IN_GG(.(T10, []), .(T10, T17)) → STAR1_IN_GG(.(T10, []), T17)

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

(28) PiDPToQDPProof (EQUIVALENT transformation)

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

(29) Obligation:

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

STAR1_IN_GG(.(T10, []), .(T10, T17)) → STAR1_IN_GG(.(T10, []), T17)

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

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

  • STAR1_IN_GG(.(T10, []), .(T10, T17)) → STAR1_IN_GG(.(T10, []), T17)
    The graph contains the following edges 1 >= 1, 2 > 2

(31) YES