(0) Obligation:
Clauses:preorder(X, Y) :- pdl(X, -(Y, [])).
pdl(nil, Y) :- ','(!, eq(Y, -(X, X))).
pdl(T, -(.(X, Xs), Zs)) :- ','(value(T, X), ','(left(T, L), ','(right(T, R), ','(pdl(L, -(Xs, Ys)), pdl(R, -(Ys, Zs)))))).
left(nil, nil).
left(tree(L, X1, X2), L).
right(nil, nil).
right(tree(X3, X4, R), R).
value(nil, X5).
value(tree(X6, X, X7), X).
eq(X, X).
Queries:
preorder(g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:pdl3(tree(T57, T58, T59), .(T58, T37)) :- pdl24(T57, T37, X39).
pdl3(tree(T57, T58, T59), .(T58, T37)) :- ','(pdlc24(T57, T37, T61), pdl3(T59, T61)).
pdl24(tree(T112, T113, T114), .(T113, T92), X131) :- pdl24(T112, T92, X130).
pdl24(tree(T112, T113, T114), .(T113, T92), X131) :- ','(pdlc24(T112, T92, T116), pdl24(T114, T116, X131)).
preorder1(T5, T7) :- pdl3(T5, T7).
Clauses:
pdlc3(nil, []).
pdlc3(tree(T57, T58, T59), .(T58, T37)) :- ','(pdlc24(T57, T37, T61), pdlc3(T59, T61)).
pdlc24(nil, T69, T69).
pdlc24(tree(T112, T113, T114), .(T113, T92), X131) :- ','(pdlc24(T112, T92, T116), pdlc24(T114, T116, X131)).
Afs:
preorder1(x1, x2) = preorder1(x1)
(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:preorder1_in: (b,f)
pdl3_in: (b,f)
pdl24_in: (b,f,f)
pdlc24_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
PREORDER1_IN_GA(T5, T7) → U7_GA(T5, T7, pdl3_in_ga(T5, T7))
PREORDER1_IN_GA(T5, T7) → PDL3_IN_GA(T5, T7)
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → U1_GA(T57, T58, T59, T37, pdl24_in_gaa(T57, T37, X39))
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → PDL24_IN_GAA(T57, T37, X39)
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → U4_GAA(T112, T113, T114, T92, X131, pdl24_in_gaa(T112, T92, X130))
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → PDL24_IN_GAA(T112, T92, X130)
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → U5_GAA(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U5_GAA(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → U6_GAA(T112, T113, T114, T92, X131, pdl24_in_gaa(T114, T116, X131))
U5_GAA(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → PDL24_IN_GAA(T114, T116, X131)
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → U2_GA(T57, T58, T59, T37, pdlc24_in_gaa(T57, T37, T61))
U2_GA(T57, T58, T59, T37, pdlc24_out_gaa(T57, T37, T61)) → U3_GA(T57, T58, T59, T37, pdl3_in_ga(T59, T61))
U2_GA(T57, T58, T59, T37, pdlc24_out_gaa(T57, T37, T61)) → PDL3_IN_GA(T59, T61)
The TRS R consists of the following rules:
pdlc24_in_gaa(nil, T69, T69) → pdlc24_out_gaa(nil, T69, T69)
pdlc24_in_gaa(tree(T112, T113, T114), .(T113, T92), X131) → U11_gaa(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U11_gaa(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_in_gaa(T114, T116, X131))
U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_out_gaa(T114, T116, X131)) → pdlc24_out_gaa(tree(T112, T113, T114), .(T113, T92), X131)
The argument filtering Pi contains the following mapping:
pdl3_in_ga(x1, x2) = pdl3_in_ga(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
pdl24_in_gaa(x1, x2, x3) = pdl24_in_gaa(x1)
pdlc24_in_gaa(x1, x2, x3) = pdlc24_in_gaa(x1)
nil = nil
pdlc24_out_gaa(x1, x2, x3) = pdlc24_out_gaa(x1)
U11_gaa(x1, x2, x3, x4, x5, x6) = U11_gaa(x1, x2, x3, x6)
U12_gaa(x1, x2, x3, x4, x5, x6, x7) = U12_gaa(x1, x2, x3, x7)
PREORDER1_IN_GA(x1, x2) = PREORDER1_IN_GA(x1)
U7_GA(x1, x2, x3) = U7_GA(x1, x3)
PDL3_IN_GA(x1, x2) = PDL3_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
PDL24_IN_GAA(x1, x2, x3) = PDL24_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6) = U4_GAA(x1, x2, x3, x6)
U5_GAA(x1, x2, x3, x4, x5, x6) = U5_GAA(x1, x2, x3, x6)
U6_GAA(x1, x2, x3, x4, x5, x6) = U6_GAA(x1, x2, x3, x6)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x3, 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:
PREORDER1_IN_GA(T5, T7) → U7_GA(T5, T7, pdl3_in_ga(T5, T7))
PREORDER1_IN_GA(T5, T7) → PDL3_IN_GA(T5, T7)
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → U1_GA(T57, T58, T59, T37, pdl24_in_gaa(T57, T37, X39))
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → PDL24_IN_GAA(T57, T37, X39)
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → U4_GAA(T112, T113, T114, T92, X131, pdl24_in_gaa(T112, T92, X130))
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → PDL24_IN_GAA(T112, T92, X130)
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → U5_GAA(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U5_GAA(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → U6_GAA(T112, T113, T114, T92, X131, pdl24_in_gaa(T114, T116, X131))
U5_GAA(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → PDL24_IN_GAA(T114, T116, X131)
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → U2_GA(T57, T58, T59, T37, pdlc24_in_gaa(T57, T37, T61))
U2_GA(T57, T58, T59, T37, pdlc24_out_gaa(T57, T37, T61)) → U3_GA(T57, T58, T59, T37, pdl3_in_ga(T59, T61))
U2_GA(T57, T58, T59, T37, pdlc24_out_gaa(T57, T37, T61)) → PDL3_IN_GA(T59, T61)
The TRS R consists of the following rules:
pdlc24_in_gaa(nil, T69, T69) → pdlc24_out_gaa(nil, T69, T69)
pdlc24_in_gaa(tree(T112, T113, T114), .(T113, T92), X131) → U11_gaa(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U11_gaa(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_in_gaa(T114, T116, X131))
U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_out_gaa(T114, T116, X131)) → pdlc24_out_gaa(tree(T112, T113, T114), .(T113, T92), X131)
The argument filtering Pi contains the following mapping:
pdl3_in_ga(x1, x2) = pdl3_in_ga(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
pdl24_in_gaa(x1, x2, x3) = pdl24_in_gaa(x1)
pdlc24_in_gaa(x1, x2, x3) = pdlc24_in_gaa(x1)
nil = nil
pdlc24_out_gaa(x1, x2, x3) = pdlc24_out_gaa(x1)
U11_gaa(x1, x2, x3, x4, x5, x6) = U11_gaa(x1, x2, x3, x6)
U12_gaa(x1, x2, x3, x4, x5, x6, x7) = U12_gaa(x1, x2, x3, x7)
PREORDER1_IN_GA(x1, x2) = PREORDER1_IN_GA(x1)
U7_GA(x1, x2, x3) = U7_GA(x1, x3)
PDL3_IN_GA(x1, x2) = PDL3_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
PDL24_IN_GAA(x1, x2, x3) = PDL24_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6) = U4_GAA(x1, x2, x3, x6)
U5_GAA(x1, x2, x3, x4, x5, x6) = U5_GAA(x1, x2, x3, x6)
U6_GAA(x1, x2, x3, x4, x5, x6) = U6_GAA(x1, x2, x3, x6)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → U5_GAA(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U5_GAA(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → PDL24_IN_GAA(T114, T116, X131)
PDL24_IN_GAA(tree(T112, T113, T114), .(T113, T92), X131) → PDL24_IN_GAA(T112, T92, X130)
The TRS R consists of the following rules:
pdlc24_in_gaa(nil, T69, T69) → pdlc24_out_gaa(nil, T69, T69)
pdlc24_in_gaa(tree(T112, T113, T114), .(T113, T92), X131) → U11_gaa(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U11_gaa(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_in_gaa(T114, T116, X131))
U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_out_gaa(T114, T116, X131)) → pdlc24_out_gaa(tree(T112, T113, T114), .(T113, T92), X131)
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
pdlc24_in_gaa(x1, x2, x3) = pdlc24_in_gaa(x1)
nil = nil
pdlc24_out_gaa(x1, x2, x3) = pdlc24_out_gaa(x1)
U11_gaa(x1, x2, x3, x4, x5, x6) = U11_gaa(x1, x2, x3, x6)
U12_gaa(x1, x2, x3, x4, x5, x6, x7) = U12_gaa(x1, x2, x3, x7)
PDL24_IN_GAA(x1, x2, x3) = PDL24_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4, x5, x6) = U5_GAA(x1, x2, x3, x6)
We have to consider all (P,R,Pi)-chains
(8) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(9) Obligation:
Q DP problem:The TRS P consists of the following rules:
PDL24_IN_GAA(tree(T112, T113, T114)) → U5_GAA(T112, T113, T114, pdlc24_in_gaa(T112))
U5_GAA(T112, T113, T114, pdlc24_out_gaa(T112)) → PDL24_IN_GAA(T114)
PDL24_IN_GAA(tree(T112, T113, T114)) → PDL24_IN_GAA(T112)
The TRS R consists of the following rules:
pdlc24_in_gaa(nil) → pdlc24_out_gaa(nil)
pdlc24_in_gaa(tree(T112, T113, T114)) → U11_gaa(T112, T113, T114, pdlc24_in_gaa(T112))
U11_gaa(T112, T113, T114, pdlc24_out_gaa(T112)) → U12_gaa(T112, T113, T114, pdlc24_in_gaa(T114))
U12_gaa(T112, T113, T114, pdlc24_out_gaa(T114)) → pdlc24_out_gaa(tree(T112, T113, T114))
The set Q consists of the following terms:
pdlc24_in_gaa(x0)
U11_gaa(x0, x1, x2, x3)
U12_gaa(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(10) 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:
- U5_GAA(T112, T113, T114, pdlc24_out_gaa(T112)) → PDL24_IN_GAA(T114)
The graph contains the following edges 3 >= 1 - PDL24_IN_GAA(tree(T112, T113, T114)) → PDL24_IN_GAA(T112)
The graph contains the following edges 1 > 1 - PDL24_IN_GAA(tree(T112, T113, T114)) → U5_GAA(T112, T113, T114, pdlc24_in_gaa(T112))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3
(11) YES
(12) Obligation:
Pi DP problem:The TRS P consists of the following rules:
PDL3_IN_GA(tree(T57, T58, T59), .(T58, T37)) → U2_GA(T57, T58, T59, T37, pdlc24_in_gaa(T57, T37, T61))
U2_GA(T57, T58, T59, T37, pdlc24_out_gaa(T57, T37, T61)) → PDL3_IN_GA(T59, T61)
The TRS R consists of the following rules:
pdlc24_in_gaa(nil, T69, T69) → pdlc24_out_gaa(nil, T69, T69)
pdlc24_in_gaa(tree(T112, T113, T114), .(T113, T92), X131) → U11_gaa(T112, T113, T114, T92, X131, pdlc24_in_gaa(T112, T92, T116))
U11_gaa(T112, T113, T114, T92, X131, pdlc24_out_gaa(T112, T92, T116)) → U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_in_gaa(T114, T116, X131))
U12_gaa(T112, T113, T114, T92, X131, T116, pdlc24_out_gaa(T114, T116, X131)) → pdlc24_out_gaa(tree(T112, T113, T114), .(T113, T92), X131)
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
pdlc24_in_gaa(x1, x2, x3) = pdlc24_in_gaa(x1)
nil = nil
pdlc24_out_gaa(x1, x2, x3) = pdlc24_out_gaa(x1)
U11_gaa(x1, x2, x3, x4, x5, x6) = U11_gaa(x1, x2, x3, x6)
U12_gaa(x1, x2, x3, x4, x5, x6, x7) = U12_gaa(x1, x2, x3, x7)
PDL3_IN_GA(x1, x2) = PDL3_IN_GA(x1)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)
We have to consider all (P,R,Pi)-chains
(13) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(14) Obligation:
Q DP problem:The TRS P consists of the following rules:
PDL3_IN_GA(tree(T57, T58, T59)) → U2_GA(T57, T58, T59, pdlc24_in_gaa(T57))
U2_GA(T57, T58, T59, pdlc24_out_gaa(T57)) → PDL3_IN_GA(T59)
The TRS R consists of the following rules:
pdlc24_in_gaa(nil) → pdlc24_out_gaa(nil)
pdlc24_in_gaa(tree(T112, T113, T114)) → U11_gaa(T112, T113, T114, pdlc24_in_gaa(T112))
U11_gaa(T112, T113, T114, pdlc24_out_gaa(T112)) → U12_gaa(T112, T113, T114, pdlc24_in_gaa(T114))
U12_gaa(T112, T113, T114, pdlc24_out_gaa(T114)) → pdlc24_out_gaa(tree(T112, T113, T114))
The set Q consists of the following terms:
pdlc24_in_gaa(x0)
U11_gaa(x0, x1, x2, x3)
U12_gaa(x0, x1, x2, x3)
We have to consider all (P,Q,R)-chains.
(15) 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:
- U2_GA(T57, T58, T59, pdlc24_out_gaa(T57)) → PDL3_IN_GA(T59)
The graph contains the following edges 3 >= 1 - PDL3_IN_GA(tree(T57, T58, T59)) → U2_GA(T57, T58, T59, pdlc24_in_gaa(T57))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3