(0) Obligation:

Clauses:

tree_member(X, tree(X, X1, X2)).
tree_member(X, tree(X3, Left, X4)) :- tree_member(X, Left).
tree_member(X, tree(X5, X6, Right)) :- tree_member(X, Right).

Queries:

tree_member(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

tree_member1(T6, tree(T6, T7, T8)).
tree_member1(T30, tree(T14, tree(T30, T31, T32), T16)).
tree_member1(T49, tree(T14, tree(T50, T53, T52), T16)) :- tree_member1(T49, T53).
tree_member1(T76, tree(T14, tree(T77, T78, T80), T16)) :- tree_member1(T76, T80).
tree_member1(T95, tree(T96, T97, T99)) :- tree_member1(T95, T99).
tree_member1(T127, tree(T111, T112, tree(T127, T128, T129))).
tree_member1(T146, tree(T111, T112, tree(T147, T150, T149))) :- tree_member1(T146, T150).
tree_member1(T165, tree(T111, T112, tree(T166, T167, T169))) :- tree_member1(T165, T169).
tree_member1(T197, tree(T181, tree(T197, T198, T199), T183)).
tree_member1(T216, tree(T181, tree(T217, T220, T219), T183)) :- tree_member1(T216, T220).
tree_member1(T243, tree(T181, tree(T244, T245, T247), T183)) :- tree_member1(T243, T247).
tree_member1(T262, tree(T263, T264, T266)) :- tree_member1(T262, T266).
tree_member1(T294, tree(T278, T279, tree(T294, T295, T296))).
tree_member1(T313, tree(T278, T279, tree(T314, T317, T316))) :- tree_member1(T313, T317).
tree_member1(T332, tree(T278, T279, tree(T333, T334, T336))) :- tree_member1(T332, T336).

Queries:

tree_member1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
tree_member1_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga(x1)
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x1, x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x1, x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x1, x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x1, x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x1, x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x1, x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x1, x7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga(x1)
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x1, x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x1, x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x1, x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x1, x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x1, x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x1, x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x1, x7)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_GA(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_GA(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → U3_GA(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_GA(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_GA(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)
TREE_MEMBER1_IN_GA(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_GA(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
TREE_MEMBER1_IN_GA(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_GA(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
TREE_MEMBER1_IN_GA(T262, tree(T263, T264, T266)) → U8_GA(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
TREE_MEMBER1_IN_GA(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_GA(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
TREE_MEMBER1_IN_GA(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_GA(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))

The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga(x1)
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x1, x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x1, x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x1, x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x1, x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x1, x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x1, x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x1, x7)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GA(x1, x7)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x1, x7)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GA(x1, x7)
U5_GA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GA(x1, x7)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x7)
U7_GA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GA(x1, x7)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x5)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x1, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x7)

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

(6) Obligation:

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

TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_GA(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_GA(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → U3_GA(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_GA(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_GA(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)
TREE_MEMBER1_IN_GA(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_GA(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
TREE_MEMBER1_IN_GA(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_GA(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
TREE_MEMBER1_IN_GA(T262, tree(T263, T264, T266)) → U8_GA(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
TREE_MEMBER1_IN_GA(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_GA(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
TREE_MEMBER1_IN_GA(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_GA(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))

The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga(x1)
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x1, x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x1, x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x1, x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x1, x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x1, x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x1, x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x1, x7)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GA(x1, x7)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x1, x7)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GA(x1, x7)
U5_GA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GA(x1, x7)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x7)
U7_GA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GA(x1, x7)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x5)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x1, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x7)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 10 less nodes.

(8) Obligation:

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

TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)

The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga(x1)
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x1, x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x1, x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x1, x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x1, x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x1, x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x1, x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x1, x7)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)

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

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

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

TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)

R is empty.
The argument filtering Pi contains the following mapping:
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)

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

(11) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(12) Obligation:

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

TREE_MEMBER1_IN_GA(T76) → TREE_MEMBER1_IN_GA(T76)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = TREE_MEMBER1_IN_GA(T76) evaluates to t =TREE_MEMBER1_IN_GA(T76)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from TREE_MEMBER1_IN_GA(T76) to TREE_MEMBER1_IN_GA(T76).



(14) NO

(15) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
tree_member1_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(16) Obligation:

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

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x7)

(17) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_GA(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_GA(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → U3_GA(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_GA(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_GA(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)
TREE_MEMBER1_IN_GA(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_GA(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
TREE_MEMBER1_IN_GA(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_GA(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
TREE_MEMBER1_IN_GA(T262, tree(T263, T264, T266)) → U8_GA(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
TREE_MEMBER1_IN_GA(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_GA(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
TREE_MEMBER1_IN_GA(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_GA(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))

The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x7)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GA(x7)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x7)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x5)
U4_GA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GA(x7)
U5_GA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GA(x7)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x7)
U7_GA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GA(x7)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x5)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x7)

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

(18) Obligation:

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

TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_GA(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_GA(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → U3_GA(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_GA(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_GA(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)
TREE_MEMBER1_IN_GA(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_GA(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
TREE_MEMBER1_IN_GA(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_GA(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
TREE_MEMBER1_IN_GA(T262, tree(T263, T264, T266)) → U8_GA(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
TREE_MEMBER1_IN_GA(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_GA(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
TREE_MEMBER1_IN_GA(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_GA(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))

The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x7)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7)  =  U1_GA(x7)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x7)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x5)
U4_GA(x1, x2, x3, x4, x5, x6, x7)  =  U4_GA(x7)
U5_GA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GA(x7)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x7)
U7_GA(x1, x2, x3, x4, x5, x6, x7)  =  U7_GA(x7)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x5)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x7)

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

(19) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 10 less nodes.

(20) Obligation:

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

TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)

The TRS R consists of the following rules:

tree_member1_in_ga(T6, tree(T6, T7, T8)) → tree_member1_out_ga(T6, tree(T6, T7, T8))
tree_member1_in_ga(T30, tree(T14, tree(T30, T31, T32), T16)) → tree_member1_out_ga(T30, tree(T14, tree(T30, T31, T32), T16))
tree_member1_in_ga(T49, tree(T14, tree(T50, T53, T52), T16)) → U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_in_ga(T49, T53))
tree_member1_in_ga(T76, tree(T14, tree(T77, T78, T80), T16)) → U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_in_ga(T76, T80))
tree_member1_in_ga(T95, tree(T96, T97, T99)) → U3_ga(T95, T96, T97, T99, tree_member1_in_ga(T95, T99))
tree_member1_in_ga(T127, tree(T111, T112, tree(T127, T128, T129))) → tree_member1_out_ga(T127, tree(T111, T112, tree(T127, T128, T129)))
tree_member1_in_ga(T146, tree(T111, T112, tree(T147, T150, T149))) → U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_in_ga(T146, T150))
tree_member1_in_ga(T165, tree(T111, T112, tree(T166, T167, T169))) → U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_in_ga(T165, T169))
tree_member1_in_ga(T216, tree(T181, tree(T217, T220, T219), T183)) → U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_in_ga(T216, T220))
tree_member1_in_ga(T243, tree(T181, tree(T244, T245, T247), T183)) → U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_in_ga(T243, T247))
tree_member1_in_ga(T262, tree(T263, T264, T266)) → U8_ga(T262, T263, T264, T266, tree_member1_in_ga(T262, T266))
tree_member1_in_ga(T313, tree(T278, T279, tree(T314, T317, T316))) → U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_in_ga(T313, T317))
tree_member1_in_ga(T332, tree(T278, T279, tree(T333, T334, T336))) → U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_in_ga(T332, T336))
U10_ga(T332, T278, T279, T333, T334, T336, tree_member1_out_ga(T332, T336)) → tree_member1_out_ga(T332, tree(T278, T279, tree(T333, T334, T336)))
U9_ga(T313, T278, T279, T314, T317, T316, tree_member1_out_ga(T313, T317)) → tree_member1_out_ga(T313, tree(T278, T279, tree(T314, T317, T316)))
U8_ga(T262, T263, T264, T266, tree_member1_out_ga(T262, T266)) → tree_member1_out_ga(T262, tree(T263, T264, T266))
U7_ga(T243, T181, T244, T245, T247, T183, tree_member1_out_ga(T243, T247)) → tree_member1_out_ga(T243, tree(T181, tree(T244, T245, T247), T183))
U6_ga(T216, T181, T217, T220, T219, T183, tree_member1_out_ga(T216, T220)) → tree_member1_out_ga(T216, tree(T181, tree(T217, T220, T219), T183))
U5_ga(T165, T111, T112, T166, T167, T169, tree_member1_out_ga(T165, T169)) → tree_member1_out_ga(T165, tree(T111, T112, tree(T166, T167, T169)))
U4_ga(T146, T111, T112, T147, T150, T149, tree_member1_out_ga(T146, T150)) → tree_member1_out_ga(T146, tree(T111, T112, tree(T147, T150, T149)))
U3_ga(T95, T96, T97, T99, tree_member1_out_ga(T95, T99)) → tree_member1_out_ga(T95, tree(T96, T97, T99))
U2_ga(T76, T14, T77, T78, T80, T16, tree_member1_out_ga(T76, T80)) → tree_member1_out_ga(T76, tree(T14, tree(T77, T78, T80), T16))
U1_ga(T49, T14, T50, T53, T52, T16, tree_member1_out_ga(T49, T53)) → tree_member1_out_ga(T49, tree(T14, tree(T50, T53, T52), T16))

The argument filtering Pi contains the following mapping:
tree_member1_in_ga(x1, x2)  =  tree_member1_in_ga(x1)
tree_member1_out_ga(x1, x2)  =  tree_member1_out_ga
U1_ga(x1, x2, x3, x4, x5, x6, x7)  =  U1_ga(x7)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x7)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x5)
U4_ga(x1, x2, x3, x4, x5, x6, x7)  =  U4_ga(x7)
U5_ga(x1, x2, x3, x4, x5, x6, x7)  =  U5_ga(x7)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x7)
U7_ga(x1, x2, x3, x4, x5, x6, x7)  =  U7_ga(x7)
U8_ga(x1, x2, x3, x4, x5)  =  U8_ga(x5)
U9_ga(x1, x2, x3, x4, x5, x6, x7)  =  U9_ga(x7)
U10_ga(x1, x2, x3, x4, x5, x6, x7)  =  U10_ga(x7)
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)

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

(21) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(22) Obligation:

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

TREE_MEMBER1_IN_GA(T76, tree(T14, tree(T77, T78, T80), T16)) → TREE_MEMBER1_IN_GA(T76, T80)
TREE_MEMBER1_IN_GA(T49, tree(T14, tree(T50, T53, T52), T16)) → TREE_MEMBER1_IN_GA(T49, T53)
TREE_MEMBER1_IN_GA(T95, tree(T96, T97, T99)) → TREE_MEMBER1_IN_GA(T95, T99)
TREE_MEMBER1_IN_GA(T146, tree(T111, T112, tree(T147, T150, T149))) → TREE_MEMBER1_IN_GA(T146, T150)
TREE_MEMBER1_IN_GA(T165, tree(T111, T112, tree(T166, T167, T169))) → TREE_MEMBER1_IN_GA(T165, T169)

R is empty.
The argument filtering Pi contains the following mapping:
TREE_MEMBER1_IN_GA(x1, x2)  =  TREE_MEMBER1_IN_GA(x1)

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

(23) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(24) Obligation:

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

TREE_MEMBER1_IN_GA(T76) → TREE_MEMBER1_IN_GA(T76)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(25) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = TREE_MEMBER1_IN_GA(T76) evaluates to t =TREE_MEMBER1_IN_GA(T76)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from TREE_MEMBER1_IN_GA(T76) to TREE_MEMBER1_IN_GA(T76).



(26) NO