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 PrologToPiTRSProof (⇐)
    ↳2 PiTRS
    ↳3 DependencyPairsProof (⇔)
    ↳4 PiDP
    ↳5 DependencyGraphProof (⇔)
    ↳6 PiDP
    ↳7 PiDPToQDPProof (⇐)
    ↳8 QDP
  ↳9 PrologToPiTRSProof (⇐)
    ↳10 PiTRS
    ↳11 DependencyPairsProof (⇔)
    ↳12 PiDP
    ↳13 DependencyGraphProof (⇔)
    ↳14 PiDP
    ↳15 PiDPToQDPProof (⇐)
    ↳16 QDP
    ↳17 QDPOrderProof (⇔)
    ↳18 QDP
    ↳19 DependencyGraphProof (⇔)
    ↳20 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) PrologToPiTRSProof (SOUND transformation)

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

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x1, x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x1, x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x

(3) 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:

HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → DISTR_IN_GGAA(s(X), X, DL, DR)
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_GA(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x1, x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE_IN_GA(x1, x2)  =  HBAL_TREE_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
DISTR_IN_GGAA(x1, x2, x3, x4)  =  DISTR_IN_GGAA(x1, x2)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x1, x5, x6)
U3_GA(x1, x2, x3, x4, x5, x6)  =  U3_GA(x1, x2, x6)

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

(4) Obligation:

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

HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → DISTR_IN_GGAA(s(X), X, DL, DR)
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_GA(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x1, x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE_IN_GA(x1, x2)  =  HBAL_TREE_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
DISTR_IN_GGAA(x1, x2, x3, x4)  =  DISTR_IN_GGAA(x1, x2)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x1, x5, x6)
U3_GA(x1, x2, x3, x4, x5, x6)  =  U3_GA(x1, x2, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x1, x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x1, x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE_IN_GA(x1, x2)  =  HBAL_TREE_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x1, x5, x6)

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:

U1_GA(X, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, DR, hbal_tree_in_ga(DL))
U2_GA(X, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR)
HBAL_TREE_IN_GA(s(s(X))) → U1_GA(X, distr_in_ggaa(s(X), X))
U1_GA(X, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(X, distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, DR, hbal_tree_in_ga(DL))
U2_ga(X, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, hbal_tree_in_ga(DR))
U3_ga(X, L, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The set Q consists of the following terms:

hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0, x1)
U2_ga(x0, x1, x2)
U3_ga(x0, x1, x2)

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

(9) PrologToPiTRSProof (SOUND transformation)

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

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(10) Obligation:

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

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x

(11) 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:

HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → DISTR_IN_GGAA(s(X), X, DL, DR)
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_GA(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE_IN_GA(x1, x2)  =  HBAL_TREE_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
DISTR_IN_GGAA(x1, x2, x3, x4)  =  DISTR_IN_GGAA(x1, x2)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x5, x6)
U3_GA(x1, x2, x3, x4, x5, x6)  =  U3_GA(x2, x6)

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

(12) Obligation:

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

HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → DISTR_IN_GGAA(s(X), X, DL, DR)
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_GA(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE_IN_GA(x1, x2)  =  HBAL_TREE_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
DISTR_IN_GGAA(x1, x2, x3, x4)  =  DISTR_IN_GGAA(x1, x2)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x5, x6)
U3_GA(x1, x2, x3, x4, x5, x6)  =  U3_GA(x2, x6)

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

(13) DependencyGraphProof (EQUIVALENT transformation)

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

(14) Obligation:

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

U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_GA(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_GA(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → HBAL_TREE_IN_GA(DR, R)
HBAL_TREE_IN_GA(s(s(X)), t(x, L, R)) → U1_GA(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
U1_GA(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → HBAL_TREE_IN_GA(DL, L)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero, nil) → hbal_tree_out_ga(zero, nil)
hbal_tree_in_ga(s(zero), t(x, nil, nil)) → hbal_tree_out_ga(s(zero), t(x, nil, nil))
hbal_tree_in_ga(s(s(X)), t(x, L, R)) → U1_ga(X, L, R, distr_in_ggaa(s(X), X, DL, DR))
distr_in_ggaa(D1, X1, D1, D1) → distr_out_ggaa(D1, X1, D1, D1)
distr_in_ggaa(D1, D2, D1, D2) → distr_out_ggaa(D1, D2, D1, D2)
distr_in_ggaa(D1, D2, D2, D1) → distr_out_ggaa(D1, D2, D2, D1)
U1_ga(X, L, R, distr_out_ggaa(s(X), X, DL, DR)) → U2_ga(X, L, R, DL, DR, hbal_tree_in_ga(DL, L))
U2_ga(X, L, R, DL, DR, hbal_tree_out_ga(DL, L)) → U3_ga(X, L, R, DL, DR, hbal_tree_in_ga(DR, R))
U3_ga(X, L, R, DL, DR, hbal_tree_out_ga(DR, R)) → hbal_tree_out_ga(s(s(X)), t(x, L, R))

The argument filtering Pi contains the following mapping:
hbal_tree_in_ga(x1, x2)  =  hbal_tree_in_ga(x1)
zero  =  zero
hbal_tree_out_ga(x1, x2)  =  hbal_tree_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
distr_in_ggaa(x1, x2, x3, x4)  =  distr_in_ggaa(x1, x2)
distr_out_ggaa(x1, x2, x3, x4)  =  distr_out_ggaa(x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6)  =  U2_ga(x5, x6)
U3_ga(x1, x2, x3, x4, x5, x6)  =  U3_ga(x2, x6)
t(x1, x2, x3)  =  t(x1, x2, x3)
x  =  x
HBAL_TREE_IN_GA(x1, x2)  =  HBAL_TREE_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U2_GA(x1, x2, x3, x4, x5, x6)  =  U2_GA(x5, x6)

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

(15) PiDPToQDPProof (SOUND transformation)

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

(16) Obligation:

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

U1_GA(distr_out_ggaa(DL, DR)) → U2_GA(DR, hbal_tree_in_ga(DL))
U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
HBAL_TREE_IN_GA(s(s(X))) → U1_GA(distr_in_ggaa(s(X), X))
U1_GA(distr_out_ggaa(DL, DR)) → HBAL_TREE_IN_GA(DL)

The TRS R consists of the following rules:

hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))

The set Q consists of the following terms:

hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)

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

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U1_GA(distr_out_ggaa(DL, DR)) → U2_GA(DR, hbal_tree_in_ga(DL))
U1_GA(distr_out_ggaa(DL, DR)) → HBAL_TREE_IN_GA(DL)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(U1_GA(x1)) = -I + 5A·x1

POL(distr_out_ggaa(x1, x2)) = 5A + 5A·x1 + 5A·x2

POL(U2_GA(x1, x2)) = 5A + 5A·x1 + -I·x2

POL(hbal_tree_in_ga(x1)) = 5A + -I·x1

POL(hbal_tree_out_ga(x1)) = 5A + 5A·x1

POL(HBAL_TREE_IN_GA(x1)) = 5A + 5A·x1

POL(s(x1)) = 5A + 5A·x1

POL(distr_in_ggaa(x1, x2)) = 5A + 5A·x1 + 5A·x2

POL(zero) = 5A

POL(nil) = 5A

POL(t(x1, x2, x3)) = 5A + 5A·x1 + 5A·x2 + 5A·x3

POL(x) = 5A

POL(U1_ga(x1)) = 5A + -I·x1

POL(U2_ga(x1, x2)) = 5A + 5A·x1 + -I·x2

POL(U3_ga(x1, x2)) = -I + -I·x1 + 5A·x2

The following usable rules [FROCOS05] were oriented:

distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)

(18) Obligation:

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

U2_GA(DR, hbal_tree_out_ga(L)) → HBAL_TREE_IN_GA(DR)
HBAL_TREE_IN_GA(s(s(X))) → U1_GA(distr_in_ggaa(s(X), X))

The TRS R consists of the following rules:

hbal_tree_in_ga(zero) → hbal_tree_out_ga(nil)
hbal_tree_in_ga(s(zero)) → hbal_tree_out_ga(t(x, nil, nil))
hbal_tree_in_ga(s(s(X))) → U1_ga(distr_in_ggaa(s(X), X))
distr_in_ggaa(D1, X1) → distr_out_ggaa(D1, D1)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D1, D2)
distr_in_ggaa(D1, D2) → distr_out_ggaa(D2, D1)
U1_ga(distr_out_ggaa(DL, DR)) → U2_ga(DR, hbal_tree_in_ga(DL))
U2_ga(DR, hbal_tree_out_ga(L)) → U3_ga(L, hbal_tree_in_ga(DR))
U3_ga(L, hbal_tree_out_ga(R)) → hbal_tree_out_ga(t(x, L, R))

The set Q consists of the following terms:

hbal_tree_in_ga(x0)
distr_in_ggaa(x0, x1)
U1_ga(x0)
U2_ga(x0, x1)
U3_ga(x0, x1)

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

(19) DependencyGraphProof (EQUIVALENT transformation)

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

(20) TRUE