(0) Obligation:
Clauses:preorder(T, Xs) :- preorder_dl(T, -(Xs, [])).
preorder_dl(nil, -(X, X)).
preorder_dl(tree(L, X, R), -(.(X, Xs), Zs)) :- ','(preorder_dl(L, -(Xs, Ys)), preorder_dl(R, -(Ys, Zs))).
Queries:
preorder(g,a).
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph.
(2) Obligation:
Triples:preorder_dl3(tree(T21, T22, T23), .(T22, T25)) :- preorder_dl12(T21, T25, X27).
preorder_dl3(tree(T21, T22, T23), .(T22, T25)) :- ','(preorder_dlc12(T21, T25, T28), preorder_dl3(T23, T28)).
preorder_dl12(tree(T44, T45, T46), .(T45, T48), X62) :- preorder_dl12(T44, T48, X61).
preorder_dl12(tree(T44, T45, T46), .(T45, T48), X62) :- ','(preorder_dlc12(T44, T48, T51), preorder_dl12(T46, T51, X62)).
preorder1(T5, T7) :- preorder_dl3(T5, T7).
Clauses:
preorder_dlc3(nil, []).
preorder_dlc3(tree(T21, T22, T23), .(T22, T25)) :- ','(preorder_dlc12(T21, T25, T28), preorder_dlc3(T23, T28)).
preorder_dlc12(nil, T35, T35).
preorder_dlc12(tree(T44, T45, T46), .(T45, T48), X62) :- ','(preorder_dlc12(T44, T48, T51), preorder_dlc12(T46, T51, X62)).
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)
preorder_dl3_in: (b,f)
preorder_dl12_in: (b,f,f)
preorder_dlc12_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, preorder_dl3_in_ga(T5, T7))
PREORDER1_IN_GA(T5, T7) → PREORDER_DL3_IN_GA(T5, T7)
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U1_GA(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PREORDER_DL12_IN_GAA(T21, T25, X27)
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → U4_GAA(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, X61))
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → PREORDER_DL12_IN_GAA(T44, T48, X61)
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → U6_GAA(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → PREORDER_DL12_IN_GAA(T46, T51, X62)
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlc12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlc12_out_gaa(T21, T25, T28)) → U3_GA(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U2_GA(T21, T22, T23, T25, preorder_dlc12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)
The TRS R consists of the following rules:
preorder_dlc12_in_gaa(nil, T35, T35) → preorder_dlc12_out_gaa(nil, T35, T35)
preorder_dlc12_in_gaa(tree(T44, T45, T46), .(T45, T48), X62) → U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_in_gaa(T46, T51, X62))
U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_out_gaa(T46, T51, X62)) → preorder_dlc12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
The argument filtering Pi contains the following mapping:
preorder_dl3_in_ga(x1, x2) = preorder_dl3_in_ga(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
preorder_dl12_in_gaa(x1, x2, x3) = preorder_dl12_in_gaa(x1)
preorder_dlc12_in_gaa(x1, x2, x3) = preorder_dlc12_in_gaa(x1)
nil = nil
preorder_dlc12_out_gaa(x1, x2, x3) = preorder_dlc12_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)
PREORDER_DL3_IN_GA(x1, x2) = PREORDER_DL3_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
PREORDER_DL12_IN_GAA(x1, x2, x3) = PREORDER_DL12_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, preorder_dl3_in_ga(T5, T7))
PREORDER1_IN_GA(T5, T7) → PREORDER_DL3_IN_GA(T5, T7)
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U1_GA(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → PREORDER_DL12_IN_GAA(T21, T25, X27)
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → U4_GAA(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, X61))
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → PREORDER_DL12_IN_GAA(T44, T48, X61)
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → U6_GAA(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → PREORDER_DL12_IN_GAA(T46, T51, X62)
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlc12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlc12_out_gaa(T21, T25, T28)) → U3_GA(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U2_GA(T21, T22, T23, T25, preorder_dlc12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)
The TRS R consists of the following rules:
preorder_dlc12_in_gaa(nil, T35, T35) → preorder_dlc12_out_gaa(nil, T35, T35)
preorder_dlc12_in_gaa(tree(T44, T45, T46), .(T45, T48), X62) → U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_in_gaa(T46, T51, X62))
U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_out_gaa(T46, T51, X62)) → preorder_dlc12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
The argument filtering Pi contains the following mapping:
preorder_dl3_in_ga(x1, x2) = preorder_dl3_in_ga(x1)
tree(x1, x2, x3) = tree(x1, x2, x3)
preorder_dl12_in_gaa(x1, x2, x3) = preorder_dl12_in_gaa(x1)
preorder_dlc12_in_gaa(x1, x2, x3) = preorder_dlc12_in_gaa(x1)
nil = nil
preorder_dlc12_out_gaa(x1, x2, x3) = preorder_dlc12_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)
PREORDER_DL3_IN_GA(x1, x2) = PREORDER_DL3_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
PREORDER_DL12_IN_GAA(x1, x2, x3) = PREORDER_DL12_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:
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → PREORDER_DL12_IN_GAA(T46, T51, X62)
PREORDER_DL12_IN_GAA(tree(T44, T45, T46), .(T45, T48), X62) → PREORDER_DL12_IN_GAA(T44, T48, X61)
The TRS R consists of the following rules:
preorder_dlc12_in_gaa(nil, T35, T35) → preorder_dlc12_out_gaa(nil, T35, T35)
preorder_dlc12_in_gaa(tree(T44, T45, T46), .(T45, T48), X62) → U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_in_gaa(T46, T51, X62))
U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_out_gaa(T46, T51, X62)) → preorder_dlc12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
preorder_dlc12_in_gaa(x1, x2, x3) = preorder_dlc12_in_gaa(x1)
nil = nil
preorder_dlc12_out_gaa(x1, x2, x3) = preorder_dlc12_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)
PREORDER_DL12_IN_GAA(x1, x2, x3) = PREORDER_DL12_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:
PREORDER_DL12_IN_GAA(tree(T44, T45, T46)) → U5_GAA(T44, T45, T46, preorder_dlc12_in_gaa(T44))
U5_GAA(T44, T45, T46, preorder_dlc12_out_gaa(T44)) → PREORDER_DL12_IN_GAA(T46)
PREORDER_DL12_IN_GAA(tree(T44, T45, T46)) → PREORDER_DL12_IN_GAA(T44)
The TRS R consists of the following rules:
preorder_dlc12_in_gaa(nil) → preorder_dlc12_out_gaa(nil)
preorder_dlc12_in_gaa(tree(T44, T45, T46)) → U11_gaa(T44, T45, T46, preorder_dlc12_in_gaa(T44))
U11_gaa(T44, T45, T46, preorder_dlc12_out_gaa(T44)) → U12_gaa(T44, T45, T46, preorder_dlc12_in_gaa(T46))
U12_gaa(T44, T45, T46, preorder_dlc12_out_gaa(T46)) → preorder_dlc12_out_gaa(tree(T44, T45, T46))
The set Q consists of the following terms:
preorder_dlc12_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(T44, T45, T46, preorder_dlc12_out_gaa(T44)) → PREORDER_DL12_IN_GAA(T46)
The graph contains the following edges 3 >= 1 - PREORDER_DL12_IN_GAA(tree(T44, T45, T46)) → PREORDER_DL12_IN_GAA(T44)
The graph contains the following edges 1 > 1 - PREORDER_DL12_IN_GAA(tree(T44, T45, T46)) → U5_GAA(T44, T45, T46, preorder_dlc12_in_gaa(T44))
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:
PREORDER_DL3_IN_GA(tree(T21, T22, T23), .(T22, T25)) → U2_GA(T21, T22, T23, T25, preorder_dlc12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dlc12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)
The TRS R consists of the following rules:
preorder_dlc12_in_gaa(nil, T35, T35) → preorder_dlc12_out_gaa(nil, T35, T35)
preorder_dlc12_in_gaa(tree(T44, T45, T46), .(T45, T48), X62) → U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_in_gaa(T44, T48, T51))
U11_gaa(T44, T45, T46, T48, X62, preorder_dlc12_out_gaa(T44, T48, T51)) → U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_in_gaa(T46, T51, X62))
U12_gaa(T44, T45, T46, T48, X62, T51, preorder_dlc12_out_gaa(T46, T51, X62)) → preorder_dlc12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
preorder_dlc12_in_gaa(x1, x2, x3) = preorder_dlc12_in_gaa(x1)
nil = nil
preorder_dlc12_out_gaa(x1, x2, x3) = preorder_dlc12_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)
PREORDER_DL3_IN_GA(x1, x2) = PREORDER_DL3_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:
PREORDER_DL3_IN_GA(tree(T21, T22, T23)) → U2_GA(T21, T22, T23, preorder_dlc12_in_gaa(T21))
U2_GA(T21, T22, T23, preorder_dlc12_out_gaa(T21)) → PREORDER_DL3_IN_GA(T23)
The TRS R consists of the following rules:
preorder_dlc12_in_gaa(nil) → preorder_dlc12_out_gaa(nil)
preorder_dlc12_in_gaa(tree(T44, T45, T46)) → U11_gaa(T44, T45, T46, preorder_dlc12_in_gaa(T44))
U11_gaa(T44, T45, T46, preorder_dlc12_out_gaa(T44)) → U12_gaa(T44, T45, T46, preorder_dlc12_in_gaa(T46))
U12_gaa(T44, T45, T46, preorder_dlc12_out_gaa(T46)) → preorder_dlc12_out_gaa(tree(T44, T45, T46))
The set Q consists of the following terms:
preorder_dlc12_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(T21, T22, T23, preorder_dlc12_out_gaa(T21)) → PREORDER_DL3_IN_GA(T23)
The graph contains the following edges 3 >= 1 - PREORDER_DL3_IN_GA(tree(T21, T22, T23)) → U2_GA(T21, T22, T23, preorder_dlc12_in_gaa(T21))
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3