(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil) :- !.
tree(X) :- ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R)))).
s2t(0, L) :- ','(!, eq(L, nil)).
s2t(X, node(T, X1, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X2, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(T, X3, nil)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X4, nil)).
left(nil, nil).
left(node(L, X5, X6), L).
right(nil, nil).
right(node(X7, X8, R), R).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

goal(g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

s2t21(s(T20), node(X110, X111, X110)) :- s2t21(T20, X110).
s2t21(s(T28), node(nil, X150, X151)) :- s2t21(T28, X151).
s2t21(s(T36), node(X190, X191, nil)) :- s2t21(T36, X190).
p63 :- tree9.
p63 :- ','(treec9, tree9).
p70(X262, X264) :- tree72(X262).
p70(T44, X264) :- ','(treec72(T44), tree72(X264)).
goal1(0) :- tree9.
goal1(s(T11)) :- s2t21(T11, X55).
goal1(s(T11)) :- ','(s2tc21(T11, T43), p63).
goal1(s(T11)) :- ','(s2tc21(T11, T43), p70(X262, X264)).
goal1(s(T52)) :- s2t21(T52, X296).
goal1(s(T52)) :- ','(s2tc21(T52, T57), p63).
goal1(s(T52)) :- ','(s2tc21(T52, T57), p70(X360, X362)).
goal1(s(T65)) :- s2t21(T65, X393).
goal1(s(T65)) :- ','(s2tc21(T65, T70), p63).
goal1(s(T65)) :- ','(s2tc21(T65, T70), p70(X458, X460)).
goal1(T73) :- p63.
goal1(T73) :- p70(X528, X530).

Clauses:

s2tc21(0, nil).
s2tc21(s(T20), node(X110, X111, X110)) :- s2tc21(T20, X110).
s2tc21(s(T28), node(nil, X150, X151)) :- s2tc21(T28, X151).
s2tc21(s(T36), node(X190, X191, nil)) :- s2tc21(T36, X190).
s2tc21(T39, node(nil, X208, nil)).
treec9.
treec72(nil).
qc63 :- ','(treec9, treec9).
qc70(T44, X264) :- ','(treec72(T44), treec72(X264)).

Afs:

goal1(x1)  =  goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2t21(s(T20), node(X110, X111, X110)) :- s2t21(T20, X110).
s2t21(s(T28), node(nil, X150, X151)) :- s2t21(T28, X151).
s2t21(s(T36), node(X190, X191, nil)) :- s2t21(T36, X190).
goal1(s(T11)) :- s2t21(T11, X55).
goal1(s(T52)) :- s2t21(T52, X296).
goal1(s(T65)) :- s2t21(T65, X393).

Clauses:

s2tc21(0, nil).
s2tc21(s(T20), node(X110, X111, X110)) :- s2tc21(T20, X110).
s2tc21(s(T28), node(nil, X150, X151)) :- s2tc21(T28, X151).
s2tc21(s(T36), node(X190, X191, nil)) :- s2tc21(T36, X190).
s2tc21(T39, node(nil, X208, nil)).
treec9.
treec72(nil).
qc63 :- ','(treec9, treec9).
qc70(T44, X264) :- ','(treec72(T44), treec72(X264)).

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

GOAL1_IN_G(s(T11)) → U4_G(T11, s2t21_in_ga(T11, X55))
GOAL1_IN_G(s(T11)) → S2T21_IN_GA(T11, X55)
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → U1_GA(T20, X110, X111, s2t21_in_ga(T20, X110))
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → S2T21_IN_GA(T20, X110)
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → U2_GA(T28, X150, X151, s2t21_in_ga(T28, X151))
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → S2T21_IN_GA(T28, X151)
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → U3_GA(T36, X190, X191, s2t21_in_ga(T36, X190))
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → S2T21_IN_GA(T36, X190)
GOAL1_IN_G(s(T52)) → U5_G(T52, s2t21_in_ga(T52, X296))
GOAL1_IN_G(s(T65)) → U6_G(T65, s2t21_in_ga(T65, X393))

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2t21_in_ga(x1, x2)  =  s2t21_in_ga(x1)
node(x1, x2, x3)  =  node(x1, x3)
nil  =  nil
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x1, x2)
S2T21_IN_GA(x1, x2)  =  S2T21_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U5_G(x1, x2)  =  U5_G(x1, x2)
U6_G(x1, x2)  =  U6_G(x1, x2)

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(T11)) → U4_G(T11, s2t21_in_ga(T11, X55))
GOAL1_IN_G(s(T11)) → S2T21_IN_GA(T11, X55)
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → U1_GA(T20, X110, X111, s2t21_in_ga(T20, X110))
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → S2T21_IN_GA(T20, X110)
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → U2_GA(T28, X150, X151, s2t21_in_ga(T28, X151))
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → S2T21_IN_GA(T28, X151)
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → U3_GA(T36, X190, X191, s2t21_in_ga(T36, X190))
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → S2T21_IN_GA(T36, X190)
GOAL1_IN_G(s(T52)) → U5_G(T52, s2t21_in_ga(T52, X296))
GOAL1_IN_G(s(T65)) → U6_G(T65, s2t21_in_ga(T65, X393))

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2t21_in_ga(x1, x2)  =  s2t21_in_ga(x1)
node(x1, x2, x3)  =  node(x1, x3)
nil  =  nil
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U4_G(x1, x2)  =  U4_G(x1, x2)
S2T21_IN_GA(x1, x2)  =  S2T21_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U5_G(x1, x2)  =  U5_G(x1, x2)
U6_G(x1, x2)  =  U6_G(x1, x2)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

S2T21_IN_GA(s(T28), node(nil, X150, X151)) → S2T21_IN_GA(T28, X151)
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → S2T21_IN_GA(T20, X110)
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → S2T21_IN_GA(T36, X190)

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

S2T21_IN_GA(s(T28)) → S2T21_IN_GA(T28)

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

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

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

(12) YES