0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 70 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 96 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 PiDP
↳7 PiDPToQDPProof (⇒, 84 ms)
↳8 QDP
↳9 QDPOrderProof (⇔, 201 ms)
↳10 QDP
↳11 DependencyGraphProof (⇔, 0 ms)
↳12 TRUE
hbal_treeA_in_ga(zero, nil) → hbal_treeA_out_ga(zero, nil)
hbal_treeA_in_ga(s(zero), t(x, nil, nil)) → hbal_treeA_out_ga(s(zero), t(x, nil, nil))
hbal_treeA_in_ga(s(s(T15)), t(x, T9, T10)) → U1_ga(T15, T9, T10, pB_in_gaa(T15, T9, T10))
pB_in_gaa(T15, T9, T16) → U4_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
hbal_treeA_in_ga(s(s(T21)), t(x, T9, T10)) → U2_ga(T21, T9, T10, pC_in_gaa(T21, T9, T10))
pC_in_gaa(T21, T9, T22) → U6_gaa(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
hbal_treeA_in_ga(s(s(T25)), t(x, T9, T10)) → U3_ga(T25, T9, T10, pD_in_gaa(T25, T9, T10))
pD_in_gaa(T25, T9, T26) → U8_gaa(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
U8_gaa(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → U9_gaa(T25, T9, T26, hbal_treeA_in_ga(s(T25), T26))
U9_gaa(T25, T9, T26, hbal_treeA_out_ga(s(T25), T26)) → pD_out_gaa(T25, T9, T26)
U3_ga(T25, T9, T10, pD_out_gaa(T25, T9, T10)) → hbal_treeA_out_ga(s(s(T25)), t(x, T9, T10))
U6_gaa(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → U7_gaa(T21, T9, T22, hbal_treeA_in_ga(T21, T22))
U7_gaa(T21, T9, T22, hbal_treeA_out_ga(T21, T22)) → pC_out_gaa(T21, T9, T22)
U2_ga(T21, T9, T10, pC_out_gaa(T21, T9, T10)) → hbal_treeA_out_ga(s(s(T21)), t(x, T9, T10))
U4_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → U5_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T16))
U5_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T16)) → pB_out_gaa(T15, T9, T16)
U1_ga(T15, T9, T10, pB_out_gaa(T15, T9, T10)) → hbal_treeA_out_ga(s(s(T15)), t(x, T9, T10))
HBAL_TREEA_IN_GA(s(s(T15)), t(x, T9, T10)) → U1_GA(T15, T9, T10, pB_in_gaa(T15, T9, T10))
HBAL_TREEA_IN_GA(s(s(T15)), t(x, T9, T10)) → PB_IN_GAA(T15, T9, T10)
PB_IN_GAA(T15, T9, T16) → U4_GAA(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
PB_IN_GAA(T15, T9, T16) → HBAL_TREEA_IN_GA(s(T15), T9)
HBAL_TREEA_IN_GA(s(s(T21)), t(x, T9, T10)) → U2_GA(T21, T9, T10, pC_in_gaa(T21, T9, T10))
HBAL_TREEA_IN_GA(s(s(T21)), t(x, T9, T10)) → PC_IN_GAA(T21, T9, T10)
PC_IN_GAA(T21, T9, T22) → U6_GAA(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
PC_IN_GAA(T21, T9, T22) → HBAL_TREEA_IN_GA(s(T21), T9)
HBAL_TREEA_IN_GA(s(s(T25)), t(x, T9, T10)) → U3_GA(T25, T9, T10, pD_in_gaa(T25, T9, T10))
HBAL_TREEA_IN_GA(s(s(T25)), t(x, T9, T10)) → PD_IN_GAA(T25, T9, T10)
PD_IN_GAA(T25, T9, T26) → U8_GAA(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
PD_IN_GAA(T25, T9, T26) → HBAL_TREEA_IN_GA(T25, T9)
U8_GAA(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → U9_GAA(T25, T9, T26, hbal_treeA_in_ga(s(T25), T26))
U8_GAA(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → HBAL_TREEA_IN_GA(s(T25), T26)
U6_GAA(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → U7_GAA(T21, T9, T22, hbal_treeA_in_ga(T21, T22))
U6_GAA(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → HBAL_TREEA_IN_GA(T21, T22)
U4_GAA(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → U5_GAA(T15, T9, T16, hbal_treeA_in_ga(s(T15), T16))
U4_GAA(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → HBAL_TREEA_IN_GA(s(T15), T16)
hbal_treeA_in_ga(zero, nil) → hbal_treeA_out_ga(zero, nil)
hbal_treeA_in_ga(s(zero), t(x, nil, nil)) → hbal_treeA_out_ga(s(zero), t(x, nil, nil))
hbal_treeA_in_ga(s(s(T15)), t(x, T9, T10)) → U1_ga(T15, T9, T10, pB_in_gaa(T15, T9, T10))
pB_in_gaa(T15, T9, T16) → U4_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
hbal_treeA_in_ga(s(s(T21)), t(x, T9, T10)) → U2_ga(T21, T9, T10, pC_in_gaa(T21, T9, T10))
pC_in_gaa(T21, T9, T22) → U6_gaa(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
hbal_treeA_in_ga(s(s(T25)), t(x, T9, T10)) → U3_ga(T25, T9, T10, pD_in_gaa(T25, T9, T10))
pD_in_gaa(T25, T9, T26) → U8_gaa(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
U8_gaa(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → U9_gaa(T25, T9, T26, hbal_treeA_in_ga(s(T25), T26))
U9_gaa(T25, T9, T26, hbal_treeA_out_ga(s(T25), T26)) → pD_out_gaa(T25, T9, T26)
U3_ga(T25, T9, T10, pD_out_gaa(T25, T9, T10)) → hbal_treeA_out_ga(s(s(T25)), t(x, T9, T10))
U6_gaa(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → U7_gaa(T21, T9, T22, hbal_treeA_in_ga(T21, T22))
U7_gaa(T21, T9, T22, hbal_treeA_out_ga(T21, T22)) → pC_out_gaa(T21, T9, T22)
U2_ga(T21, T9, T10, pC_out_gaa(T21, T9, T10)) → hbal_treeA_out_ga(s(s(T21)), t(x, T9, T10))
U4_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → U5_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T16))
U5_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T16)) → pB_out_gaa(T15, T9, T16)
U1_ga(T15, T9, T10, pB_out_gaa(T15, T9, T10)) → hbal_treeA_out_ga(s(s(T15)), t(x, T9, T10))
HBAL_TREEA_IN_GA(s(s(T15)), t(x, T9, T10)) → U1_GA(T15, T9, T10, pB_in_gaa(T15, T9, T10))
HBAL_TREEA_IN_GA(s(s(T15)), t(x, T9, T10)) → PB_IN_GAA(T15, T9, T10)
PB_IN_GAA(T15, T9, T16) → U4_GAA(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
PB_IN_GAA(T15, T9, T16) → HBAL_TREEA_IN_GA(s(T15), T9)
HBAL_TREEA_IN_GA(s(s(T21)), t(x, T9, T10)) → U2_GA(T21, T9, T10, pC_in_gaa(T21, T9, T10))
HBAL_TREEA_IN_GA(s(s(T21)), t(x, T9, T10)) → PC_IN_GAA(T21, T9, T10)
PC_IN_GAA(T21, T9, T22) → U6_GAA(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
PC_IN_GAA(T21, T9, T22) → HBAL_TREEA_IN_GA(s(T21), T9)
HBAL_TREEA_IN_GA(s(s(T25)), t(x, T9, T10)) → U3_GA(T25, T9, T10, pD_in_gaa(T25, T9, T10))
HBAL_TREEA_IN_GA(s(s(T25)), t(x, T9, T10)) → PD_IN_GAA(T25, T9, T10)
PD_IN_GAA(T25, T9, T26) → U8_GAA(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
PD_IN_GAA(T25, T9, T26) → HBAL_TREEA_IN_GA(T25, T9)
U8_GAA(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → U9_GAA(T25, T9, T26, hbal_treeA_in_ga(s(T25), T26))
U8_GAA(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → HBAL_TREEA_IN_GA(s(T25), T26)
U6_GAA(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → U7_GAA(T21, T9, T22, hbal_treeA_in_ga(T21, T22))
U6_GAA(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → HBAL_TREEA_IN_GA(T21, T22)
U4_GAA(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → U5_GAA(T15, T9, T16, hbal_treeA_in_ga(s(T15), T16))
U4_GAA(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → HBAL_TREEA_IN_GA(s(T15), T16)
hbal_treeA_in_ga(zero, nil) → hbal_treeA_out_ga(zero, nil)
hbal_treeA_in_ga(s(zero), t(x, nil, nil)) → hbal_treeA_out_ga(s(zero), t(x, nil, nil))
hbal_treeA_in_ga(s(s(T15)), t(x, T9, T10)) → U1_ga(T15, T9, T10, pB_in_gaa(T15, T9, T10))
pB_in_gaa(T15, T9, T16) → U4_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
hbal_treeA_in_ga(s(s(T21)), t(x, T9, T10)) → U2_ga(T21, T9, T10, pC_in_gaa(T21, T9, T10))
pC_in_gaa(T21, T9, T22) → U6_gaa(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
hbal_treeA_in_ga(s(s(T25)), t(x, T9, T10)) → U3_ga(T25, T9, T10, pD_in_gaa(T25, T9, T10))
pD_in_gaa(T25, T9, T26) → U8_gaa(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
U8_gaa(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → U9_gaa(T25, T9, T26, hbal_treeA_in_ga(s(T25), T26))
U9_gaa(T25, T9, T26, hbal_treeA_out_ga(s(T25), T26)) → pD_out_gaa(T25, T9, T26)
U3_ga(T25, T9, T10, pD_out_gaa(T25, T9, T10)) → hbal_treeA_out_ga(s(s(T25)), t(x, T9, T10))
U6_gaa(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → U7_gaa(T21, T9, T22, hbal_treeA_in_ga(T21, T22))
U7_gaa(T21, T9, T22, hbal_treeA_out_ga(T21, T22)) → pC_out_gaa(T21, T9, T22)
U2_ga(T21, T9, T10, pC_out_gaa(T21, T9, T10)) → hbal_treeA_out_ga(s(s(T21)), t(x, T9, T10))
U4_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → U5_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T16))
U5_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T16)) → pB_out_gaa(T15, T9, T16)
U1_ga(T15, T9, T10, pB_out_gaa(T15, T9, T10)) → hbal_treeA_out_ga(s(s(T15)), t(x, T9, T10))
HBAL_TREEA_IN_GA(s(s(T15)), t(x, T9, T10)) → PB_IN_GAA(T15, T9, T10)
PB_IN_GAA(T15, T9, T16) → U4_GAA(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
U4_GAA(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → HBAL_TREEA_IN_GA(s(T15), T16)
HBAL_TREEA_IN_GA(s(s(T21)), t(x, T9, T10)) → PC_IN_GAA(T21, T9, T10)
PC_IN_GAA(T21, T9, T22) → U6_GAA(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
U6_GAA(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → HBAL_TREEA_IN_GA(T21, T22)
HBAL_TREEA_IN_GA(s(s(T25)), t(x, T9, T10)) → PD_IN_GAA(T25, T9, T10)
PD_IN_GAA(T25, T9, T26) → U8_GAA(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
U8_GAA(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → HBAL_TREEA_IN_GA(s(T25), T26)
PD_IN_GAA(T25, T9, T26) → HBAL_TREEA_IN_GA(T25, T9)
PC_IN_GAA(T21, T9, T22) → HBAL_TREEA_IN_GA(s(T21), T9)
PB_IN_GAA(T15, T9, T16) → HBAL_TREEA_IN_GA(s(T15), T9)
hbal_treeA_in_ga(zero, nil) → hbal_treeA_out_ga(zero, nil)
hbal_treeA_in_ga(s(zero), t(x, nil, nil)) → hbal_treeA_out_ga(s(zero), t(x, nil, nil))
hbal_treeA_in_ga(s(s(T15)), t(x, T9, T10)) → U1_ga(T15, T9, T10, pB_in_gaa(T15, T9, T10))
pB_in_gaa(T15, T9, T16) → U4_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T9))
hbal_treeA_in_ga(s(s(T21)), t(x, T9, T10)) → U2_ga(T21, T9, T10, pC_in_gaa(T21, T9, T10))
pC_in_gaa(T21, T9, T22) → U6_gaa(T21, T9, T22, hbal_treeA_in_ga(s(T21), T9))
hbal_treeA_in_ga(s(s(T25)), t(x, T9, T10)) → U3_ga(T25, T9, T10, pD_in_gaa(T25, T9, T10))
pD_in_gaa(T25, T9, T26) → U8_gaa(T25, T9, T26, hbal_treeA_in_ga(T25, T9))
U8_gaa(T25, T9, T26, hbal_treeA_out_ga(T25, T9)) → U9_gaa(T25, T9, T26, hbal_treeA_in_ga(s(T25), T26))
U9_gaa(T25, T9, T26, hbal_treeA_out_ga(s(T25), T26)) → pD_out_gaa(T25, T9, T26)
U3_ga(T25, T9, T10, pD_out_gaa(T25, T9, T10)) → hbal_treeA_out_ga(s(s(T25)), t(x, T9, T10))
U6_gaa(T21, T9, T22, hbal_treeA_out_ga(s(T21), T9)) → U7_gaa(T21, T9, T22, hbal_treeA_in_ga(T21, T22))
U7_gaa(T21, T9, T22, hbal_treeA_out_ga(T21, T22)) → pC_out_gaa(T21, T9, T22)
U2_ga(T21, T9, T10, pC_out_gaa(T21, T9, T10)) → hbal_treeA_out_ga(s(s(T21)), t(x, T9, T10))
U4_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T9)) → U5_gaa(T15, T9, T16, hbal_treeA_in_ga(s(T15), T16))
U5_gaa(T15, T9, T16, hbal_treeA_out_ga(s(T15), T16)) → pB_out_gaa(T15, T9, T16)
U1_ga(T15, T9, T10, pB_out_gaa(T15, T9, T10)) → hbal_treeA_out_ga(s(s(T15)), t(x, T9, T10))
HBAL_TREEA_IN_GA(s(s(T15))) → PB_IN_GAA(T15)
PB_IN_GAA(T15) → U4_GAA(T15, hbal_treeA_in_ga(s(T15)))
U4_GAA(T15, hbal_treeA_out_ga(s(T15), T9)) → HBAL_TREEA_IN_GA(s(T15))
HBAL_TREEA_IN_GA(s(s(T21))) → PC_IN_GAA(T21)
PC_IN_GAA(T21) → U6_GAA(T21, hbal_treeA_in_ga(s(T21)))
U6_GAA(T21, hbal_treeA_out_ga(s(T21), T9)) → HBAL_TREEA_IN_GA(T21)
HBAL_TREEA_IN_GA(s(s(T25))) → PD_IN_GAA(T25)
PD_IN_GAA(T25) → U8_GAA(T25, hbal_treeA_in_ga(T25))
U8_GAA(T25, hbal_treeA_out_ga(T25, T9)) → HBAL_TREEA_IN_GA(s(T25))
PD_IN_GAA(T25) → HBAL_TREEA_IN_GA(T25)
PC_IN_GAA(T21) → HBAL_TREEA_IN_GA(s(T21))
PB_IN_GAA(T15) → HBAL_TREEA_IN_GA(s(T15))
hbal_treeA_in_ga(zero) → hbal_treeA_out_ga(zero, nil)
hbal_treeA_in_ga(s(zero)) → hbal_treeA_out_ga(s(zero), t(x, nil, nil))
hbal_treeA_in_ga(s(s(T15))) → U1_ga(T15, pB_in_gaa(T15))
pB_in_gaa(T15) → U4_gaa(T15, hbal_treeA_in_ga(s(T15)))
hbal_treeA_in_ga(s(s(T21))) → U2_ga(T21, pC_in_gaa(T21))
pC_in_gaa(T21) → U6_gaa(T21, hbal_treeA_in_ga(s(T21)))
hbal_treeA_in_ga(s(s(T25))) → U3_ga(T25, pD_in_gaa(T25))
pD_in_gaa(T25) → U8_gaa(T25, hbal_treeA_in_ga(T25))
U8_gaa(T25, hbal_treeA_out_ga(T25, T9)) → U9_gaa(T25, T9, hbal_treeA_in_ga(s(T25)))
U9_gaa(T25, T9, hbal_treeA_out_ga(s(T25), T26)) → pD_out_gaa(T25, T9, T26)
U3_ga(T25, pD_out_gaa(T25, T9, T10)) → hbal_treeA_out_ga(s(s(T25)), t(x, T9, T10))
U6_gaa(T21, hbal_treeA_out_ga(s(T21), T9)) → U7_gaa(T21, T9, hbal_treeA_in_ga(T21))
U7_gaa(T21, T9, hbal_treeA_out_ga(T21, T22)) → pC_out_gaa(T21, T9, T22)
U2_ga(T21, pC_out_gaa(T21, T9, T10)) → hbal_treeA_out_ga(s(s(T21)), t(x, T9, T10))
U4_gaa(T15, hbal_treeA_out_ga(s(T15), T9)) → U5_gaa(T15, T9, hbal_treeA_in_ga(s(T15)))
U5_gaa(T15, T9, hbal_treeA_out_ga(s(T15), T16)) → pB_out_gaa(T15, T9, T16)
U1_ga(T15, pB_out_gaa(T15, T9, T10)) → hbal_treeA_out_ga(s(s(T15)), t(x, T9, T10))
hbal_treeA_in_ga(x0)
pB_in_gaa(x0)
pC_in_gaa(x0)
pD_in_gaa(x0)
U8_gaa(x0, x1)
U9_gaa(x0, x1, x2)
U3_ga(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1, x2)
U2_ga(x0, x1)
U4_gaa(x0, x1)
U5_gaa(x0, x1, x2)
U1_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HBAL_TREEA_IN_GA(s(s(T15))) → PB_IN_GAA(T15)
HBAL_TREEA_IN_GA(s(s(T21))) → PC_IN_GAA(T21)
PC_IN_GAA(T21) → U6_GAA(T21, hbal_treeA_in_ga(s(T21)))
HBAL_TREEA_IN_GA(s(s(T25))) → PD_IN_GAA(T25)
PD_IN_GAA(T25) → HBAL_TREEA_IN_GA(T25)
POL(HBAL_TREEA_IN_GA(x1)) = x1
POL(PB_IN_GAA(x1)) = 1 + x1
POL(PC_IN_GAA(x1)) = 1 + x1
POL(PD_IN_GAA(x1)) = 1 + x1
POL(U1_ga(x1, x2)) = 0
POL(U2_ga(x1, x2)) = 0
POL(U3_ga(x1, x2)) = 0
POL(U4_GAA(x1, x2)) = 1 + x1
POL(U4_gaa(x1, x2)) = 0
POL(U5_gaa(x1, x2, x3)) = 0
POL(U6_GAA(x1, x2)) = x1
POL(U6_gaa(x1, x2)) = 0
POL(U7_gaa(x1, x2, x3)) = 0
POL(U8_GAA(x1, x2)) = 1 + x1
POL(U8_gaa(x1, x2)) = 0
POL(U9_gaa(x1, x2, x3)) = 0
POL(hbal_treeA_in_ga(x1)) = 0
POL(hbal_treeA_out_ga(x1, x2)) = 0
POL(nil) = 0
POL(pB_in_gaa(x1)) = 0
POL(pB_out_gaa(x1, x2, x3)) = 0
POL(pC_in_gaa(x1)) = 0
POL(pC_out_gaa(x1, x2, x3)) = 0
POL(pD_in_gaa(x1)) = 0
POL(pD_out_gaa(x1, x2, x3)) = 0
POL(s(x1)) = 1 + x1
POL(t(x1, x2, x3)) = 0
POL(x) = 0
POL(zero) = 0
PB_IN_GAA(T15) → U4_GAA(T15, hbal_treeA_in_ga(s(T15)))
U4_GAA(T15, hbal_treeA_out_ga(s(T15), T9)) → HBAL_TREEA_IN_GA(s(T15))
U6_GAA(T21, hbal_treeA_out_ga(s(T21), T9)) → HBAL_TREEA_IN_GA(T21)
PD_IN_GAA(T25) → U8_GAA(T25, hbal_treeA_in_ga(T25))
U8_GAA(T25, hbal_treeA_out_ga(T25, T9)) → HBAL_TREEA_IN_GA(s(T25))
PC_IN_GAA(T21) → HBAL_TREEA_IN_GA(s(T21))
PB_IN_GAA(T15) → HBAL_TREEA_IN_GA(s(T15))
hbal_treeA_in_ga(zero) → hbal_treeA_out_ga(zero, nil)
hbal_treeA_in_ga(s(zero)) → hbal_treeA_out_ga(s(zero), t(x, nil, nil))
hbal_treeA_in_ga(s(s(T15))) → U1_ga(T15, pB_in_gaa(T15))
pB_in_gaa(T15) → U4_gaa(T15, hbal_treeA_in_ga(s(T15)))
hbal_treeA_in_ga(s(s(T21))) → U2_ga(T21, pC_in_gaa(T21))
pC_in_gaa(T21) → U6_gaa(T21, hbal_treeA_in_ga(s(T21)))
hbal_treeA_in_ga(s(s(T25))) → U3_ga(T25, pD_in_gaa(T25))
pD_in_gaa(T25) → U8_gaa(T25, hbal_treeA_in_ga(T25))
U8_gaa(T25, hbal_treeA_out_ga(T25, T9)) → U9_gaa(T25, T9, hbal_treeA_in_ga(s(T25)))
U9_gaa(T25, T9, hbal_treeA_out_ga(s(T25), T26)) → pD_out_gaa(T25, T9, T26)
U3_ga(T25, pD_out_gaa(T25, T9, T10)) → hbal_treeA_out_ga(s(s(T25)), t(x, T9, T10))
U6_gaa(T21, hbal_treeA_out_ga(s(T21), T9)) → U7_gaa(T21, T9, hbal_treeA_in_ga(T21))
U7_gaa(T21, T9, hbal_treeA_out_ga(T21, T22)) → pC_out_gaa(T21, T9, T22)
U2_ga(T21, pC_out_gaa(T21, T9, T10)) → hbal_treeA_out_ga(s(s(T21)), t(x, T9, T10))
U4_gaa(T15, hbal_treeA_out_ga(s(T15), T9)) → U5_gaa(T15, T9, hbal_treeA_in_ga(s(T15)))
U5_gaa(T15, T9, hbal_treeA_out_ga(s(T15), T16)) → pB_out_gaa(T15, T9, T16)
U1_ga(T15, pB_out_gaa(T15, T9, T10)) → hbal_treeA_out_ga(s(s(T15)), t(x, T9, T10))
hbal_treeA_in_ga(x0)
pB_in_gaa(x0)
pC_in_gaa(x0)
pD_in_gaa(x0)
U8_gaa(x0, x1)
U9_gaa(x0, x1, x2)
U3_ga(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1, x2)
U2_ga(x0, x1)
U4_gaa(x0, x1)
U5_gaa(x0, x1, x2)
U1_ga(x0, x1)