Left Termination of the query pattern add_in_3(g, g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
  ↳1 PrologToPiTRSProof (⇐)
    ↳2 PiTRS
    ↳3 DependencyPairsProof (⇔)
    ↳4 PiDP
    ↳5 DependencyGraphProof (⇔)
    ↳6 AND
      ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 TRUE
      ↳14 PiDP
        ↳15 UsableRulesProof (⇔)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇐)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔)
        ↳20 TRUE
      ↳21 PiDP
        ↳22 UsableRulesProof (⇔)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇐)
        ↳25 QDP
  ↳26 PrologToPiTRSProof (⇐)
    ↳27 PiTRS
    ↳28 DependencyPairsProof (⇔)
    ↳29 PiDP
    ↳30 DependencyGraphProof (⇔)
    ↳31 AND
      ↳32 PiDP
        ↳33 UsableRulesProof (⇔)
        ↳34 PiDP
        ↳35 PiDPToQDPProof (⇔)
        ↳36 QDP
        ↳37 QDPSizeChangeProof (⇔)
        ↳38 TRUE
      ↳39 PiDP
        ↳40 UsableRulesProof (⇔)
        ↳41 PiDP
        ↳42 PiDPToQDPProof (⇐)
        ↳43 QDP
        ↳44 QDPSizeChangeProof (⇔)
        ↳45 TRUE
      ↳46 PiDP
        ↳47 UsableRulesProof (⇔)
        ↳48 PiDP
        ↳49 PiDPToQDPProof (⇐)
        ↳50 QDP
        ↳51 QDPSizeChangeProof (⇔)
        ↳52 TRUE

(0) Obligation:

Clauses:

add(b, b, b).
add(X, b, X) :- binaryZ(X).
add(b, Y, Y) :- binaryZ(Y).
add(X, Y, Z) :- addz(X, Y, Z).
addx(one(X), b, one(X)) :- binary(X).
addx(zero(X), b, zero(X)) :- binaryZ(X).
addx(X, Y, Z) :- addz(X, Y, Z).
addy(b, one(Y), one(Y)) :- binary(Y).
addy(b, zero(Y), zero(Y)) :- binaryZ(Y).
addy(X, Y, Z) :- addz(X, Y, Z).
addz(zero(X), zero(Y), zero(Z)) :- addz(X, Y, Z).
addz(zero(X), one(Y), one(Z)) :- addx(X, Y, Z).
addz(one(X), zero(Y), one(Z)) :- addy(X, Y, Z).
addz(one(X), one(Y), zero(Z)) :- addc(X, Y, Z).
addc(b, b, one(b)).
addc(X, b, Z) :- succZ(X, Z).
addc(b, Y, Z) :- succZ(Y, Z).
addc(X, Y, Z) :- addC(X, Y, Z).
addX(zero(X), b, one(X)) :- binaryZ(X).
addX(one(X), b, zero(Z)) :- succ(X, Z).
addX(X, Y, Z) :- addC(X, Y, Z).
addY(b, zero(Y), one(Y)) :- binaryZ(Y).
addY(b, one(Y), zero(Z)) :- succ(Y, Z).
addY(X, Y, Z) :- addC(X, Y, Z).
addC(zero(X), zero(Y), one(Z)) :- addz(X, Y, Z).
addC(zero(X), one(Y), zero(Z)) :- addX(X, Y, Z).
addC(one(X), zero(Y), zero(Z)) :- addY(X, Y, Z).
addC(one(X), one(Y), one(Z)) :- addc(X, Y, Z).
binary(b).
binary(zero(X)) :- binaryZ(X).
binary(one(X)) :- binary(X).
binaryZ(zero(X)) :- binaryZ(X).
binaryZ(one(X)) :- binary(X).
succ(b, one(b)).
succ(zero(X), one(X)) :- binaryZ(X).
succ(one(X), zero(Z)) :- succ(X, Z).
succZ(zero(X), one(X)) :- binaryZ(X).
succZ(one(X), zero(Z)) :- succ(X, Z).
times(one(b), X, X).
times(zero(R), S, zero(RS)) :- times(R, S, RS).
times(one(R), S, RSS) :- ','(times(R, S, RS), add(S, zero(RS), RSS)).

Queries:

add(g,g,a).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
add_in: (b,b,f)
binaryZ_in: (b)
binary_in: (b)
addz_in: (b,b,f)
addx_in: (b,b,f)
addy_in: (b,b,f)
addc_in: (b,b,f)
succZ_in: (b,f)
succ_in: (b,f)
addC_in: (b,b,f)
addX_in: (b,b,f)
addY_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(X, b, X) → U1_GGA(X, binaryZ_in_g(X))
ADD_IN_GGA(X, b, X) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → U29_G(X, binaryZ_in_g(X))
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(one(X)) → U30_G(X, binary_in_g(X))
BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → U27_G(X, binaryZ_in_g(X))
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → U28_G(X, binary_in_g(X))
BINARY_IN_G(one(X)) → BINARY_IN_G(X)
ADD_IN_GGA(b, Y, Y) → U2_GGA(Y, binaryZ_in_g(Y))
ADD_IN_GGA(b, Y, Y) → BINARYZ_IN_G(Y)
ADD_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADD_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → U10_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → U11_GGA(X, Y, Z, addx_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDX_IN_GGA(one(X), b, one(X)) → U4_GGA(X, binary_in_g(X))
ADDX_IN_GGA(one(X), b, one(X)) → BINARY_IN_G(X)
ADDX_IN_GGA(zero(X), b, zero(X)) → U5_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA(zero(X), b, zero(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → U12_GGA(X, Y, Z, addy_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(b, one(Y), one(Y)) → U7_GGA(Y, binary_in_g(Y))
ADDY_IN_GGA(b, one(Y), one(Y)) → BINARY_IN_G(Y)
ADDY_IN_GGA(b, zero(Y), zero(Y)) → U8_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA(b, zero(Y), zero(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA(X, Y, Z) → U9_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → U13_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, b, Z) → U14_GGA(X, Z, succZ_in_ga(X, Z))
ADDC_IN_GGA(X, b, Z) → SUCCZ_IN_GA(X, Z)
SUCCZ_IN_GA(zero(X), one(X)) → U33_GA(X, binaryZ_in_g(X))
SUCCZ_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCCZ_IN_GA(one(X), zero(Z)) → U34_GA(X, Z, succ_in_ga(X, Z))
SUCCZ_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
SUCC_IN_GA(zero(X), one(X)) → U31_GA(X, binaryZ_in_g(X))
SUCC_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCC_IN_GA(one(X), zero(Z)) → U32_GA(X, Z, succ_in_ga(X, Z))
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
ADDC_IN_GGA(b, Y, Z) → U15_GGA(Y, Z, succZ_in_ga(Y, Z))
ADDC_IN_GGA(b, Y, Z) → SUCCZ_IN_GA(Y, Z)
ADDC_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → U23_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → U24_GGA(X, Y, Z, addX_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(zero(X), b, one(X)) → U17_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA1(zero(X), b, one(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA1(one(X), b, zero(Z)) → U18_GGA(X, Z, succ_in_ga(X, Z))
ADDX_IN_GGA1(one(X), b, zero(Z)) → SUCC_IN_GA(X, Z)
ADDX_IN_GGA1(X, Y, Z) → U19_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → U25_GGA(X, Y, Z, addY_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(b, zero(Y), one(Y)) → U20_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA1(b, zero(Y), one(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA1(b, one(Y), zero(Z)) → U21_GGA(Y, Z, succ_in_ga(Y, Z))
ADDY_IN_GGA1(b, one(Y), zero(Z)) → SUCC_IN_GA(Y, Z)
ADDY_IN_GGA1(X, Y, Z) → U22_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → U26_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U1_GGA(x1, x2)  =  U1_GGA(x1, x2)
BINARYZ_IN_G(x1)  =  BINARYZ_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x2)
U30_G(x1, x2)  =  U30_G(x2)
BINARY_IN_G(x1)  =  BINARY_IN_G(x1)
U27_G(x1, x2)  =  U27_G(x2)
U28_G(x1, x2)  =  U28_G(x2)
U2_GGA(x1, x2)  =  U2_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x4)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
U4_GGA(x1, x2)  =  U4_GGA(x1, x2)
U5_GGA(x1, x2)  =  U5_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
U7_GGA(x1, x2)  =  U7_GGA(x1, x2)
U8_GGA(x1, x2)  =  U8_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
SUCCZ_IN_GA(x1, x2)  =  SUCCZ_IN_GA(x1)
U33_GA(x1, x2)  =  U33_GA(x1, x2)
U34_GA(x1, x2, x3)  =  U34_GA(x3)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)
U31_GA(x1, x2)  =  U31_GA(x1, x2)
U32_GA(x1, x2, x3)  =  U32_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x4)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x4)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
U17_GGA(x1, x2)  =  U17_GGA(x1, x2)
U18_GGA(x1, x2, x3)  =  U18_GGA(x3)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x4)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)
U20_GGA(x1, x2)  =  U20_GGA(x1, x2)
U21_GGA(x1, x2, x3)  =  U21_GGA(x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x4)

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

(4) Obligation:

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

ADD_IN_GGA(X, b, X) → U1_GGA(X, binaryZ_in_g(X))
ADD_IN_GGA(X, b, X) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → U29_G(X, binaryZ_in_g(X))
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(one(X)) → U30_G(X, binary_in_g(X))
BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → U27_G(X, binaryZ_in_g(X))
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → U28_G(X, binary_in_g(X))
BINARY_IN_G(one(X)) → BINARY_IN_G(X)
ADD_IN_GGA(b, Y, Y) → U2_GGA(Y, binaryZ_in_g(Y))
ADD_IN_GGA(b, Y, Y) → BINARYZ_IN_G(Y)
ADD_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADD_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → U10_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → U11_GGA(X, Y, Z, addx_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDX_IN_GGA(one(X), b, one(X)) → U4_GGA(X, binary_in_g(X))
ADDX_IN_GGA(one(X), b, one(X)) → BINARY_IN_G(X)
ADDX_IN_GGA(zero(X), b, zero(X)) → U5_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA(zero(X), b, zero(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → U12_GGA(X, Y, Z, addy_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(b, one(Y), one(Y)) → U7_GGA(Y, binary_in_g(Y))
ADDY_IN_GGA(b, one(Y), one(Y)) → BINARY_IN_G(Y)
ADDY_IN_GGA(b, zero(Y), zero(Y)) → U8_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA(b, zero(Y), zero(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA(X, Y, Z) → U9_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → U13_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, b, Z) → U14_GGA(X, Z, succZ_in_ga(X, Z))
ADDC_IN_GGA(X, b, Z) → SUCCZ_IN_GA(X, Z)
SUCCZ_IN_GA(zero(X), one(X)) → U33_GA(X, binaryZ_in_g(X))
SUCCZ_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCCZ_IN_GA(one(X), zero(Z)) → U34_GA(X, Z, succ_in_ga(X, Z))
SUCCZ_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
SUCC_IN_GA(zero(X), one(X)) → U31_GA(X, binaryZ_in_g(X))
SUCC_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCC_IN_GA(one(X), zero(Z)) → U32_GA(X, Z, succ_in_ga(X, Z))
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
ADDC_IN_GGA(b, Y, Z) → U15_GGA(Y, Z, succZ_in_ga(Y, Z))
ADDC_IN_GGA(b, Y, Z) → SUCCZ_IN_GA(Y, Z)
ADDC_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → U23_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → U24_GGA(X, Y, Z, addX_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(zero(X), b, one(X)) → U17_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA1(zero(X), b, one(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA1(one(X), b, zero(Z)) → U18_GGA(X, Z, succ_in_ga(X, Z))
ADDX_IN_GGA1(one(X), b, zero(Z)) → SUCC_IN_GA(X, Z)
ADDX_IN_GGA1(X, Y, Z) → U19_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → U25_GGA(X, Y, Z, addY_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(b, zero(Y), one(Y)) → U20_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA1(b, zero(Y), one(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA1(b, one(Y), zero(Z)) → U21_GGA(Y, Z, succ_in_ga(Y, Z))
ADDY_IN_GGA1(b, one(Y), zero(Z)) → SUCC_IN_GA(Y, Z)
ADDY_IN_GGA1(X, Y, Z) → U22_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → U26_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U1_GGA(x1, x2)  =  U1_GGA(x1, x2)
BINARYZ_IN_G(x1)  =  BINARYZ_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x2)
U30_G(x1, x2)  =  U30_G(x2)
BINARY_IN_G(x1)  =  BINARY_IN_G(x1)
U27_G(x1, x2)  =  U27_G(x2)
U28_G(x1, x2)  =  U28_G(x2)
U2_GGA(x1, x2)  =  U2_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x4)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x4)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
U4_GGA(x1, x2)  =  U4_GGA(x1, x2)
U5_GGA(x1, x2)  =  U5_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
U7_GGA(x1, x2)  =  U7_GGA(x1, x2)
U8_GGA(x1, x2)  =  U8_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x4)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
SUCCZ_IN_GA(x1, x2)  =  SUCCZ_IN_GA(x1)
U33_GA(x1, x2)  =  U33_GA(x1, x2)
U34_GA(x1, x2, x3)  =  U34_GA(x3)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)
U31_GA(x1, x2)  =  U31_GA(x1, x2)
U32_GA(x1, x2, x3)  =  U32_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x4)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x4)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
U17_GGA(x1, x2)  =  U17_GGA(x1, x2)
U18_GGA(x1, x2, x3)  =  U18_GGA(x3)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x4)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)
U20_GGA(x1, x2)  =  U20_GGA(x1, x2)
U21_GGA(x1, x2, x3)  =  U21_GGA(x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 50 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → BINARY_IN_G(X)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
BINARYZ_IN_G(x1)  =  BINARYZ_IN_G(x1)
BINARY_IN_G(x1)  =  BINARY_IN_G(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → BINARY_IN_G(X)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → BINARY_IN_G(X)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
    The graph contains the following edges 1 > 1

  • BINARY_IN_G(one(X)) → BINARY_IN_G(X)
    The graph contains the following edges 1 > 1

  • BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
    The graph contains the following edges 1 > 1

  • BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
    The graph contains the following edges 1 > 1

(13) TRUE

(14) Obligation:

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

SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

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

SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
one(x1)  =  one(x1)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SUCC_IN_GA(one(X)) → SUCC_IN_GA(X)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUCC_IN_GA(one(X)) → SUCC_IN_GA(X)
    The graph contains the following edges 1 > 1

(20) TRUE

(21) Obligation:

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

ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g
U27_g(x1, x2)  =  U27_g(x2)
binaryZ_out_g(x1)  =  binaryZ_out_g
U28_g(x1, x2)  =  U28_g(x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x2)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x3)
U18_gga(x1, x2, x3)  =  U18_gga(x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x3)
U21_gga(x1, x2, x3)  =  U21_gga(x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)

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

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

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

ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
one(x1)  =  one(x1)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

ADDX_IN_GGA(X, Y) → ADDZ_IN_GGA(X, Y)
ADDZ_IN_GGA(zero(X), zero(Y)) → ADDZ_IN_GGA(X, Y)
ADDZ_IN_GGA(zero(X), one(Y)) → ADDX_IN_GGA(X, Y)
ADDZ_IN_GGA(one(X), zero(Y)) → ADDY_IN_GGA(X, Y)
ADDY_IN_GGA(X, Y) → ADDZ_IN_GGA(X, Y)
ADDZ_IN_GGA(one(X), one(Y)) → ADDC_IN_GGA(X, Y)
ADDC_IN_GGA(X, Y) → ADDC_IN_GGA1(X, Y)
ADDC_IN_GGA1(zero(X), zero(Y)) → ADDZ_IN_GGA(X, Y)
ADDC_IN_GGA1(zero(X), one(Y)) → ADDX_IN_GGA1(X, Y)
ADDX_IN_GGA1(X, Y) → ADDC_IN_GGA1(X, Y)
ADDC_IN_GGA1(one(X), zero(Y)) → ADDY_IN_GGA1(X, Y)
ADDY_IN_GGA1(X, Y) → ADDC_IN_GGA1(X, Y)
ADDC_IN_GGA1(one(X), one(Y)) → ADDC_IN_GGA(X, Y)

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

(26) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
add_in: (b,b,f)
binaryZ_in: (b)
binary_in: (b)
addz_in: (b,b,f)
addx_in: (b,b,f)
addy_in: (b,b,f)
addc_in: (b,b,f)
succZ_in: (b,f)
succ_in: (b,f)
addC_in: (b,b,f)
addX_in: (b,b,f)
addY_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(27) Obligation:

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

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)

(28) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

ADD_IN_GGA(X, b, X) → U1_GGA(X, binaryZ_in_g(X))
ADD_IN_GGA(X, b, X) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → U29_G(X, binaryZ_in_g(X))
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(one(X)) → U30_G(X, binary_in_g(X))
BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → U27_G(X, binaryZ_in_g(X))
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → U28_G(X, binary_in_g(X))
BINARY_IN_G(one(X)) → BINARY_IN_G(X)
ADD_IN_GGA(b, Y, Y) → U2_GGA(Y, binaryZ_in_g(Y))
ADD_IN_GGA(b, Y, Y) → BINARYZ_IN_G(Y)
ADD_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADD_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → U10_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → U11_GGA(X, Y, Z, addx_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDX_IN_GGA(one(X), b, one(X)) → U4_GGA(X, binary_in_g(X))
ADDX_IN_GGA(one(X), b, one(X)) → BINARY_IN_G(X)
ADDX_IN_GGA(zero(X), b, zero(X)) → U5_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA(zero(X), b, zero(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → U12_GGA(X, Y, Z, addy_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(b, one(Y), one(Y)) → U7_GGA(Y, binary_in_g(Y))
ADDY_IN_GGA(b, one(Y), one(Y)) → BINARY_IN_G(Y)
ADDY_IN_GGA(b, zero(Y), zero(Y)) → U8_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA(b, zero(Y), zero(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA(X, Y, Z) → U9_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → U13_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, b, Z) → U14_GGA(X, Z, succZ_in_ga(X, Z))
ADDC_IN_GGA(X, b, Z) → SUCCZ_IN_GA(X, Z)
SUCCZ_IN_GA(zero(X), one(X)) → U33_GA(X, binaryZ_in_g(X))
SUCCZ_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCCZ_IN_GA(one(X), zero(Z)) → U34_GA(X, Z, succ_in_ga(X, Z))
SUCCZ_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
SUCC_IN_GA(zero(X), one(X)) → U31_GA(X, binaryZ_in_g(X))
SUCC_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCC_IN_GA(one(X), zero(Z)) → U32_GA(X, Z, succ_in_ga(X, Z))
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
ADDC_IN_GGA(b, Y, Z) → U15_GGA(Y, Z, succZ_in_ga(Y, Z))
ADDC_IN_GGA(b, Y, Z) → SUCCZ_IN_GA(Y, Z)
ADDC_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → U23_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → U24_GGA(X, Y, Z, addX_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(zero(X), b, one(X)) → U17_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA1(zero(X), b, one(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA1(one(X), b, zero(Z)) → U18_GGA(X, Z, succ_in_ga(X, Z))
ADDX_IN_GGA1(one(X), b, zero(Z)) → SUCC_IN_GA(X, Z)
ADDX_IN_GGA1(X, Y, Z) → U19_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → U25_GGA(X, Y, Z, addY_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(b, zero(Y), one(Y)) → U20_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA1(b, zero(Y), one(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA1(b, one(Y), zero(Z)) → U21_GGA(Y, Z, succ_in_ga(Y, Z))
ADDY_IN_GGA1(b, one(Y), zero(Z)) → SUCC_IN_GA(Y, Z)
ADDY_IN_GGA1(X, Y, Z) → U22_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → U26_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U1_GGA(x1, x2)  =  U1_GGA(x1, x2)
BINARYZ_IN_G(x1)  =  BINARYZ_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x1, x2)
U30_G(x1, x2)  =  U30_G(x1, x2)
BINARY_IN_G(x1)  =  BINARY_IN_G(x1)
U27_G(x1, x2)  =  U27_G(x1, x2)
U28_G(x1, x2)  =  U28_G(x1, x2)
U2_GGA(x1, x2)  =  U2_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
U4_GGA(x1, x2)  =  U4_GGA(x1, x2)
U5_GGA(x1, x2)  =  U5_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
U7_GGA(x1, x2)  =  U7_GGA(x1, x2)
U8_GGA(x1, x2)  =  U8_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
SUCCZ_IN_GA(x1, x2)  =  SUCCZ_IN_GA(x1)
U33_GA(x1, x2)  =  U33_GA(x1, x2)
U34_GA(x1, x2, x3)  =  U34_GA(x1, x3)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)
U31_GA(x1, x2)  =  U31_GA(x1, x2)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
U17_GGA(x1, x2)  =  U17_GGA(x1, x2)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)
U20_GGA(x1, x2)  =  U20_GGA(x1, x2)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)

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

(29) Obligation:

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

ADD_IN_GGA(X, b, X) → U1_GGA(X, binaryZ_in_g(X))
ADD_IN_GGA(X, b, X) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → U29_G(X, binaryZ_in_g(X))
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(one(X)) → U30_G(X, binary_in_g(X))
BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → U27_G(X, binaryZ_in_g(X))
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → U28_G(X, binary_in_g(X))
BINARY_IN_G(one(X)) → BINARY_IN_G(X)
ADD_IN_GGA(b, Y, Y) → U2_GGA(Y, binaryZ_in_g(Y))
ADD_IN_GGA(b, Y, Y) → BINARYZ_IN_G(Y)
ADD_IN_GGA(X, Y, Z) → U3_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADD_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → U10_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → U11_GGA(X, Y, Z, addx_in_gga(X, Y, Z))
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDX_IN_GGA(one(X), b, one(X)) → U4_GGA(X, binary_in_g(X))
ADDX_IN_GGA(one(X), b, one(X)) → BINARY_IN_G(X)
ADDX_IN_GGA(zero(X), b, zero(X)) → U5_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA(zero(X), b, zero(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA(X, Y, Z) → U6_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → U12_GGA(X, Y, Z, addy_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(b, one(Y), one(Y)) → U7_GGA(Y, binary_in_g(Y))
ADDY_IN_GGA(b, one(Y), one(Y)) → BINARY_IN_G(Y)
ADDY_IN_GGA(b, zero(Y), zero(Y)) → U8_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA(b, zero(Y), zero(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA(X, Y, Z) → U9_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → U13_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, b, Z) → U14_GGA(X, Z, succZ_in_ga(X, Z))
ADDC_IN_GGA(X, b, Z) → SUCCZ_IN_GA(X, Z)
SUCCZ_IN_GA(zero(X), one(X)) → U33_GA(X, binaryZ_in_g(X))
SUCCZ_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCCZ_IN_GA(one(X), zero(Z)) → U34_GA(X, Z, succ_in_ga(X, Z))
SUCCZ_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
SUCC_IN_GA(zero(X), one(X)) → U31_GA(X, binaryZ_in_g(X))
SUCC_IN_GA(zero(X), one(X)) → BINARYZ_IN_G(X)
SUCC_IN_GA(one(X), zero(Z)) → U32_GA(X, Z, succ_in_ga(X, Z))
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
ADDC_IN_GGA(b, Y, Z) → U15_GGA(Y, Z, succZ_in_ga(Y, Z))
ADDC_IN_GGA(b, Y, Z) → SUCCZ_IN_GA(Y, Z)
ADDC_IN_GGA(X, Y, Z) → U16_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → U23_GGA(X, Y, Z, addz_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → U24_GGA(X, Y, Z, addX_in_gga(X, Y, Z))
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(zero(X), b, one(X)) → U17_GGA(X, binaryZ_in_g(X))
ADDX_IN_GGA1(zero(X), b, one(X)) → BINARYZ_IN_G(X)
ADDX_IN_GGA1(one(X), b, zero(Z)) → U18_GGA(X, Z, succ_in_ga(X, Z))
ADDX_IN_GGA1(one(X), b, zero(Z)) → SUCC_IN_GA(X, Z)
ADDX_IN_GGA1(X, Y, Z) → U19_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → U25_GGA(X, Y, Z, addY_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(b, zero(Y), one(Y)) → U20_GGA(Y, binaryZ_in_g(Y))
ADDY_IN_GGA1(b, zero(Y), one(Y)) → BINARYZ_IN_G(Y)
ADDY_IN_GGA1(b, one(Y), zero(Z)) → U21_GGA(Y, Z, succ_in_ga(Y, Z))
ADDY_IN_GGA1(b, one(Y), zero(Z)) → SUCC_IN_GA(Y, Z)
ADDY_IN_GGA1(X, Y, Z) → U22_GGA(X, Y, Z, addC_in_gga(X, Y, Z))
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → U26_GGA(X, Y, Z, addc_in_gga(X, Y, Z))
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
ADD_IN_GGA(x1, x2, x3)  =  ADD_IN_GGA(x1, x2)
U1_GGA(x1, x2)  =  U1_GGA(x1, x2)
BINARYZ_IN_G(x1)  =  BINARYZ_IN_G(x1)
U29_G(x1, x2)  =  U29_G(x1, x2)
U30_G(x1, x2)  =  U30_G(x1, x2)
BINARY_IN_G(x1)  =  BINARY_IN_G(x1)
U27_G(x1, x2)  =  U27_G(x1, x2)
U28_G(x1, x2)  =  U28_G(x1, x2)
U2_GGA(x1, x2)  =  U2_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
U4_GGA(x1, x2)  =  U4_GGA(x1, x2)
U5_GGA(x1, x2)  =  U5_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
U7_GGA(x1, x2)  =  U7_GGA(x1, x2)
U8_GGA(x1, x2)  =  U8_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
SUCCZ_IN_GA(x1, x2)  =  SUCCZ_IN_GA(x1)
U33_GA(x1, x2)  =  U33_GA(x1, x2)
U34_GA(x1, x2, x3)  =  U34_GA(x1, x3)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)
U31_GA(x1, x2)  =  U31_GA(x1, x2)
U32_GA(x1, x2, x3)  =  U32_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
U17_GGA(x1, x2)  =  U17_GGA(x1, x2)
U18_GGA(x1, x2, x3)  =  U18_GGA(x1, x3)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)
U20_GGA(x1, x2)  =  U20_GGA(x1, x2)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x1, x2, x4)

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

(30) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 50 less nodes.

(31) Complex Obligation (AND)

(32) Obligation:

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

BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → BINARY_IN_G(X)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
BINARYZ_IN_G(x1)  =  BINARYZ_IN_G(x1)
BINARY_IN_G(x1)  =  BINARY_IN_G(x1)

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

(33) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(34) Obligation:

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

BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → BINARY_IN_G(X)

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

(35) PiDPToQDPProof (EQUIVALENT transformation)

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

(36) Obligation:

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

BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
BINARY_IN_G(one(X)) → BINARY_IN_G(X)

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

(37) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • BINARY_IN_G(zero(X)) → BINARYZ_IN_G(X)
    The graph contains the following edges 1 > 1

  • BINARY_IN_G(one(X)) → BINARY_IN_G(X)
    The graph contains the following edges 1 > 1

  • BINARYZ_IN_G(zero(X)) → BINARYZ_IN_G(X)
    The graph contains the following edges 1 > 1

  • BINARYZ_IN_G(one(X)) → BINARY_IN_G(X)
    The graph contains the following edges 1 > 1

(38) TRUE

(39) Obligation:

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

SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)

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

(40) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(41) Obligation:

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

SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
one(x1)  =  one(x1)
SUCC_IN_GA(x1, x2)  =  SUCC_IN_GA(x1)

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

(42) PiDPToQDPProof (SOUND transformation)

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

(43) Obligation:

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

SUCC_IN_GA(one(X)) → SUCC_IN_GA(X)

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

(44) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SUCC_IN_GA(one(X)) → SUCC_IN_GA(X)
    The graph contains the following edges 1 > 1

(45) TRUE

(46) Obligation:

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

ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

add_in_gga(b, b, b) → add_out_gga(b, b, b)
add_in_gga(X, b, X) → U1_gga(X, binaryZ_in_g(X))
binaryZ_in_g(zero(X)) → U29_g(X, binaryZ_in_g(X))
binaryZ_in_g(one(X)) → U30_g(X, binary_in_g(X))
binary_in_g(b) → binary_out_g(b)
binary_in_g(zero(X)) → U27_g(X, binaryZ_in_g(X))
U27_g(X, binaryZ_out_g(X)) → binary_out_g(zero(X))
binary_in_g(one(X)) → U28_g(X, binary_in_g(X))
U28_g(X, binary_out_g(X)) → binary_out_g(one(X))
U30_g(X, binary_out_g(X)) → binaryZ_out_g(one(X))
U29_g(X, binaryZ_out_g(X)) → binaryZ_out_g(zero(X))
U1_gga(X, binaryZ_out_g(X)) → add_out_gga(X, b, X)
add_in_gga(b, Y, Y) → U2_gga(Y, binaryZ_in_g(Y))
U2_gga(Y, binaryZ_out_g(Y)) → add_out_gga(b, Y, Y)
add_in_gga(X, Y, Z) → U3_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), zero(Y), zero(Z)) → U10_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(zero(X), one(Y), one(Z)) → U11_gga(X, Y, Z, addx_in_gga(X, Y, Z))
addx_in_gga(one(X), b, one(X)) → U4_gga(X, binary_in_g(X))
U4_gga(X, binary_out_g(X)) → addx_out_gga(one(X), b, one(X))
addx_in_gga(zero(X), b, zero(X)) → U5_gga(X, binaryZ_in_g(X))
U5_gga(X, binaryZ_out_g(X)) → addx_out_gga(zero(X), b, zero(X))
addx_in_gga(X, Y, Z) → U6_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), zero(Y), one(Z)) → U12_gga(X, Y, Z, addy_in_gga(X, Y, Z))
addy_in_gga(b, one(Y), one(Y)) → U7_gga(Y, binary_in_g(Y))
U7_gga(Y, binary_out_g(Y)) → addy_out_gga(b, one(Y), one(Y))
addy_in_gga(b, zero(Y), zero(Y)) → U8_gga(Y, binaryZ_in_g(Y))
U8_gga(Y, binaryZ_out_g(Y)) → addy_out_gga(b, zero(Y), zero(Y))
addy_in_gga(X, Y, Z) → U9_gga(X, Y, Z, addz_in_gga(X, Y, Z))
addz_in_gga(one(X), one(Y), zero(Z)) → U13_gga(X, Y, Z, addc_in_gga(X, Y, Z))
addc_in_gga(b, b, one(b)) → addc_out_gga(b, b, one(b))
addc_in_gga(X, b, Z) → U14_gga(X, Z, succZ_in_ga(X, Z))
succZ_in_ga(zero(X), one(X)) → U33_ga(X, binaryZ_in_g(X))
U33_ga(X, binaryZ_out_g(X)) → succZ_out_ga(zero(X), one(X))
succZ_in_ga(one(X), zero(Z)) → U34_ga(X, Z, succ_in_ga(X, Z))
succ_in_ga(b, one(b)) → succ_out_ga(b, one(b))
succ_in_ga(zero(X), one(X)) → U31_ga(X, binaryZ_in_g(X))
U31_ga(X, binaryZ_out_g(X)) → succ_out_ga(zero(X), one(X))
succ_in_ga(one(X), zero(Z)) → U32_ga(X, Z, succ_in_ga(X, Z))
U32_ga(X, Z, succ_out_ga(X, Z)) → succ_out_ga(one(X), zero(Z))
U34_ga(X, Z, succ_out_ga(X, Z)) → succZ_out_ga(one(X), zero(Z))
U14_gga(X, Z, succZ_out_ga(X, Z)) → addc_out_gga(X, b, Z)
addc_in_gga(b, Y, Z) → U15_gga(Y, Z, succZ_in_ga(Y, Z))
U15_gga(Y, Z, succZ_out_ga(Y, Z)) → addc_out_gga(b, Y, Z)
addc_in_gga(X, Y, Z) → U16_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(zero(X), zero(Y), one(Z)) → U23_gga(X, Y, Z, addz_in_gga(X, Y, Z))
U23_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addC_out_gga(zero(X), zero(Y), one(Z))
addC_in_gga(zero(X), one(Y), zero(Z)) → U24_gga(X, Y, Z, addX_in_gga(X, Y, Z))
addX_in_gga(zero(X), b, one(X)) → U17_gga(X, binaryZ_in_g(X))
U17_gga(X, binaryZ_out_g(X)) → addX_out_gga(zero(X), b, one(X))
addX_in_gga(one(X), b, zero(Z)) → U18_gga(X, Z, succ_in_ga(X, Z))
U18_gga(X, Z, succ_out_ga(X, Z)) → addX_out_gga(one(X), b, zero(Z))
addX_in_gga(X, Y, Z) → U19_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), zero(Y), zero(Z)) → U25_gga(X, Y, Z, addY_in_gga(X, Y, Z))
addY_in_gga(b, zero(Y), one(Y)) → U20_gga(Y, binaryZ_in_g(Y))
U20_gga(Y, binaryZ_out_g(Y)) → addY_out_gga(b, zero(Y), one(Y))
addY_in_gga(b, one(Y), zero(Z)) → U21_gga(Y, Z, succ_in_ga(Y, Z))
U21_gga(Y, Z, succ_out_ga(Y, Z)) → addY_out_gga(b, one(Y), zero(Z))
addY_in_gga(X, Y, Z) → U22_gga(X, Y, Z, addC_in_gga(X, Y, Z))
addC_in_gga(one(X), one(Y), one(Z)) → U26_gga(X, Y, Z, addc_in_gga(X, Y, Z))
U26_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addC_out_gga(one(X), one(Y), one(Z))
U22_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addY_out_gga(X, Y, Z)
U25_gga(X, Y, Z, addY_out_gga(X, Y, Z)) → addC_out_gga(one(X), zero(Y), zero(Z))
U19_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addX_out_gga(X, Y, Z)
U24_gga(X, Y, Z, addX_out_gga(X, Y, Z)) → addC_out_gga(zero(X), one(Y), zero(Z))
U16_gga(X, Y, Z, addC_out_gga(X, Y, Z)) → addc_out_gga(X, Y, Z)
U13_gga(X, Y, Z, addc_out_gga(X, Y, Z)) → addz_out_gga(one(X), one(Y), zero(Z))
U9_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addy_out_gga(X, Y, Z)
U12_gga(X, Y, Z, addy_out_gga(X, Y, Z)) → addz_out_gga(one(X), zero(Y), one(Z))
U6_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addx_out_gga(X, Y, Z)
U11_gga(X, Y, Z, addx_out_gga(X, Y, Z)) → addz_out_gga(zero(X), one(Y), one(Z))
U10_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → addz_out_gga(zero(X), zero(Y), zero(Z))
U3_gga(X, Y, Z, addz_out_gga(X, Y, Z)) → add_out_gga(X, Y, Z)

The argument filtering Pi contains the following mapping:
add_in_gga(x1, x2, x3)  =  add_in_gga(x1, x2)
b  =  b
add_out_gga(x1, x2, x3)  =  add_out_gga(x1, x2, x3)
U1_gga(x1, x2)  =  U1_gga(x1, x2)
binaryZ_in_g(x1)  =  binaryZ_in_g(x1)
zero(x1)  =  zero(x1)
U29_g(x1, x2)  =  U29_g(x1, x2)
one(x1)  =  one(x1)
U30_g(x1, x2)  =  U30_g(x1, x2)
binary_in_g(x1)  =  binary_in_g(x1)
binary_out_g(x1)  =  binary_out_g(x1)
U27_g(x1, x2)  =  U27_g(x1, x2)
binaryZ_out_g(x1)  =  binaryZ_out_g(x1)
U28_g(x1, x2)  =  U28_g(x1, x2)
U2_gga(x1, x2)  =  U2_gga(x1, x2)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
addz_in_gga(x1, x2, x3)  =  addz_in_gga(x1, x2)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x1, x2, x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
addx_in_gga(x1, x2, x3)  =  addx_in_gga(x1, x2)
U4_gga(x1, x2)  =  U4_gga(x1, x2)
addx_out_gga(x1, x2, x3)  =  addx_out_gga(x1, x2, x3)
U5_gga(x1, x2)  =  U5_gga(x1, x2)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x1, x2, x4)
addy_in_gga(x1, x2, x3)  =  addy_in_gga(x1, x2)
U7_gga(x1, x2)  =  U7_gga(x1, x2)
addy_out_gga(x1, x2, x3)  =  addy_out_gga(x1, x2, x3)
U8_gga(x1, x2)  =  U8_gga(x1, x2)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x2, x4)
U13_gga(x1, x2, x3, x4)  =  U13_gga(x1, x2, x4)
addc_in_gga(x1, x2, x3)  =  addc_in_gga(x1, x2)
addc_out_gga(x1, x2, x3)  =  addc_out_gga(x1, x2, x3)
U14_gga(x1, x2, x3)  =  U14_gga(x1, x3)
succZ_in_ga(x1, x2)  =  succZ_in_ga(x1)
U33_ga(x1, x2)  =  U33_ga(x1, x2)
succZ_out_ga(x1, x2)  =  succZ_out_ga(x1, x2)
U34_ga(x1, x2, x3)  =  U34_ga(x1, x3)
succ_in_ga(x1, x2)  =  succ_in_ga(x1)
succ_out_ga(x1, x2)  =  succ_out_ga(x1, x2)
U31_ga(x1, x2)  =  U31_ga(x1, x2)
U32_ga(x1, x2, x3)  =  U32_ga(x1, x3)
U15_gga(x1, x2, x3)  =  U15_gga(x1, x3)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
addC_in_gga(x1, x2, x3)  =  addC_in_gga(x1, x2)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x1, x2, x4)
addz_out_gga(x1, x2, x3)  =  addz_out_gga(x1, x2, x3)
addC_out_gga(x1, x2, x3)  =  addC_out_gga(x1, x2, x3)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
addX_in_gga(x1, x2, x3)  =  addX_in_gga(x1, x2)
U17_gga(x1, x2)  =  U17_gga(x1, x2)
addX_out_gga(x1, x2, x3)  =  addX_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3)  =  U18_gga(x1, x3)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x1, x2, x4)
addY_in_gga(x1, x2, x3)  =  addY_in_gga(x1, x2)
U20_gga(x1, x2)  =  U20_gga(x1, x2)
addY_out_gga(x1, x2, x3)  =  addY_out_gga(x1, x2, x3)
U21_gga(x1, x2, x3)  =  U21_gga(x1, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)

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

(47) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(48) Obligation:

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

ADDX_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), zero(Y), zero(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(zero(X), one(Y), one(Z)) → ADDX_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), zero(Y), one(Z)) → ADDY_IN_GGA(X, Y, Z)
ADDY_IN_GGA(X, Y, Z) → ADDZ_IN_GGA(X, Y, Z)
ADDZ_IN_GGA(one(X), one(Y), zero(Z)) → ADDC_IN_GGA(X, Y, Z)
ADDC_IN_GGA(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(zero(X), zero(Y), one(Z)) → ADDZ_IN_GGA(X, Y, Z)
ADDC_IN_GGA1(zero(X), one(Y), zero(Z)) → ADDX_IN_GGA1(X, Y, Z)
ADDX_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), zero(Y), zero(Z)) → ADDY_IN_GGA1(X, Y, Z)
ADDY_IN_GGA1(X, Y, Z) → ADDC_IN_GGA1(X, Y, Z)
ADDC_IN_GGA1(one(X), one(Y), one(Z)) → ADDC_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
zero(x1)  =  zero(x1)
one(x1)  =  one(x1)
ADDZ_IN_GGA(x1, x2, x3)  =  ADDZ_IN_GGA(x1, x2)
ADDX_IN_GGA(x1, x2, x3)  =  ADDX_IN_GGA(x1, x2)
ADDY_IN_GGA(x1, x2, x3)  =  ADDY_IN_GGA(x1, x2)
ADDC_IN_GGA(x1, x2, x3)  =  ADDC_IN_GGA(x1, x2)
ADDC_IN_GGA1(x1, x2, x3)  =  ADDC_IN_GGA1(x1, x2)
ADDX_IN_GGA1(x1, x2, x3)  =  ADDX_IN_GGA1(x1, x2)
ADDY_IN_GGA1(x1, x2, x3)  =  ADDY_IN_GGA1(x1, x2)

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

(49) PiDPToQDPProof (SOUND transformation)

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

(50) Obligation:

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

ADDX_IN_GGA(X, Y) → ADDZ_IN_GGA(X, Y)
ADDZ_IN_GGA(zero(X), zero(Y)) → ADDZ_IN_GGA(X, Y)
ADDZ_IN_GGA(zero(X), one(Y)) → ADDX_IN_GGA(X, Y)
ADDZ_IN_GGA(one(X), zero(Y)) → ADDY_IN_GGA(X, Y)
ADDY_IN_GGA(X, Y) → ADDZ_IN_GGA(X, Y)
ADDZ_IN_GGA(one(X), one(Y)) → ADDC_IN_GGA(X, Y)
ADDC_IN_GGA(X, Y) → ADDC_IN_GGA1(X, Y)
ADDC_IN_GGA1(zero(X), zero(Y)) → ADDZ_IN_GGA(X, Y)
ADDC_IN_GGA1(zero(X), one(Y)) → ADDX_IN_GGA1(X, Y)
ADDX_IN_GGA1(X, Y) → ADDC_IN_GGA1(X, Y)
ADDC_IN_GGA1(one(X), zero(Y)) → ADDY_IN_GGA1(X, Y)
ADDY_IN_GGA1(X, Y) → ADDC_IN_GGA1(X, Y)
ADDC_IN_GGA1(one(X), one(Y)) → ADDC_IN_GGA(X, Y)

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

(51) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ADDZ_IN_GGA(zero(X), one(Y)) → ADDX_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDZ_IN_GGA(zero(X), zero(Y)) → ADDZ_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDX_IN_GGA(X, Y) → ADDZ_IN_GGA(X, Y)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDY_IN_GGA(X, Y) → ADDZ_IN_GGA(X, Y)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDC_IN_GGA1(zero(X), zero(Y)) → ADDZ_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDZ_IN_GGA(one(X), zero(Y)) → ADDY_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDZ_IN_GGA(one(X), one(Y)) → ADDC_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDC_IN_GGA(X, Y) → ADDC_IN_GGA1(X, Y)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDC_IN_GGA1(one(X), one(Y)) → ADDC_IN_GGA(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDX_IN_GGA1(X, Y) → ADDC_IN_GGA1(X, Y)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDY_IN_GGA1(X, Y) → ADDC_IN_GGA1(X, Y)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • ADDC_IN_GGA1(zero(X), one(Y)) → ADDX_IN_GGA1(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

  • ADDC_IN_GGA1(one(X), zero(Y)) → ADDY_IN_GGA1(X, Y)
    The graph contains the following edges 1 > 1, 2 > 2

(52) TRUE