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



↳ PROLOG
  ↳ PrologToPiTRSProof

sameleaves2(leaf1(L), leaf1(L)).
sameleaves2(tree2(T1, T2), tree2(S1, S2)) :- getleave4(T1, T2, L, T), getleave4(S1, S2, L, S), sameleaves2(T, S).
getleave4(leaf1(A), C, A, C).
getleave4(tree2(A, B), C, L, O) :- getleave4(A, tree2(B, C), L, O).


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


sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)

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:

sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)


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

SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> GETLEAVE_4_IN_GGAA4(T1, T2, L, T)
GETLEAVE_4_IN_GGAA4(tree_22(A, B), C, L, O) -> IF_GETLEAVE_4_IN_1_GGAA6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
GETLEAVE_4_IN_GGAA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGAA4(A, tree_22(B, C), L, O)
IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> GETLEAVE_4_IN_GGGA4(S1, S2, L, S)
GETLEAVE_4_IN_GGGA4(tree_22(A, B), C, L, O) -> IF_GETLEAVE_4_IN_1_GGGA6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
GETLEAVE_4_IN_GGGA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGGA4(A, tree_22(B, C), L, O)
IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> IF_SAMELEAVES_2_IN_3_GG7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> SAMELEAVES_2_IN_GG2(T, S)

The TRS R consists of the following rules:

sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)
IF_SAMELEAVES_2_IN_1_GG5(x1, x2, x3, x4, x5)  =  IF_SAMELEAVES_2_IN_1_GG3(x3, x4, x5)
GETLEAVE_4_IN_GGGA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGGA3(x1, x2, x3)
IF_GETLEAVE_4_IN_1_GGGA6(x1, x2, x3, x4, x5, x6)  =  IF_GETLEAVE_4_IN_1_GGGA1(x6)
SAMELEAVES_2_IN_GG2(x1, x2)  =  SAMELEAVES_2_IN_GG2(x1, x2)
IF_GETLEAVE_4_IN_1_GGAA6(x1, x2, x3, x4, x5, x6)  =  IF_GETLEAVE_4_IN_1_GGAA1(x6)
GETLEAVE_4_IN_GGAA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGAA2(x1, x2)
IF_SAMELEAVES_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_SAMELEAVES_2_IN_2_GG2(x6, x7)
IF_SAMELEAVES_2_IN_3_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_SAMELEAVES_2_IN_3_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:

SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> GETLEAVE_4_IN_GGAA4(T1, T2, L, T)
GETLEAVE_4_IN_GGAA4(tree_22(A, B), C, L, O) -> IF_GETLEAVE_4_IN_1_GGAA6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
GETLEAVE_4_IN_GGAA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGAA4(A, tree_22(B, C), L, O)
IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> GETLEAVE_4_IN_GGGA4(S1, S2, L, S)
GETLEAVE_4_IN_GGGA4(tree_22(A, B), C, L, O) -> IF_GETLEAVE_4_IN_1_GGGA6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
GETLEAVE_4_IN_GGGA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGGA4(A, tree_22(B, C), L, O)
IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> IF_SAMELEAVES_2_IN_3_GG7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> SAMELEAVES_2_IN_GG2(T, S)

The TRS R consists of the following rules:

sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)
IF_SAMELEAVES_2_IN_1_GG5(x1, x2, x3, x4, x5)  =  IF_SAMELEAVES_2_IN_1_GG3(x3, x4, x5)
GETLEAVE_4_IN_GGGA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGGA3(x1, x2, x3)
IF_GETLEAVE_4_IN_1_GGGA6(x1, x2, x3, x4, x5, x6)  =  IF_GETLEAVE_4_IN_1_GGGA1(x6)
SAMELEAVES_2_IN_GG2(x1, x2)  =  SAMELEAVES_2_IN_GG2(x1, x2)
IF_GETLEAVE_4_IN_1_GGAA6(x1, x2, x3, x4, x5, x6)  =  IF_GETLEAVE_4_IN_1_GGAA1(x6)
GETLEAVE_4_IN_GGAA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGAA2(x1, x2)
IF_SAMELEAVES_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_SAMELEAVES_2_IN_2_GG2(x6, x7)
IF_SAMELEAVES_2_IN_3_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_SAMELEAVES_2_IN_3_GG1(x7)

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

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

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

GETLEAVE_4_IN_GGGA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGGA4(A, tree_22(B, C), L, O)

The TRS R consists of the following rules:

sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)
GETLEAVE_4_IN_GGGA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGGA3(x1, x2, x3)

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
              ↳ PiDP

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

GETLEAVE_4_IN_GGGA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGGA4(A, tree_22(B, C), L, O)

R is empty.
The argument filtering Pi contains the following mapping:
tree_22(x1, x2)  =  tree_22(x1, x2)
GETLEAVE_4_IN_GGGA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGGA3(x1, x2, x3)

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
              ↳ PiDP

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

GETLEAVE_4_IN_GGGA3(tree_22(A, B), C, L) -> GETLEAVE_4_IN_GGGA3(A, tree_22(B, C), L)

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

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

GETLEAVE_4_IN_GGAA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGAA4(A, tree_22(B, C), L, O)

The TRS R consists of the following rules:

sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)
GETLEAVE_4_IN_GGAA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGAA2(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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

GETLEAVE_4_IN_GGAA4(tree_22(A, B), C, L, O) -> GETLEAVE_4_IN_GGAA4(A, tree_22(B, C), L, O)

R is empty.
The argument filtering Pi contains the following mapping:
tree_22(x1, x2)  =  tree_22(x1, x2)
GETLEAVE_4_IN_GGAA4(x1, x2, x3, x4)  =  GETLEAVE_4_IN_GGAA2(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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

GETLEAVE_4_IN_GGAA2(tree_22(A, B), C) -> GETLEAVE_4_IN_GGAA2(A, tree_22(B, C))

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

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

IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> SAMELEAVES_2_IN_GG2(T, S)

The TRS R consists of the following rules:

sameleaves_2_in_gg2(leaf_11(L), leaf_11(L)) -> sameleaves_2_out_gg2(leaf_11(L), leaf_11(L))
sameleaves_2_in_gg2(tree_22(T1, T2), tree_22(S1, S2)) -> if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_1_gg5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_sameleaves_2_in_2_gg7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_in_gg2(T, S))
if_sameleaves_2_in_3_gg7(T1, T2, S1, S2, T, S, sameleaves_2_out_gg2(T, S)) -> sameleaves_2_out_gg2(tree_22(T1, T2), tree_22(S1, S2))

The argument filtering Pi contains the following mapping:
sameleaves_2_in_gg2(x1, x2)  =  sameleaves_2_in_gg2(x1, x2)
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
sameleaves_2_out_gg2(x1, x2)  =  sameleaves_2_out_gg
if_sameleaves_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_sameleaves_2_in_1_gg3(x3, x4, x5)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
if_sameleaves_2_in_2_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_2_gg2(x6, x7)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
if_sameleaves_2_in_3_gg7(x1, x2, x3, x4, x5, x6, x7)  =  if_sameleaves_2_in_3_gg1(x7)
IF_SAMELEAVES_2_IN_1_GG5(x1, x2, x3, x4, x5)  =  IF_SAMELEAVES_2_IN_1_GG3(x3, x4, x5)
SAMELEAVES_2_IN_GG2(x1, x2)  =  SAMELEAVES_2_IN_GG2(x1, x2)
IF_SAMELEAVES_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_SAMELEAVES_2_IN_2_GG2(x6, x7)

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

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

IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_out_ggaa4(T1, T2, L, T)) -> IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_in_ggga4(S1, S2, L, S))
SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG5(T1, T2, S1, S2, getleave_4_in_ggaa4(T1, T2, L, T))
IF_SAMELEAVES_2_IN_2_GG7(T1, T2, S1, S2, L, T, getleave_4_out_ggga4(S1, S2, L, S)) -> SAMELEAVES_2_IN_GG2(T, S)

The TRS R consists of the following rules:

getleave_4_in_ggga4(leaf_11(A), C, A, C) -> getleave_4_out_ggga4(leaf_11(A), C, A, C)
getleave_4_in_ggga4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_in_ggga4(A, tree_22(B, C), L, O))
getleave_4_in_ggaa4(leaf_11(A), C, A, C) -> getleave_4_out_ggaa4(leaf_11(A), C, A, C)
getleave_4_in_ggaa4(tree_22(A, B), C, L, O) -> if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_in_ggaa4(A, tree_22(B, C), L, O))
if_getleave_4_in_1_ggga6(A, B, C, L, O, getleave_4_out_ggga4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggga4(tree_22(A, B), C, L, O)
if_getleave_4_in_1_ggaa6(A, B, C, L, O, getleave_4_out_ggaa4(A, tree_22(B, C), L, O)) -> getleave_4_out_ggaa4(tree_22(A, B), C, L, O)

The argument filtering Pi contains the following mapping:
leaf_11(x1)  =  leaf_11(x1)
tree_22(x1, x2)  =  tree_22(x1, x2)
getleave_4_in_ggaa4(x1, x2, x3, x4)  =  getleave_4_in_ggaa2(x1, x2)
getleave_4_out_ggaa4(x1, x2, x3, x4)  =  getleave_4_out_ggaa2(x3, x4)
if_getleave_4_in_1_ggaa6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggaa1(x6)
getleave_4_in_ggga4(x1, x2, x3, x4)  =  getleave_4_in_ggga3(x1, x2, x3)
getleave_4_out_ggga4(x1, x2, x3, x4)  =  getleave_4_out_ggga1(x4)
if_getleave_4_in_1_ggga6(x1, x2, x3, x4, x5, x6)  =  if_getleave_4_in_1_ggga1(x6)
IF_SAMELEAVES_2_IN_1_GG5(x1, x2, x3, x4, x5)  =  IF_SAMELEAVES_2_IN_1_GG3(x3, x4, x5)
SAMELEAVES_2_IN_GG2(x1, x2)  =  SAMELEAVES_2_IN_GG2(x1, x2)
IF_SAMELEAVES_2_IN_2_GG7(x1, x2, x3, x4, x5, x6, x7)  =  IF_SAMELEAVES_2_IN_2_GG2(x6, x7)

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

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

IF_SAMELEAVES_2_IN_1_GG3(S1, S2, getleave_4_out_ggaa2(L, T)) -> IF_SAMELEAVES_2_IN_2_GG2(T, getleave_4_in_ggga3(S1, S2, L))
SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG3(S1, S2, getleave_4_in_ggaa2(T1, T2))
IF_SAMELEAVES_2_IN_2_GG2(T, getleave_4_out_ggga1(S)) -> SAMELEAVES_2_IN_GG2(T, S)

The TRS R consists of the following rules:

getleave_4_in_ggga3(leaf_11(A), C, A) -> getleave_4_out_ggga1(C)
getleave_4_in_ggga3(tree_22(A, B), C, L) -> if_getleave_4_in_1_ggga1(getleave_4_in_ggga3(A, tree_22(B, C), L))
getleave_4_in_ggaa2(leaf_11(A), C) -> getleave_4_out_ggaa2(A, C)
getleave_4_in_ggaa2(tree_22(A, B), C) -> if_getleave_4_in_1_ggaa1(getleave_4_in_ggaa2(A, tree_22(B, C)))
if_getleave_4_in_1_ggga1(getleave_4_out_ggga1(O)) -> getleave_4_out_ggga1(O)
if_getleave_4_in_1_ggaa1(getleave_4_out_ggaa2(L, O)) -> getleave_4_out_ggaa2(L, O)

The set Q consists of the following terms:

getleave_4_in_ggga3(x0, x1, x2)
getleave_4_in_ggaa2(x0, x1)
if_getleave_4_in_1_ggga1(x0)
if_getleave_4_in_1_ggaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_SAMELEAVES_2_IN_2_GG2, IF_SAMELEAVES_2_IN_1_GG3, SAMELEAVES_2_IN_GG2}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

IF_SAMELEAVES_2_IN_1_GG3(S1, S2, getleave_4_out_ggaa2(L, T)) -> IF_SAMELEAVES_2_IN_2_GG2(T, getleave_4_in_ggga3(S1, S2, L))
The remaining Dependency Pairs were at least non-strictly be oriented.

SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG3(S1, S2, getleave_4_in_ggaa2(T1, T2))
IF_SAMELEAVES_2_IN_2_GG2(T, getleave_4_out_ggga1(S)) -> SAMELEAVES_2_IN_GG2(T, S)
With the implicit AFS we had to orient the following set of usable rules non-strictly.

getleave_4_in_ggaa2(tree_22(A, B), C) -> if_getleave_4_in_1_ggaa1(getleave_4_in_ggaa2(A, tree_22(B, C)))
getleave_4_in_ggaa2(leaf_11(A), C) -> getleave_4_out_ggaa2(A, C)
if_getleave_4_in_1_ggaa1(getleave_4_out_ggaa2(L, O)) -> getleave_4_out_ggaa2(L, O)
Used ordering: POLO with Polynomial interpretation:

POL(leaf_11(x1)) = 1   
POL(getleave_4_out_ggaa2(x1, x2)) = 1 + x2   
POL(getleave_4_in_ggaa2(x1, x2)) = x1 + x2   
POL(if_getleave_4_in_1_ggga1(x1)) = 0   
POL(tree_22(x1, x2)) = x1 + x2   
POL(IF_SAMELEAVES_2_IN_2_GG2(x1, x2)) = x1   
POL(if_getleave_4_in_1_ggaa1(x1)) = x1   
POL(getleave_4_in_ggga3(x1, x2, x3)) = 0   
POL(getleave_4_out_ggga1(x1)) = 0   
POL(IF_SAMELEAVES_2_IN_1_GG3(x1, x2, x3)) = x3   
POL(SAMELEAVES_2_IN_GG2(x1, x2)) = x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPPoloProof
                          ↳ QDP
                            ↳ DependencyGraphProof

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

SAMELEAVES_2_IN_GG2(tree_22(T1, T2), tree_22(S1, S2)) -> IF_SAMELEAVES_2_IN_1_GG3(S1, S2, getleave_4_in_ggaa2(T1, T2))
IF_SAMELEAVES_2_IN_2_GG2(T, getleave_4_out_ggga1(S)) -> SAMELEAVES_2_IN_GG2(T, S)

The TRS R consists of the following rules:

getleave_4_in_ggga3(leaf_11(A), C, A) -> getleave_4_out_ggga1(C)
getleave_4_in_ggga3(tree_22(A, B), C, L) -> if_getleave_4_in_1_ggga1(getleave_4_in_ggga3(A, tree_22(B, C), L))
getleave_4_in_ggaa2(leaf_11(A), C) -> getleave_4_out_ggaa2(A, C)
getleave_4_in_ggaa2(tree_22(A, B), C) -> if_getleave_4_in_1_ggaa1(getleave_4_in_ggaa2(A, tree_22(B, C)))
if_getleave_4_in_1_ggga1(getleave_4_out_ggga1(O)) -> getleave_4_out_ggga1(O)
if_getleave_4_in_1_ggaa1(getleave_4_out_ggaa2(L, O)) -> getleave_4_out_ggaa2(L, O)

The set Q consists of the following terms:

getleave_4_in_ggga3(x0, x1, x2)
getleave_4_in_ggaa2(x0, x1)
if_getleave_4_in_1_ggga1(x0)
if_getleave_4_in_1_ggaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_SAMELEAVES_2_IN_1_GG3, SAMELEAVES_2_IN_GG2, IF_SAMELEAVES_2_IN_2_GG2}.
The approximation of the Dependency Graph contains 0 SCCs with 2 less nodes.