Left Termination of the query pattern preorder(b,f) w.r.t. the given Prolog program could successfully be proven:



↳ PROLOG
  ↳ PrologToPiTRSProof

preorder2(T, Xs) :- preorderdl2(T, Xs - {}0).
preorderdl2(nil0, X - X).
preorderdl2(tree3(L, X, R), .2(X, Xs) - Zs) :- preorderdl2(L, Xs - Ys), preorderdl2(R, Ys - Zs).


With regard to the inferred argument filtering the predicates were used in the following modes:
preorder2: (b,f)
preorder_dl2: (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


preorder_2_in_ga2(T, Xs) -> if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
preorder_dl_2_in_gg2(nil_0, -2(X, X)) -> preorder_dl_2_out_gg2(nil_0, -2(X, X))
preorder_dl_2_in_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_out_gg2(R, -2(Ys, Zs))) -> preorder_dl_2_out_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs))
if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_out_gg2(T, -2(Xs, []_0))) -> preorder_2_out_ga2(T, Xs)

The argument filtering Pi contains the following mapping:
preorder_2_in_ga2(x1, x2)  =  preorder_2_in_ga1(x1)
-2(x1, x2)  =  -
[]_0  =  []_0
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
._22(x1, x2)  =  ._22(x1, x2)
if_preorder_2_in_1_ga3(x1, x2, x3)  =  if_preorder_2_in_1_ga1(x3)
preorder_dl_2_in_gg2(x1, x2)  =  preorder_dl_2_in_gg2(x1, x2)
preorder_dl_2_out_gg2(x1, x2)  =  preorder_dl_2_out_gg
if_preorder_dl_2_in_1_gg6(x1, x2, x3, x4, x5, x6)  =  if_preorder_dl_2_in_1_gg2(x3, x6)
if_preorder_dl_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_preorder_dl_2_in_2_gg1(x7)
preorder_2_out_ga2(x1, x2)  =  preorder_2_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

preorder_2_in_ga2(T, Xs) -> if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
preorder_dl_2_in_gg2(nil_0, -2(X, X)) -> preorder_dl_2_out_gg2(nil_0, -2(X, X))
preorder_dl_2_in_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_out_gg2(R, -2(Ys, Zs))) -> preorder_dl_2_out_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs))
if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_out_gg2(T, -2(Xs, []_0))) -> preorder_2_out_ga2(T, Xs)

The argument filtering Pi contains the following mapping:
preorder_2_in_ga2(x1, x2)  =  preorder_2_in_ga1(x1)
-2(x1, x2)  =  -
[]_0  =  []_0
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
._22(x1, x2)  =  ._22(x1, x2)
if_preorder_2_in_1_ga3(x1, x2, x3)  =  if_preorder_2_in_1_ga1(x3)
preorder_dl_2_in_gg2(x1, x2)  =  preorder_dl_2_in_gg2(x1, x2)
preorder_dl_2_out_gg2(x1, x2)  =  preorder_dl_2_out_gg
if_preorder_dl_2_in_1_gg6(x1, x2, x3, x4, x5, x6)  =  if_preorder_dl_2_in_1_gg2(x3, x6)
if_preorder_dl_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_preorder_dl_2_in_2_gg1(x7)
preorder_2_out_ga2(x1, x2)  =  preorder_2_out_ga


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

PREORDER_2_IN_GA2(T, Xs) -> IF_PREORDER_2_IN_1_GA3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
PREORDER_2_IN_GA2(T, Xs) -> PREORDER_DL_2_IN_GG2(T, -2(Xs, []_0))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> PREORDER_DL_2_IN_GG2(L, -2(Xs, Ys))
IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> IF_PREORDER_DL_2_IN_2_GG7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> PREORDER_DL_2_IN_GG2(R, -2(Ys, Zs))

The TRS R consists of the following rules:

preorder_2_in_ga2(T, Xs) -> if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
preorder_dl_2_in_gg2(nil_0, -2(X, X)) -> preorder_dl_2_out_gg2(nil_0, -2(X, X))
preorder_dl_2_in_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_out_gg2(R, -2(Ys, Zs))) -> preorder_dl_2_out_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs))
if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_out_gg2(T, -2(Xs, []_0))) -> preorder_2_out_ga2(T, Xs)

The argument filtering Pi contains the following mapping:
preorder_2_in_ga2(x1, x2)  =  preorder_2_in_ga1(x1)
-2(x1, x2)  =  -
[]_0  =  []_0
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
._22(x1, x2)  =  ._22(x1, x2)
if_preorder_2_in_1_ga3(x1, x2, x3)  =  if_preorder_2_in_1_ga1(x3)
preorder_dl_2_in_gg2(x1, x2)  =  preorder_dl_2_in_gg2(x1, x2)
preorder_dl_2_out_gg2(x1, x2)  =  preorder_dl_2_out_gg
if_preorder_dl_2_in_1_gg6(x1, x2, x3, x4, x5, x6)  =  if_preorder_dl_2_in_1_gg2(x3, x6)
if_preorder_dl_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_preorder_dl_2_in_2_gg1(x7)
preorder_2_out_ga2(x1, x2)  =  preorder_2_out_ga
IF_PREORDER_2_IN_1_GA3(x1, x2, x3)  =  IF_PREORDER_2_IN_1_GA1(x3)
IF_PREORDER_DL_2_IN_1_GG6(x1, x2, x3, x4, x5, x6)  =  IF_PREORDER_DL_2_IN_1_GG2(x3, x6)
PREORDER_DL_2_IN_GG2(x1, x2)  =  PREORDER_DL_2_IN_GG2(x1, x2)
PREORDER_2_IN_GA2(x1, x2)  =  PREORDER_2_IN_GA1(x1)
IF_PREORDER_DL_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_PREORDER_DL_2_IN_2_GG1(x7)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

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

PREORDER_2_IN_GA2(T, Xs) -> IF_PREORDER_2_IN_1_GA3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
PREORDER_2_IN_GA2(T, Xs) -> PREORDER_DL_2_IN_GG2(T, -2(Xs, []_0))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> PREORDER_DL_2_IN_GG2(L, -2(Xs, Ys))
IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> IF_PREORDER_DL_2_IN_2_GG7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> PREORDER_DL_2_IN_GG2(R, -2(Ys, Zs))

The TRS R consists of the following rules:

preorder_2_in_ga2(T, Xs) -> if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
preorder_dl_2_in_gg2(nil_0, -2(X, X)) -> preorder_dl_2_out_gg2(nil_0, -2(X, X))
preorder_dl_2_in_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_out_gg2(R, -2(Ys, Zs))) -> preorder_dl_2_out_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs))
if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_out_gg2(T, -2(Xs, []_0))) -> preorder_2_out_ga2(T, Xs)

The argument filtering Pi contains the following mapping:
preorder_2_in_ga2(x1, x2)  =  preorder_2_in_ga1(x1)
-2(x1, x2)  =  -
[]_0  =  []_0
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
._22(x1, x2)  =  ._22(x1, x2)
if_preorder_2_in_1_ga3(x1, x2, x3)  =  if_preorder_2_in_1_ga1(x3)
preorder_dl_2_in_gg2(x1, x2)  =  preorder_dl_2_in_gg2(x1, x2)
preorder_dl_2_out_gg2(x1, x2)  =  preorder_dl_2_out_gg
if_preorder_dl_2_in_1_gg6(x1, x2, x3, x4, x5, x6)  =  if_preorder_dl_2_in_1_gg2(x3, x6)
if_preorder_dl_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_preorder_dl_2_in_2_gg1(x7)
preorder_2_out_ga2(x1, x2)  =  preorder_2_out_ga
IF_PREORDER_2_IN_1_GA3(x1, x2, x3)  =  IF_PREORDER_2_IN_1_GA1(x3)
IF_PREORDER_DL_2_IN_1_GG6(x1, x2, x3, x4, x5, x6)  =  IF_PREORDER_DL_2_IN_1_GG2(x3, x6)
PREORDER_DL_2_IN_GG2(x1, x2)  =  PREORDER_DL_2_IN_GG2(x1, x2)
PREORDER_2_IN_GA2(x1, x2)  =  PREORDER_2_IN_GA1(x1)
IF_PREORDER_DL_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_PREORDER_DL_2_IN_2_GG1(x7)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 3 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof

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

IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> PREORDER_DL_2_IN_GG2(R, -2(Ys, Zs))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> PREORDER_DL_2_IN_GG2(L, -2(Xs, Ys))

The TRS R consists of the following rules:

preorder_2_in_ga2(T, Xs) -> if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_in_gg2(T, -2(Xs, []_0)))
preorder_dl_2_in_gg2(nil_0, -2(X, X)) -> preorder_dl_2_out_gg2(nil_0, -2(X, X))
preorder_dl_2_in_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_out_gg2(R, -2(Ys, Zs))) -> preorder_dl_2_out_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs))
if_preorder_2_in_1_ga3(T, Xs, preorder_dl_2_out_gg2(T, -2(Xs, []_0))) -> preorder_2_out_ga2(T, Xs)

The argument filtering Pi contains the following mapping:
preorder_2_in_ga2(x1, x2)  =  preorder_2_in_ga1(x1)
-2(x1, x2)  =  -
[]_0  =  []_0
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
._22(x1, x2)  =  ._22(x1, x2)
if_preorder_2_in_1_ga3(x1, x2, x3)  =  if_preorder_2_in_1_ga1(x3)
preorder_dl_2_in_gg2(x1, x2)  =  preorder_dl_2_in_gg2(x1, x2)
preorder_dl_2_out_gg2(x1, x2)  =  preorder_dl_2_out_gg
if_preorder_dl_2_in_1_gg6(x1, x2, x3, x4, x5, x6)  =  if_preorder_dl_2_in_1_gg2(x3, x6)
if_preorder_dl_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_preorder_dl_2_in_2_gg1(x7)
preorder_2_out_ga2(x1, x2)  =  preorder_2_out_ga
IF_PREORDER_DL_2_IN_1_GG6(x1, x2, x3, x4, x5, x6)  =  IF_PREORDER_DL_2_IN_1_GG2(x3, x6)
PREORDER_DL_2_IN_GG2(x1, x2)  =  PREORDER_DL_2_IN_GG2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof

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

IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> PREORDER_DL_2_IN_GG2(R, -2(Ys, Zs))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> IF_PREORDER_DL_2_IN_1_GG6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> PREORDER_DL_2_IN_GG2(L, -2(Xs, Ys))

The TRS R consists of the following rules:

preorder_dl_2_in_gg2(nil_0, -2(X, X)) -> preorder_dl_2_out_gg2(nil_0, -2(X, X))
preorder_dl_2_in_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs)) -> if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_in_gg2(L, -2(Xs, Ys)))
if_preorder_dl_2_in_1_gg6(L, X, R, Xs, Zs, preorder_dl_2_out_gg2(L, -2(Xs, Ys))) -> if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_in_gg2(R, -2(Ys, Zs)))
if_preorder_dl_2_in_2_gg7(L, X, R, Xs, Zs, Ys, preorder_dl_2_out_gg2(R, -2(Ys, Zs))) -> preorder_dl_2_out_gg2(tree_33(L, X, R), -2(._22(X, Xs), Zs))

The argument filtering Pi contains the following mapping:
-2(x1, x2)  =  -
nil_0  =  nil_0
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
._22(x1, x2)  =  ._22(x1, x2)
preorder_dl_2_in_gg2(x1, x2)  =  preorder_dl_2_in_gg2(x1, x2)
preorder_dl_2_out_gg2(x1, x2)  =  preorder_dl_2_out_gg
if_preorder_dl_2_in_1_gg6(x1, x2, x3, x4, x5, x6)  =  if_preorder_dl_2_in_1_gg2(x3, x6)
if_preorder_dl_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_preorder_dl_2_in_2_gg1(x7)
IF_PREORDER_DL_2_IN_1_GG6(x1, x2, x3, x4, x5, x6)  =  IF_PREORDER_DL_2_IN_1_GG2(x3, x6)
PREORDER_DL_2_IN_GG2(x1, x2)  =  PREORDER_DL_2_IN_GG2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ QDPSizeChangeProof

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

IF_PREORDER_DL_2_IN_1_GG2(R, preorder_dl_2_out_gg) -> PREORDER_DL_2_IN_GG2(R, -)
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -) -> IF_PREORDER_DL_2_IN_1_GG2(R, preorder_dl_2_in_gg2(L, -))
PREORDER_DL_2_IN_GG2(tree_33(L, X, R), -) -> PREORDER_DL_2_IN_GG2(L, -)

The TRS R consists of the following rules:

preorder_dl_2_in_gg2(nil_0, -) -> preorder_dl_2_out_gg
preorder_dl_2_in_gg2(tree_33(L, X, R), -) -> if_preorder_dl_2_in_1_gg2(R, preorder_dl_2_in_gg2(L, -))
if_preorder_dl_2_in_1_gg2(R, preorder_dl_2_out_gg) -> if_preorder_dl_2_in_2_gg1(preorder_dl_2_in_gg2(R, -))
if_preorder_dl_2_in_2_gg1(preorder_dl_2_out_gg) -> preorder_dl_2_out_gg

The set Q consists of the following terms:

preorder_dl_2_in_gg2(x0, x1)
if_preorder_dl_2_in_1_gg2(x0, x1)
if_preorder_dl_2_in_2_gg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {PREORDER_DL_2_IN_GG2, IF_PREORDER_DL_2_IN_1_GG2}.
By using the subterm criterion together with the size-change analysis 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: