(0) Obligation:

Clauses:

goal(X) :- ','(s2l(X, Xs), list(Xs)).
list([]).
list(X) :- ','(no(empty(X)), ','(tail(X, T), list(T))).
s2l(0, []).
s2l(X, .(X1, Xs)) :- ','(no(zero(X)), ','(p(X, P), s2l(P, Xs))).
tail([], []).
tail(.(X2, Xs), Xs).
p(0, 0).
p(s(X), X).
empty([]).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X3).
failure(b).

Queries:

goal(g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

s2l40(s(T28), .(X77, X78)) :- s2l40(T28, X78).
list78([]) :- list7.
list78(.(T69, T71)) :- list78(T71).
goal1(0) :- list7.
goal1(s(T15)) :- s2l40(T15, X35).
goal1(s(T15)) :- ','(s2lc40(T15, T49), list78(T49)).

Clauses:

s2lc40(0, []).
s2lc40(s(T28), .(X77, X78)) :- s2lc40(T28, X78).
listc7.
listc78([]).
listc78([]) :- listc7.
listc78(.(T69, T71)) :- listc78(T71).

Afs:

goal1(x1)  =  goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2l40(s(T28), .(X77, X78)) :- s2l40(T28, X78).
list78(.(T69, T71)) :- list78(T71).
goal1(s(T15)) :- s2l40(T15, X35).
goal1(s(T15)) :- ','(s2lc40(T15, T49), list78(T49)).

Clauses:

s2lc40(0, []).
s2lc40(s(T28), .(X77, X78)) :- s2lc40(T28, X78).
listc7.
listc78([]).
listc78([]) :- listc7.
listc78(.(T69, T71)) :- listc78(T71).

Afs:

goal1(x1)  =  goal1(x1)

(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:
goal1_in: (b)
s2l40_in: (b,f)
s2lc40_in: (b,f)
list78_in: (b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_G(s(T15)) → U3_G(T15, s2l40_in_ga(T15, X35))
GOAL1_IN_G(s(T15)) → S2L40_IN_GA(T15, X35)
S2L40_IN_GA(s(T28), .(X77, X78)) → U1_GA(T28, X77, X78, s2l40_in_ga(T28, X78))
S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)
GOAL1_IN_G(s(T15)) → U4_G(T15, s2lc40_in_ga(T15, T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → U5_G(T15, list78_in_g(T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → LIST78_IN_G(T49)
LIST78_IN_G(.(T69, T71)) → U2_G(T69, T71, list78_in_g(T71))
LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2l40_in_ga(x1, x2)  =  s2l40_in_ga(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
list78_in_g(x1)  =  list78_in_g(x1)
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
S2L40_IN_GA(x1, x2)  =  S2L40_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
U5_G(x1, x2)  =  U5_G(x1, x2)
LIST78_IN_G(x1)  =  LIST78_IN_G(x1)
U2_G(x1, x2, x3)  =  U2_G(x2, x3)

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:

GOAL1_IN_G(s(T15)) → U3_G(T15, s2l40_in_ga(T15, X35))
GOAL1_IN_G(s(T15)) → S2L40_IN_GA(T15, X35)
S2L40_IN_GA(s(T28), .(X77, X78)) → U1_GA(T28, X77, X78, s2l40_in_ga(T28, X78))
S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)
GOAL1_IN_G(s(T15)) → U4_G(T15, s2lc40_in_ga(T15, T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → U5_G(T15, list78_in_g(T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → LIST78_IN_G(T49)
LIST78_IN_G(.(T69, T71)) → U2_G(T69, T71, list78_in_g(T71))
LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2l40_in_ga(x1, x2)  =  s2l40_in_ga(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
list78_in_g(x1)  =  list78_in_g(x1)
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
S2L40_IN_GA(x1, x2)  =  S2L40_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
U5_G(x1, x2)  =  U5_G(x1, x2)
LIST78_IN_G(x1)  =  LIST78_IN_G(x1)
U2_G(x1, x2, x3)  =  U2_G(x2, x3)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
LIST78_IN_G(x1)  =  LIST78_IN_G(x1)

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:

LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

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

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:

LIST78_IN_G(.(T71)) → LIST78_IN_G(T71)

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:

  • LIST78_IN_G(.(T71)) → LIST78_IN_G(T71)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
S2L40_IN_GA(x1, x2)  =  S2L40_IN_GA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

S2L40_IN_GA(s(T28)) → S2L40_IN_GA(T28)

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

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

  • S2L40_IN_GA(s(T28)) → S2L40_IN_GA(T28)
    The graph contains the following edges 1 > 1

(22) YES