↳ PROLOG
↳ PrologToPiTRSProof
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))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
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))
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)
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))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
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)
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))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PiDP
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)
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))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PiDP
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)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
↳ PiDP
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)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
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))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
SUCC_2_IN_GA2(one_11(X), zero_11(Z)) -> SUCC_2_IN_GA2(X, Z)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
↳ PiDP
SUCC_2_IN_GA1(one_11(X)) -> SUCC_2_IN_GA1(X)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
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)
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))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
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)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
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)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
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)
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))
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
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)
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
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)
From the DPs we obtained the following set of size-change graphs: