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 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 PiDP
↳29 UsableRulesProof (⇔)
↳30 PiDP
↳31 PiDPToQDPProof (⇐)
↳32 QDP
↳33 QDPSizeChangeProof (⇔)
↳34 TRUE
↳35 PrologToPiTRSProof (⇐)
↳36 PiTRS
↳37 DependencyPairsProof (⇔)
↳38 PiDP
↳39 DependencyGraphProof (⇔)
↳40 AND
↳41 PiDP
↳42 UsableRulesProof (⇔)
↳43 PiDP
↳44 PiDPToQDPProof (⇔)
↳45 QDP
↳46 QDPSizeChangeProof (⇔)
↳47 TRUE
↳48 PiDP
↳49 UsableRulesProof (⇔)
↳50 PiDP
↳51 PiDPToQDPProof (⇐)
↳52 QDP
↳53 QDPSizeChangeProof (⇔)
↳54 TRUE
↳55 PiDP
↳56 UsableRulesProof (⇔)
↳57 PiDP
↳58 PiDPToQDPProof (⇐)
↳59 QDP
↳60 PiDP
↳61 UsableRulesProof (⇔)
↳62 PiDP
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → U35_GGA(R, S, RS, times_in_gga(R, S, RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(one(R), S, RSS) → U36_GGA(R, S, RSS, times_in_gga(R, S, RS))
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → U37_GGA(R, S, RSS, add_in_gga(S, zero(RS), RSS))
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → ADD_IN_GGA(S, zero(RS), RSS)
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → U35_GGA(R, S, RS, times_in_gga(R, S, RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(one(R), S, RSS) → U36_GGA(R, S, RSS, times_in_gga(R, S, RS))
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → U37_GGA(R, S, RSS, add_in_gga(S, zero(RS), RSS))
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → ADD_IN_GGA(S, zero(RS), RSS)
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
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)
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)
From the DPs we obtained the following set of size-change graphs:
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
SUCC_IN_GA(one(X)) → SUCC_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
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)
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)
From the DPs we obtained the following set of size-change graphs:
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(one(R), S) → TIMES_IN_GGA(R, S)
TIMES_IN_GGA(zero(R), S) → TIMES_IN_GGA(R, S)
From the DPs we obtained the following set of size-change graphs:
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → U35_GGA(R, S, RS, times_in_gga(R, S, RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(one(R), S, RSS) → U36_GGA(R, S, RSS, times_in_gga(R, S, RS))
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → U37_GGA(R, S, RSS, add_in_gga(S, zero(RS), RSS))
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → ADD_IN_GGA(S, zero(RS), RSS)
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → U35_GGA(R, S, RS, times_in_gga(R, S, RS))
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(one(R), S, RSS) → U36_GGA(R, S, RSS, times_in_gga(R, S, RS))
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → U37_GGA(R, S, RSS, add_in_gga(S, zero(RS), RSS))
U36_GGA(R, S, RSS, times_out_gga(R, S, RS)) → ADD_IN_GGA(S, zero(RS), RSS)
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
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)
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)
From the DPs we obtained the following set of size-change graphs:
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
SUCC_IN_GA(one(X), zero(Z)) → SUCC_IN_GA(X, Z)
SUCC_IN_GA(one(X)) → SUCC_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
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)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
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)
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)
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)
times_in_gga(one(b), X, X) → times_out_gga(one(b), X, X)
times_in_gga(zero(R), S, zero(RS)) → U35_gga(R, S, RS, times_in_gga(R, S, RS))
times_in_gga(one(R), S, RSS) → U36_gga(R, S, RSS, times_in_gga(R, S, RS))
U36_gga(R, S, RSS, times_out_gga(R, S, RS)) → U37_gga(R, S, RSS, add_in_gga(S, zero(RS), RSS))
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)
U37_gga(R, S, RSS, add_out_gga(S, zero(RS), RSS)) → times_out_gga(one(R), S, RSS)
U35_gga(R, S, RS, times_out_gga(R, S, RS)) → times_out_gga(zero(R), S, zero(RS))
TIMES_IN_GGA(one(R), S, RSS) → TIMES_IN_GGA(R, S, RS)
TIMES_IN_GGA(zero(R), S, zero(RS)) → TIMES_IN_GGA(R, S, RS)