(0) Obligation:

Clauses:

tree(nil).
tree(node(L, X, R)) :- ','(tree(L), tree(R)).
s2t(s(X), node(T, Y, T)) :- s2t(X, T).
s2t(s(X), node(nil, Y, T)) :- s2t(X, T).
s2t(s(X), node(T, Y, nil)) :- s2t(X, T).
s2t(s(X), node(nil, Y, nil)).
s2t(0, nil).
goal(X) :- ','(s2t(X, T), tree(T)).

Queries:

goal(g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

s2t9(s(T16), node(X65, X66, X65)) :- s2t9(T16, X65).
s2t9(s(T22), node(nil, X98, X99)) :- s2t9(T22, X99).
s2t9(s(T28), node(X131, X132, nil)) :- s2t9(T28, X131).
tree36(node(T51, T49, T52)) :- tree36(T51).
tree36(node(T51, T49, T53)) :- ','(treec36(T51), tree36(T53)).
goal1(s(T8)) :- s2t9(T8, X27).
goal1(s(T8)) :- ','(s2tc9(T8, T40), tree36(T40)).
goal1(s(T8)) :- ','(s2tc9(T8, T41), ','(treec36(T41), tree36(T41))).
goal1(s(T58)) :- s2t9(T58, X210).
goal1(s(T58)) :- ','(s2tc9(T58, T60), tree36(node(nil, X209, T60))).
goal1(s(T67)) :- s2t9(T67, X251).
goal1(s(T67)) :- ','(s2tc9(T67, T69), tree36(node(T69, X252, nil))).
goal1(s(T76)) :- tree67.
goal1(s(T76)) :- ','(treec67, tree67).
goal1(0) :- tree67.

Clauses:

s2tc9(s(T16), node(X65, X66, X65)) :- s2tc9(T16, X65).
s2tc9(s(T22), node(nil, X98, X99)) :- s2tc9(T22, X99).
s2tc9(s(T28), node(X131, X132, nil)) :- s2tc9(T28, X131).
s2tc9(s(T34), node(nil, X155, nil)).
s2tc9(0, nil).
treec36(nil).
treec36(node(T51, T49, T53)) :- ','(treec36(T51), treec36(T53)).
treec67.

Afs:

goal1(x1)  =  goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2t9(s(T16), node(X65, X66, X65)) :- s2t9(T16, X65).
s2t9(s(T22), node(nil, X98, X99)) :- s2t9(T22, X99).
s2t9(s(T28), node(X131, X132, nil)) :- s2t9(T28, X131).
tree36(node(T51, T49, T52)) :- tree36(T51).
tree36(node(T51, T49, T53)) :- ','(treec36(T51), tree36(T53)).
goal1(s(T8)) :- s2t9(T8, X27).
goal1(s(T8)) :- ','(s2tc9(T8, T40), tree36(T40)).
goal1(s(T8)) :- ','(s2tc9(T8, T41), ','(treec36(T41), tree36(T41))).
goal1(s(T58)) :- s2t9(T58, X210).
goal1(s(T58)) :- ','(s2tc9(T58, T60), tree36(node(nil, X209, T60))).
goal1(s(T67)) :- s2t9(T67, X251).
goal1(s(T67)) :- ','(s2tc9(T67, T69), tree36(node(T69, X252, nil))).

Clauses:

s2tc9(s(T16), node(X65, X66, X65)) :- s2tc9(T16, X65).
s2tc9(s(T22), node(nil, X98, X99)) :- s2tc9(T22, X99).
s2tc9(s(T28), node(X131, X132, nil)) :- s2tc9(T28, X131).
s2tc9(s(T34), node(nil, X155, nil)).
s2tc9(0, nil).
treec36(nil).
treec36(node(T51, T49, T53)) :- ','(treec36(T51), treec36(T53)).
treec67.

Afs:

goal1(x1)  =  goal1(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
goal1_in: (b)
s2t9_in: (b,f)
s2tc9_in: (b,f)
tree36_in: (b)
treec36_in: (b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_G(s(T8)) → U7_G(T8, s2t9_in_ga(T8, X27))
GOAL1_IN_G(s(T8)) → S2T9_IN_GA(T8, X27)
S2T9_IN_GA(s(T16), node(X65, X66, X65)) → U1_GA(T16, X65, X66, s2t9_in_ga(T16, X65))
S2T9_IN_GA(s(T16), node(X65, X66, X65)) → S2T9_IN_GA(T16, X65)
S2T9_IN_GA(s(T22), node(nil, X98, X99)) → U2_GA(T22, X98, X99, s2t9_in_ga(T22, X99))
S2T9_IN_GA(s(T22), node(nil, X98, X99)) → S2T9_IN_GA(T22, X99)
S2T9_IN_GA(s(T28), node(X131, X132, nil)) → U3_GA(T28, X131, X132, s2t9_in_ga(T28, X131))
S2T9_IN_GA(s(T28), node(X131, X132, nil)) → S2T9_IN_GA(T28, X131)
GOAL1_IN_G(s(T8)) → U8_G(T8, s2tc9_in_ga(T8, T40))
U8_G(T8, s2tc9_out_ga(T8, T40)) → U9_G(T8, tree36_in_g(T40))
U8_G(T8, s2tc9_out_ga(T8, T40)) → TREE36_IN_G(T40)
TREE36_IN_G(node(T51, T49, T52)) → U4_G(T51, T49, T52, tree36_in_g(T51))
TREE36_IN_G(node(T51, T49, T52)) → TREE36_IN_G(T51)
TREE36_IN_G(node(T51, T49, T53)) → U5_G(T51, T49, T53, treec36_in_g(T51))
U5_G(T51, T49, T53, treec36_out_g(T51)) → U6_G(T51, T49, T53, tree36_in_g(T53))
U5_G(T51, T49, T53, treec36_out_g(T51)) → TREE36_IN_G(T53)
GOAL1_IN_G(s(T8)) → U10_G(T8, s2tc9_in_ga(T8, T41))
U10_G(T8, s2tc9_out_ga(T8, T41)) → U11_G(T8, T41, treec36_in_g(T41))
U11_G(T8, T41, treec36_out_g(T41)) → U12_G(T8, tree36_in_g(T41))
U11_G(T8, T41, treec36_out_g(T41)) → TREE36_IN_G(T41)
GOAL1_IN_G(s(T58)) → U13_G(T58, s2t9_in_ga(T58, X210))
GOAL1_IN_G(s(T58)) → U14_G(T58, s2tc9_in_ga(T58, T60))
U14_G(T58, s2tc9_out_ga(T58, T60)) → U15_G(T58, tree36_in_g(node(nil, X209, T60)))
U14_G(T58, s2tc9_out_ga(T58, T60)) → TREE36_IN_G(node(nil, X209, T60))
GOAL1_IN_G(s(T67)) → U16_G(T67, s2t9_in_ga(T67, X251))
GOAL1_IN_G(s(T67)) → U17_G(T67, s2tc9_in_ga(T67, T69))
U17_G(T67, s2tc9_out_ga(T67, T69)) → U18_G(T67, tree36_in_g(node(T69, X252, nil)))
U17_G(T67, s2tc9_out_ga(T67, T69)) → TREE36_IN_G(node(T69, X252, nil))

The TRS R consists of the following rules:

s2tc9_in_ga(s(T16), node(X65, X66, X65)) → U20_ga(T16, X65, X66, s2tc9_in_ga(T16, X65))
s2tc9_in_ga(s(T22), node(nil, X98, X99)) → U21_ga(T22, X98, X99, s2tc9_in_ga(T22, X99))
s2tc9_in_ga(s(T28), node(X131, X132, nil)) → U22_ga(T28, X131, X132, s2tc9_in_ga(T28, X131))
s2tc9_in_ga(s(T34), node(nil, X155, nil)) → s2tc9_out_ga(s(T34), node(nil, X155, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U22_ga(T28, X131, X132, s2tc9_out_ga(T28, X131)) → s2tc9_out_ga(s(T28), node(X131, X132, nil))
U21_ga(T22, X98, X99, s2tc9_out_ga(T22, X99)) → s2tc9_out_ga(s(T22), node(nil, X98, X99))
U20_ga(T16, X65, X66, s2tc9_out_ga(T16, X65)) → s2tc9_out_ga(s(T16), node(X65, X66, X65))
treec36_in_g(nil) → treec36_out_g(nil)
treec36_in_g(node(T51, T49, T53)) → U23_g(T51, T49, T53, treec36_in_g(T51))
U23_g(T51, T49, T53, treec36_out_g(T51)) → U24_g(T51, T49, T53, treec36_in_g(T53))
U24_g(T51, T49, T53, treec36_out_g(T53)) → treec36_out_g(node(T51, T49, T53))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2t9_in_ga(x1, x2)  =  s2t9_in_ga(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tc9_in_ga(x1, x2)  =  s2tc9_in_ga(x1)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x1, x4)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x1, x4)
s2tc9_out_ga(x1, x2)  =  s2tc9_out_ga(x1, x2)
0  =  0
tree36_in_g(x1)  =  tree36_in_g(x1)
treec36_in_g(x1)  =  treec36_in_g(x1)
nil  =  nil
treec36_out_g(x1)  =  treec36_out_g(x1)
U23_g(x1, x2, x3, x4)  =  U23_g(x1, x3, x4)
U24_g(x1, x2, x3, x4)  =  U24_g(x1, x3, x4)
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U7_G(x1, x2)  =  U7_G(x1, x2)
S2T9_IN_GA(x1, x2)  =  S2T9_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U8_G(x1, x2)  =  U8_G(x1, x2)
U9_G(x1, x2)  =  U9_G(x1, x2)
TREE36_IN_G(x1)  =  TREE36_IN_G(x1)
U4_G(x1, x2, x3, x4)  =  U4_G(x1, x3, x4)
U5_G(x1, x2, x3, x4)  =  U5_G(x1, x3, x4)
U6_G(x1, x2, x3, x4)  =  U6_G(x1, x3, x4)
U10_G(x1, x2)  =  U10_G(x1, x2)
U11_G(x1, x2, x3)  =  U11_G(x1, x2, x3)
U12_G(x1, x2)  =  U12_G(x1, x2)
U13_G(x1, x2)  =  U13_G(x1, x2)
U14_G(x1, x2)  =  U14_G(x1, x2)
U15_G(x1, x2)  =  U15_G(x1, x2)
U16_G(x1, x2)  =  U16_G(x1, x2)
U17_G(x1, x2)  =  U17_G(x1, x2)
U18_G(x1, x2)  =  U18_G(x1, x2)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

GOAL1_IN_G(s(T8)) → U7_G(T8, s2t9_in_ga(T8, X27))
GOAL1_IN_G(s(T8)) → S2T9_IN_GA(T8, X27)
S2T9_IN_GA(s(T16), node(X65, X66, X65)) → U1_GA(T16, X65, X66, s2t9_in_ga(T16, X65))
S2T9_IN_GA(s(T16), node(X65, X66, X65)) → S2T9_IN_GA(T16, X65)
S2T9_IN_GA(s(T22), node(nil, X98, X99)) → U2_GA(T22, X98, X99, s2t9_in_ga(T22, X99))
S2T9_IN_GA(s(T22), node(nil, X98, X99)) → S2T9_IN_GA(T22, X99)
S2T9_IN_GA(s(T28), node(X131, X132, nil)) → U3_GA(T28, X131, X132, s2t9_in_ga(T28, X131))
S2T9_IN_GA(s(T28), node(X131, X132, nil)) → S2T9_IN_GA(T28, X131)
GOAL1_IN_G(s(T8)) → U8_G(T8, s2tc9_in_ga(T8, T40))
U8_G(T8, s2tc9_out_ga(T8, T40)) → U9_G(T8, tree36_in_g(T40))
U8_G(T8, s2tc9_out_ga(T8, T40)) → TREE36_IN_G(T40)
TREE36_IN_G(node(T51, T49, T52)) → U4_G(T51, T49, T52, tree36_in_g(T51))
TREE36_IN_G(node(T51, T49, T52)) → TREE36_IN_G(T51)
TREE36_IN_G(node(T51, T49, T53)) → U5_G(T51, T49, T53, treec36_in_g(T51))
U5_G(T51, T49, T53, treec36_out_g(T51)) → U6_G(T51, T49, T53, tree36_in_g(T53))
U5_G(T51, T49, T53, treec36_out_g(T51)) → TREE36_IN_G(T53)
GOAL1_IN_G(s(T8)) → U10_G(T8, s2tc9_in_ga(T8, T41))
U10_G(T8, s2tc9_out_ga(T8, T41)) → U11_G(T8, T41, treec36_in_g(T41))
U11_G(T8, T41, treec36_out_g(T41)) → U12_G(T8, tree36_in_g(T41))
U11_G(T8, T41, treec36_out_g(T41)) → TREE36_IN_G(T41)
GOAL1_IN_G(s(T58)) → U13_G(T58, s2t9_in_ga(T58, X210))
GOAL1_IN_G(s(T58)) → U14_G(T58, s2tc9_in_ga(T58, T60))
U14_G(T58, s2tc9_out_ga(T58, T60)) → U15_G(T58, tree36_in_g(node(nil, X209, T60)))
U14_G(T58, s2tc9_out_ga(T58, T60)) → TREE36_IN_G(node(nil, X209, T60))
GOAL1_IN_G(s(T67)) → U16_G(T67, s2t9_in_ga(T67, X251))
GOAL1_IN_G(s(T67)) → U17_G(T67, s2tc9_in_ga(T67, T69))
U17_G(T67, s2tc9_out_ga(T67, T69)) → U18_G(T67, tree36_in_g(node(T69, X252, nil)))
U17_G(T67, s2tc9_out_ga(T67, T69)) → TREE36_IN_G(node(T69, X252, nil))

The TRS R consists of the following rules:

s2tc9_in_ga(s(T16), node(X65, X66, X65)) → U20_ga(T16, X65, X66, s2tc9_in_ga(T16, X65))
s2tc9_in_ga(s(T22), node(nil, X98, X99)) → U21_ga(T22, X98, X99, s2tc9_in_ga(T22, X99))
s2tc9_in_ga(s(T28), node(X131, X132, nil)) → U22_ga(T28, X131, X132, s2tc9_in_ga(T28, X131))
s2tc9_in_ga(s(T34), node(nil, X155, nil)) → s2tc9_out_ga(s(T34), node(nil, X155, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U22_ga(T28, X131, X132, s2tc9_out_ga(T28, X131)) → s2tc9_out_ga(s(T28), node(X131, X132, nil))
U21_ga(T22, X98, X99, s2tc9_out_ga(T22, X99)) → s2tc9_out_ga(s(T22), node(nil, X98, X99))
U20_ga(T16, X65, X66, s2tc9_out_ga(T16, X65)) → s2tc9_out_ga(s(T16), node(X65, X66, X65))
treec36_in_g(nil) → treec36_out_g(nil)
treec36_in_g(node(T51, T49, T53)) → U23_g(T51, T49, T53, treec36_in_g(T51))
U23_g(T51, T49, T53, treec36_out_g(T51)) → U24_g(T51, T49, T53, treec36_in_g(T53))
U24_g(T51, T49, T53, treec36_out_g(T53)) → treec36_out_g(node(T51, T49, T53))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2t9_in_ga(x1, x2)  =  s2t9_in_ga(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tc9_in_ga(x1, x2)  =  s2tc9_in_ga(x1)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x1, x4)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x1, x4)
s2tc9_out_ga(x1, x2)  =  s2tc9_out_ga(x1, x2)
0  =  0
tree36_in_g(x1)  =  tree36_in_g(x1)
treec36_in_g(x1)  =  treec36_in_g(x1)
nil  =  nil
treec36_out_g(x1)  =  treec36_out_g(x1)
U23_g(x1, x2, x3, x4)  =  U23_g(x1, x3, x4)
U24_g(x1, x2, x3, x4)  =  U24_g(x1, x3, x4)
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U7_G(x1, x2)  =  U7_G(x1, x2)
S2T9_IN_GA(x1, x2)  =  S2T9_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U8_G(x1, x2)  =  U8_G(x1, x2)
U9_G(x1, x2)  =  U9_G(x1, x2)
TREE36_IN_G(x1)  =  TREE36_IN_G(x1)
U4_G(x1, x2, x3, x4)  =  U4_G(x1, x3, x4)
U5_G(x1, x2, x3, x4)  =  U5_G(x1, x3, x4)
U6_G(x1, x2, x3, x4)  =  U6_G(x1, x3, x4)
U10_G(x1, x2)  =  U10_G(x1, x2)
U11_G(x1, x2, x3)  =  U11_G(x1, x2, x3)
U12_G(x1, x2)  =  U12_G(x1, x2)
U13_G(x1, x2)  =  U13_G(x1, x2)
U14_G(x1, x2)  =  U14_G(x1, x2)
U15_G(x1, x2)  =  U15_G(x1, x2)
U16_G(x1, x2)  =  U16_G(x1, x2)
U17_G(x1, x2)  =  U17_G(x1, x2)
U18_G(x1, x2)  =  U18_G(x1, x2)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 22 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

TREE36_IN_G(node(T51, T49, T53)) → U5_G(T51, T49, T53, treec36_in_g(T51))
U5_G(T51, T49, T53, treec36_out_g(T51)) → TREE36_IN_G(T53)
TREE36_IN_G(node(T51, T49, T52)) → TREE36_IN_G(T51)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T16), node(X65, X66, X65)) → U20_ga(T16, X65, X66, s2tc9_in_ga(T16, X65))
s2tc9_in_ga(s(T22), node(nil, X98, X99)) → U21_ga(T22, X98, X99, s2tc9_in_ga(T22, X99))
s2tc9_in_ga(s(T28), node(X131, X132, nil)) → U22_ga(T28, X131, X132, s2tc9_in_ga(T28, X131))
s2tc9_in_ga(s(T34), node(nil, X155, nil)) → s2tc9_out_ga(s(T34), node(nil, X155, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U22_ga(T28, X131, X132, s2tc9_out_ga(T28, X131)) → s2tc9_out_ga(s(T28), node(X131, X132, nil))
U21_ga(T22, X98, X99, s2tc9_out_ga(T22, X99)) → s2tc9_out_ga(s(T22), node(nil, X98, X99))
U20_ga(T16, X65, X66, s2tc9_out_ga(T16, X65)) → s2tc9_out_ga(s(T16), node(X65, X66, X65))
treec36_in_g(nil) → treec36_out_g(nil)
treec36_in_g(node(T51, T49, T53)) → U23_g(T51, T49, T53, treec36_in_g(T51))
U23_g(T51, T49, T53, treec36_out_g(T51)) → U24_g(T51, T49, T53, treec36_in_g(T53))
U24_g(T51, T49, T53, treec36_out_g(T53)) → treec36_out_g(node(T51, T49, T53))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tc9_in_ga(x1, x2)  =  s2tc9_in_ga(x1)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x1, x4)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x1, x4)
s2tc9_out_ga(x1, x2)  =  s2tc9_out_ga(x1, x2)
0  =  0
treec36_in_g(x1)  =  treec36_in_g(x1)
nil  =  nil
treec36_out_g(x1)  =  treec36_out_g(x1)
U23_g(x1, x2, x3, x4)  =  U23_g(x1, x3, x4)
U24_g(x1, x2, x3, x4)  =  U24_g(x1, x3, x4)
TREE36_IN_G(x1)  =  TREE36_IN_G(x1)
U5_G(x1, x2, x3, x4)  =  U5_G(x1, x3, x4)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

TREE36_IN_G(node(T51, T49, T53)) → U5_G(T51, T49, T53, treec36_in_g(T51))
U5_G(T51, T49, T53, treec36_out_g(T51)) → TREE36_IN_G(T53)
TREE36_IN_G(node(T51, T49, T52)) → TREE36_IN_G(T51)

The TRS R consists of the following rules:

treec36_in_g(nil) → treec36_out_g(nil)
treec36_in_g(node(T51, T49, T53)) → U23_g(T51, T49, T53, treec36_in_g(T51))
U23_g(T51, T49, T53, treec36_out_g(T51)) → U24_g(T51, T49, T53, treec36_in_g(T53))
U24_g(T51, T49, T53, treec36_out_g(T53)) → treec36_out_g(node(T51, T49, T53))

The argument filtering Pi contains the following mapping:
node(x1, x2, x3)  =  node(x1, x3)
treec36_in_g(x1)  =  treec36_in_g(x1)
nil  =  nil
treec36_out_g(x1)  =  treec36_out_g(x1)
U23_g(x1, x2, x3, x4)  =  U23_g(x1, x3, x4)
U24_g(x1, x2, x3, x4)  =  U24_g(x1, x3, x4)
TREE36_IN_G(x1)  =  TREE36_IN_G(x1)
U5_G(x1, x2, x3, x4)  =  U5_G(x1, x3, x4)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

TREE36_IN_G(node(T51, T53)) → U5_G(T51, T53, treec36_in_g(T51))
U5_G(T51, T53, treec36_out_g(T51)) → TREE36_IN_G(T53)
TREE36_IN_G(node(T51, T52)) → TREE36_IN_G(T51)

The TRS R consists of the following rules:

treec36_in_g(nil) → treec36_out_g(nil)
treec36_in_g(node(T51, T53)) → U23_g(T51, T53, treec36_in_g(T51))
U23_g(T51, T53, treec36_out_g(T51)) → U24_g(T51, T53, treec36_in_g(T53))
U24_g(T51, T53, treec36_out_g(T53)) → treec36_out_g(node(T51, T53))

The set Q consists of the following terms:

treec36_in_g(x0)
U23_g(x0, x1, x2)
U24_g(x0, x1, x2)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • U5_G(T51, T53, treec36_out_g(T51)) → TREE36_IN_G(T53)
    The graph contains the following edges 2 >= 1

  • TREE36_IN_G(node(T51, T52)) → TREE36_IN_G(T51)
    The graph contains the following edges 1 > 1

  • TREE36_IN_G(node(T51, T53)) → U5_G(T51, T53, treec36_in_g(T51))
    The graph contains the following edges 1 > 1, 1 > 2

(15) YES

(16) Obligation:

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

S2T9_IN_GA(s(T22), node(nil, X98, X99)) → S2T9_IN_GA(T22, X99)
S2T9_IN_GA(s(T16), node(X65, X66, X65)) → S2T9_IN_GA(T16, X65)
S2T9_IN_GA(s(T28), node(X131, X132, nil)) → S2T9_IN_GA(T28, X131)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T16), node(X65, X66, X65)) → U20_ga(T16, X65, X66, s2tc9_in_ga(T16, X65))
s2tc9_in_ga(s(T22), node(nil, X98, X99)) → U21_ga(T22, X98, X99, s2tc9_in_ga(T22, X99))
s2tc9_in_ga(s(T28), node(X131, X132, nil)) → U22_ga(T28, X131, X132, s2tc9_in_ga(T28, X131))
s2tc9_in_ga(s(T34), node(nil, X155, nil)) → s2tc9_out_ga(s(T34), node(nil, X155, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U22_ga(T28, X131, X132, s2tc9_out_ga(T28, X131)) → s2tc9_out_ga(s(T28), node(X131, X132, nil))
U21_ga(T22, X98, X99, s2tc9_out_ga(T22, X99)) → s2tc9_out_ga(s(T22), node(nil, X98, X99))
U20_ga(T16, X65, X66, s2tc9_out_ga(T16, X65)) → s2tc9_out_ga(s(T16), node(X65, X66, X65))
treec36_in_g(nil) → treec36_out_g(nil)
treec36_in_g(node(T51, T49, T53)) → U23_g(T51, T49, T53, treec36_in_g(T51))
U23_g(T51, T49, T53, treec36_out_g(T51)) → U24_g(T51, T49, T53, treec36_in_g(T53))
U24_g(T51, T49, T53, treec36_out_g(T53)) → treec36_out_g(node(T51, T49, T53))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
s2tc9_in_ga(x1, x2)  =  s2tc9_in_ga(x1)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x1, x4)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x1, x4)
s2tc9_out_ga(x1, x2)  =  s2tc9_out_ga(x1, x2)
0  =  0
treec36_in_g(x1)  =  treec36_in_g(x1)
nil  =  nil
treec36_out_g(x1)  =  treec36_out_g(x1)
U23_g(x1, x2, x3, x4)  =  U23_g(x1, x3, x4)
U24_g(x1, x2, x3, x4)  =  U24_g(x1, x3, x4)
S2T9_IN_GA(x1, x2)  =  S2T9_IN_GA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

S2T9_IN_GA(s(T22), node(nil, X98, X99)) → S2T9_IN_GA(T22, X99)
S2T9_IN_GA(s(T16), node(X65, X66, X65)) → S2T9_IN_GA(T16, X65)
S2T9_IN_GA(s(T28), node(X131, X132, nil)) → S2T9_IN_GA(T28, X131)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
nil  =  nil
S2T9_IN_GA(x1, x2)  =  S2T9_IN_GA(x1)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

S2T9_IN_GA(s(T22)) → S2T9_IN_GA(T22)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • S2T9_IN_GA(s(T22)) → S2T9_IN_GA(T22)
    The graph contains the following edges 1 > 1

(22) YES