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



↳ PROLOG
  ↳ PrologToPiTRSProof

tree1(nil0).
tree1(node3(L, X, R)) :- tree1(L), tree1(R).
s2t2(s1(X), node3(T, Y, T)) :- s2t2(X, T).
s2t2(s1(X), node3(nil0, Y, T)) :- s2t2(X, T).
s2t2(s1(X), node3(T, Y, nil0)) :- s2t2(X, T).
s2t2(s1(X), node3(nil0, Y, nil0)).
s2t2(00, nil0).
goal1(X) :- s2t2(X, T), tree1(T).


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


goal_1_in_g1(X) -> if_goal_1_in_1_g2(X, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, T)) -> if_s2t_2_in_1_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, T)) -> if_s2t_2_in_2_ga4(X, Y, T, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, nil_0)) -> if_s2t_2_in_3_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, nil_0)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, nil_0))
s2t_2_in_ga2(0_0, nil_0) -> s2t_2_out_ga2(0_0, nil_0)
if_s2t_2_in_3_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, nil_0))
if_s2t_2_in_2_ga4(X, Y, T, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, T))
if_s2t_2_in_1_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, T))
if_goal_1_in_1_g2(X, s2t_2_out_ga2(X, T)) -> if_goal_1_in_2_g3(X, T, tree_1_in_g1(T))
tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))
if_goal_1_in_2_g3(X, T, tree_1_out_g1(T)) -> goal_1_out_g1(X)

The argument filtering Pi contains the following mapping:
goal_1_in_g1(x1)  =  goal_1_in_g1(x1)
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_goal_1_in_1_g2(x1, x2)  =  if_goal_1_in_1_g1(x2)
s2t_2_in_ga2(x1, x2)  =  s2t_2_in_ga1(x1)
if_s2t_2_in_1_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_1_ga1(x4)
if_s2t_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_2_ga1(x4)
if_s2t_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_3_ga1(x4)
s2t_2_out_ga2(x1, x2)  =  s2t_2_out_ga1(x2)
if_goal_1_in_2_g3(x1, x2, x3)  =  if_goal_1_in_2_g1(x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
goal_1_out_g1(x1)  =  goal_1_out_g

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:

goal_1_in_g1(X) -> if_goal_1_in_1_g2(X, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, T)) -> if_s2t_2_in_1_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, T)) -> if_s2t_2_in_2_ga4(X, Y, T, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, nil_0)) -> if_s2t_2_in_3_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, nil_0)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, nil_0))
s2t_2_in_ga2(0_0, nil_0) -> s2t_2_out_ga2(0_0, nil_0)
if_s2t_2_in_3_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, nil_0))
if_s2t_2_in_2_ga4(X, Y, T, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, T))
if_s2t_2_in_1_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, T))
if_goal_1_in_1_g2(X, s2t_2_out_ga2(X, T)) -> if_goal_1_in_2_g3(X, T, tree_1_in_g1(T))
tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))
if_goal_1_in_2_g3(X, T, tree_1_out_g1(T)) -> goal_1_out_g1(X)

The argument filtering Pi contains the following mapping:
goal_1_in_g1(x1)  =  goal_1_in_g1(x1)
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_goal_1_in_1_g2(x1, x2)  =  if_goal_1_in_1_g1(x2)
s2t_2_in_ga2(x1, x2)  =  s2t_2_in_ga1(x1)
if_s2t_2_in_1_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_1_ga1(x4)
if_s2t_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_2_ga1(x4)
if_s2t_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_3_ga1(x4)
s2t_2_out_ga2(x1, x2)  =  s2t_2_out_ga1(x2)
if_goal_1_in_2_g3(x1, x2, x3)  =  if_goal_1_in_2_g1(x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
goal_1_out_g1(x1)  =  goal_1_out_g


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

GOAL_1_IN_G1(X) -> IF_GOAL_1_IN_1_G2(X, s2t_2_in_ga2(X, T))
GOAL_1_IN_G1(X) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(T, Y, T)) -> IF_S2T_2_IN_1_GA4(X, T, Y, s2t_2_in_ga2(X, T))
S2T_2_IN_GA2(s_11(X), node_33(T, Y, T)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(nil_0, Y, T)) -> IF_S2T_2_IN_2_GA4(X, Y, T, s2t_2_in_ga2(X, T))
S2T_2_IN_GA2(s_11(X), node_33(nil_0, Y, T)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(T, Y, nil_0)) -> IF_S2T_2_IN_3_GA4(X, T, Y, s2t_2_in_ga2(X, T))
S2T_2_IN_GA2(s_11(X), node_33(T, Y, nil_0)) -> S2T_2_IN_GA2(X, T)
IF_GOAL_1_IN_1_G2(X, s2t_2_out_ga2(X, T)) -> IF_GOAL_1_IN_2_G3(X, T, tree_1_in_g1(T))
IF_GOAL_1_IN_1_G2(X, s2t_2_out_ga2(X, T)) -> TREE_1_IN_G1(T)
TREE_1_IN_G1(node_33(L, X, R)) -> IF_TREE_1_IN_1_G4(L, X, R, tree_1_in_g1(L))
TREE_1_IN_G1(node_33(L, X, R)) -> TREE_1_IN_G1(L)
IF_TREE_1_IN_1_G4(L, X, R, tree_1_out_g1(L)) -> IF_TREE_1_IN_2_G4(L, X, R, tree_1_in_g1(R))
IF_TREE_1_IN_1_G4(L, X, R, tree_1_out_g1(L)) -> TREE_1_IN_G1(R)

The TRS R consists of the following rules:

goal_1_in_g1(X) -> if_goal_1_in_1_g2(X, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, T)) -> if_s2t_2_in_1_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, T)) -> if_s2t_2_in_2_ga4(X, Y, T, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, nil_0)) -> if_s2t_2_in_3_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, nil_0)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, nil_0))
s2t_2_in_ga2(0_0, nil_0) -> s2t_2_out_ga2(0_0, nil_0)
if_s2t_2_in_3_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, nil_0))
if_s2t_2_in_2_ga4(X, Y, T, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, T))
if_s2t_2_in_1_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, T))
if_goal_1_in_1_g2(X, s2t_2_out_ga2(X, T)) -> if_goal_1_in_2_g3(X, T, tree_1_in_g1(T))
tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))
if_goal_1_in_2_g3(X, T, tree_1_out_g1(T)) -> goal_1_out_g1(X)

The argument filtering Pi contains the following mapping:
goal_1_in_g1(x1)  =  goal_1_in_g1(x1)
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_goal_1_in_1_g2(x1, x2)  =  if_goal_1_in_1_g1(x2)
s2t_2_in_ga2(x1, x2)  =  s2t_2_in_ga1(x1)
if_s2t_2_in_1_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_1_ga1(x4)
if_s2t_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_2_ga1(x4)
if_s2t_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_3_ga1(x4)
s2t_2_out_ga2(x1, x2)  =  s2t_2_out_ga1(x2)
if_goal_1_in_2_g3(x1, x2, x3)  =  if_goal_1_in_2_g1(x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
goal_1_out_g1(x1)  =  goal_1_out_g
GOAL_1_IN_G1(x1)  =  GOAL_1_IN_G1(x1)
S2T_2_IN_GA2(x1, x2)  =  S2T_2_IN_GA1(x1)
IF_S2T_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2T_2_IN_3_GA1(x4)
IF_TREE_1_IN_2_G4(x1, x2, x3, x4)  =  IF_TREE_1_IN_2_G1(x4)
TREE_1_IN_G1(x1)  =  TREE_1_IN_G1(x1)
IF_GOAL_1_IN_1_G2(x1, x2)  =  IF_GOAL_1_IN_1_G1(x2)
IF_GOAL_1_IN_2_G3(x1, x2, x3)  =  IF_GOAL_1_IN_2_G1(x3)
IF_S2T_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_S2T_2_IN_1_GA1(x4)
IF_TREE_1_IN_1_G4(x1, x2, x3, x4)  =  IF_TREE_1_IN_1_G2(x3, x4)
IF_S2T_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_S2T_2_IN_2_GA1(x4)

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:

GOAL_1_IN_G1(X) -> IF_GOAL_1_IN_1_G2(X, s2t_2_in_ga2(X, T))
GOAL_1_IN_G1(X) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(T, Y, T)) -> IF_S2T_2_IN_1_GA4(X, T, Y, s2t_2_in_ga2(X, T))
S2T_2_IN_GA2(s_11(X), node_33(T, Y, T)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(nil_0, Y, T)) -> IF_S2T_2_IN_2_GA4(X, Y, T, s2t_2_in_ga2(X, T))
S2T_2_IN_GA2(s_11(X), node_33(nil_0, Y, T)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(T, Y, nil_0)) -> IF_S2T_2_IN_3_GA4(X, T, Y, s2t_2_in_ga2(X, T))
S2T_2_IN_GA2(s_11(X), node_33(T, Y, nil_0)) -> S2T_2_IN_GA2(X, T)
IF_GOAL_1_IN_1_G2(X, s2t_2_out_ga2(X, T)) -> IF_GOAL_1_IN_2_G3(X, T, tree_1_in_g1(T))
IF_GOAL_1_IN_1_G2(X, s2t_2_out_ga2(X, T)) -> TREE_1_IN_G1(T)
TREE_1_IN_G1(node_33(L, X, R)) -> IF_TREE_1_IN_1_G4(L, X, R, tree_1_in_g1(L))
TREE_1_IN_G1(node_33(L, X, R)) -> TREE_1_IN_G1(L)
IF_TREE_1_IN_1_G4(L, X, R, tree_1_out_g1(L)) -> IF_TREE_1_IN_2_G4(L, X, R, tree_1_in_g1(R))
IF_TREE_1_IN_1_G4(L, X, R, tree_1_out_g1(L)) -> TREE_1_IN_G1(R)

The TRS R consists of the following rules:

goal_1_in_g1(X) -> if_goal_1_in_1_g2(X, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, T)) -> if_s2t_2_in_1_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, T)) -> if_s2t_2_in_2_ga4(X, Y, T, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, nil_0)) -> if_s2t_2_in_3_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, nil_0)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, nil_0))
s2t_2_in_ga2(0_0, nil_0) -> s2t_2_out_ga2(0_0, nil_0)
if_s2t_2_in_3_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, nil_0))
if_s2t_2_in_2_ga4(X, Y, T, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, T))
if_s2t_2_in_1_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, T))
if_goal_1_in_1_g2(X, s2t_2_out_ga2(X, T)) -> if_goal_1_in_2_g3(X, T, tree_1_in_g1(T))
tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))
if_goal_1_in_2_g3(X, T, tree_1_out_g1(T)) -> goal_1_out_g1(X)

The argument filtering Pi contains the following mapping:
goal_1_in_g1(x1)  =  goal_1_in_g1(x1)
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_goal_1_in_1_g2(x1, x2)  =  if_goal_1_in_1_g1(x2)
s2t_2_in_ga2(x1, x2)  =  s2t_2_in_ga1(x1)
if_s2t_2_in_1_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_1_ga1(x4)
if_s2t_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_2_ga1(x4)
if_s2t_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_3_ga1(x4)
s2t_2_out_ga2(x1, x2)  =  s2t_2_out_ga1(x2)
if_goal_1_in_2_g3(x1, x2, x3)  =  if_goal_1_in_2_g1(x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
goal_1_out_g1(x1)  =  goal_1_out_g
GOAL_1_IN_G1(x1)  =  GOAL_1_IN_G1(x1)
S2T_2_IN_GA2(x1, x2)  =  S2T_2_IN_GA1(x1)
IF_S2T_2_IN_3_GA4(x1, x2, x3, x4)  =  IF_S2T_2_IN_3_GA1(x4)
IF_TREE_1_IN_2_G4(x1, x2, x3, x4)  =  IF_TREE_1_IN_2_G1(x4)
TREE_1_IN_G1(x1)  =  TREE_1_IN_G1(x1)
IF_GOAL_1_IN_1_G2(x1, x2)  =  IF_GOAL_1_IN_1_G1(x2)
IF_GOAL_1_IN_2_G3(x1, x2, x3)  =  IF_GOAL_1_IN_2_G1(x3)
IF_S2T_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_S2T_2_IN_1_GA1(x4)
IF_TREE_1_IN_1_G4(x1, x2, x3, x4)  =  IF_TREE_1_IN_1_G2(x3, x4)
IF_S2T_2_IN_2_GA4(x1, x2, x3, x4)  =  IF_S2T_2_IN_2_GA1(x4)

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

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

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

TREE_1_IN_G1(node_33(L, X, R)) -> TREE_1_IN_G1(L)
TREE_1_IN_G1(node_33(L, X, R)) -> IF_TREE_1_IN_1_G4(L, X, R, tree_1_in_g1(L))
IF_TREE_1_IN_1_G4(L, X, R, tree_1_out_g1(L)) -> TREE_1_IN_G1(R)

The TRS R consists of the following rules:

goal_1_in_g1(X) -> if_goal_1_in_1_g2(X, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, T)) -> if_s2t_2_in_1_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, T)) -> if_s2t_2_in_2_ga4(X, Y, T, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, nil_0)) -> if_s2t_2_in_3_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, nil_0)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, nil_0))
s2t_2_in_ga2(0_0, nil_0) -> s2t_2_out_ga2(0_0, nil_0)
if_s2t_2_in_3_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, nil_0))
if_s2t_2_in_2_ga4(X, Y, T, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, T))
if_s2t_2_in_1_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, T))
if_goal_1_in_1_g2(X, s2t_2_out_ga2(X, T)) -> if_goal_1_in_2_g3(X, T, tree_1_in_g1(T))
tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))
if_goal_1_in_2_g3(X, T, tree_1_out_g1(T)) -> goal_1_out_g1(X)

The argument filtering Pi contains the following mapping:
goal_1_in_g1(x1)  =  goal_1_in_g1(x1)
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_goal_1_in_1_g2(x1, x2)  =  if_goal_1_in_1_g1(x2)
s2t_2_in_ga2(x1, x2)  =  s2t_2_in_ga1(x1)
if_s2t_2_in_1_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_1_ga1(x4)
if_s2t_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_2_ga1(x4)
if_s2t_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_3_ga1(x4)
s2t_2_out_ga2(x1, x2)  =  s2t_2_out_ga1(x2)
if_goal_1_in_2_g3(x1, x2, x3)  =  if_goal_1_in_2_g1(x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
goal_1_out_g1(x1)  =  goal_1_out_g
TREE_1_IN_G1(x1)  =  TREE_1_IN_G1(x1)
IF_TREE_1_IN_1_G4(x1, x2, x3, x4)  =  IF_TREE_1_IN_1_G2(x3, x4)

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
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

TREE_1_IN_G1(node_33(L, X, R)) -> TREE_1_IN_G1(L)
TREE_1_IN_G1(node_33(L, X, R)) -> IF_TREE_1_IN_1_G4(L, X, R, tree_1_in_g1(L))
IF_TREE_1_IN_1_G4(L, X, R, tree_1_out_g1(L)) -> TREE_1_IN_G1(R)

The TRS R consists of the following rules:

tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))

The argument filtering Pi contains the following mapping:
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
TREE_1_IN_G1(x1)  =  TREE_1_IN_G1(x1)
IF_TREE_1_IN_1_G4(x1, x2, x3, x4)  =  IF_TREE_1_IN_1_G2(x3, x4)

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
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

TREE_1_IN_G1(node_32(L, R)) -> TREE_1_IN_G1(L)
TREE_1_IN_G1(node_32(L, R)) -> IF_TREE_1_IN_1_G2(R, tree_1_in_g1(L))
IF_TREE_1_IN_1_G2(R, tree_1_out_g) -> TREE_1_IN_G1(R)

The TRS R consists of the following rules:

tree_1_in_g1(nil_0) -> tree_1_out_g
tree_1_in_g1(node_32(L, R)) -> if_tree_1_in_1_g2(R, tree_1_in_g1(L))
if_tree_1_in_1_g2(R, tree_1_out_g) -> if_tree_1_in_2_g1(tree_1_in_g1(R))
if_tree_1_in_2_g1(tree_1_out_g) -> tree_1_out_g

The set Q consists of the following terms:

tree_1_in_g1(x0)
if_tree_1_in_1_g2(x0, x1)
if_tree_1_in_2_g1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TREE_1_IN_G1, IF_TREE_1_IN_1_G2}.
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: 



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

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

S2T_2_IN_GA2(s_11(X), node_33(T, Y, nil_0)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(nil_0, Y, T)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(T, Y, T)) -> S2T_2_IN_GA2(X, T)

The TRS R consists of the following rules:

goal_1_in_g1(X) -> if_goal_1_in_1_g2(X, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, T)) -> if_s2t_2_in_1_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, T)) -> if_s2t_2_in_2_ga4(X, Y, T, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(T, Y, nil_0)) -> if_s2t_2_in_3_ga4(X, T, Y, s2t_2_in_ga2(X, T))
s2t_2_in_ga2(s_11(X), node_33(nil_0, Y, nil_0)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, nil_0))
s2t_2_in_ga2(0_0, nil_0) -> s2t_2_out_ga2(0_0, nil_0)
if_s2t_2_in_3_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, nil_0))
if_s2t_2_in_2_ga4(X, Y, T, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(nil_0, Y, T))
if_s2t_2_in_1_ga4(X, T, Y, s2t_2_out_ga2(X, T)) -> s2t_2_out_ga2(s_11(X), node_33(T, Y, T))
if_goal_1_in_1_g2(X, s2t_2_out_ga2(X, T)) -> if_goal_1_in_2_g3(X, T, tree_1_in_g1(T))
tree_1_in_g1(nil_0) -> tree_1_out_g1(nil_0)
tree_1_in_g1(node_33(L, X, R)) -> if_tree_1_in_1_g4(L, X, R, tree_1_in_g1(L))
if_tree_1_in_1_g4(L, X, R, tree_1_out_g1(L)) -> if_tree_1_in_2_g4(L, X, R, tree_1_in_g1(R))
if_tree_1_in_2_g4(L, X, R, tree_1_out_g1(R)) -> tree_1_out_g1(node_33(L, X, R))
if_goal_1_in_2_g3(X, T, tree_1_out_g1(T)) -> goal_1_out_g1(X)

The argument filtering Pi contains the following mapping:
goal_1_in_g1(x1)  =  goal_1_in_g1(x1)
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
if_goal_1_in_1_g2(x1, x2)  =  if_goal_1_in_1_g1(x2)
s2t_2_in_ga2(x1, x2)  =  s2t_2_in_ga1(x1)
if_s2t_2_in_1_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_1_ga1(x4)
if_s2t_2_in_2_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_2_ga1(x4)
if_s2t_2_in_3_ga4(x1, x2, x3, x4)  =  if_s2t_2_in_3_ga1(x4)
s2t_2_out_ga2(x1, x2)  =  s2t_2_out_ga1(x2)
if_goal_1_in_2_g3(x1, x2, x3)  =  if_goal_1_in_2_g1(x3)
tree_1_in_g1(x1)  =  tree_1_in_g1(x1)
tree_1_out_g1(x1)  =  tree_1_out_g
if_tree_1_in_1_g4(x1, x2, x3, x4)  =  if_tree_1_in_1_g2(x3, x4)
if_tree_1_in_2_g4(x1, x2, x3, x4)  =  if_tree_1_in_2_g1(x4)
goal_1_out_g1(x1)  =  goal_1_out_g
S2T_2_IN_GA2(x1, x2)  =  S2T_2_IN_GA1(x1)

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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

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

S2T_2_IN_GA2(s_11(X), node_33(T, Y, nil_0)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(nil_0, Y, T)) -> S2T_2_IN_GA2(X, T)
S2T_2_IN_GA2(s_11(X), node_33(T, Y, T)) -> S2T_2_IN_GA2(X, T)

R is empty.
The argument filtering Pi contains the following mapping:
nil_0  =  nil_0
node_33(x1, x2, x3)  =  node_32(x1, x3)
s_11(x1)  =  s_11(x1)
S2T_2_IN_GA2(x1, x2)  =  S2T_2_IN_GA1(x1)

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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

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

S2T_2_IN_GA1(s_11(X)) -> S2T_2_IN_GA1(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {S2T_2_IN_GA1}.
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: