Left Termination of the query pattern preorder_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇐)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇐)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔)
        ↳22 YES

(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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

preorder_dl3(nil, []).
preorder_dl3(tree(T21, T22, T23), .(T22, T25)) :- preorder_dl12(T21, T25, X27).
preorder_dl3(tree(T21, T22, T23), .(T22, T25)) :- ','(preorder_dl12(T21, T25, T28), preorder_dl3(T23, T28)).
preorder_dl12(nil, T35, T35).
preorder_dl12(tree(T44, T45, T46), .(T45, T48), X62) :- preorder_dl12(T44, T48, X61).
preorder_dl12(tree(T44, T45, T46), .(T45, T48), X62) :- ','(preorder_dl12(T44, T48, T51), preorder_dl12(T46, T51, X62)).
preorder1(T5, T7) :- preorder_dl3(T5, T7).

Queries:

preorder1(g,a).

(3) PrologToPiTRSProof (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)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

preorder1_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dl3_in_ga(T5, T7))
preorder_dl3_in_ga(nil, []) → preorder_dl3_out_ga(nil, [])
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U1_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, X27)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dl3_out_ga(T23, T28)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dl3_out_ga(T5, T7)) → preorder1_out_ga(T5, T7)

The argument filtering Pi contains the following mapping:
preorder1_in_ga(x1, x2)  =  preorder1_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
preorder_dl3_in_ga(x1, x2)  =  preorder_dl3_in_ga(x1)
nil  =  nil
preorder_dl3_out_ga(x1, x2)  =  preorder_dl3_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x3, x5)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
preorder1_out_ga(x1, x2)  =  preorder1_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

preorder1_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dl3_in_ga(T5, T7))
preorder_dl3_in_ga(nil, []) → preorder_dl3_out_ga(nil, [])
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U1_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, X27)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dl3_out_ga(T23, T28)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dl3_out_ga(T5, T7)) → preorder1_out_ga(T5, T7)

The argument filtering Pi contains the following mapping:
preorder1_in_ga(x1, x2)  =  preorder1_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
preorder_dl3_in_ga(x1, x2)  =  preorder_dl3_in_ga(x1)
nil  =  nil
preorder_dl3_out_ga(x1, x2)  =  preorder_dl3_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x3, x5)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
preorder1_out_ga(x1, x2)  =  preorder1_out_ga

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
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_dl12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dl12_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_dl12_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_dl12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_GA(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U2_GA(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)

The TRS R consists of the following rules:

preorder1_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dl3_in_ga(T5, T7))
preorder_dl3_in_ga(nil, []) → preorder_dl3_out_ga(nil, [])
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U1_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, X27)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dl3_out_ga(T23, T28)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dl3_out_ga(T5, T7)) → preorder1_out_ga(T5, T7)

The argument filtering Pi contains the following mapping:
preorder1_in_ga(x1, x2)  =  preorder1_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
preorder_dl3_in_ga(x1, x2)  =  preorder_dl3_in_ga(x1)
nil  =  nil
preorder_dl3_out_ga(x1, x2)  =  preorder_dl3_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x3, x5)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
preorder1_out_ga(x1, x2)  =  preorder1_out_ga
PREORDER1_IN_GA(x1, x2)  =  PREORDER1_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
PREORDER_DL3_IN_GA(x1, x2)  =  PREORDER_DL3_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x5)
PREORDER_DL12_IN_GAA(x1, x2, x3)  =  PREORDER_DL12_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6)  =  U4_GAA(x6)
U5_GAA(x1, x2, x3, x4, x5, x6)  =  U5_GAA(x3, x6)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x6)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x3, x5)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x5)

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

(6) 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_dl12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dl12_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_dl12_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_dl12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_GA(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U2_GA(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)

The TRS R consists of the following rules:

preorder1_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dl3_in_ga(T5, T7))
preorder_dl3_in_ga(nil, []) → preorder_dl3_out_ga(nil, [])
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U1_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, X27)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dl3_out_ga(T23, T28)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dl3_out_ga(T5, T7)) → preorder1_out_ga(T5, T7)

The argument filtering Pi contains the following mapping:
preorder1_in_ga(x1, x2)  =  preorder1_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
preorder_dl3_in_ga(x1, x2)  =  preorder_dl3_in_ga(x1)
nil  =  nil
preorder_dl3_out_ga(x1, x2)  =  preorder_dl3_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x3, x5)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
preorder1_out_ga(x1, x2)  =  preorder1_out_ga
PREORDER1_IN_GA(x1, x2)  =  PREORDER1_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
PREORDER_DL3_IN_GA(x1, x2)  =  PREORDER_DL3_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x5)
PREORDER_DL12_IN_GAA(x1, x2, x3)  =  PREORDER_DL12_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6)  =  U4_GAA(x6)
U5_GAA(x1, x2, x3, x4, x5, x6)  =  U5_GAA(x3, x6)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x6)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x3, x5)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.

(8) Complex Obligation (AND)

(9) 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_dl12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dl12_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:

preorder1_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dl3_in_ga(T5, T7))
preorder_dl3_in_ga(nil, []) → preorder_dl3_out_ga(nil, [])
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U1_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, X27)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dl3_out_ga(T23, T28)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dl3_out_ga(T5, T7)) → preorder1_out_ga(T5, T7)

The argument filtering Pi contains the following mapping:
preorder1_in_ga(x1, x2)  =  preorder1_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
preorder_dl3_in_ga(x1, x2)  =  preorder_dl3_in_ga(x1)
nil  =  nil
preorder_dl3_out_ga(x1, x2)  =  preorder_dl3_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x3, x5)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
preorder1_out_ga(x1, x2)  =  preorder1_out_ga
PREORDER_DL12_IN_GAA(x1, x2, x3)  =  PREORDER_DL12_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4, x5, x6)  =  U5_GAA(x3, x6)

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) 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_dl12_in_gaa(T44, T48, T51))
U5_GAA(T44, T45, T46, T48, X62, preorder_dl12_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_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)

The argument filtering Pi contains the following mapping:
nil  =  nil
tree(x1, x2, x3)  =  tree(x1, x2, x3)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
PREORDER_DL12_IN_GAA(x1, x2, x3)  =  PREORDER_DL12_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4, x5, x6)  =  U5_GAA(x3, x6)

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

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

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

PREORDER_DL12_IN_GAA(tree(T44, T45, T46)) → U5_GAA(T46, preorder_dl12_in_gaa(T44))
U5_GAA(T46, preorder_dl12_out_gaa) → 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_dl12_in_gaa(nil) → preorder_dl12_out_gaa
preorder_dl12_in_gaa(tree(T44, T45, T46)) → U4_gaa(preorder_dl12_in_gaa(T44))
preorder_dl12_in_gaa(tree(T44, T45, T46)) → U5_gaa(T46, preorder_dl12_in_gaa(T44))
U4_gaa(preorder_dl12_out_gaa) → preorder_dl12_out_gaa
U5_gaa(T46, preorder_dl12_out_gaa) → U6_gaa(preorder_dl12_in_gaa(T46))
U6_gaa(preorder_dl12_out_gaa) → preorder_dl12_out_gaa

The set Q consists of the following terms:

preorder_dl12_in_gaa(x0)
U4_gaa(x0)
U5_gaa(x0, x1)
U6_gaa(x0)

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

(14) 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(T46, preorder_dl12_out_gaa) → PREORDER_DL12_IN_GAA(T46)
    The graph contains the following edges 1 >= 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(T46, preorder_dl12_in_gaa(T44))
    The graph contains the following edges 1 > 1

(15) YES

(16) 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_dl12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)

The TRS R consists of the following rules:

preorder1_in_ga(T5, T7) → U7_ga(T5, T7, preorder_dl3_in_ga(T5, T7))
preorder_dl3_in_ga(nil, []) → preorder_dl3_out_ga(nil, [])
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U1_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, X27))
preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U1_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, X27)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
preorder_dl3_in_ga(tree(T21, T22, T23), .(T22, T25)) → U2_ga(T21, T22, T23, T25, preorder_dl12_in_gaa(T21, T25, T28))
U2_ga(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → U3_ga(T21, T22, T23, T25, preorder_dl3_in_ga(T23, T28))
U3_ga(T21, T22, T23, T25, preorder_dl3_out_ga(T23, T28)) → preorder_dl3_out_ga(tree(T21, T22, T23), .(T22, T25))
U7_ga(T5, T7, preorder_dl3_out_ga(T5, T7)) → preorder1_out_ga(T5, T7)

The argument filtering Pi contains the following mapping:
preorder1_in_ga(x1, x2)  =  preorder1_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
preorder_dl3_in_ga(x1, x2)  =  preorder_dl3_in_ga(x1)
nil  =  nil
preorder_dl3_out_ga(x1, x2)  =  preorder_dl3_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x3, x5)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
preorder1_out_ga(x1, x2)  =  preorder1_out_ga
PREORDER_DL3_IN_GA(x1, x2)  =  PREORDER_DL3_IN_GA(x1)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x3, x5)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) 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_dl12_in_gaa(T21, T25, T28))
U2_GA(T21, T22, T23, T25, preorder_dl12_out_gaa(T21, T25, T28)) → PREORDER_DL3_IN_GA(T23, T28)

The TRS R consists of the following rules:

preorder_dl12_in_gaa(nil, T35, T35) → preorder_dl12_out_gaa(nil, T35, T35)
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) → U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T44, T48, T51))
U4_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, X61)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)
U5_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T44, T48, T51)) → U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_in_gaa(T46, T51, X62))
U6_gaa(T44, T45, T46, T48, X62, preorder_dl12_out_gaa(T46, T51, X62)) → preorder_dl12_out_gaa(tree(T44, T45, T46), .(T45, T48), X62)

The argument filtering Pi contains the following mapping:
nil  =  nil
tree(x1, x2, x3)  =  tree(x1, x2, x3)
preorder_dl12_in_gaa(x1, x2, x3)  =  preorder_dl12_in_gaa(x1)
preorder_dl12_out_gaa(x1, x2, x3)  =  preorder_dl12_out_gaa
U4_gaa(x1, x2, x3, x4, x5, x6)  =  U4_gaa(x6)
U5_gaa(x1, x2, x3, x4, x5, x6)  =  U5_gaa(x3, x6)
U6_gaa(x1, x2, x3, x4, x5, x6)  =  U6_gaa(x6)
PREORDER_DL3_IN_GA(x1, x2)  =  PREORDER_DL3_IN_GA(x1)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x3, x5)

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

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

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

PREORDER_DL3_IN_GA(tree(T21, T22, T23)) → U2_GA(T23, preorder_dl12_in_gaa(T21))
U2_GA(T23, preorder_dl12_out_gaa) → PREORDER_DL3_IN_GA(T23)

The TRS R consists of the following rules:

preorder_dl12_in_gaa(nil) → preorder_dl12_out_gaa
preorder_dl12_in_gaa(tree(T44, T45, T46)) → U4_gaa(preorder_dl12_in_gaa(T44))
preorder_dl12_in_gaa(tree(T44, T45, T46)) → U5_gaa(T46, preorder_dl12_in_gaa(T44))
U4_gaa(preorder_dl12_out_gaa) → preorder_dl12_out_gaa
U5_gaa(T46, preorder_dl12_out_gaa) → U6_gaa(preorder_dl12_in_gaa(T46))
U6_gaa(preorder_dl12_out_gaa) → preorder_dl12_out_gaa

The set Q consists of the following terms:

preorder_dl12_in_gaa(x0)
U4_gaa(x0)
U5_gaa(x0, x1)
U6_gaa(x0)

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

(21) 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(T23, preorder_dl12_out_gaa) → PREORDER_DL3_IN_GA(T23)
    The graph contains the following edges 1 >= 1

  • PREORDER_DL3_IN_GA(tree(T21, T22, T23)) → U2_GA(T23, preorder_dl12_in_gaa(T21))
    The graph contains the following edges 1 > 1

(22) YES