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

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 PiDP
↳7 PiDPToQDPProof (⇐)
↳8 QDP
↳9 MRRProof (⇔)
↳10 QDP
↳11 DependencyGraphProof (⇔)
↳12 TRUE

(0) Obligation:

Clauses:

hbal_tree(zero, nil).
hbal_tree(s(zero), t(x, nil, nil)).
hbal_tree(s(s(X)), t(x, L, R)) :- ','(distr(s(X), X, DL, DR), ','(hbal_tree(DL, L), hbal_tree(DR, R))).
distr(D1, X1, D1, D1).
distr(D1, D2, D1, D2).
distr(D1, D2, D2, D1).

Queries:

hbal_tree(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

hbal_tree1(s(s(T15)), t(x, T9, T10)) :- hbal_tree1(s(T15), T9).
hbal_tree1(s(s(T15)), t(x, T9, T16)) :- ','(hbal_treec1(s(T15), T9), hbal_tree1(s(T15), T16)).
hbal_tree1(s(s(T21)), t(x, T9, T10)) :- hbal_tree1(s(T21), T9).
hbal_tree1(s(s(T21)), t(x, T9, T22)) :- ','(hbal_treec1(s(T21), T9), hbal_tree1(T21, T22)).
hbal_tree1(s(s(T25)), t(x, T9, T10)) :- hbal_tree1(T25, T9).
hbal_tree1(s(s(T25)), t(x, T9, T26)) :- ','(hbal_treec1(T25, T9), hbal_tree1(s(T25), T26)).

Clauses:

hbal_treec1(zero, nil).
hbal_treec1(s(zero), t(x, nil, nil)).
hbal_treec1(s(s(T15)), t(x, T9, T16)) :- ','(hbal_treec1(s(T15), T9), hbal_treec1(s(T15), T16)).
hbal_treec1(s(s(T21)), t(x, T9, T22)) :- ','(hbal_treec1(s(T21), T9), hbal_treec1(T21, T22)).
hbal_treec1(s(s(T25)), t(x, T9, T26)) :- ','(hbal_treec1(T25, T9), hbal_treec1(s(T25), T26)).

Afs:

hbal_tree1(x1, x2)  =  hbal_tree1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

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

HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T10)) → U1_GA(T15, T9, T10, hbal_tree1_in_ga(s(T15), T9))
HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T10)) → HBAL_TREE1_IN_GA(s(T15), T9)
HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T16)) → U2_GA(T15, T9, T16, hbal_treec1_in_ga(s(T15), T9))
U2_GA(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → U3_GA(T15, T9, T16, hbal_tree1_in_ga(s(T15), T16))
U2_GA(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → HBAL_TREE1_IN_GA(s(T15), T16)
HBAL_TREE1_IN_GA(s(s(T21)), t(x, T9, T10)) → U4_GA(T21, T9, T10, hbal_tree1_in_ga(s(T21), T9))
HBAL_TREE1_IN_GA(s(s(T21)), t(x, T9, T22)) → U5_GA(T21, T9, T22, hbal_treec1_in_ga(s(T21), T9))
U5_GA(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → U6_GA(T21, T9, T22, hbal_tree1_in_ga(T21, T22))
U5_GA(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → HBAL_TREE1_IN_GA(T21, T22)
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T10)) → U7_GA(T25, T9, T10, hbal_tree1_in_ga(T25, T9))
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T10)) → HBAL_TREE1_IN_GA(T25, T9)
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T26)) → U8_GA(T25, T9, T26, hbal_treec1_in_ga(T25, T9))
U8_GA(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → U9_GA(T25, T9, T26, hbal_tree1_in_ga(s(T25), T26))
U8_GA(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → HBAL_TREE1_IN_GA(s(T25), T26)

The TRS R consists of the following rules:

hbal_treec1_in_ga(zero, nil) → hbal_treec1_out_ga(zero, nil)
hbal_treec1_in_ga(s(zero), t(x, nil, nil)) → hbal_treec1_out_ga(s(zero), t(x, nil, nil))
hbal_treec1_in_ga(s(s(T15)), t(x, T9, T16)) → U11_ga(T15, T9, T16, hbal_treec1_in_ga(s(T15), T9))
hbal_treec1_in_ga(s(s(T21)), t(x, T9, T22)) → U13_ga(T21, T9, T22, hbal_treec1_in_ga(s(T21), T9))
hbal_treec1_in_ga(s(s(T25)), t(x, T9, T26)) → U15_ga(T25, T9, T26, hbal_treec1_in_ga(T25, T9))
U15_ga(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → U16_ga(T25, T9, T26, hbal_treec1_in_ga(s(T25), T26))
U16_ga(T25, T9, T26, hbal_treec1_out_ga(s(T25), T26)) → hbal_treec1_out_ga(s(s(T25)), t(x, T9, T26))
U13_ga(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → U14_ga(T21, T9, T22, hbal_treec1_in_ga(T21, T22))
U14_ga(T21, T9, T22, hbal_treec1_out_ga(T21, T22)) → hbal_treec1_out_ga(s(s(T21)), t(x, T9, T22))
U11_ga(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → U12_ga(T15, T9, T16, hbal_treec1_in_ga(s(T15), T16))
U12_ga(T15, T9, T16, hbal_treec1_out_ga(s(T15), T16)) → hbal_treec1_out_ga(s(s(T15)), t(x, T9, T16))

The argument filtering Pi contains the following mapping:
hbal_tree1_in_ga(x1, x2)  =  hbal_tree1_in_ga(x1)
s(x1)  =  s(x1)
hbal_treec1_in_ga(x1, x2)  =  hbal_treec1_in_ga(x1)
zero  =  zero
hbal_treec1_out_ga(x1, x2)  =  hbal_treec1_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4)  =  U12_ga(x1, x2, x4)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE1_IN_GA(x1, x2)  =  HBAL_TREE1_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)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T10)) → U1_GA(T15, T9, T10, hbal_tree1_in_ga(s(T15), T9))
HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T10)) → HBAL_TREE1_IN_GA(s(T15), T9)
HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T16)) → U2_GA(T15, T9, T16, hbal_treec1_in_ga(s(T15), T9))
U2_GA(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → U3_GA(T15, T9, T16, hbal_tree1_in_ga(s(T15), T16))
U2_GA(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → HBAL_TREE1_IN_GA(s(T15), T16)
HBAL_TREE1_IN_GA(s(s(T21)), t(x, T9, T10)) → U4_GA(T21, T9, T10, hbal_tree1_in_ga(s(T21), T9))
HBAL_TREE1_IN_GA(s(s(T21)), t(x, T9, T22)) → U5_GA(T21, T9, T22, hbal_treec1_in_ga(s(T21), T9))
U5_GA(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → U6_GA(T21, T9, T22, hbal_tree1_in_ga(T21, T22))
U5_GA(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → HBAL_TREE1_IN_GA(T21, T22)
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T10)) → U7_GA(T25, T9, T10, hbal_tree1_in_ga(T25, T9))
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T10)) → HBAL_TREE1_IN_GA(T25, T9)
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T26)) → U8_GA(T25, T9, T26, hbal_treec1_in_ga(T25, T9))
U8_GA(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → U9_GA(T25, T9, T26, hbal_tree1_in_ga(s(T25), T26))
U8_GA(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → HBAL_TREE1_IN_GA(s(T25), T26)

The TRS R consists of the following rules:

hbal_treec1_in_ga(zero, nil) → hbal_treec1_out_ga(zero, nil)
hbal_treec1_in_ga(s(zero), t(x, nil, nil)) → hbal_treec1_out_ga(s(zero), t(x, nil, nil))
hbal_treec1_in_ga(s(s(T15)), t(x, T9, T16)) → U11_ga(T15, T9, T16, hbal_treec1_in_ga(s(T15), T9))
hbal_treec1_in_ga(s(s(T21)), t(x, T9, T22)) → U13_ga(T21, T9, T22, hbal_treec1_in_ga(s(T21), T9))
hbal_treec1_in_ga(s(s(T25)), t(x, T9, T26)) → U15_ga(T25, T9, T26, hbal_treec1_in_ga(T25, T9))
U15_ga(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → U16_ga(T25, T9, T26, hbal_treec1_in_ga(s(T25), T26))
U16_ga(T25, T9, T26, hbal_treec1_out_ga(s(T25), T26)) → hbal_treec1_out_ga(s(s(T25)), t(x, T9, T26))
U13_ga(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → U14_ga(T21, T9, T22, hbal_treec1_in_ga(T21, T22))
U14_ga(T21, T9, T22, hbal_treec1_out_ga(T21, T22)) → hbal_treec1_out_ga(s(s(T21)), t(x, T9, T22))
U11_ga(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → U12_ga(T15, T9, T16, hbal_treec1_in_ga(s(T15), T16))
U12_ga(T15, T9, T16, hbal_treec1_out_ga(s(T15), T16)) → hbal_treec1_out_ga(s(s(T15)), t(x, T9, T16))

The argument filtering Pi contains the following mapping:
hbal_tree1_in_ga(x1, x2)  =  hbal_tree1_in_ga(x1)
s(x1)  =  s(x1)
hbal_treec1_in_ga(x1, x2)  =  hbal_treec1_in_ga(x1)
zero  =  zero
hbal_treec1_out_ga(x1, x2)  =  hbal_treec1_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4)  =  U12_ga(x1, x2, x4)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE1_IN_GA(x1, x2)  =  HBAL_TREE1_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)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T16)) → U2_GA(T15, T9, T16, hbal_treec1_in_ga(s(T15), T9))
U2_GA(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → HBAL_TREE1_IN_GA(s(T15), T16)
HBAL_TREE1_IN_GA(s(s(T15)), t(x, T9, T10)) → HBAL_TREE1_IN_GA(s(T15), T9)
HBAL_TREE1_IN_GA(s(s(T21)), t(x, T9, T22)) → U5_GA(T21, T9, T22, hbal_treec1_in_ga(s(T21), T9))
U5_GA(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → HBAL_TREE1_IN_GA(T21, T22)
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T10)) → HBAL_TREE1_IN_GA(T25, T9)
HBAL_TREE1_IN_GA(s(s(T25)), t(x, T9, T26)) → U8_GA(T25, T9, T26, hbal_treec1_in_ga(T25, T9))
U8_GA(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → HBAL_TREE1_IN_GA(s(T25), T26)

The TRS R consists of the following rules:

hbal_treec1_in_ga(zero, nil) → hbal_treec1_out_ga(zero, nil)
hbal_treec1_in_ga(s(zero), t(x, nil, nil)) → hbal_treec1_out_ga(s(zero), t(x, nil, nil))
hbal_treec1_in_ga(s(s(T15)), t(x, T9, T16)) → U11_ga(T15, T9, T16, hbal_treec1_in_ga(s(T15), T9))
hbal_treec1_in_ga(s(s(T21)), t(x, T9, T22)) → U13_ga(T21, T9, T22, hbal_treec1_in_ga(s(T21), T9))
hbal_treec1_in_ga(s(s(T25)), t(x, T9, T26)) → U15_ga(T25, T9, T26, hbal_treec1_in_ga(T25, T9))
U15_ga(T25, T9, T26, hbal_treec1_out_ga(T25, T9)) → U16_ga(T25, T9, T26, hbal_treec1_in_ga(s(T25), T26))
U16_ga(T25, T9, T26, hbal_treec1_out_ga(s(T25), T26)) → hbal_treec1_out_ga(s(s(T25)), t(x, T9, T26))
U13_ga(T21, T9, T22, hbal_treec1_out_ga(s(T21), T9)) → U14_ga(T21, T9, T22, hbal_treec1_in_ga(T21, T22))
U14_ga(T21, T9, T22, hbal_treec1_out_ga(T21, T22)) → hbal_treec1_out_ga(s(s(T21)), t(x, T9, T22))
U11_ga(T15, T9, T16, hbal_treec1_out_ga(s(T15), T9)) → U12_ga(T15, T9, T16, hbal_treec1_in_ga(s(T15), T16))
U12_ga(T15, T9, T16, hbal_treec1_out_ga(s(T15), T16)) → hbal_treec1_out_ga(s(s(T15)), t(x, T9, T16))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
hbal_treec1_in_ga(x1, x2)  =  hbal_treec1_in_ga(x1)
zero  =  zero
hbal_treec1_out_ga(x1, x2)  =  hbal_treec1_out_ga(x1, x2)
U11_ga(x1, x2, x3, x4)  =  U11_ga(x1, x4)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
U12_ga(x1, x2, x3, x4)  =  U12_ga(x1, x2, x4)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE1_IN_GA(x1, x2)  =  HBAL_TREE1_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)

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

(7) PiDPToQDPProof (SOUND transformation)

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

(8) Obligation:

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

HBAL_TREE1_IN_GA(s(s(T15))) → U2_GA(T15, hbal_treec1_in_ga(s(T15)))
U2_GA(T15, hbal_treec1_out_ga(s(T15), T9)) → HBAL_TREE1_IN_GA(s(T15))
HBAL_TREE1_IN_GA(s(s(T15))) → HBAL_TREE1_IN_GA(s(T15))
HBAL_TREE1_IN_GA(s(s(T21))) → U5_GA(T21, hbal_treec1_in_ga(s(T21)))
U5_GA(T21, hbal_treec1_out_ga(s(T21), T9)) → HBAL_TREE1_IN_GA(T21)
HBAL_TREE1_IN_GA(s(s(T25))) → HBAL_TREE1_IN_GA(T25)
HBAL_TREE1_IN_GA(s(s(T25))) → U8_GA(T25, hbal_treec1_in_ga(T25))
U8_GA(T25, hbal_treec1_out_ga(T25, T9)) → HBAL_TREE1_IN_GA(s(T25))

The TRS R consists of the following rules:

hbal_treec1_in_ga(zero) → hbal_treec1_out_ga(zero, nil)
hbal_treec1_in_ga(s(zero)) → hbal_treec1_out_ga(s(zero), t(x, nil, nil))
hbal_treec1_in_ga(s(s(T15))) → U11_ga(T15, hbal_treec1_in_ga(s(T15)))
hbal_treec1_in_ga(s(s(T21))) → U13_ga(T21, hbal_treec1_in_ga(s(T21)))
hbal_treec1_in_ga(s(s(T25))) → U15_ga(T25, hbal_treec1_in_ga(T25))
U15_ga(T25, hbal_treec1_out_ga(T25, T9)) → U16_ga(T25, T9, hbal_treec1_in_ga(s(T25)))
U16_ga(T25, T9, hbal_treec1_out_ga(s(T25), T26)) → hbal_treec1_out_ga(s(s(T25)), t(x, T9, T26))
U13_ga(T21, hbal_treec1_out_ga(s(T21), T9)) → U14_ga(T21, T9, hbal_treec1_in_ga(T21))
U14_ga(T21, T9, hbal_treec1_out_ga(T21, T22)) → hbal_treec1_out_ga(s(s(T21)), t(x, T9, T22))
U11_ga(T15, hbal_treec1_out_ga(s(T15), T9)) → U12_ga(T15, T9, hbal_treec1_in_ga(s(T15)))
U12_ga(T15, T9, hbal_treec1_out_ga(s(T15), T16)) → hbal_treec1_out_ga(s(s(T15)), t(x, T9, T16))

The set Q consists of the following terms:

hbal_treec1_in_ga(x0)
U15_ga(x0, x1)
U16_ga(x0, x1, x2)
U13_ga(x0, x1)
U14_ga(x0, x1, x2)
U11_ga(x0, x1)
U12_ga(x0, x1, x2)

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

(9) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

HBAL_TREE1_IN_GA(s(s(T15))) → U2_GA(T15, hbal_treec1_in_ga(s(T15)))
HBAL_TREE1_IN_GA(s(s(T15))) → HBAL_TREE1_IN_GA(s(T15))
HBAL_TREE1_IN_GA(s(s(T21))) → U5_GA(T21, hbal_treec1_in_ga(s(T21)))
U5_GA(T21, hbal_treec1_out_ga(s(T21), T9)) → HBAL_TREE1_IN_GA(T21)
HBAL_TREE1_IN_GA(s(s(T25))) → HBAL_TREE1_IN_GA(T25)
HBAL_TREE1_IN_GA(s(s(T25))) → U8_GA(T25, hbal_treec1_in_ga(T25))
U8_GA(T25, hbal_treec1_out_ga(T25, T9)) → HBAL_TREE1_IN_GA(s(T25))


Used ordering: Polynomial interpretation [POLO]:

POL(HBAL_TREE1_IN_GA(x1)) = 2 + x1   
POL(U11_ga(x1, x2)) = 2 + 2·x1 + x2   
POL(U12_ga(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3   
POL(U13_ga(x1, x2)) = 2 + 2·x1 + x2   
POL(U14_ga(x1, x2, x3)) = 1 + 2·x1 + 2·x2 + 2·x3   
POL(U15_ga(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U16_ga(x1, x2, x3)) = 2 + 2·x1 + 2·x2 + x3   
POL(U2_GA(x1, x2)) = 2·x1 + x2   
POL(U5_GA(x1, x2)) = x1 + x2   
POL(U8_GA(x1, x2)) = 2·x1 + 2·x2   
POL(hbal_treec1_in_ga(x1)) = 2 + x1   
POL(hbal_treec1_out_ga(x1, x2)) = 2 + x1 + 2·x2   
POL(nil) = 0   
POL(s(x1)) = 1 + 2·x1   
POL(t(x1, x2, x3)) = x1 + x2 + x3   
POL(x) = 0   
POL(zero) = 0   

(10) Obligation:

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

U2_GA(T15, hbal_treec1_out_ga(s(T15), T9)) → HBAL_TREE1_IN_GA(s(T15))

The TRS R consists of the following rules:

hbal_treec1_in_ga(zero) → hbal_treec1_out_ga(zero, nil)
hbal_treec1_in_ga(s(zero)) → hbal_treec1_out_ga(s(zero), t(x, nil, nil))
hbal_treec1_in_ga(s(s(T15))) → U11_ga(T15, hbal_treec1_in_ga(s(T15)))
hbal_treec1_in_ga(s(s(T21))) → U13_ga(T21, hbal_treec1_in_ga(s(T21)))
hbal_treec1_in_ga(s(s(T25))) → U15_ga(T25, hbal_treec1_in_ga(T25))
U15_ga(T25, hbal_treec1_out_ga(T25, T9)) → U16_ga(T25, T9, hbal_treec1_in_ga(s(T25)))
U16_ga(T25, T9, hbal_treec1_out_ga(s(T25), T26)) → hbal_treec1_out_ga(s(s(T25)), t(x, T9, T26))
U13_ga(T21, hbal_treec1_out_ga(s(T21), T9)) → U14_ga(T21, T9, hbal_treec1_in_ga(T21))
U14_ga(T21, T9, hbal_treec1_out_ga(T21, T22)) → hbal_treec1_out_ga(s(s(T21)), t(x, T9, T22))
U11_ga(T15, hbal_treec1_out_ga(s(T15), T9)) → U12_ga(T15, T9, hbal_treec1_in_ga(s(T15)))
U12_ga(T15, T9, hbal_treec1_out_ga(s(T15), T16)) → hbal_treec1_out_ga(s(s(T15)), t(x, T9, T16))

The set Q consists of the following terms:

hbal_treec1_in_ga(x0)
U15_ga(x0, x1)
U16_ga(x0, x1, x2)
U13_ga(x0, x1)
U14_ga(x0, x1, x2)
U11_ga(x0, x1)
U12_ga(x0, x1, x2)

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

(11) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(12) TRUE