(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil).
tree(X) :- ','(no(empty(X)), ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R))))).
s2t(0, nil).
s2t(X, node(T, X1, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X2, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(T, X3, nil)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X4, nil)) :- no(zero(X)).
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).
empty(nil).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X9).
failure(b).

Queries:

goal(g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

s2t42(s(T32), node(X125, X126, X125)) :- s2t42(T32, X125).
s2t42(s(T46), node(nil, X163, X164)) :- s2t42(T46, X164).
s2t42(s(T60), node(X201, X202, nil)) :- s2t42(T60, X201).
p139 :- tree7.
p139 :- ','(treec7, tree7).
p146(X293, X295) :- tree148(X293).
p146(T84, X295) :- ','(treec148(T84), tree148(X295)).
goal1(0) :- tree7.
goal1(s(T17)) :- s2t42(T17, X63).
goal1(s(T17)) :- ','(s2tc42(T17, T83), p139).
goal1(s(T17)) :- ','(s2tc42(T17, T83), p146(X293, X295)).
goal1(s(T98)) :- s2t42(T98, X353).
goal1(s(T98)) :- ','(s2tc42(T98, T113), p139).
goal1(s(T98)) :- ','(s2tc42(T98, T113), p146(X453, X455)).
goal1(s(T127)) :- s2t42(T127, X494).
goal1(s(T127)) :- ','(s2tc42(T127, T142), p139).
goal1(s(T127)) :- ','(s2tc42(T127, T142), p146(X595, X597)).
goal1(T151) :- p139.
goal1(T151) :- p146(X698, X700).

Clauses:

s2tc42(0, nil).
s2tc42(s(T32), node(X125, X126, X125)) :- s2tc42(T32, X125).
s2tc42(s(T46), node(nil, X163, X164)) :- s2tc42(T46, X164).
s2tc42(s(T60), node(X201, X202, nil)) :- s2tc42(T60, X201).
s2tc42(T69, node(nil, X221, nil)).
treec7.
treec148(nil).
qc139 :- ','(treec7, treec7).
qc146(T84, X295) :- ','(treec148(T84), treec148(X295)).

Afs:

goal1(x1)  =  goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2t42(s(T32), node(X125, X126, X125)) :- s2t42(T32, X125).
s2t42(s(T46), node(nil, X163, X164)) :- s2t42(T46, X164).
s2t42(s(T60), node(X201, X202, nil)) :- s2t42(T60, X201).
goal1(s(T17)) :- s2t42(T17, X63).
goal1(s(T98)) :- s2t42(T98, X353).
goal1(s(T127)) :- s2t42(T127, X494).

Clauses:

s2tc42(0, nil).
s2tc42(s(T32), node(X125, X126, X125)) :- s2tc42(T32, X125).
s2tc42(s(T46), node(nil, X163, X164)) :- s2tc42(T46, X164).
s2tc42(s(T60), node(X201, X202, nil)) :- s2tc42(T60, X201).
s2tc42(T69, node(nil, X221, nil)).
treec7.
treec148(nil).
qc139 :- ','(treec7, treec7).
qc146(T84, X295) :- ','(treec148(T84), treec148(X295)).

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)
s2t42_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(T17)) → U4_G(T17, s2t42_in_ga(T17, X63))
GOAL1_IN_G(s(T17)) → S2T42_IN_GA(T17, X63)
S2T42_IN_GA(s(T32), node(X125, X126, X125)) → U1_GA(T32, X125, X126, s2t42_in_ga(T32, X125))
S2T42_IN_GA(s(T32), node(X125, X126, X125)) → S2T42_IN_GA(T32, X125)
S2T42_IN_GA(s(T46), node(nil, X163, X164)) → U2_GA(T46, X163, X164, s2t42_in_ga(T46, X164))
S2T42_IN_GA(s(T46), node(nil, X163, X164)) → S2T42_IN_GA(T46, X164)
S2T42_IN_GA(s(T60), node(X201, X202, nil)) → U3_GA(T60, X201, X202, s2t42_in_ga(T60, X201))
S2T42_IN_GA(s(T60), node(X201, X202, nil)) → S2T42_IN_GA(T60, X201)
GOAL1_IN_G(s(T98)) → U5_G(T98, s2t42_in_ga(T98, X353))
GOAL1_IN_G(s(T127)) → U6_G(T127, s2t42_in_ga(T127, X494))

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2t42_in_ga(x1, x2)  =  s2t42_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)
S2T42_IN_GA(x1, x2)  =  S2T42_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(T17)) → U4_G(T17, s2t42_in_ga(T17, X63))
GOAL1_IN_G(s(T17)) → S2T42_IN_GA(T17, X63)
S2T42_IN_GA(s(T32), node(X125, X126, X125)) → U1_GA(T32, X125, X126, s2t42_in_ga(T32, X125))
S2T42_IN_GA(s(T32), node(X125, X126, X125)) → S2T42_IN_GA(T32, X125)
S2T42_IN_GA(s(T46), node(nil, X163, X164)) → U2_GA(T46, X163, X164, s2t42_in_ga(T46, X164))
S2T42_IN_GA(s(T46), node(nil, X163, X164)) → S2T42_IN_GA(T46, X164)
S2T42_IN_GA(s(T60), node(X201, X202, nil)) → U3_GA(T60, X201, X202, s2t42_in_ga(T60, X201))
S2T42_IN_GA(s(T60), node(X201, X202, nil)) → S2T42_IN_GA(T60, X201)
GOAL1_IN_G(s(T98)) → U5_G(T98, s2t42_in_ga(T98, X353))
GOAL1_IN_G(s(T127)) → U6_G(T127, s2t42_in_ga(T127, X494))

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2t42_in_ga(x1, x2)  =  s2t42_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)
S2T42_IN_GA(x1, x2)  =  S2T42_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:

S2T42_IN_GA(s(T46), node(nil, X163, X164)) → S2T42_IN_GA(T46, X164)
S2T42_IN_GA(s(T32), node(X125, X126, X125)) → S2T42_IN_GA(T32, X125)
S2T42_IN_GA(s(T60), node(X201, X202, nil)) → S2T42_IN_GA(T60, X201)

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

S2T42_IN_GA(s(T46)) → S2T42_IN_GA(T46)

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:

  • S2T42_IN_GA(s(T46)) → S2T42_IN_GA(T46)
    The graph contains the following edges 1 > 1

(12) YES