Left Termination of the query pattern times(b,b,f) w.r.t. the given Prolog program could successfully be proven:



PROLOG
  ↳ PrologToPiTRSProof

add3(b0, b0, b0).
add3(X, b0, X) :- binaryZ1(X).
add3(b0, Y, Y) :- binaryZ1(Y).
add3(X, Y, Z) :- addz3(X, Y, Z).
addx3(one1(X), b0, one1(X)) :- binary1(X).
addx3(zero1(X), b0, zero1(X)) :- binaryZ1(X).
addx3(X, Y, Z) :- addz3(X, Y, Z).
addy3(b0, one1(Y), one1(Y)) :- binary1(Y).
addy3(b0, zero1(Y), zero1(Y)) :- binaryZ1(Y).
addy3(X, Y, Z) :- addz3(X, Y, Z).
addz3(zero1(X), zero1(Y), zero1(Z)) :- addz3(X, Y, Z).
addz3(zero1(X), one1(Y), one1(Z)) :- addx3(X, Y, Z).
addz3(one1(X), zero1(Y), one1(Z)) :- addy3(X, Y, Z).
addz3(one1(X), one1(Y), zero1(Z)) :- addc3(X, Y, Z).
addc3(b0, b0, one1(b0)).
addc3(X, b0, Z) :- succZ2(X, Z).
addc3(b0, Y, Z) :- succZ2(Y, Z).
addc3(X, Y, Z) :- addC3(X, Y, Z).
addX3(zero1(X), b0, one1(X)) :- binaryZ1(X).
addX3(one1(X), b0, zero1(Z)) :- succ2(X, Z).
addX3(X, Y, Z) :- addC3(X, Y, Z).
addY3(b0, zero1(Y), one1(Y)) :- binaryZ1(Y).
addY3(b0, one1(Y), zero1(Z)) :- succ2(Y, Z).
addY3(X, Y, Z) :- addC3(X, Y, Z).
addC3(zero1(X), zero1(Y), one1(Z)) :- addz3(X, Y, Z).
addC3(zero1(X), one1(Y), zero1(Z)) :- addX3(X, Y, Z).
addC3(one1(X), zero1(Y), zero1(Z)) :- addY3(X, Y, Z).
addC3(one1(X), one1(Y), one1(Z)) :- addc3(X, Y, Z).
binary1(b0).
binary1(zero1(X)) :- binaryZ1(X).
binary1(one1(X)) :- binary1(X).
binaryZ1(zero1(X)) :- binaryZ1(X).
binaryZ1(one1(X)) :- binary1(X).
succ2(b0, one1(b0)).
succ2(zero1(X), one1(X)) :- binaryZ1(X).
succ2(one1(X), zero1(Z)) :- succ2(X, Z).
succZ2(zero1(X), one1(X)) :- binaryZ1(X).
succZ2(one1(X), zero1(Z)) :- succ2(X, Z).
times3(one1(b0), X, X).
times3(zero1(R), S, zero1(RS)) :- times3(R, S, RS).
times3(one1(R), S, RSS) :- times3(R, S, RS), add3(S, zero1(RS), RSS).


With regard to the inferred argument filtering the predicates were used in the following modes:
times3: (b,b,f)
add3: (b,b,f)
binaryZ1: (b)
binary1: (b)
addz3: (b,b,f)
addx3: (b,b,f)
addy3: (b,b,f)
addc3: (b,b,f)
succZ2: (b,f)
succ2: (b,f)
addC3: (b,b,f)
addX3: (b,b,f)
addY3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

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

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)


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

TIMES_3_IN_GGA3(zero_11(R), S, zero_11(RS)) -> IF_TIMES_3_IN_1_GGA4(R, S, RS, times_3_in_gga3(R, S, RS))
TIMES_3_IN_GGA3(zero_11(R), S, zero_11(RS)) -> TIMES_3_IN_GGA3(R, S, RS)
TIMES_3_IN_GGA3(one_11(R), S, RSS) -> IF_TIMES_3_IN_2_GGA4(R, S, RSS, times_3_in_gga3(R, S, RS))
TIMES_3_IN_GGA3(one_11(R), S, RSS) -> TIMES_3_IN_GGA3(R, S, RS)
IF_TIMES_3_IN_2_GGA4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> IF_TIMES_3_IN_3_GGA5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
IF_TIMES_3_IN_2_GGA4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> ADD_3_IN_GGA3(S, zero_11(RS), RSS)
ADD_3_IN_GGA3(X, b_0, X) -> IF_ADD_3_IN_1_GGA2(X, binaryZ_1_in_g1(X))
ADD_3_IN_GGA3(X, b_0, X) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(zero_11(X)) -> IF_BINARYZ_1_IN_1_G2(X, binaryZ_1_in_g1(X))
BINARYZ_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(one_11(X)) -> IF_BINARYZ_1_IN_2_G2(X, binary_1_in_g1(X))
BINARYZ_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(zero_11(X)) -> IF_BINARY_1_IN_1_G2(X, binaryZ_1_in_g1(X))
BINARY_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARY_1_IN_G1(one_11(X)) -> IF_BINARY_1_IN_2_G2(X, binary_1_in_g1(X))
BINARY_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
ADD_3_IN_GGA3(b_0, Y, Y) -> IF_ADD_3_IN_2_GGA2(Y, binaryZ_1_in_g1(Y))
ADD_3_IN_GGA3(b_0, Y, Y) -> BINARYZ_1_IN_G1(Y)
ADD_3_IN_GGA3(X, Y, Z) -> IF_ADD_3_IN_3_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_1_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), one_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_2_GGA4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_GGA3(X, Y, Z)
ADDX_3_IN_GGA3(one_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_GGA2(X, binary_1_in_g1(X))
ADDX_3_IN_GGA3(one_11(X), b_0, one_11(X)) -> BINARY_1_IN_G1(X)
ADDX_3_IN_GGA3(zero_11(X), b_0, zero_11(X)) -> IF_ADDX_3_IN_2_GGA2(X, binaryZ_1_in_g1(X))
ADDX_3_IN_GGA3(zero_11(X), b_0, zero_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_GGA3(X, Y, Z) -> IF_ADDX_3_IN_3_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDX_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), zero_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_3_GGA4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_GGA3(X, Y, Z)
ADDY_3_IN_GGA3(b_0, one_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_GGA2(Y, binary_1_in_g1(Y))
ADDY_3_IN_GGA3(b_0, one_11(Y), one_11(Y)) -> BINARY_1_IN_G1(Y)
ADDY_3_IN_GGA3(b_0, zero_11(Y), zero_11(Y)) -> IF_ADDY_3_IN_2_GGA2(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_GGA3(b_0, zero_11(Y), zero_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_GGA3(X, Y, Z) -> IF_ADDY_3_IN_3_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDY_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), one_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_4_GGA4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA3(X, b_0, Z) -> IF_ADDC_3_IN_1_GGA3(X, Z, succZ_2_in_ga2(X, Z))
ADDC_3_IN_GGA3(X, b_0, Z) -> SUCCZ_2_IN_GA2(X, Z)
SUCCZ_2_IN_GA2(zero_11(X), one_11(X)) -> IF_SUCCZ_2_IN_1_GA2(X, binaryZ_1_in_g1(X))
SUCCZ_2_IN_GA2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCCZ_2_IN_GA2(one_11(X), zero_11(Z)) -> IF_SUCCZ_2_IN_2_GA3(X, Z, succ_2_in_ga2(X, Z))
SUCCZ_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
SUCC_2_IN_GA2(zero_11(X), one_11(X)) -> IF_SUCC_2_IN_1_GA2(X, binaryZ_1_in_g1(X))
SUCC_2_IN_GA2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> IF_SUCC_2_IN_2_GA3(X, Z, succ_2_in_ga2(X, Z))
SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
ADDC_3_IN_GGA3(b_0, Y, Z) -> IF_ADDC_3_IN_2_GGA3(Y, Z, succZ_2_in_ga2(Y, Z))
ADDC_3_IN_GGA3(b_0, Y, Z) -> SUCCZ_2_IN_GA2(Y, Z)
ADDC_3_IN_GGA3(X, Y, Z) -> IF_ADDC_3_IN_3_GGA4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA3(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), zero_11(Y), one_11(Z)) -> IF_ADDC_3_IN_1_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), one_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_2_GGA4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_GGA13(X, Y, Z)
ADDX_3_IN_GGA13(zero_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_GGA12(X, binaryZ_1_in_g1(X))
ADDX_3_IN_GGA13(zero_11(X), b_0, one_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_GGA13(one_11(X), b_0, zero_11(Z)) -> IF_ADDX_3_IN_2_GGA3(X, Z, succ_2_in_ga2(X, Z))
ADDX_3_IN_GGA13(one_11(X), b_0, zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
ADDX_3_IN_GGA13(X, Y, Z) -> IF_ADDX_3_IN_3_GGA14(X, Y, Z, addC_3_in_gga3(X, Y, Z))
ADDX_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_3_GGA14(X, Y, Z, addY_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_GGA13(X, Y, Z)
ADDY_3_IN_GGA13(b_0, zero_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_GGA12(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_GGA13(b_0, zero_11(Y), one_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_GGA13(b_0, one_11(Y), zero_11(Z)) -> IF_ADDY_3_IN_2_GGA3(Y, Z, succ_2_in_ga2(Y, Z))
ADDY_3_IN_GGA13(b_0, one_11(Y), zero_11(Z)) -> SUCC_2_IN_GA2(Y, Z)
ADDY_3_IN_GGA13(X, Y, Z) -> IF_ADDY_3_IN_3_GGA14(X, Y, Z, addC_3_in_gga3(X, Y, Z))
ADDY_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), one_11(Y), one_11(Z)) -> IF_ADDC_3_IN_4_GGA4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)
IF_TIMES_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_1_GGA1(x4)
IF_ADDC_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_2_GGA1(x4)
IF_ADDY_3_IN_1_GGA12(x1, x2)  =  IF_ADDY_3_IN_1_GGA12(x1, x2)
IF_ADDY_3_IN_2_GGA3(x1, x2, x3)  =  IF_ADDY_3_IN_2_GGA1(x3)
IF_ADDX_3_IN_3_GGA14(x1, x2, x3, x4)  =  IF_ADDX_3_IN_3_GGA11(x4)
IF_ADDC_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_1_GGA1(x4)
IF_ADDC_3_IN_3_GGA14(x1, x2, x3, x4)  =  IF_ADDC_3_IN_3_GGA11(x4)
IF_ADDX_3_IN_2_GGA3(x1, x2, x3)  =  IF_ADDX_3_IN_2_GGA1(x3)
IF_BINARYZ_1_IN_1_G2(x1, x2)  =  IF_BINARYZ_1_IN_1_G1(x2)
ADDY_3_IN_GGA13(x1, x2, x3)  =  ADDY_3_IN_GGA12(x1, x2)
IF_ADDZ_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_2_GGA1(x4)
IF_ADDC_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_3_GGA1(x4)
IF_BINARY_1_IN_1_G2(x1, x2)  =  IF_BINARY_1_IN_1_G1(x2)
IF_ADDX_3_IN_1_GGA12(x1, x2)  =  IF_ADDX_3_IN_1_GGA12(x1, x2)
IF_ADD_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_3_GGA1(x4)
SUCCZ_2_IN_GA2(x1, x2)  =  SUCCZ_2_IN_GA1(x1)
IF_TIMES_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_TIMES_3_IN_3_GGA1(x5)
IF_ADD_3_IN_1_GGA2(x1, x2)  =  IF_ADD_3_IN_1_GGA2(x1, x2)
IF_BINARYZ_1_IN_2_G2(x1, x2)  =  IF_BINARYZ_1_IN_2_G1(x2)
IF_ADDZ_3_IN_4_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_4_GGA1(x4)
IF_ADDZ_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_3_GGA1(x4)
IF_SUCCZ_2_IN_2_GA3(x1, x2, x3)  =  IF_SUCCZ_2_IN_2_GA1(x3)
IF_ADDC_3_IN_1_GGA3(x1, x2, x3)  =  IF_ADDC_3_IN_1_GGA1(x3)
IF_ADDY_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDY_3_IN_3_GGA1(x4)
ADDY_3_IN_GGA3(x1, x2, x3)  =  ADDY_3_IN_GGA2(x1, x2)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
BINARYZ_1_IN_G1(x1)  =  BINARYZ_1_IN_G1(x1)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)
ADDZ_3_IN_GGA3(x1, x2, x3)  =  ADDZ_3_IN_GGA2(x1, x2)
IF_ADD_3_IN_2_GGA2(x1, x2)  =  IF_ADD_3_IN_2_GGA2(x1, x2)
IF_SUCC_2_IN_1_GA2(x1, x2)  =  IF_SUCC_2_IN_1_GA2(x1, x2)
IF_ADDX_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDX_3_IN_3_GGA1(x4)
ADDC_3_IN_GGA13(x1, x2, x3)  =  ADDC_3_IN_GGA12(x1, x2)
IF_ADDC_3_IN_4_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_4_GGA1(x4)
IF_ADDX_3_IN_1_GGA2(x1, x2)  =  IF_ADDX_3_IN_1_GGA2(x1, x2)
IF_BINARY_1_IN_2_G2(x1, x2)  =  IF_BINARY_1_IN_2_G1(x2)
ADDC_3_IN_GGA3(x1, x2, x3)  =  ADDC_3_IN_GGA2(x1, x2)
IF_ADDY_3_IN_1_GGA2(x1, x2)  =  IF_ADDY_3_IN_1_GGA2(x1, x2)
IF_TIMES_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_2_GGA2(x2, x4)
ADDX_3_IN_GGA13(x1, x2, x3)  =  ADDX_3_IN_GGA12(x1, x2)
IF_ADDZ_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_1_GGA1(x4)
IF_SUCCZ_2_IN_1_GA2(x1, x2)  =  IF_SUCCZ_2_IN_1_GA2(x1, x2)
IF_ADDY_3_IN_2_GGA2(x1, x2)  =  IF_ADDY_3_IN_2_GGA2(x1, x2)
SUCC_2_IN_GA2(x1, x2)  =  SUCC_2_IN_GA1(x1)
IF_ADDY_3_IN_3_GGA14(x1, x2, x3, x4)  =  IF_ADDY_3_IN_3_GGA11(x4)
IF_ADDX_3_IN_2_GGA2(x1, x2)  =  IF_ADDX_3_IN_2_GGA2(x1, x2)
BINARY_1_IN_G1(x1)  =  BINARY_1_IN_G1(x1)
ADDX_3_IN_GGA3(x1, x2, x3)  =  ADDX_3_IN_GGA2(x1, x2)
IF_SUCC_2_IN_2_GA3(x1, x2, x3)  =  IF_SUCC_2_IN_2_GA1(x3)
IF_ADDC_3_IN_2_GGA3(x1, x2, x3)  =  IF_ADDC_3_IN_2_GGA1(x3)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

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

TIMES_3_IN_GGA3(zero_11(R), S, zero_11(RS)) -> IF_TIMES_3_IN_1_GGA4(R, S, RS, times_3_in_gga3(R, S, RS))
TIMES_3_IN_GGA3(zero_11(R), S, zero_11(RS)) -> TIMES_3_IN_GGA3(R, S, RS)
TIMES_3_IN_GGA3(one_11(R), S, RSS) -> IF_TIMES_3_IN_2_GGA4(R, S, RSS, times_3_in_gga3(R, S, RS))
TIMES_3_IN_GGA3(one_11(R), S, RSS) -> TIMES_3_IN_GGA3(R, S, RS)
IF_TIMES_3_IN_2_GGA4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> IF_TIMES_3_IN_3_GGA5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
IF_TIMES_3_IN_2_GGA4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> ADD_3_IN_GGA3(S, zero_11(RS), RSS)
ADD_3_IN_GGA3(X, b_0, X) -> IF_ADD_3_IN_1_GGA2(X, binaryZ_1_in_g1(X))
ADD_3_IN_GGA3(X, b_0, X) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(zero_11(X)) -> IF_BINARYZ_1_IN_1_G2(X, binaryZ_1_in_g1(X))
BINARYZ_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(one_11(X)) -> IF_BINARYZ_1_IN_2_G2(X, binary_1_in_g1(X))
BINARYZ_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(zero_11(X)) -> IF_BINARY_1_IN_1_G2(X, binaryZ_1_in_g1(X))
BINARY_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARY_1_IN_G1(one_11(X)) -> IF_BINARY_1_IN_2_G2(X, binary_1_in_g1(X))
BINARY_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
ADD_3_IN_GGA3(b_0, Y, Y) -> IF_ADD_3_IN_2_GGA2(Y, binaryZ_1_in_g1(Y))
ADD_3_IN_GGA3(b_0, Y, Y) -> BINARYZ_1_IN_G1(Y)
ADD_3_IN_GGA3(X, Y, Z) -> IF_ADD_3_IN_3_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_1_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), one_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_2_GGA4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_GGA3(X, Y, Z)
ADDX_3_IN_GGA3(one_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_GGA2(X, binary_1_in_g1(X))
ADDX_3_IN_GGA3(one_11(X), b_0, one_11(X)) -> BINARY_1_IN_G1(X)
ADDX_3_IN_GGA3(zero_11(X), b_0, zero_11(X)) -> IF_ADDX_3_IN_2_GGA2(X, binaryZ_1_in_g1(X))
ADDX_3_IN_GGA3(zero_11(X), b_0, zero_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_GGA3(X, Y, Z) -> IF_ADDX_3_IN_3_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDX_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), zero_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_3_GGA4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_GGA3(X, Y, Z)
ADDY_3_IN_GGA3(b_0, one_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_GGA2(Y, binary_1_in_g1(Y))
ADDY_3_IN_GGA3(b_0, one_11(Y), one_11(Y)) -> BINARY_1_IN_G1(Y)
ADDY_3_IN_GGA3(b_0, zero_11(Y), zero_11(Y)) -> IF_ADDY_3_IN_2_GGA2(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_GGA3(b_0, zero_11(Y), zero_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_GGA3(X, Y, Z) -> IF_ADDY_3_IN_3_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDY_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), one_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_4_GGA4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
ADDZ_3_IN_GGA3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA3(X, b_0, Z) -> IF_ADDC_3_IN_1_GGA3(X, Z, succZ_2_in_ga2(X, Z))
ADDC_3_IN_GGA3(X, b_0, Z) -> SUCCZ_2_IN_GA2(X, Z)
SUCCZ_2_IN_GA2(zero_11(X), one_11(X)) -> IF_SUCCZ_2_IN_1_GA2(X, binaryZ_1_in_g1(X))
SUCCZ_2_IN_GA2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCCZ_2_IN_GA2(one_11(X), zero_11(Z)) -> IF_SUCCZ_2_IN_2_GA3(X, Z, succ_2_in_ga2(X, Z))
SUCCZ_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
SUCC_2_IN_GA2(zero_11(X), one_11(X)) -> IF_SUCC_2_IN_1_GA2(X, binaryZ_1_in_g1(X))
SUCC_2_IN_GA2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> IF_SUCC_2_IN_2_GA3(X, Z, succ_2_in_ga2(X, Z))
SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
ADDC_3_IN_GGA3(b_0, Y, Z) -> IF_ADDC_3_IN_2_GGA3(Y, Z, succZ_2_in_ga2(Y, Z))
ADDC_3_IN_GGA3(b_0, Y, Z) -> SUCCZ_2_IN_GA2(Y, Z)
ADDC_3_IN_GGA3(X, Y, Z) -> IF_ADDC_3_IN_3_GGA4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA3(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), zero_11(Y), one_11(Z)) -> IF_ADDC_3_IN_1_GGA4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), one_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_2_GGA4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_GGA13(X, Y, Z)
ADDX_3_IN_GGA13(zero_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_GGA12(X, binaryZ_1_in_g1(X))
ADDX_3_IN_GGA13(zero_11(X), b_0, one_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_GGA13(one_11(X), b_0, zero_11(Z)) -> IF_ADDX_3_IN_2_GGA3(X, Z, succ_2_in_ga2(X, Z))
ADDX_3_IN_GGA13(one_11(X), b_0, zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
ADDX_3_IN_GGA13(X, Y, Z) -> IF_ADDX_3_IN_3_GGA14(X, Y, Z, addC_3_in_gga3(X, Y, Z))
ADDX_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_3_GGA14(X, Y, Z, addY_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_GGA13(X, Y, Z)
ADDY_3_IN_GGA13(b_0, zero_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_GGA12(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_GGA13(b_0, zero_11(Y), one_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_GGA13(b_0, one_11(Y), zero_11(Z)) -> IF_ADDY_3_IN_2_GGA3(Y, Z, succ_2_in_ga2(Y, Z))
ADDY_3_IN_GGA13(b_0, one_11(Y), zero_11(Z)) -> SUCC_2_IN_GA2(Y, Z)
ADDY_3_IN_GGA13(X, Y, Z) -> IF_ADDY_3_IN_3_GGA14(X, Y, Z, addC_3_in_gga3(X, Y, Z))
ADDY_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), one_11(Y), one_11(Z)) -> IF_ADDC_3_IN_4_GGA4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
ADDC_3_IN_GGA13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)
IF_TIMES_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_1_GGA1(x4)
IF_ADDC_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_2_GGA1(x4)
IF_ADDY_3_IN_1_GGA12(x1, x2)  =  IF_ADDY_3_IN_1_GGA12(x1, x2)
IF_ADDY_3_IN_2_GGA3(x1, x2, x3)  =  IF_ADDY_3_IN_2_GGA1(x3)
IF_ADDX_3_IN_3_GGA14(x1, x2, x3, x4)  =  IF_ADDX_3_IN_3_GGA11(x4)
IF_ADDC_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_1_GGA1(x4)
IF_ADDC_3_IN_3_GGA14(x1, x2, x3, x4)  =  IF_ADDC_3_IN_3_GGA11(x4)
IF_ADDX_3_IN_2_GGA3(x1, x2, x3)  =  IF_ADDX_3_IN_2_GGA1(x3)
IF_BINARYZ_1_IN_1_G2(x1, x2)  =  IF_BINARYZ_1_IN_1_G1(x2)
ADDY_3_IN_GGA13(x1, x2, x3)  =  ADDY_3_IN_GGA12(x1, x2)
IF_ADDZ_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_2_GGA1(x4)
IF_ADDC_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_3_GGA1(x4)
IF_BINARY_1_IN_1_G2(x1, x2)  =  IF_BINARY_1_IN_1_G1(x2)
IF_ADDX_3_IN_1_GGA12(x1, x2)  =  IF_ADDX_3_IN_1_GGA12(x1, x2)
IF_ADD_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_3_GGA1(x4)
SUCCZ_2_IN_GA2(x1, x2)  =  SUCCZ_2_IN_GA1(x1)
IF_TIMES_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_TIMES_3_IN_3_GGA1(x5)
IF_ADD_3_IN_1_GGA2(x1, x2)  =  IF_ADD_3_IN_1_GGA2(x1, x2)
IF_BINARYZ_1_IN_2_G2(x1, x2)  =  IF_BINARYZ_1_IN_2_G1(x2)
IF_ADDZ_3_IN_4_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_4_GGA1(x4)
IF_ADDZ_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_3_GGA1(x4)
IF_SUCCZ_2_IN_2_GA3(x1, x2, x3)  =  IF_SUCCZ_2_IN_2_GA1(x3)
IF_ADDC_3_IN_1_GGA3(x1, x2, x3)  =  IF_ADDC_3_IN_1_GGA1(x3)
IF_ADDY_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDY_3_IN_3_GGA1(x4)
ADDY_3_IN_GGA3(x1, x2, x3)  =  ADDY_3_IN_GGA2(x1, x2)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
BINARYZ_1_IN_G1(x1)  =  BINARYZ_1_IN_G1(x1)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)
ADDZ_3_IN_GGA3(x1, x2, x3)  =  ADDZ_3_IN_GGA2(x1, x2)
IF_ADD_3_IN_2_GGA2(x1, x2)  =  IF_ADD_3_IN_2_GGA2(x1, x2)
IF_SUCC_2_IN_1_GA2(x1, x2)  =  IF_SUCC_2_IN_1_GA2(x1, x2)
IF_ADDX_3_IN_3_GGA4(x1, x2, x3, x4)  =  IF_ADDX_3_IN_3_GGA1(x4)
ADDC_3_IN_GGA13(x1, x2, x3)  =  ADDC_3_IN_GGA12(x1, x2)
IF_ADDC_3_IN_4_GGA4(x1, x2, x3, x4)  =  IF_ADDC_3_IN_4_GGA1(x4)
IF_ADDX_3_IN_1_GGA2(x1, x2)  =  IF_ADDX_3_IN_1_GGA2(x1, x2)
IF_BINARY_1_IN_2_G2(x1, x2)  =  IF_BINARY_1_IN_2_G1(x2)
ADDC_3_IN_GGA3(x1, x2, x3)  =  ADDC_3_IN_GGA2(x1, x2)
IF_ADDY_3_IN_1_GGA2(x1, x2)  =  IF_ADDY_3_IN_1_GGA2(x1, x2)
IF_TIMES_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_TIMES_3_IN_2_GGA2(x2, x4)
ADDX_3_IN_GGA13(x1, x2, x3)  =  ADDX_3_IN_GGA12(x1, x2)
IF_ADDZ_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADDZ_3_IN_1_GGA1(x4)
IF_SUCCZ_2_IN_1_GA2(x1, x2)  =  IF_SUCCZ_2_IN_1_GA2(x1, x2)
IF_ADDY_3_IN_2_GGA2(x1, x2)  =  IF_ADDY_3_IN_2_GGA2(x1, x2)
SUCC_2_IN_GA2(x1, x2)  =  SUCC_2_IN_GA1(x1)
IF_ADDY_3_IN_3_GGA14(x1, x2, x3, x4)  =  IF_ADDY_3_IN_3_GGA11(x4)
IF_ADDX_3_IN_2_GGA2(x1, x2)  =  IF_ADDX_3_IN_2_GGA2(x1, x2)
BINARY_1_IN_G1(x1)  =  BINARY_1_IN_G1(x1)
ADDX_3_IN_GGA3(x1, x2, x3)  =  ADDX_3_IN_GGA2(x1, x2)
IF_SUCC_2_IN_2_GA3(x1, x2, x3)  =  IF_SUCC_2_IN_2_GA1(x3)
IF_ADDC_3_IN_2_GGA3(x1, x2, x3)  =  IF_ADDC_3_IN_2_GGA1(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 4 SCCs with 54 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

BINARYZ_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)

The TRS R consists of the following rules:

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)
BINARYZ_1_IN_G1(x1)  =  BINARYZ_1_IN_G1(x1)
BINARY_1_IN_G1(x1)  =  BINARY_1_IN_G1(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

BINARYZ_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

BINARYZ_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(one_11(X)) -> BINARY_1_IN_G1(X)
BINARY_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)
BINARYZ_1_IN_G1(zero_11(X)) -> BINARYZ_1_IN_G1(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {BINARY_1_IN_G1, BINARYZ_1_IN_G1}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

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

SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)

The TRS R consists of the following rules:

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)
SUCC_2_IN_GA2(x1, x2)  =  SUCC_2_IN_GA1(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

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

SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)

R is empty.
The argument filtering Pi contains the following mapping:
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
SUCC_2_IN_GA2(x1, x2)  =  SUCC_2_IN_GA1(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

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

SUCC_2_IN_GA1(one_11(X)) -> SUCC_2_IN_GA1(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SUCC_2_IN_GA1}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP

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

ADDX_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA3(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_GGA13(X, Y, Z)
ADDY_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)
ADDX_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDY_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)
ADDY_3_IN_GGA13(x1, x2, x3)  =  ADDY_3_IN_GGA12(x1, x2)
ADDY_3_IN_GGA3(x1, x2, x3)  =  ADDY_3_IN_GGA2(x1, x2)
ADDZ_3_IN_GGA3(x1, x2, x3)  =  ADDZ_3_IN_GGA2(x1, x2)
ADDC_3_IN_GGA13(x1, x2, x3)  =  ADDC_3_IN_GGA12(x1, x2)
ADDC_3_IN_GGA3(x1, x2, x3)  =  ADDC_3_IN_GGA2(x1, x2)
ADDX_3_IN_GGA13(x1, x2, x3)  =  ADDX_3_IN_GGA12(x1, x2)
ADDX_3_IN_GGA3(x1, x2, x3)  =  ADDX_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

ADDX_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_GGA3(X, Y, Z)
ADDC_3_IN_GGA13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA3(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDC_3_IN_GGA13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_GGA13(X, Y, Z)
ADDY_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_GGA3(X, Y, Z)
ADDX_3_IN_GGA3(X, Y, Z) -> ADDZ_3_IN_GGA3(X, Y, Z)
ADDY_3_IN_GGA13(X, Y, Z) -> ADDC_3_IN_GGA13(X, Y, Z)
ADDZ_3_IN_GGA3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_GGA3(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
ADDY_3_IN_GGA13(x1, x2, x3)  =  ADDY_3_IN_GGA12(x1, x2)
ADDY_3_IN_GGA3(x1, x2, x3)  =  ADDY_3_IN_GGA2(x1, x2)
ADDZ_3_IN_GGA3(x1, x2, x3)  =  ADDZ_3_IN_GGA2(x1, x2)
ADDC_3_IN_GGA13(x1, x2, x3)  =  ADDC_3_IN_GGA12(x1, x2)
ADDC_3_IN_GGA3(x1, x2, x3)  =  ADDC_3_IN_GGA2(x1, x2)
ADDX_3_IN_GGA13(x1, x2, x3)  =  ADDX_3_IN_GGA12(x1, x2)
ADDX_3_IN_GGA3(x1, x2, x3)  =  ADDX_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

ADDX_3_IN_GGA12(X, Y) -> ADDC_3_IN_GGA12(X, Y)
ADDC_3_IN_GGA12(zero_11(X), zero_11(Y)) -> ADDZ_3_IN_GGA2(X, Y)
ADDC_3_IN_GGA12(one_11(X), one_11(Y)) -> ADDC_3_IN_GGA2(X, Y)
ADDZ_3_IN_GGA2(zero_11(X), one_11(Y)) -> ADDX_3_IN_GGA2(X, Y)
ADDC_3_IN_GGA12(zero_11(X), one_11(Y)) -> ADDX_3_IN_GGA12(X, Y)
ADDC_3_IN_GGA2(X, Y) -> ADDC_3_IN_GGA12(X, Y)
ADDC_3_IN_GGA12(one_11(X), zero_11(Y)) -> ADDY_3_IN_GGA12(X, Y)
ADDY_3_IN_GGA2(X, Y) -> ADDZ_3_IN_GGA2(X, Y)
ADDZ_3_IN_GGA2(zero_11(X), zero_11(Y)) -> ADDZ_3_IN_GGA2(X, Y)
ADDZ_3_IN_GGA2(one_11(X), one_11(Y)) -> ADDC_3_IN_GGA2(X, Y)
ADDX_3_IN_GGA2(X, Y) -> ADDZ_3_IN_GGA2(X, Y)
ADDY_3_IN_GGA12(X, Y) -> ADDC_3_IN_GGA12(X, Y)
ADDZ_3_IN_GGA2(one_11(X), zero_11(Y)) -> ADDY_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ADDC_3_IN_GGA12, ADDX_3_IN_GGA12, ADDZ_3_IN_GGA2, ADDC_3_IN_GGA2, ADDX_3_IN_GGA2, ADDY_3_IN_GGA12, ADDY_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof

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

TIMES_3_IN_GGA3(zero_11(R), S, zero_11(RS)) -> TIMES_3_IN_GGA3(R, S, RS)
TIMES_3_IN_GGA3(one_11(R), S, RSS) -> TIMES_3_IN_GGA3(R, S, RS)

The TRS R consists of the following rules:

times_3_in_gga3(one_11(b_0), X, X) -> times_3_out_gga3(one_11(b_0), X, X)
times_3_in_gga3(zero_11(R), S, zero_11(RS)) -> if_times_3_in_1_gga4(R, S, RS, times_3_in_gga3(R, S, RS))
times_3_in_gga3(one_11(R), S, RSS) -> if_times_3_in_2_gga4(R, S, RSS, times_3_in_gga3(R, S, RS))
if_times_3_in_2_gga4(R, S, RSS, times_3_out_gga3(R, S, RS)) -> if_times_3_in_3_gga5(R, S, RSS, RS, add_3_in_gga3(S, zero_11(RS), RSS))
add_3_in_gga3(b_0, b_0, b_0) -> add_3_out_gga3(b_0, b_0, b_0)
add_3_in_gga3(X, b_0, X) -> if_add_3_in_1_gga2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(zero_11(X)) -> if_binaryZ_1_in_1_g2(X, binaryZ_1_in_g1(X))
binaryZ_1_in_g1(one_11(X)) -> if_binaryZ_1_in_2_g2(X, binary_1_in_g1(X))
binary_1_in_g1(b_0) -> binary_1_out_g1(b_0)
binary_1_in_g1(zero_11(X)) -> if_binary_1_in_1_g2(X, binaryZ_1_in_g1(X))
if_binary_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binary_1_out_g1(zero_11(X))
binary_1_in_g1(one_11(X)) -> if_binary_1_in_2_g2(X, binary_1_in_g1(X))
if_binary_1_in_2_g2(X, binary_1_out_g1(X)) -> binary_1_out_g1(one_11(X))
if_binaryZ_1_in_2_g2(X, binary_1_out_g1(X)) -> binaryZ_1_out_g1(one_11(X))
if_binaryZ_1_in_1_g2(X, binaryZ_1_out_g1(X)) -> binaryZ_1_out_g1(zero_11(X))
if_add_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> add_3_out_gga3(X, b_0, X)
add_3_in_gga3(b_0, Y, Y) -> if_add_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_gga3(b_0, Y, Y)
add_3_in_gga3(X, Y, Z) -> if_add_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_gga4(X, Y, Z, addx_3_in_gga3(X, Y, Z))
addx_3_in_gga3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_gga2(X, binary_1_in_g1(X))
if_addx_3_in_1_gga2(X, binary_1_out_g1(X)) -> addx_3_out_gga3(one_11(X), b_0, one_11(X))
addx_3_in_gga3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_gga2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_gga2(X, binaryZ_1_out_g1(X)) -> addx_3_out_gga3(zero_11(X), b_0, zero_11(X))
addx_3_in_gga3(X, Y, Z) -> if_addx_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_gga4(X, Y, Z, addy_3_in_gga3(X, Y, Z))
addy_3_in_gga3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_gga2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_gga2(Y, binary_1_out_g1(Y)) -> addy_3_out_gga3(b_0, one_11(Y), one_11(Y))
addy_3_in_gga3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_gga2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_gga2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_gga3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_gga3(X, Y, Z) -> if_addy_3_in_3_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
addz_3_in_gga3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
addc_3_in_gga3(b_0, b_0, one_11(b_0)) -> addc_3_out_gga3(b_0, b_0, one_11(b_0))
addc_3_in_gga3(X, b_0, Z) -> if_addc_3_in_1_gga3(X, Z, succZ_2_in_ga2(X, Z))
succZ_2_in_ga2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ga2(zero_11(X), one_11(X))
succZ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
succ_2_in_ga2(b_0, one_11(b_0)) -> succ_2_out_ga2(b_0, one_11(b_0))
succ_2_in_ga2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ga2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ga2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ga2(zero_11(X), one_11(X))
succ_2_in_ga2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ga3(X, Z, succ_2_in_ga2(X, Z))
if_succ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succ_2_out_ga2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ga3(X, Z, succ_2_out_ga2(X, Z)) -> succZ_2_out_ga2(one_11(X), zero_11(Z))
if_addc_3_in_1_gga3(X, Z, succZ_2_out_ga2(X, Z)) -> addc_3_out_gga3(X, b_0, Z)
addc_3_in_gga3(b_0, Y, Z) -> if_addc_3_in_2_gga3(Y, Z, succZ_2_in_ga2(Y, Z))
if_addc_3_in_2_gga3(Y, Z, succZ_2_out_ga2(Y, Z)) -> addc_3_out_gga3(b_0, Y, Z)
addc_3_in_gga3(X, Y, Z) -> if_addc_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_gga4(X, Y, Z, addz_3_in_gga3(X, Y, Z))
if_addC_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_gga3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_gga4(X, Y, Z, addX_3_in_gga3(X, Y, Z))
addX_3_in_gga3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_gga2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_gga2(X, binaryZ_1_out_g1(X)) -> addX_3_out_gga3(zero_11(X), b_0, one_11(X))
addX_3_in_gga3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_gga3(X, Z, succ_2_in_ga2(X, Z))
if_addX_3_in_2_gga3(X, Z, succ_2_out_ga2(X, Z)) -> addX_3_out_gga3(one_11(X), b_0, zero_11(Z))
addX_3_in_gga3(X, Y, Z) -> if_addX_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_gga4(X, Y, Z, addY_3_in_gga3(X, Y, Z))
addY_3_in_gga3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_gga2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_gga2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_gga3(b_0, zero_11(Y), one_11(Y))
addY_3_in_gga3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_gga3(Y, Z, succ_2_in_ga2(Y, Z))
if_addY_3_in_2_gga3(Y, Z, succ_2_out_ga2(Y, Z)) -> addY_3_out_gga3(b_0, one_11(Y), zero_11(Z))
addY_3_in_gga3(X, Y, Z) -> if_addY_3_in_3_gga4(X, Y, Z, addC_3_in_gga3(X, Y, Z))
addC_3_in_gga3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_gga4(X, Y, Z, addc_3_in_gga3(X, Y, Z))
if_addC_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addY_3_out_gga3(X, Y, Z)
if_addC_3_in_3_gga4(X, Y, Z, addY_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addX_3_out_gga3(X, Y, Z)
if_addC_3_in_2_gga4(X, Y, Z, addX_3_out_gga3(X, Y, Z)) -> addC_3_out_gga3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_gga4(X, Y, Z, addC_3_out_gga3(X, Y, Z)) -> addc_3_out_gga3(X, Y, Z)
if_addz_3_in_4_gga4(X, Y, Z, addc_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addy_3_out_gga3(X, Y, Z)
if_addz_3_in_3_gga4(X, Y, Z, addy_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addx_3_out_gga3(X, Y, Z)
if_addz_3_in_2_gga4(X, Y, Z, addx_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> addz_3_out_gga3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_gga4(X, Y, Z, addz_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(X, Y, Z)
if_times_3_in_3_gga5(R, S, RSS, RS, add_3_out_gga3(S, zero_11(RS), RSS)) -> times_3_out_gga3(one_11(R), S, RSS)
if_times_3_in_1_gga4(R, S, RS, times_3_out_gga3(R, S, RS)) -> times_3_out_gga3(zero_11(R), S, zero_11(RS))

The argument filtering Pi contains the following mapping:
times_3_in_gga3(x1, x2, x3)  =  times_3_in_gga2(x1, x2)
b_0  =  b_0
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
times_3_out_gga3(x1, x2, x3)  =  times_3_out_gga1(x3)
if_times_3_in_1_gga4(x1, x2, x3, x4)  =  if_times_3_in_1_gga1(x4)
if_times_3_in_2_gga4(x1, x2, x3, x4)  =  if_times_3_in_2_gga2(x2, x4)
if_times_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_times_3_in_3_gga1(x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga2(x1, x2)  =  if_add_3_in_1_gga2(x1, x2)
binaryZ_1_in_g1(x1)  =  binaryZ_1_in_g1(x1)
if_binaryZ_1_in_1_g2(x1, x2)  =  if_binaryZ_1_in_1_g1(x2)
if_binaryZ_1_in_2_g2(x1, x2)  =  if_binaryZ_1_in_2_g1(x2)
binary_1_in_g1(x1)  =  binary_1_in_g1(x1)
binary_1_out_g1(x1)  =  binary_1_out_g
if_binary_1_in_1_g2(x1, x2)  =  if_binary_1_in_1_g1(x2)
binaryZ_1_out_g1(x1)  =  binaryZ_1_out_g
if_binary_1_in_2_g2(x1, x2)  =  if_binary_1_in_2_g1(x2)
if_add_3_in_2_gga2(x1, x2)  =  if_add_3_in_2_gga2(x1, x2)
if_add_3_in_3_gga4(x1, x2, x3, x4)  =  if_add_3_in_3_gga1(x4)
addz_3_in_gga3(x1, x2, x3)  =  addz_3_in_gga2(x1, x2)
if_addz_3_in_1_gga4(x1, x2, x3, x4)  =  if_addz_3_in_1_gga1(x4)
if_addz_3_in_2_gga4(x1, x2, x3, x4)  =  if_addz_3_in_2_gga1(x4)
addx_3_in_gga3(x1, x2, x3)  =  addx_3_in_gga2(x1, x2)
if_addx_3_in_1_gga2(x1, x2)  =  if_addx_3_in_1_gga2(x1, x2)
addx_3_out_gga3(x1, x2, x3)  =  addx_3_out_gga1(x3)
if_addx_3_in_2_gga2(x1, x2)  =  if_addx_3_in_2_gga2(x1, x2)
if_addx_3_in_3_gga4(x1, x2, x3, x4)  =  if_addx_3_in_3_gga1(x4)
if_addz_3_in_3_gga4(x1, x2, x3, x4)  =  if_addz_3_in_3_gga1(x4)
addy_3_in_gga3(x1, x2, x3)  =  addy_3_in_gga2(x1, x2)
if_addy_3_in_1_gga2(x1, x2)  =  if_addy_3_in_1_gga2(x1, x2)
addy_3_out_gga3(x1, x2, x3)  =  addy_3_out_gga1(x3)
if_addy_3_in_2_gga2(x1, x2)  =  if_addy_3_in_2_gga2(x1, x2)
if_addy_3_in_3_gga4(x1, x2, x3, x4)  =  if_addy_3_in_3_gga1(x4)
if_addz_3_in_4_gga4(x1, x2, x3, x4)  =  if_addz_3_in_4_gga1(x4)
addc_3_in_gga3(x1, x2, x3)  =  addc_3_in_gga2(x1, x2)
addc_3_out_gga3(x1, x2, x3)  =  addc_3_out_gga1(x3)
if_addc_3_in_1_gga3(x1, x2, x3)  =  if_addc_3_in_1_gga1(x3)
succZ_2_in_ga2(x1, x2)  =  succZ_2_in_ga1(x1)
if_succZ_2_in_1_ga2(x1, x2)  =  if_succZ_2_in_1_ga2(x1, x2)
succZ_2_out_ga2(x1, x2)  =  succZ_2_out_ga1(x2)
if_succZ_2_in_2_ga3(x1, x2, x3)  =  if_succZ_2_in_2_ga1(x3)
succ_2_in_ga2(x1, x2)  =  succ_2_in_ga1(x1)
succ_2_out_ga2(x1, x2)  =  succ_2_out_ga1(x2)
if_succ_2_in_1_ga2(x1, x2)  =  if_succ_2_in_1_ga2(x1, x2)
if_succ_2_in_2_ga3(x1, x2, x3)  =  if_succ_2_in_2_ga1(x3)
if_addc_3_in_2_gga3(x1, x2, x3)  =  if_addc_3_in_2_gga1(x3)
if_addc_3_in_3_gga4(x1, x2, x3, x4)  =  if_addc_3_in_3_gga1(x4)
addC_3_in_gga3(x1, x2, x3)  =  addC_3_in_gga2(x1, x2)
if_addC_3_in_1_gga4(x1, x2, x3, x4)  =  if_addC_3_in_1_gga1(x4)
addz_3_out_gga3(x1, x2, x3)  =  addz_3_out_gga1(x3)
addC_3_out_gga3(x1, x2, x3)  =  addC_3_out_gga1(x3)
if_addC_3_in_2_gga4(x1, x2, x3, x4)  =  if_addC_3_in_2_gga1(x4)
addX_3_in_gga3(x1, x2, x3)  =  addX_3_in_gga2(x1, x2)
if_addX_3_in_1_gga2(x1, x2)  =  if_addX_3_in_1_gga2(x1, x2)
addX_3_out_gga3(x1, x2, x3)  =  addX_3_out_gga1(x3)
if_addX_3_in_2_gga3(x1, x2, x3)  =  if_addX_3_in_2_gga1(x3)
if_addX_3_in_3_gga4(x1, x2, x3, x4)  =  if_addX_3_in_3_gga1(x4)
if_addC_3_in_3_gga4(x1, x2, x3, x4)  =  if_addC_3_in_3_gga1(x4)
addY_3_in_gga3(x1, x2, x3)  =  addY_3_in_gga2(x1, x2)
if_addY_3_in_1_gga2(x1, x2)  =  if_addY_3_in_1_gga2(x1, x2)
addY_3_out_gga3(x1, x2, x3)  =  addY_3_out_gga1(x3)
if_addY_3_in_2_gga3(x1, x2, x3)  =  if_addY_3_in_2_gga1(x3)
if_addY_3_in_3_gga4(x1, x2, x3, x4)  =  if_addY_3_in_3_gga1(x4)
if_addC_3_in_4_gga4(x1, x2, x3, x4)  =  if_addC_3_in_4_gga1(x4)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof

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

TIMES_3_IN_GGA3(zero_11(R), S, zero_11(RS)) -> TIMES_3_IN_GGA3(R, S, RS)
TIMES_3_IN_GGA3(one_11(R), S, RSS) -> TIMES_3_IN_GGA3(R, S, RS)

R is empty.
The argument filtering Pi contains the following mapping:
one_11(x1)  =  one_11(x1)
zero_11(x1)  =  zero_11(x1)
TIMES_3_IN_GGA3(x1, x2, x3)  =  TIMES_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof

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

TIMES_3_IN_GGA2(zero_11(R), S) -> TIMES_3_IN_GGA2(R, S)
TIMES_3_IN_GGA2(one_11(R), S) -> TIMES_3_IN_GGA2(R, S)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TIMES_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis 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: