(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