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



↳ PROLOG
  ↳ PrologToPiTRSProof

tappend3(nil0, T, T).
tappend3(node3(nil0, X, T2), T1, node3(T1, X, T2)).
tappend3(node3(T1, X, nil0), T2, node3(T1, X, T2)).
tappend3(node3(T1, X, T2), T3, node3(U, X, T2)) :- tappend3(T1, T3, U).
tappend3(node3(T1, X, T2), T3, node3(T1, X, U)) :- tappend3(T2, T3, U).
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, T1), tappend3(T1, T2, T3).


With regard to the inferred argument filtering the predicates were used in the following modes:
goal1: (b)
s2t2: (b,f)
tappend3: (b,f,f)
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, T1))
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, T1)) -> if_goal_1_in_2_g3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
tappend_3_in_gaa3(nil_0, T, T) -> tappend_3_out_gaa3(nil_0, T, T)
tappend_3_in_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T2, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U))
if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T1, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2))
if_goal_1_in_2_g3(X, T1, tappend_3_out_gaa3(T1, T2, T3)) -> 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)
tappend_3_in_gaa3(x1, x2, x3)  =  tappend_3_in_gaa1(x1)
tappend_3_out_gaa3(x1, x2, x3)  =  tappend_3_out_gaa
if_tappend_3_in_1_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_1_gaa1(x6)
if_tappend_3_in_2_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_2_gaa1(x6)
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, T1))
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, T1)) -> if_goal_1_in_2_g3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
tappend_3_in_gaa3(nil_0, T, T) -> tappend_3_out_gaa3(nil_0, T, T)
tappend_3_in_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T2, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U))
if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T1, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2))
if_goal_1_in_2_g3(X, T1, tappend_3_out_gaa3(T1, T2, T3)) -> 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)
tappend_3_in_gaa3(x1, x2, x3)  =  tappend_3_in_gaa1(x1)
tappend_3_out_gaa3(x1, x2, x3)  =  tappend_3_out_gaa
if_tappend_3_in_1_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_1_gaa1(x6)
if_tappend_3_in_2_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_2_gaa1(x6)
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, T1))
GOAL_1_IN_G1(X) -> S2T_2_IN_GA2(X, T1)
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, T1)) -> IF_GOAL_1_IN_2_G3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
IF_GOAL_1_IN_1_G2(X, s2t_2_out_ga2(X, T1)) -> TAPPEND_3_IN_GAA3(T1, T2, T3)
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> IF_TAPPEND_3_IN_1_GAA6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> TAPPEND_3_IN_GAA3(T1, T3, U)
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> IF_TAPPEND_3_IN_2_GAA6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> TAPPEND_3_IN_GAA3(T2, T3, U)

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, T1))
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, T1)) -> if_goal_1_in_2_g3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
tappend_3_in_gaa3(nil_0, T, T) -> tappend_3_out_gaa3(nil_0, T, T)
tappend_3_in_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T2, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U))
if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T1, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2))
if_goal_1_in_2_g3(X, T1, tappend_3_out_gaa3(T1, T2, T3)) -> 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)
tappend_3_in_gaa3(x1, x2, x3)  =  tappend_3_in_gaa1(x1)
tappend_3_out_gaa3(x1, x2, x3)  =  tappend_3_out_gaa
if_tappend_3_in_1_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_1_gaa1(x6)
if_tappend_3_in_2_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_2_gaa1(x6)
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_TAPPEND_3_IN_1_GAA6(x1, x2, x3, x4, x5, x6)  =  IF_TAPPEND_3_IN_1_GAA1(x6)
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)
TAPPEND_3_IN_GAA3(x1, x2, x3)  =  TAPPEND_3_IN_GAA1(x1)
IF_TAPPEND_3_IN_2_GAA6(x1, x2, x3, x4, x5, x6)  =  IF_TAPPEND_3_IN_2_GAA1(x6)
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, T1))
GOAL_1_IN_G1(X) -> S2T_2_IN_GA2(X, T1)
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, T1)) -> IF_GOAL_1_IN_2_G3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
IF_GOAL_1_IN_1_G2(X, s2t_2_out_ga2(X, T1)) -> TAPPEND_3_IN_GAA3(T1, T2, T3)
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> IF_TAPPEND_3_IN_1_GAA6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> TAPPEND_3_IN_GAA3(T1, T3, U)
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> IF_TAPPEND_3_IN_2_GAA6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> TAPPEND_3_IN_GAA3(T2, T3, U)

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, T1))
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, T1)) -> if_goal_1_in_2_g3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
tappend_3_in_gaa3(nil_0, T, T) -> tappend_3_out_gaa3(nil_0, T, T)
tappend_3_in_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T2, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U))
if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T1, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2))
if_goal_1_in_2_g3(X, T1, tappend_3_out_gaa3(T1, T2, T3)) -> 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)
tappend_3_in_gaa3(x1, x2, x3)  =  tappend_3_in_gaa1(x1)
tappend_3_out_gaa3(x1, x2, x3)  =  tappend_3_out_gaa
if_tappend_3_in_1_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_1_gaa1(x6)
if_tappend_3_in_2_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_2_gaa1(x6)
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_TAPPEND_3_IN_1_GAA6(x1, x2, x3, x4, x5, x6)  =  IF_TAPPEND_3_IN_1_GAA1(x6)
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)
TAPPEND_3_IN_GAA3(x1, x2, x3)  =  TAPPEND_3_IN_GAA1(x1)
IF_TAPPEND_3_IN_2_GAA6(x1, x2, x3, x4, x5, x6)  =  IF_TAPPEND_3_IN_2_GAA1(x6)
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 9 less nodes.

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

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

TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> TAPPEND_3_IN_GAA3(T1, T3, U)
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> TAPPEND_3_IN_GAA3(T2, T3, U)

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, T1))
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, T1)) -> if_goal_1_in_2_g3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
tappend_3_in_gaa3(nil_0, T, T) -> tappend_3_out_gaa3(nil_0, T, T)
tappend_3_in_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T2, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U))
if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T1, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2))
if_goal_1_in_2_g3(X, T1, tappend_3_out_gaa3(T1, T2, T3)) -> 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)
tappend_3_in_gaa3(x1, x2, x3)  =  tappend_3_in_gaa1(x1)
tappend_3_out_gaa3(x1, x2, x3)  =  tappend_3_out_gaa
if_tappend_3_in_1_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_1_gaa1(x6)
if_tappend_3_in_2_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_2_gaa1(x6)
goal_1_out_g1(x1)  =  goal_1_out_g
TAPPEND_3_IN_GAA3(x1, x2, x3)  =  TAPPEND_3_IN_GAA1(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
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> TAPPEND_3_IN_GAA3(T1, T3, U)
TAPPEND_3_IN_GAA3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> TAPPEND_3_IN_GAA3(T2, T3, U)

R is empty.
The argument filtering Pi contains the following mapping:
node_33(x1, x2, x3)  =  node_32(x1, x3)
TAPPEND_3_IN_GAA3(x1, x2, x3)  =  TAPPEND_3_IN_GAA1(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
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

TAPPEND_3_IN_GAA1(node_32(T1, T2)) -> TAPPEND_3_IN_GAA1(T1)
TAPPEND_3_IN_GAA1(node_32(T1, T2)) -> TAPPEND_3_IN_GAA1(T2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TAPPEND_3_IN_GAA1}.
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, T1))
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, T1)) -> if_goal_1_in_2_g3(X, T1, tappend_3_in_gaa3(T1, T2, T3))
tappend_3_in_gaa3(nil_0, T, T) -> tappend_3_out_gaa3(nil_0, T, T)
tappend_3_in_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(nil_0, X, T2), T1, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2)) -> tappend_3_out_gaa3(node_33(T1, X, nil_0), T2, node_33(T1, X, T2))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2)) -> if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T1, T3, U))
tappend_3_in_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U)) -> if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_in_gaa3(T2, T3, U))
if_tappend_3_in_2_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T2, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(T1, X, U))
if_tappend_3_in_1_gaa6(T1, X, T2, T3, U, tappend_3_out_gaa3(T1, T3, U)) -> tappend_3_out_gaa3(node_33(T1, X, T2), T3, node_33(U, X, T2))
if_goal_1_in_2_g3(X, T1, tappend_3_out_gaa3(T1, T2, T3)) -> 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)
tappend_3_in_gaa3(x1, x2, x3)  =  tappend_3_in_gaa1(x1)
tappend_3_out_gaa3(x1, x2, x3)  =  tappend_3_out_gaa
if_tappend_3_in_1_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_1_gaa1(x6)
if_tappend_3_in_2_gaa6(x1, x2, x3, x4, x5, x6)  =  if_tappend_3_in_2_gaa1(x6)
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: