↳ PROLOG
↳ UnrequestedClauseRemoverProof
The clauses
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).
can be ignored, as they are not needed by any of the given querys.
Deleting these clauses results in the following prolog program:
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).
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
With regard to the inferred argument filtering the predicates were used in the following modes:
add3: (f,f,b)
binaryZ1: (b)
binary1: (b)
addz3: (f,f,b)
addx3: (f,f,b)
addy3: (f,f,b)
addc3: (f,f,b)
succZ2: (f,b)
succ2: (f,b)
addC3: (f,f,b)
addX3: (f,f,b)
addY3: (f,f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
ADD_3_IN_AAG3(X, b_0, X) -> IF_ADD_3_IN_1_AAG2(X, binaryZ_1_in_g1(X))
ADD_3_IN_AAG3(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_AAG3(b_0, Y, Y) -> IF_ADD_3_IN_2_AAG2(Y, binaryZ_1_in_g1(Y))
ADD_3_IN_AAG3(b_0, Y, Y) -> BINARYZ_1_IN_G1(Y)
ADD_3_IN_AAG3(X, Y, Z) -> IF_ADD_3_IN_3_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADD_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(zero_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_1_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(zero_11(X), one_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_2_AAG4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_AAG3(X, Y, Z)
ADDX_3_IN_AAG3(one_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_AAG2(X, binary_1_in_g1(X))
ADDX_3_IN_AAG3(one_11(X), b_0, one_11(X)) -> BINARY_1_IN_G1(X)
ADDX_3_IN_AAG3(zero_11(X), b_0, zero_11(X)) -> IF_ADDX_3_IN_2_AAG2(X, binaryZ_1_in_g1(X))
ADDX_3_IN_AAG3(zero_11(X), b_0, zero_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_AAG3(X, Y, Z) -> IF_ADDX_3_IN_3_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDX_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), zero_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_3_AAG4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_AAG3(X, Y, Z)
ADDY_3_IN_AAG3(b_0, one_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_AAG2(Y, binary_1_in_g1(Y))
ADDY_3_IN_AAG3(b_0, one_11(Y), one_11(Y)) -> BINARY_1_IN_G1(Y)
ADDY_3_IN_AAG3(b_0, zero_11(Y), zero_11(Y)) -> IF_ADDY_3_IN_2_AAG2(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_AAG3(b_0, zero_11(Y), zero_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_AAG3(X, Y, Z) -> IF_ADDY_3_IN_3_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDY_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), one_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_4_AAG4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG3(X, b_0, Z) -> IF_ADDC_3_IN_1_AAG3(X, Z, succZ_2_in_ag2(X, Z))
ADDC_3_IN_AAG3(X, b_0, Z) -> SUCCZ_2_IN_AG2(X, Z)
SUCCZ_2_IN_AG2(zero_11(X), one_11(X)) -> IF_SUCCZ_2_IN_1_AG2(X, binaryZ_1_in_g1(X))
SUCCZ_2_IN_AG2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCCZ_2_IN_AG2(one_11(X), zero_11(Z)) -> IF_SUCCZ_2_IN_2_AG3(X, Z, succ_2_in_ag2(X, Z))
SUCCZ_2_IN_AG2(one_11(X), zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
SUCC_2_IN_AG2(zero_11(X), one_11(X)) -> IF_SUCC_2_IN_1_AG2(X, binaryZ_1_in_g1(X))
SUCC_2_IN_AG2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCC_2_IN_AG2(one_11(X), zero_11(Z)) -> IF_SUCC_2_IN_2_AG3(X, Z, succ_2_in_ag2(X, Z))
SUCC_2_IN_AG2(one_11(X), zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
ADDC_3_IN_AAG3(b_0, Y, Z) -> IF_ADDC_3_IN_2_AAG3(Y, Z, succZ_2_in_ag2(Y, Z))
ADDC_3_IN_AAG3(b_0, Y, Z) -> SUCCZ_2_IN_AG2(Y, Z)
ADDC_3_IN_AAG3(X, Y, Z) -> IF_ADDC_3_IN_3_AAG4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG3(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), zero_11(Y), one_11(Z)) -> IF_ADDC_3_IN_1_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), one_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_2_AAG4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_AAG13(X, Y, Z)
ADDX_3_IN_AAG13(zero_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_AAG12(X, binaryZ_1_in_g1(X))
ADDX_3_IN_AAG13(zero_11(X), b_0, one_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_AAG13(one_11(X), b_0, zero_11(Z)) -> IF_ADDX_3_IN_2_AAG3(X, Z, succ_2_in_ag2(X, Z))
ADDX_3_IN_AAG13(one_11(X), b_0, zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
ADDX_3_IN_AAG13(X, Y, Z) -> IF_ADDX_3_IN_3_AAG14(X, Y, Z, addC_3_in_aag3(X, Y, Z))
ADDX_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_3_AAG14(X, Y, Z, addY_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_AAG13(X, Y, Z)
ADDY_3_IN_AAG13(b_0, zero_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_AAG12(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_AAG13(b_0, zero_11(Y), one_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_AAG13(b_0, one_11(Y), zero_11(Z)) -> IF_ADDY_3_IN_2_AAG3(Y, Z, succ_2_in_ag2(Y, Z))
ADDY_3_IN_AAG13(b_0, one_11(Y), zero_11(Z)) -> SUCC_2_IN_AG2(Y, Z)
ADDY_3_IN_AAG13(X, Y, Z) -> IF_ADDY_3_IN_3_AAG14(X, Y, Z, addC_3_in_aag3(X, Y, Z))
ADDY_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), one_11(Y), one_11(Z)) -> IF_ADDC_3_IN_4_AAG4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
ADD_3_IN_AAG3(X, b_0, X) -> IF_ADD_3_IN_1_AAG2(X, binaryZ_1_in_g1(X))
ADD_3_IN_AAG3(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_AAG3(b_0, Y, Y) -> IF_ADD_3_IN_2_AAG2(Y, binaryZ_1_in_g1(Y))
ADD_3_IN_AAG3(b_0, Y, Y) -> BINARYZ_1_IN_G1(Y)
ADD_3_IN_AAG3(X, Y, Z) -> IF_ADD_3_IN_3_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADD_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(zero_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_1_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(zero_11(X), one_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_2_AAG4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_AAG3(X, Y, Z)
ADDX_3_IN_AAG3(one_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_AAG2(X, binary_1_in_g1(X))
ADDX_3_IN_AAG3(one_11(X), b_0, one_11(X)) -> BINARY_1_IN_G1(X)
ADDX_3_IN_AAG3(zero_11(X), b_0, zero_11(X)) -> IF_ADDX_3_IN_2_AAG2(X, binaryZ_1_in_g1(X))
ADDX_3_IN_AAG3(zero_11(X), b_0, zero_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_AAG3(X, Y, Z) -> IF_ADDX_3_IN_3_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDX_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), zero_11(Y), one_11(Z)) -> IF_ADDZ_3_IN_3_AAG4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_AAG3(X, Y, Z)
ADDY_3_IN_AAG3(b_0, one_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_AAG2(Y, binary_1_in_g1(Y))
ADDY_3_IN_AAG3(b_0, one_11(Y), one_11(Y)) -> BINARY_1_IN_G1(Y)
ADDY_3_IN_AAG3(b_0, zero_11(Y), zero_11(Y)) -> IF_ADDY_3_IN_2_AAG2(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_AAG3(b_0, zero_11(Y), zero_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_AAG3(X, Y, Z) -> IF_ADDY_3_IN_3_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDY_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), one_11(Y), zero_11(Z)) -> IF_ADDZ_3_IN_4_AAG4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
ADDZ_3_IN_AAG3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG3(X, b_0, Z) -> IF_ADDC_3_IN_1_AAG3(X, Z, succZ_2_in_ag2(X, Z))
ADDC_3_IN_AAG3(X, b_0, Z) -> SUCCZ_2_IN_AG2(X, Z)
SUCCZ_2_IN_AG2(zero_11(X), one_11(X)) -> IF_SUCCZ_2_IN_1_AG2(X, binaryZ_1_in_g1(X))
SUCCZ_2_IN_AG2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCCZ_2_IN_AG2(one_11(X), zero_11(Z)) -> IF_SUCCZ_2_IN_2_AG3(X, Z, succ_2_in_ag2(X, Z))
SUCCZ_2_IN_AG2(one_11(X), zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
SUCC_2_IN_AG2(zero_11(X), one_11(X)) -> IF_SUCC_2_IN_1_AG2(X, binaryZ_1_in_g1(X))
SUCC_2_IN_AG2(zero_11(X), one_11(X)) -> BINARYZ_1_IN_G1(X)
SUCC_2_IN_AG2(one_11(X), zero_11(Z)) -> IF_SUCC_2_IN_2_AG3(X, Z, succ_2_in_ag2(X, Z))
SUCC_2_IN_AG2(one_11(X), zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
ADDC_3_IN_AAG3(b_0, Y, Z) -> IF_ADDC_3_IN_2_AAG3(Y, Z, succZ_2_in_ag2(Y, Z))
ADDC_3_IN_AAG3(b_0, Y, Z) -> SUCCZ_2_IN_AG2(Y, Z)
ADDC_3_IN_AAG3(X, Y, Z) -> IF_ADDC_3_IN_3_AAG4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG3(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), zero_11(Y), one_11(Z)) -> IF_ADDC_3_IN_1_AAG4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), one_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_2_AAG4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_AAG13(X, Y, Z)
ADDX_3_IN_AAG13(zero_11(X), b_0, one_11(X)) -> IF_ADDX_3_IN_1_AAG12(X, binaryZ_1_in_g1(X))
ADDX_3_IN_AAG13(zero_11(X), b_0, one_11(X)) -> BINARYZ_1_IN_G1(X)
ADDX_3_IN_AAG13(one_11(X), b_0, zero_11(Z)) -> IF_ADDX_3_IN_2_AAG3(X, Z, succ_2_in_ag2(X, Z))
ADDX_3_IN_AAG13(one_11(X), b_0, zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
ADDX_3_IN_AAG13(X, Y, Z) -> IF_ADDX_3_IN_3_AAG14(X, Y, Z, addC_3_in_aag3(X, Y, Z))
ADDX_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), zero_11(Y), zero_11(Z)) -> IF_ADDC_3_IN_3_AAG14(X, Y, Z, addY_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_AAG13(X, Y, Z)
ADDY_3_IN_AAG13(b_0, zero_11(Y), one_11(Y)) -> IF_ADDY_3_IN_1_AAG12(Y, binaryZ_1_in_g1(Y))
ADDY_3_IN_AAG13(b_0, zero_11(Y), one_11(Y)) -> BINARYZ_1_IN_G1(Y)
ADDY_3_IN_AAG13(b_0, one_11(Y), zero_11(Z)) -> IF_ADDY_3_IN_2_AAG3(Y, Z, succ_2_in_ag2(Y, Z))
ADDY_3_IN_AAG13(b_0, one_11(Y), zero_11(Z)) -> SUCC_2_IN_AG2(Y, Z)
ADDY_3_IN_AAG13(X, Y, Z) -> IF_ADDY_3_IN_3_AAG14(X, Y, Z, addC_3_in_aag3(X, Y, Z))
ADDY_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), one_11(Y), one_11(Z)) -> IF_ADDC_3_IN_4_AAG4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
ADDC_3_IN_AAG13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ 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)
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ 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
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ 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
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
SUCC_2_IN_AG2(one_11(X), zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
SUCC_2_IN_AG2(one_11(X), zero_11(Z)) -> SUCC_2_IN_AG2(X, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
↳ PiDP
SUCC_2_IN_AG1(zero_11(Z)) -> SUCC_2_IN_AG1(Z)
From the DPs we obtained the following set of size-change graphs:
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
ADDZ_3_IN_AAG3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDY_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_AAG3(X, Y, Z)
ADDY_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG3(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDX_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_AAG13(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_AAG13(X, Y, Z)
ADDX_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
add_3_in_aag3(b_0, b_0, b_0) -> add_3_out_aag3(b_0, b_0, b_0)
add_3_in_aag3(X, b_0, X) -> if_add_3_in_1_aag2(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_aag2(X, binaryZ_1_out_g1(X)) -> add_3_out_aag3(X, b_0, X)
add_3_in_aag3(b_0, Y, Y) -> if_add_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_add_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> add_3_out_aag3(b_0, Y, Y)
add_3_in_aag3(X, Y, Z) -> if_add_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), zero_11(Y), zero_11(Z)) -> if_addz_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(zero_11(X), one_11(Y), one_11(Z)) -> if_addz_3_in_2_aag4(X, Y, Z, addx_3_in_aag3(X, Y, Z))
addx_3_in_aag3(one_11(X), b_0, one_11(X)) -> if_addx_3_in_1_aag2(X, binary_1_in_g1(X))
if_addx_3_in_1_aag2(X, binary_1_out_g1(X)) -> addx_3_out_aag3(one_11(X), b_0, one_11(X))
addx_3_in_aag3(zero_11(X), b_0, zero_11(X)) -> if_addx_3_in_2_aag2(X, binaryZ_1_in_g1(X))
if_addx_3_in_2_aag2(X, binaryZ_1_out_g1(X)) -> addx_3_out_aag3(zero_11(X), b_0, zero_11(X))
addx_3_in_aag3(X, Y, Z) -> if_addx_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), zero_11(Y), one_11(Z)) -> if_addz_3_in_3_aag4(X, Y, Z, addy_3_in_aag3(X, Y, Z))
addy_3_in_aag3(b_0, one_11(Y), one_11(Y)) -> if_addy_3_in_1_aag2(Y, binary_1_in_g1(Y))
if_addy_3_in_1_aag2(Y, binary_1_out_g1(Y)) -> addy_3_out_aag3(b_0, one_11(Y), one_11(Y))
addy_3_in_aag3(b_0, zero_11(Y), zero_11(Y)) -> if_addy_3_in_2_aag2(Y, binaryZ_1_in_g1(Y))
if_addy_3_in_2_aag2(Y, binaryZ_1_out_g1(Y)) -> addy_3_out_aag3(b_0, zero_11(Y), zero_11(Y))
addy_3_in_aag3(X, Y, Z) -> if_addy_3_in_3_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
addz_3_in_aag3(one_11(X), one_11(Y), zero_11(Z)) -> if_addz_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
addc_3_in_aag3(b_0, b_0, one_11(b_0)) -> addc_3_out_aag3(b_0, b_0, one_11(b_0))
addc_3_in_aag3(X, b_0, Z) -> if_addc_3_in_1_aag3(X, Z, succZ_2_in_ag2(X, Z))
succZ_2_in_ag2(zero_11(X), one_11(X)) -> if_succZ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succZ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succZ_2_out_ag2(zero_11(X), one_11(X))
succZ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succZ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
succ_2_in_ag2(b_0, one_11(b_0)) -> succ_2_out_ag2(b_0, one_11(b_0))
succ_2_in_ag2(zero_11(X), one_11(X)) -> if_succ_2_in_1_ag2(X, binaryZ_1_in_g1(X))
if_succ_2_in_1_ag2(X, binaryZ_1_out_g1(X)) -> succ_2_out_ag2(zero_11(X), one_11(X))
succ_2_in_ag2(one_11(X), zero_11(Z)) -> if_succ_2_in_2_ag3(X, Z, succ_2_in_ag2(X, Z))
if_succ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succ_2_out_ag2(one_11(X), zero_11(Z))
if_succZ_2_in_2_ag3(X, Z, succ_2_out_ag2(X, Z)) -> succZ_2_out_ag2(one_11(X), zero_11(Z))
if_addc_3_in_1_aag3(X, Z, succZ_2_out_ag2(X, Z)) -> addc_3_out_aag3(X, b_0, Z)
addc_3_in_aag3(b_0, Y, Z) -> if_addc_3_in_2_aag3(Y, Z, succZ_2_in_ag2(Y, Z))
if_addc_3_in_2_aag3(Y, Z, succZ_2_out_ag2(Y, Z)) -> addc_3_out_aag3(b_0, Y, Z)
addc_3_in_aag3(X, Y, Z) -> if_addc_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(zero_11(X), zero_11(Y), one_11(Z)) -> if_addC_3_in_1_aag4(X, Y, Z, addz_3_in_aag3(X, Y, Z))
if_addC_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), zero_11(Y), one_11(Z))
addC_3_in_aag3(zero_11(X), one_11(Y), zero_11(Z)) -> if_addC_3_in_2_aag4(X, Y, Z, addX_3_in_aag3(X, Y, Z))
addX_3_in_aag3(zero_11(X), b_0, one_11(X)) -> if_addX_3_in_1_aag2(X, binaryZ_1_in_g1(X))
if_addX_3_in_1_aag2(X, binaryZ_1_out_g1(X)) -> addX_3_out_aag3(zero_11(X), b_0, one_11(X))
addX_3_in_aag3(one_11(X), b_0, zero_11(Z)) -> if_addX_3_in_2_aag3(X, Z, succ_2_in_ag2(X, Z))
if_addX_3_in_2_aag3(X, Z, succ_2_out_ag2(X, Z)) -> addX_3_out_aag3(one_11(X), b_0, zero_11(Z))
addX_3_in_aag3(X, Y, Z) -> if_addX_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), zero_11(Y), zero_11(Z)) -> if_addC_3_in_3_aag4(X, Y, Z, addY_3_in_aag3(X, Y, Z))
addY_3_in_aag3(b_0, zero_11(Y), one_11(Y)) -> if_addY_3_in_1_aag2(Y, binaryZ_1_in_g1(Y))
if_addY_3_in_1_aag2(Y, binaryZ_1_out_g1(Y)) -> addY_3_out_aag3(b_0, zero_11(Y), one_11(Y))
addY_3_in_aag3(b_0, one_11(Y), zero_11(Z)) -> if_addY_3_in_2_aag3(Y, Z, succ_2_in_ag2(Y, Z))
if_addY_3_in_2_aag3(Y, Z, succ_2_out_ag2(Y, Z)) -> addY_3_out_aag3(b_0, one_11(Y), zero_11(Z))
addY_3_in_aag3(X, Y, Z) -> if_addY_3_in_3_aag4(X, Y, Z, addC_3_in_aag3(X, Y, Z))
addC_3_in_aag3(one_11(X), one_11(Y), one_11(Z)) -> if_addC_3_in_4_aag4(X, Y, Z, addc_3_in_aag3(X, Y, Z))
if_addC_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), one_11(Y), one_11(Z))
if_addY_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addY_3_out_aag3(X, Y, Z)
if_addC_3_in_3_aag4(X, Y, Z, addY_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(one_11(X), zero_11(Y), zero_11(Z))
if_addX_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addX_3_out_aag3(X, Y, Z)
if_addC_3_in_2_aag4(X, Y, Z, addX_3_out_aag3(X, Y, Z)) -> addC_3_out_aag3(zero_11(X), one_11(Y), zero_11(Z))
if_addc_3_in_3_aag4(X, Y, Z, addC_3_out_aag3(X, Y, Z)) -> addc_3_out_aag3(X, Y, Z)
if_addz_3_in_4_aag4(X, Y, Z, addc_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), one_11(Y), zero_11(Z))
if_addy_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addy_3_out_aag3(X, Y, Z)
if_addz_3_in_3_aag4(X, Y, Z, addy_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(one_11(X), zero_11(Y), one_11(Z))
if_addx_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addx_3_out_aag3(X, Y, Z)
if_addz_3_in_2_aag4(X, Y, Z, addx_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), one_11(Y), one_11(Z))
if_addz_3_in_1_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> addz_3_out_aag3(zero_11(X), zero_11(Y), zero_11(Z))
if_add_3_in_3_aag4(X, Y, Z, addz_3_out_aag3(X, Y, Z)) -> add_3_out_aag3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
ADDZ_3_IN_AAG3(zero_11(X), one_11(Y), one_11(Z)) -> ADDX_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(zero_11(X), zero_11(Y), zero_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDY_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), zero_11(Y), one_11(Z)) -> ADDZ_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), one_11(Y), one_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), zero_11(Y), one_11(Z)) -> ADDY_3_IN_AAG3(X, Y, Z)
ADDY_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG3(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDX_3_IN_AAG13(X, Y, Z) -> ADDC_3_IN_AAG13(X, Y, Z)
ADDC_3_IN_AAG13(one_11(X), zero_11(Y), zero_11(Z)) -> ADDY_3_IN_AAG13(X, Y, Z)
ADDZ_3_IN_AAG3(one_11(X), one_11(Y), zero_11(Z)) -> ADDC_3_IN_AAG3(X, Y, Z)
ADDC_3_IN_AAG13(zero_11(X), one_11(Y), zero_11(Z)) -> ADDX_3_IN_AAG13(X, Y, Z)
ADDX_3_IN_AAG3(X, Y, Z) -> ADDZ_3_IN_AAG3(X, Y, Z)
↳ PROLOG
↳ UnrequestedClauseRemoverProof
↳ PROLOG
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ QDPSizeChangeProof
ADDZ_3_IN_AAG1(one_11(Z)) -> ADDX_3_IN_AAG1(Z)
ADDZ_3_IN_AAG1(zero_11(Z)) -> ADDZ_3_IN_AAG1(Z)
ADDY_3_IN_AAG1(Z) -> ADDZ_3_IN_AAG1(Z)
ADDC_3_IN_AAG11(one_11(Z)) -> ADDZ_3_IN_AAG1(Z)
ADDC_3_IN_AAG11(one_11(Z)) -> ADDC_3_IN_AAG1(Z)
ADDZ_3_IN_AAG1(one_11(Z)) -> ADDY_3_IN_AAG1(Z)
ADDY_3_IN_AAG11(Z) -> ADDC_3_IN_AAG11(Z)
ADDC_3_IN_AAG1(Z) -> ADDC_3_IN_AAG11(Z)
ADDX_3_IN_AAG11(Z) -> ADDC_3_IN_AAG11(Z)
ADDC_3_IN_AAG11(zero_11(Z)) -> ADDY_3_IN_AAG11(Z)
ADDZ_3_IN_AAG1(zero_11(Z)) -> ADDC_3_IN_AAG1(Z)
ADDC_3_IN_AAG11(zero_11(Z)) -> ADDX_3_IN_AAG11(Z)
ADDX_3_IN_AAG1(Z) -> ADDZ_3_IN_AAG1(Z)
From the DPs we obtained the following set of size-change graphs: