0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 389 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 50 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 370 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 27 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 12 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
ADDJ_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZA_in_g(T23))
ADDJ_IN_GGA(zero(T23), b, zero(T23)) → BINARYZA_IN_G(T23)
BINARYZA_IN_G(zero(T29)) → U1_G(T29, binaryZA_in_g(T29))
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYZA_IN_G(one(T33)) → U2_G(T33, binaryB_in_g(T33))
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → U3_G(T38, binaryZA_in_g(T38))
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYB_IN_G(one(T42)) → U4_G(T42, binaryB_in_g(T42))
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
ADDJ_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binaryB_in_g(T47))
ADDJ_IN_GGA(one(T47), b, one(T47)) → BINARYB_IN_G(T47)
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → U32_GGA(T68, binaryZA_in_g(T68))
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → BINARYZA_IN_G(T68)
ADDJ_IN_GGA(b, one(T74), one(T74)) → U33_GGA(T74, binaryB_in_g(T74))
ADDJ_IN_GGA(b, one(T74), one(T74)) → BINARYB_IN_G(T74)
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → U34_GGA(T102, T103, T105, addzC_in_gga(T102, T103, T105))
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → ADDZC_IN_GGA(T102, T103, T105)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → U5_GGA(T121, T122, T124, addzC_in_gga(T121, T122, T124))
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → U6_GGA(T140, T141, T143, addxD_in_gga(T140, T141, T143))
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDXD_IN_GGA(one(T149), b, one(T149)) → U24_GGA(T149, binaryB_in_g(T149))
ADDXD_IN_GGA(one(T149), b, one(T149)) → BINARYB_IN_G(T149)
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → U25_GGA(T154, binaryZA_in_g(T154))
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → BINARYZA_IN_G(T154)
ADDXD_IN_GGA(T166, T167, T169) → U26_GGA(T166, T167, T169, addzC_in_gga(T166, T167, T169))
ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → U7_GGA(T185, T186, T188, addyE_in_gga(T185, T186, T188))
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(b, one(T194), one(T194)) → U27_GGA(T194, binaryB_in_g(T194))
ADDYE_IN_GGA(b, one(T194), one(T194)) → BINARYB_IN_G(T194)
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → U28_GGA(T199, binaryZA_in_g(T199))
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → BINARYZA_IN_G(T199)
ADDYE_IN_GGA(T211, T212, T214) → U29_GGA(T211, T212, T214, addzC_in_gga(T211, T212, T214))
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → U8_GGA(T224, T225, T227, addcF_in_gga(T224, T225, T227))
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T236, b, T238) → U21_GGA(T236, T238, succZH_in_ga(T236, T238))
ADDCF_IN_GGA(T236, b, T238) → SUCCZH_IN_GA(T236, T238)
SUCCZH_IN_GA(zero(T244), one(T244)) → U11_GA(T244, binaryZA_in_g(T244))
SUCCZH_IN_GA(zero(T244), one(T244)) → BINARYZA_IN_G(T244)
SUCCZH_IN_GA(one(T250), zero(T252)) → U12_GA(T250, T252, succG_in_ga(T250, T252))
SUCCZH_IN_GA(one(T250), zero(T252)) → SUCCG_IN_GA(T250, T252)
SUCCG_IN_GA(zero(T257), one(T257)) → U9_GA(T257, binaryZA_in_g(T257))
SUCCG_IN_GA(zero(T257), one(T257)) → BINARYZA_IN_G(T257)
SUCCG_IN_GA(one(T263), zero(T265)) → U10_GA(T263, T265, succG_in_ga(T263, T265))
SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)
ADDCF_IN_GGA(b, T274, T276) → U22_GGA(T274, T276, succZH_in_ga(T274, T276))
ADDCF_IN_GGA(b, T274, T276) → SUCCZH_IN_GA(T274, T276)
ADDCF_IN_GGA(T288, T289, T291) → U23_GGA(T288, T289, T291, addCI_in_gga(T288, T289, T291))
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → U13_GGA(T307, T308, T310, addzC_in_gga(T307, T308, T310))
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → U14_GGA(T335, binaryZA_in_g(T335))
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → BINARYZA_IN_G(T335)
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → U15_GGA(T345, T347, succG_in_ga(T345, T347))
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → SUCCG_IN_GA(T345, T347)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → U16_GGA(T358, T359, T361, addCI_in_gga(T358, T359, T361))
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → U17_GGA(T386, binaryZA_in_g(T386))
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → BINARYZA_IN_G(T386)
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → U18_GGA(T396, T398, succG_in_ga(T396, T398))
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → SUCCG_IN_GA(T396, T398)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → U19_GGA(T409, T410, T412, addCI_in_gga(T409, T410, T412))
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → U20_GGA(T422, T423, T425, addcF_in_gga(T422, T423, T425))
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → U35_GGA(T438, T439, T441, addxD_in_gga(T438, T439, T441))
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → ADDXD_IN_GGA(T438, T439, T441)
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → U36_GGA(T455, T456, T458, addyE_in_gga(T455, T456, T458))
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → ADDYE_IN_GGA(T455, T456, T458)
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → U37_GGA(T466, T467, T469, addcF_in_gga(T466, T467, T469))
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → ADDCF_IN_GGA(T466, T467, T469)
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
ADDJ_IN_GGA(zero(T23), b, zero(T23)) → U30_GGA(T23, binaryZA_in_g(T23))
ADDJ_IN_GGA(zero(T23), b, zero(T23)) → BINARYZA_IN_G(T23)
BINARYZA_IN_G(zero(T29)) → U1_G(T29, binaryZA_in_g(T29))
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYZA_IN_G(one(T33)) → U2_G(T33, binaryB_in_g(T33))
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → U3_G(T38, binaryZA_in_g(T38))
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYB_IN_G(one(T42)) → U4_G(T42, binaryB_in_g(T42))
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
ADDJ_IN_GGA(one(T47), b, one(T47)) → U31_GGA(T47, binaryB_in_g(T47))
ADDJ_IN_GGA(one(T47), b, one(T47)) → BINARYB_IN_G(T47)
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → U32_GGA(T68, binaryZA_in_g(T68))
ADDJ_IN_GGA(b, zero(T68), zero(T68)) → BINARYZA_IN_G(T68)
ADDJ_IN_GGA(b, one(T74), one(T74)) → U33_GGA(T74, binaryB_in_g(T74))
ADDJ_IN_GGA(b, one(T74), one(T74)) → BINARYB_IN_G(T74)
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → U34_GGA(T102, T103, T105, addzC_in_gga(T102, T103, T105))
ADDJ_IN_GGA(zero(T102), zero(T103), zero(T105)) → ADDZC_IN_GGA(T102, T103, T105)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → U5_GGA(T121, T122, T124, addzC_in_gga(T121, T122, T124))
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → U6_GGA(T140, T141, T143, addxD_in_gga(T140, T141, T143))
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDXD_IN_GGA(one(T149), b, one(T149)) → U24_GGA(T149, binaryB_in_g(T149))
ADDXD_IN_GGA(one(T149), b, one(T149)) → BINARYB_IN_G(T149)
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → U25_GGA(T154, binaryZA_in_g(T154))
ADDXD_IN_GGA(zero(T154), b, zero(T154)) → BINARYZA_IN_G(T154)
ADDXD_IN_GGA(T166, T167, T169) → U26_GGA(T166, T167, T169, addzC_in_gga(T166, T167, T169))
ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → U7_GGA(T185, T186, T188, addyE_in_gga(T185, T186, T188))
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(b, one(T194), one(T194)) → U27_GGA(T194, binaryB_in_g(T194))
ADDYE_IN_GGA(b, one(T194), one(T194)) → BINARYB_IN_G(T194)
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → U28_GGA(T199, binaryZA_in_g(T199))
ADDYE_IN_GGA(b, zero(T199), zero(T199)) → BINARYZA_IN_G(T199)
ADDYE_IN_GGA(T211, T212, T214) → U29_GGA(T211, T212, T214, addzC_in_gga(T211, T212, T214))
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → U8_GGA(T224, T225, T227, addcF_in_gga(T224, T225, T227))
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T236, b, T238) → U21_GGA(T236, T238, succZH_in_ga(T236, T238))
ADDCF_IN_GGA(T236, b, T238) → SUCCZH_IN_GA(T236, T238)
SUCCZH_IN_GA(zero(T244), one(T244)) → U11_GA(T244, binaryZA_in_g(T244))
SUCCZH_IN_GA(zero(T244), one(T244)) → BINARYZA_IN_G(T244)
SUCCZH_IN_GA(one(T250), zero(T252)) → U12_GA(T250, T252, succG_in_ga(T250, T252))
SUCCZH_IN_GA(one(T250), zero(T252)) → SUCCG_IN_GA(T250, T252)
SUCCG_IN_GA(zero(T257), one(T257)) → U9_GA(T257, binaryZA_in_g(T257))
SUCCG_IN_GA(zero(T257), one(T257)) → BINARYZA_IN_G(T257)
SUCCG_IN_GA(one(T263), zero(T265)) → U10_GA(T263, T265, succG_in_ga(T263, T265))
SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)
ADDCF_IN_GGA(b, T274, T276) → U22_GGA(T274, T276, succZH_in_ga(T274, T276))
ADDCF_IN_GGA(b, T274, T276) → SUCCZH_IN_GA(T274, T276)
ADDCF_IN_GGA(T288, T289, T291) → U23_GGA(T288, T289, T291, addCI_in_gga(T288, T289, T291))
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → U13_GGA(T307, T308, T310, addzC_in_gga(T307, T308, T310))
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → U14_GGA(T335, binaryZA_in_g(T335))
ADDCI_IN_GGA(zero(zero(T335)), one(b), zero(one(T335))) → BINARYZA_IN_G(T335)
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → U15_GGA(T345, T347, succG_in_ga(T345, T347))
ADDCI_IN_GGA(zero(one(T345)), one(b), zero(zero(T347))) → SUCCG_IN_GA(T345, T347)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → U16_GGA(T358, T359, T361, addCI_in_gga(T358, T359, T361))
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → U17_GGA(T386, binaryZA_in_g(T386))
ADDCI_IN_GGA(one(b), zero(zero(T386)), zero(one(T386))) → BINARYZA_IN_G(T386)
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → U18_GGA(T396, T398, succG_in_ga(T396, T398))
ADDCI_IN_GGA(one(b), zero(one(T396)), zero(zero(T398))) → SUCCG_IN_GA(T396, T398)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → U19_GGA(T409, T410, T412, addCI_in_gga(T409, T410, T412))
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → U20_GGA(T422, T423, T425, addcF_in_gga(T422, T423, T425))
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → U35_GGA(T438, T439, T441, addxD_in_gga(T438, T439, T441))
ADDJ_IN_GGA(zero(T438), one(T439), one(T441)) → ADDXD_IN_GGA(T438, T439, T441)
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → U36_GGA(T455, T456, T458, addyE_in_gga(T455, T456, T458))
ADDJ_IN_GGA(one(T455), zero(T456), one(T458)) → ADDYE_IN_GGA(T455, T456, T458)
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → U37_GGA(T466, T467, T469, addcF_in_gga(T466, T467, T469))
ADDJ_IN_GGA(one(T466), one(T467), zero(T469)) → ADDCF_IN_GGA(T466, T467, T469)
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
BINARYZA_IN_G(one(T33)) → BINARYB_IN_G(T33)
BINARYB_IN_G(zero(T38)) → BINARYZA_IN_G(T38)
BINARYZA_IN_G(zero(T29)) → BINARYZA_IN_G(T29)
BINARYB_IN_G(one(T42)) → BINARYB_IN_G(T42)
From the DPs we obtained the following set of size-change graphs:
SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
SUCCG_IN_GA(one(T263), zero(T265)) → SUCCG_IN_GA(T263, T265)
SUCCG_IN_GA(one(T263)) → SUCCG_IN_GA(T263)
From the DPs we obtained the following set of size-change graphs:
ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)
addJ_in_gga(b, b, b) → addJ_out_gga(b, b, b)
addJ_in_gga(zero(T23), b, zero(T23)) → U30_gga(T23, binaryZA_in_g(T23))
binaryZA_in_g(zero(T29)) → U1_g(T29, binaryZA_in_g(T29))
binaryZA_in_g(one(T33)) → U2_g(T33, binaryB_in_g(T33))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T38)) → U3_g(T38, binaryZA_in_g(T38))
U3_g(T38, binaryZA_out_g(T38)) → binaryB_out_g(zero(T38))
binaryB_in_g(one(T42)) → U4_g(T42, binaryB_in_g(T42))
U4_g(T42, binaryB_out_g(T42)) → binaryB_out_g(one(T42))
U2_g(T33, binaryB_out_g(T33)) → binaryZA_out_g(one(T33))
U1_g(T29, binaryZA_out_g(T29)) → binaryZA_out_g(zero(T29))
U30_gga(T23, binaryZA_out_g(T23)) → addJ_out_gga(zero(T23), b, zero(T23))
addJ_in_gga(one(T47), b, one(T47)) → U31_gga(T47, binaryB_in_g(T47))
U31_gga(T47, binaryB_out_g(T47)) → addJ_out_gga(one(T47), b, one(T47))
addJ_in_gga(b, zero(T68), zero(T68)) → U32_gga(T68, binaryZA_in_g(T68))
U32_gga(T68, binaryZA_out_g(T68)) → addJ_out_gga(b, zero(T68), zero(T68))
addJ_in_gga(b, one(T74), one(T74)) → U33_gga(T74, binaryB_in_g(T74))
U33_gga(T74, binaryB_out_g(T74)) → addJ_out_gga(b, one(T74), one(T74))
addJ_in_gga(zero(T102), zero(T103), zero(T105)) → U34_gga(T102, T103, T105, addzC_in_gga(T102, T103, T105))
addzC_in_gga(zero(T121), zero(T122), zero(T124)) → U5_gga(T121, T122, T124, addzC_in_gga(T121, T122, T124))
addzC_in_gga(zero(T140), one(T141), one(T143)) → U6_gga(T140, T141, T143, addxD_in_gga(T140, T141, T143))
addxD_in_gga(one(T149), b, one(T149)) → U24_gga(T149, binaryB_in_g(T149))
U24_gga(T149, binaryB_out_g(T149)) → addxD_out_gga(one(T149), b, one(T149))
addxD_in_gga(zero(T154), b, zero(T154)) → U25_gga(T154, binaryZA_in_g(T154))
U25_gga(T154, binaryZA_out_g(T154)) → addxD_out_gga(zero(T154), b, zero(T154))
addxD_in_gga(T166, T167, T169) → U26_gga(T166, T167, T169, addzC_in_gga(T166, T167, T169))
addzC_in_gga(one(T185), zero(T186), one(T188)) → U7_gga(T185, T186, T188, addyE_in_gga(T185, T186, T188))
addyE_in_gga(b, one(T194), one(T194)) → U27_gga(T194, binaryB_in_g(T194))
U27_gga(T194, binaryB_out_g(T194)) → addyE_out_gga(b, one(T194), one(T194))
addyE_in_gga(b, zero(T199), zero(T199)) → U28_gga(T199, binaryZA_in_g(T199))
U28_gga(T199, binaryZA_out_g(T199)) → addyE_out_gga(b, zero(T199), zero(T199))
addyE_in_gga(T211, T212, T214) → U29_gga(T211, T212, T214, addzC_in_gga(T211, T212, T214))
addzC_in_gga(one(T224), one(T225), zero(T227)) → U8_gga(T224, T225, T227, addcF_in_gga(T224, T225, T227))
addcF_in_gga(b, b, one(b)) → addcF_out_gga(b, b, one(b))
addcF_in_gga(T236, b, T238) → U21_gga(T236, T238, succZH_in_ga(T236, T238))
succZH_in_ga(zero(T244), one(T244)) → U11_ga(T244, binaryZA_in_g(T244))
U11_ga(T244, binaryZA_out_g(T244)) → succZH_out_ga(zero(T244), one(T244))
succZH_in_ga(one(T250), zero(T252)) → U12_ga(T250, T252, succG_in_ga(T250, T252))
succG_in_ga(b, one(b)) → succG_out_ga(b, one(b))
succG_in_ga(zero(T257), one(T257)) → U9_ga(T257, binaryZA_in_g(T257))
U9_ga(T257, binaryZA_out_g(T257)) → succG_out_ga(zero(T257), one(T257))
succG_in_ga(one(T263), zero(T265)) → U10_ga(T263, T265, succG_in_ga(T263, T265))
U10_ga(T263, T265, succG_out_ga(T263, T265)) → succG_out_ga(one(T263), zero(T265))
U12_ga(T250, T252, succG_out_ga(T250, T252)) → succZH_out_ga(one(T250), zero(T252))
U21_gga(T236, T238, succZH_out_ga(T236, T238)) → addcF_out_gga(T236, b, T238)
addcF_in_gga(b, T274, T276) → U22_gga(T274, T276, succZH_in_ga(T274, T276))
U22_gga(T274, T276, succZH_out_ga(T274, T276)) → addcF_out_gga(b, T274, T276)
addcF_in_gga(T288, T289, T291) → U23_gga(T288, T289, T291, addCI_in_gga(T288, T289, T291))
addCI_in_gga(zero(T307), zero(T308), one(T310)) → U13_gga(T307, T308, T310, addzC_in_gga(T307, T308, T310))
U13_gga(T307, T308, T310, addzC_out_gga(T307, T308, T310)) → addCI_out_gga(zero(T307), zero(T308), one(T310))
addCI_in_gga(zero(zero(T335)), one(b), zero(one(T335))) → U14_gga(T335, binaryZA_in_g(T335))
U14_gga(T335, binaryZA_out_g(T335)) → addCI_out_gga(zero(zero(T335)), one(b), zero(one(T335)))
addCI_in_gga(zero(one(T345)), one(b), zero(zero(T347))) → U15_gga(T345, T347, succG_in_ga(T345, T347))
U15_gga(T345, T347, succG_out_ga(T345, T347)) → addCI_out_gga(zero(one(T345)), one(b), zero(zero(T347)))
addCI_in_gga(zero(T358), one(T359), zero(T361)) → U16_gga(T358, T359, T361, addCI_in_gga(T358, T359, T361))
addCI_in_gga(one(b), zero(zero(T386)), zero(one(T386))) → U17_gga(T386, binaryZA_in_g(T386))
U17_gga(T386, binaryZA_out_g(T386)) → addCI_out_gga(one(b), zero(zero(T386)), zero(one(T386)))
addCI_in_gga(one(b), zero(one(T396)), zero(zero(T398))) → U18_gga(T396, T398, succG_in_ga(T396, T398))
U18_gga(T396, T398, succG_out_ga(T396, T398)) → addCI_out_gga(one(b), zero(one(T396)), zero(zero(T398)))
addCI_in_gga(one(T409), zero(T410), zero(T412)) → U19_gga(T409, T410, T412, addCI_in_gga(T409, T410, T412))
addCI_in_gga(one(T422), one(T423), one(T425)) → U20_gga(T422, T423, T425, addcF_in_gga(T422, T423, T425))
U20_gga(T422, T423, T425, addcF_out_gga(T422, T423, T425)) → addCI_out_gga(one(T422), one(T423), one(T425))
U19_gga(T409, T410, T412, addCI_out_gga(T409, T410, T412)) → addCI_out_gga(one(T409), zero(T410), zero(T412))
U16_gga(T358, T359, T361, addCI_out_gga(T358, T359, T361)) → addCI_out_gga(zero(T358), one(T359), zero(T361))
U23_gga(T288, T289, T291, addCI_out_gga(T288, T289, T291)) → addcF_out_gga(T288, T289, T291)
U8_gga(T224, T225, T227, addcF_out_gga(T224, T225, T227)) → addzC_out_gga(one(T224), one(T225), zero(T227))
U29_gga(T211, T212, T214, addzC_out_gga(T211, T212, T214)) → addyE_out_gga(T211, T212, T214)
U7_gga(T185, T186, T188, addyE_out_gga(T185, T186, T188)) → addzC_out_gga(one(T185), zero(T186), one(T188))
U26_gga(T166, T167, T169, addzC_out_gga(T166, T167, T169)) → addxD_out_gga(T166, T167, T169)
U6_gga(T140, T141, T143, addxD_out_gga(T140, T141, T143)) → addzC_out_gga(zero(T140), one(T141), one(T143))
U5_gga(T121, T122, T124, addzC_out_gga(T121, T122, T124)) → addzC_out_gga(zero(T121), zero(T122), zero(T124))
U34_gga(T102, T103, T105, addzC_out_gga(T102, T103, T105)) → addJ_out_gga(zero(T102), zero(T103), zero(T105))
addJ_in_gga(zero(T438), one(T439), one(T441)) → U35_gga(T438, T439, T441, addxD_in_gga(T438, T439, T441))
U35_gga(T438, T439, T441, addxD_out_gga(T438, T439, T441)) → addJ_out_gga(zero(T438), one(T439), one(T441))
addJ_in_gga(one(T455), zero(T456), one(T458)) → U36_gga(T455, T456, T458, addyE_in_gga(T455, T456, T458))
U36_gga(T455, T456, T458, addyE_out_gga(T455, T456, T458)) → addJ_out_gga(one(T455), zero(T456), one(T458))
addJ_in_gga(one(T466), one(T467), zero(T469)) → U37_gga(T466, T467, T469, addcF_in_gga(T466, T467, T469))
U37_gga(T466, T467, T469, addcF_out_gga(T466, T467, T469)) → addJ_out_gga(one(T466), one(T467), zero(T469))
ADDXD_IN_GGA(T166, T167, T169) → ADDZC_IN_GGA(T166, T167, T169)
ADDZC_IN_GGA(zero(T121), zero(T122), zero(T124)) → ADDZC_IN_GGA(T121, T122, T124)
ADDZC_IN_GGA(zero(T140), one(T141), one(T143)) → ADDXD_IN_GGA(T140, T141, T143)
ADDZC_IN_GGA(one(T185), zero(T186), one(T188)) → ADDYE_IN_GGA(T185, T186, T188)
ADDYE_IN_GGA(T211, T212, T214) → ADDZC_IN_GGA(T211, T212, T214)
ADDZC_IN_GGA(one(T224), one(T225), zero(T227)) → ADDCF_IN_GGA(T224, T225, T227)
ADDCF_IN_GGA(T288, T289, T291) → ADDCI_IN_GGA(T288, T289, T291)
ADDCI_IN_GGA(zero(T307), zero(T308), one(T310)) → ADDZC_IN_GGA(T307, T308, T310)
ADDCI_IN_GGA(zero(T358), one(T359), zero(T361)) → ADDCI_IN_GGA(T358, T359, T361)
ADDCI_IN_GGA(one(T409), zero(T410), zero(T412)) → ADDCI_IN_GGA(T409, T410, T412)
ADDCI_IN_GGA(one(T422), one(T423), one(T425)) → ADDCF_IN_GGA(T422, T423, T425)
ADDXD_IN_GGA(T166, T167) → ADDZC_IN_GGA(T166, T167)
ADDZC_IN_GGA(zero(T121), zero(T122)) → ADDZC_IN_GGA(T121, T122)
ADDZC_IN_GGA(zero(T140), one(T141)) → ADDXD_IN_GGA(T140, T141)
ADDZC_IN_GGA(one(T185), zero(T186)) → ADDYE_IN_GGA(T185, T186)
ADDYE_IN_GGA(T211, T212) → ADDZC_IN_GGA(T211, T212)
ADDZC_IN_GGA(one(T224), one(T225)) → ADDCF_IN_GGA(T224, T225)
ADDCF_IN_GGA(T288, T289) → ADDCI_IN_GGA(T288, T289)
ADDCI_IN_GGA(zero(T307), zero(T308)) → ADDZC_IN_GGA(T307, T308)
ADDCI_IN_GGA(zero(T358), one(T359)) → ADDCI_IN_GGA(T358, T359)
ADDCI_IN_GGA(one(T409), zero(T410)) → ADDCI_IN_GGA(T409, T410)
ADDCI_IN_GGA(one(T422), one(T423)) → ADDCF_IN_GGA(T422, T423)
From the DPs we obtained the following set of size-change graphs: