↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
flat2: (f,b) (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ PrologToPiTRSProof
FLAT_2_IN_GG2(tree_3, cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG2(YS, right_2_in_ga1(tree_3))
FLAT_2_IN_AG1(cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG2(YS, right_2_in_ga1(tree_3))
IF_FLAT_2_IN_1_AG2(YS, right_2_out_ga) -> FLAT_2_IN_AG1(YS)
FLAT_2_IN_GG2(tree_3, ZS) -> FLAT_2_IN_GG2(tree_3, ZS)
IF_FLAT_2_IN_1_GG2(YS, right_2_out_ga) -> FLAT_2_IN_AG1(YS)
FLAT_2_IN_AG1(ZS) -> FLAT_2_IN_GG2(tree_3, ZS)
right_2_in_ga1(tree_3) -> right_2_out_ga
right_2_in_ga1(x0)
right_2_in_ga1(tree_3) -> right_2_out_ga
POL(FLAT_2_IN_AG1(x1)) = 1 + x1
POL(FLAT_2_IN_GG2(x1, x2)) = x1 + x2
POL(IF_FLAT_2_IN_1_GG2(x1, x2)) = x1 + x2
POL(tree_3) = 1
POL(IF_FLAT_2_IN_1_AG2(x1, x2)) = x1 + x2
POL(right_2_in_ga1(x1)) = 2·x1
POL(right_2_out_ga) = 1
POL(cons_22(x1, x2)) = 1 + x1 + x2
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
FLAT_2_IN_GG2(tree_3, cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG2(YS, right_2_in_ga1(tree_3))
FLAT_2_IN_AG1(cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG2(YS, right_2_in_ga1(tree_3))
IF_FLAT_2_IN_1_AG2(YS, right_2_out_ga) -> FLAT_2_IN_AG1(YS)
FLAT_2_IN_GG2(tree_3, ZS) -> FLAT_2_IN_GG2(tree_3, ZS)
IF_FLAT_2_IN_1_GG2(YS, right_2_out_ga) -> FLAT_2_IN_AG1(YS)
FLAT_2_IN_AG1(ZS) -> FLAT_2_IN_GG2(tree_3, ZS)
right_2_in_ga1(x0)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ RuleRemovalProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ PrologToPiTRSProof
FLAT_2_IN_GG2(tree_3, ZS) -> FLAT_2_IN_GG2(tree_3, ZS)
right_2_in_ga1(x0)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
flat_2_in_ag2(niltree_0, nil_0) -> flat_2_out_ag2(niltree_0, nil_0)
flat_2_in_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ag4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ag4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
flat_2_in_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
flat_2_in_gg2(niltree_0, nil_0) -> flat_2_out_gg2(niltree_0, nil_0)
flat_2_in_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_gg4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_in_ag2(ZS, YS))
if_flat_2_in_2_gg5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_gg2(tree_33(X, niltree_0, XS), cons_22(X, YS))
flat_2_in_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_gg7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_gg2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag7(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ag2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag5(X, XS, YS, ZS, flat_2_out_ag2(ZS, YS)) -> flat_2_out_ag2(tree_33(X, niltree_0, XS), cons_22(X, YS))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PiDP
↳ UsableRulesProof
↳ PiDP
FLAT_2_IN_GG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_AG2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_GG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG2(ZS, YS)
FLAT_2_IN_AG2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)