0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔)
↳9 PiDP
↳10 PiDPToQDPProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔)
↳16 PiDP
↳17 PiDPToQDPProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔)
↳23 PiDP
↳24 PiDPToQDPProof (⇔)
↳25 QDP
↳26 QDPSizeChangeProof (⇔)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔)
↳30 PiDP
↳31 PiDPToQDPProof (⇐)
↳32 QDP
↳33 QDPSizeChangeProof (⇔)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔)
↳37 PiDP
↳38 PiDPToQDPProof (⇐)
↳39 QDP
↳40 QDPSizeChangeProof (⇔)
↳41 YES
↳42 PiDP
↳43 UsableRulesProof (⇔)
↳44 PiDP
↳45 PiDPToQDPProof (⇐)
↳46 QDP
↳47 NonTerminationProof (⇔)
↳48 NO
↳49 PiDP
↳50 UsableRulesProof (⇔)
↳51 PiDP
↳52 PiDPToQDPProof (⇐)
↳53 QDP
↳54 NonTerminationProof (⇔)
↳55 NO
↳56 PiDP
↳57 UsableRulesProof (⇔)
↳58 PiDP
↳59 PiDPToQDPProof (⇐)
↳60 QDP
↳61 NonTerminationProof (⇔)
↳62 NO
↳63 PiDP
↳64 UsableRulesProof (⇔)
↳65 PiDP
↳66 PiDPToQDPProof (⇐)
↳67 QDP
↳68 NonTerminationProof (⇔)
↳69 NO
↳70 PiDP
↳71 UsableRulesProof (⇔)
↳72 PiDP
↳73 PiDPToQDPProof (⇐)
↳74 QDP
↳75 QDPSizeChangeProof (⇔)
↳76 YES
TIMES1_IN_AAG(zero(zero(T34)), T35, zero(zero(T33))) → U76_AAG(T34, T35, T33, times1_in_aag(T34, T35, T33))
TIMES1_IN_AAG(zero(zero(T34)), T35, zero(zero(T33))) → TIMES1_IN_AAG(T34, T35, T33)
TIMES1_IN_AAG(zero(one(T53)), T54, zero(T52)) → U77_AAG(T53, T54, T52, p20_in_aaag(T53, T54, X56, T52))
TIMES1_IN_AAG(zero(one(T53)), T54, zero(T52)) → P20_IN_AAAG(T53, T54, X56, T52)
P20_IN_AAAG(T53, T54, X56, T52) → U58_AAAG(T53, T54, X56, T52, times22_in_aaa(T53, T54, X56))
P20_IN_AAAG(T53, T54, X56, T52) → TIMES22_IN_AAA(T53, T54, X56)
TIMES22_IN_AAA(zero(T76), T77, zero(X89)) → U1_AAA(T76, T77, X89, times22_in_aaa(T76, T77, X89))
TIMES22_IN_AAA(zero(T76), T77, zero(X89)) → TIMES22_IN_AAA(T76, T77, X89)
TIMES22_IN_AAA(one(T86), T87, X108) → U2_AAA(T86, T87, X108, times22_in_aaa(T86, T87, X107))
TIMES22_IN_AAA(one(T86), T87, X108) → TIMES22_IN_AAA(T86, T87, X107)
TIMES22_IN_AAA(one(T86), T91, X108) → U3_AAA(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U3_AAA(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U4_AAA(T86, T91, X108, add37_in_aaa(T91, T90, X108))
U3_AAA(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → ADD37_IN_AAA(T91, T90, X108)
ADD37_IN_AAA(b, T102, zero(T102)) → U64_AAA(T102, binaryZ43_in_a(T102))
ADD37_IN_AAA(b, T102, zero(T102)) → BINARYZ43_IN_A(T102)
BINARYZ43_IN_A(T113) → U33_A(T113, binaryZ48_in_a(T113))
BINARYZ43_IN_A(T113) → BINARYZ48_IN_A(T113)
BINARYZ48_IN_A(zero(T120)) → U5_A(T120, binaryZ48_in_a(T120))
BINARYZ48_IN_A(zero(T120)) → BINARYZ48_IN_A(T120)
BINARYZ48_IN_A(one(T125)) → U6_A(T125, binary54_in_a(T125))
BINARYZ48_IN_A(one(T125)) → BINARY54_IN_A(T125)
BINARY54_IN_A(zero(T131)) → U7_A(T131, binaryZ48_in_a(T131))
BINARY54_IN_A(zero(T131)) → BINARYZ48_IN_A(T131)
BINARY54_IN_A(one(T136)) → U8_A(T136, binary54_in_a(T136))
BINARY54_IN_A(one(T136)) → BINARY54_IN_A(T136)
ADD37_IN_AAA(zero(T161), T162, zero(X196)) → U65_AAA(T161, T162, X196, addz73_in_aaa(T161, T162, X196))
ADD37_IN_AAA(zero(T161), T162, zero(X196)) → ADDZ73_IN_AAA(T161, T162, X196)
ADDZ73_IN_AAA(zero(T175), zero(T176), zero(X223)) → U9_AAA(T175, T176, X223, addz73_in_aaa(T175, T176, X223))
ADDZ73_IN_AAA(zero(T175), zero(T176), zero(X223)) → ADDZ73_IN_AAA(T175, T176, X223)
ADDZ73_IN_AAA(zero(one(T197)), one(b), one(one(T197))) → U10_AAA(T197, binary54_in_a(T197))
ADDZ73_IN_AAA(zero(one(T197)), one(b), one(one(T197))) → BINARY54_IN_A(T197)
ADDZ73_IN_AAA(zero(zero(T203)), one(b), one(zero(T203))) → U11_AAA(T203, binaryZ48_in_a(T203))
ADDZ73_IN_AAA(zero(zero(T203)), one(b), one(zero(T203))) → BINARYZ48_IN_A(T203)
ADDZ73_IN_AAA(zero(T215), one(T216), one(X283)) → U12_AAA(T215, T216, X283, addz73_in_aaa(T215, T216, X283))
ADDZ73_IN_AAA(zero(T215), one(T216), one(X283)) → ADDZ73_IN_AAA(T215, T216, X283)
ADDZ73_IN_AAA(one(T229), zero(T230), one(X307)) → U13_AAA(T229, T230, X307, addy96_in_aaa(T229, T230, X307))
ADDZ73_IN_AAA(one(T229), zero(T230), one(X307)) → ADDY96_IN_AAA(T229, T230, X307)
ADDY96_IN_AAA(b, one(T237), one(T237)) → U30_AAA(T237, binary54_in_a(T237))
ADDY96_IN_AAA(b, one(T237), one(T237)) → BINARY54_IN_A(T237)
ADDY96_IN_AAA(b, zero(T243), zero(T243)) → U31_AAA(T243, binaryZ48_in_a(T243))
ADDY96_IN_AAA(b, zero(T243), zero(T243)) → BINARYZ48_IN_A(T243)
ADDY96_IN_AAA(T255, T256, X340) → U32_AAA(T255, T256, X340, addz73_in_aaa(T255, T256, X340))
ADDY96_IN_AAA(T255, T256, X340) → ADDZ73_IN_AAA(T255, T256, X340)
ADDZ73_IN_AAA(one(T265), one(T266), zero(X356)) → U14_AAA(T265, T266, X356, addc108_in_aaa(T265, T266, X356))
ADDZ73_IN_AAA(one(T265), one(T266), zero(X356)) → ADDC108_IN_AAA(T265, T266, X356)
ADDC108_IN_AAA(T272, b, X374) → U27_AAA(T272, X374, succZ118_in_aa(T272, X374))
ADDC108_IN_AAA(T272, b, X374) → SUCCZ118_IN_AA(T272, X374)
SUCCZ118_IN_AA(zero(T279), one(T279)) → U17_AA(T279, binaryZ48_in_a(T279))
SUCCZ118_IN_AA(zero(T279), one(T279)) → BINARYZ48_IN_A(T279)
SUCCZ118_IN_AA(one(T284), zero(X393)) → U18_AA(T284, X393, succ125_in_aa(T284, X393))
SUCCZ118_IN_AA(one(T284), zero(X393)) → SUCC125_IN_AA(T284, X393)
SUCC125_IN_AA(zero(T290), one(T290)) → U15_AA(T290, binaryZ48_in_a(T290))
SUCC125_IN_AA(zero(T290), one(T290)) → BINARYZ48_IN_A(T290)
SUCC125_IN_AA(one(T295), zero(X411)) → U16_AA(T295, X411, succ125_in_aa(T295, X411))
SUCC125_IN_AA(one(T295), zero(X411)) → SUCC125_IN_AA(T295, X411)
ADDC108_IN_AAA(b, T301, X428) → U28_AAA(T301, X428, succZ118_in_aa(T301, X428))
ADDC108_IN_AAA(b, T301, X428) → SUCCZ118_IN_AA(T301, X428)
ADDC108_IN_AAA(T313, T314, X447) → U29_AAA(T313, T314, X447, addC143_in_aaa(T313, T314, X447))
ADDC108_IN_AAA(T313, T314, X447) → ADDC143_IN_AAA(T313, T314, X447)
ADDC143_IN_AAA(zero(T327), zero(T328), one(X471)) → U19_AAA(T327, T328, X471, addz73_in_aaa(T327, T328, X471))
ADDC143_IN_AAA(zero(T327), zero(T328), one(X471)) → ADDZ73_IN_AAA(T327, T328, X471)
ADDC143_IN_AAA(zero(zero(T349)), one(b), zero(one(T349))) → U20_AAA(T349, binaryZ48_in_a(T349))
ADDC143_IN_AAA(zero(zero(T349)), one(b), zero(one(T349))) → BINARYZ48_IN_A(T349)
ADDC143_IN_AAA(zero(one(T356)), one(b), zero(zero(X524))) → U21_AAA(T356, X524, succ125_in_aa(T356, X524))
ADDC143_IN_AAA(zero(one(T356)), one(b), zero(zero(X524))) → SUCC125_IN_AA(T356, X524)
ADDC143_IN_AAA(zero(T367), one(T368), zero(X542)) → U22_AAA(T367, T368, X542, addC143_in_aaa(T367, T368, X542))
ADDC143_IN_AAA(zero(T367), one(T368), zero(X542)) → ADDC143_IN_AAA(T367, T368, X542)
ADDC143_IN_AAA(one(b), zero(zero(T389)), zero(one(T389))) → U23_AAA(T389, binaryZ48_in_a(T389))
ADDC143_IN_AAA(one(b), zero(zero(T389)), zero(one(T389))) → BINARYZ48_IN_A(T389)
ADDC143_IN_AAA(one(b), zero(one(T396)), zero(zero(X592))) → U24_AAA(T396, X592, succ125_in_aa(T396, X592))
ADDC143_IN_AAA(one(b), zero(one(T396)), zero(zero(X592))) → SUCC125_IN_AA(T396, X592)
ADDC143_IN_AAA(one(T407), zero(T408), zero(X610)) → U25_AAA(T407, T408, X610, addC143_in_aaa(T407, T408, X610))
ADDC143_IN_AAA(one(T407), zero(T408), zero(X610)) → ADDC143_IN_AAA(T407, T408, X610)
ADDC143_IN_AAA(one(T417), one(T418), one(X626)) → U26_AAA(T417, T418, X626, addc108_in_aaa(T417, T418, X626))
ADDC143_IN_AAA(one(T417), one(T418), one(X626)) → ADDC108_IN_AAA(T417, T418, X626)
ADD37_IN_AAA(one(T430), T431, one(X652)) → U66_AAA(T430, T431, X652, addy96_in_aaa(T430, T431, X652))
ADD37_IN_AAA(one(T430), T431, one(X652)) → ADDY96_IN_AAA(T430, T431, X652)
P20_IN_AAAG(T53, T58, T57, T52) → U59_AAAG(T53, T58, T57, T52, timesc22_in_aaa(T53, T58, T57))
U59_AAAG(T53, T58, T57, T52, timesc22_out_aaa(T53, T58, T57)) → U60_AAAG(T53, T58, T57, T52, add23_in_aag(T58, T57, T52))
U59_AAAG(T53, T58, T57, T52, timesc22_out_aaa(T53, T58, T57)) → ADD23_IN_AAG(T58, T57, T52)
ADD23_IN_AAG(b, T441, zero(T441)) → U61_AAG(T441, binaryZ43_in_g(T441))
ADD23_IN_AAG(b, T441, zero(T441)) → BINARYZ43_IN_G(T441)
BINARYZ43_IN_G(T113) → U33_G(T113, binaryZ48_in_g(T113))
BINARYZ43_IN_G(T113) → BINARYZ48_IN_G(T113)
BINARYZ48_IN_G(zero(T120)) → U5_G(T120, binaryZ48_in_g(T120))
BINARYZ48_IN_G(zero(T120)) → BINARYZ48_IN_G(T120)
BINARYZ48_IN_G(one(T125)) → U6_G(T125, binary54_in_g(T125))
BINARYZ48_IN_G(one(T125)) → BINARY54_IN_G(T125)
BINARY54_IN_G(zero(T131)) → U7_G(T131, binaryZ48_in_g(T131))
BINARY54_IN_G(zero(T131)) → BINARYZ48_IN_G(T131)
BINARY54_IN_G(one(T136)) → U8_G(T136, binary54_in_g(T136))
BINARY54_IN_G(one(T136)) → BINARY54_IN_G(T136)
ADD23_IN_AAG(zero(T477), T478, zero(T476)) → U62_AAG(T477, T478, T476, addz196_in_aag(T477, T478, T476))
ADD23_IN_AAG(zero(T477), T478, zero(T476)) → ADDZ196_IN_AAG(T477, T478, T476)
ADDZ196_IN_AAG(zero(T497), zero(T498), zero(T496)) → U34_AAG(T497, T498, T496, addz196_in_aag(T497, T498, T496))
ADDZ196_IN_AAG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_AAG(T497, T498, T496)
ADDZ196_IN_AAG(zero(one(T524)), one(b), one(one(T524))) → U35_AAG(T524, binary54_in_g(T524))
ADDZ196_IN_AAG(zero(one(T524)), one(b), one(one(T524))) → BINARY54_IN_G(T524)
ADDZ196_IN_AAG(zero(zero(T529)), one(b), one(zero(T529))) → U36_AAG(T529, binaryZ48_in_g(T529))
ADDZ196_IN_AAG(zero(zero(T529)), one(b), one(zero(T529))) → BINARYZ48_IN_G(T529)
ADDZ196_IN_AAG(zero(T545), one(T546), one(T544)) → U37_AAG(T545, T546, T544, addz196_in_aag(T545, T546, T544))
ADDZ196_IN_AAG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_AAG(T545, T546, T544)
ADDZ196_IN_AAG(one(T565), zero(T566), one(T564)) → U38_AAG(T565, T566, T564, addy219_in_aag(T565, T566, T564))
ADDZ196_IN_AAG(one(T565), zero(T566), one(T564)) → ADDY219_IN_AAG(T565, T566, T564)
ADDY219_IN_AAG(b, one(T572), one(T572)) → U55_AAG(T572, binary54_in_g(T572))
ADDY219_IN_AAG(b, one(T572), one(T572)) → BINARY54_IN_G(T572)
ADDY219_IN_AAG(b, zero(T577), zero(T577)) → U56_AAG(T577, binaryZ48_in_g(T577))
ADDY219_IN_AAG(b, zero(T577), zero(T577)) → BINARYZ48_IN_G(T577)
ADDY219_IN_AAG(T593, T594, T592) → U57_AAG(T593, T594, T592, addz196_in_aag(T593, T594, T592))
ADDY219_IN_AAG(T593, T594, T592) → ADDZ196_IN_AAG(T593, T594, T592)
ADDZ196_IN_AAG(one(T607), one(T608), zero(T606)) → U39_AAG(T607, T608, T606, addc231_in_aag(T607, T608, T606))
ADDZ196_IN_AAG(one(T607), one(T608), zero(T606)) → ADDC231_IN_AAG(T607, T608, T606)
ADDC231_IN_AAG(T619, b, T618) → U52_AAG(T619, T618, succZ241_in_ag(T619, T618))
ADDC231_IN_AAG(T619, b, T618) → SUCCZ241_IN_AG(T619, T618)
SUCCZ241_IN_AG(zero(T625), one(T625)) → U42_AG(T625, binaryZ48_in_g(T625))
SUCCZ241_IN_AG(zero(T625), one(T625)) → BINARYZ48_IN_G(T625)
SUCCZ241_IN_AG(one(T633), zero(T632)) → U43_AG(T633, T632, succ248_in_ag(T633, T632))
SUCCZ241_IN_AG(one(T633), zero(T632)) → SUCC248_IN_AG(T633, T632)
SUCC248_IN_AG(zero(T638), one(T638)) → U40_AG(T638, binaryZ48_in_g(T638))
SUCC248_IN_AG(zero(T638), one(T638)) → BINARYZ48_IN_G(T638)
SUCC248_IN_AG(one(T646), zero(T645)) → U41_AG(T646, T645, succ248_in_ag(T646, T645))
SUCC248_IN_AG(one(T646), zero(T645)) → SUCC248_IN_AG(T646, T645)
ADDC231_IN_AAG(b, T657, T656) → U53_AAG(T657, T656, succZ241_in_ag(T657, T656))
ADDC231_IN_AAG(b, T657, T656) → SUCCZ241_IN_AG(T657, T656)
ADDC231_IN_AAG(T673, T674, T672) → U54_AAG(T673, T674, T672, addC266_in_aag(T673, T674, T672))
ADDC231_IN_AAG(T673, T674, T672) → ADDC266_IN_AAG(T673, T674, T672)
ADDC266_IN_AAG(zero(T693), zero(T694), one(T692)) → U44_AAG(T693, T694, T692, addz196_in_aag(T693, T694, T692))
ADDC266_IN_AAG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_AAG(T693, T694, T692)
ADDC266_IN_AAG(zero(zero(T720)), one(b), zero(one(T720))) → U45_AAG(T720, binaryZ48_in_g(T720))
ADDC266_IN_AAG(zero(zero(T720)), one(b), zero(one(T720))) → BINARYZ48_IN_G(T720)
ADDC266_IN_AAG(zero(one(T732)), one(b), zero(zero(T731))) → U46_AAG(T732, T731, succ248_in_ag(T732, T731))
ADDC266_IN_AAG(zero(one(T732)), one(b), zero(zero(T731))) → SUCC248_IN_AG(T732, T731)
ADDC266_IN_AAG(zero(T747), one(T748), zero(T746)) → U47_AAG(T747, T748, T746, addC266_in_aag(T747, T748, T746))
ADDC266_IN_AAG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_AAG(T747, T748, T746)
ADDC266_IN_AAG(one(b), zero(zero(T774)), zero(one(T774))) → U48_AAG(T774, binaryZ48_in_g(T774))
ADDC266_IN_AAG(one(b), zero(zero(T774)), zero(one(T774))) → BINARYZ48_IN_G(T774)
ADDC266_IN_AAG(one(b), zero(one(T786)), zero(zero(T785))) → U49_AAG(T786, T785, succ248_in_ag(T786, T785))
ADDC266_IN_AAG(one(b), zero(one(T786)), zero(zero(T785))) → SUCC248_IN_AG(T786, T785)
ADDC266_IN_AAG(one(T801), zero(T802), zero(T800)) → U50_AAG(T801, T802, T800, addC266_in_aag(T801, T802, T800))
ADDC266_IN_AAG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_AAG(T801, T802, T800)
ADDC266_IN_AAG(one(T815), one(T816), one(T814)) → U51_AAG(T815, T816, T814, addc231_in_aag(T815, T816, T814))
ADDC266_IN_AAG(one(T815), one(T816), one(T814)) → ADDC231_IN_AAG(T815, T816, T814)
ADD23_IN_AAG(one(T833), T834, one(T832)) → U63_AAG(T833, T834, T832, addy219_in_aag(T833, T834, T832))
ADD23_IN_AAG(one(T833), T834, one(T832)) → ADDY219_IN_AAG(T833, T834, T832)
TIMES1_IN_AAG(one(T846), T847, zero(T845)) → U78_AAG(T846, T847, T845, p20_in_aaag(T846, T847, X1078, zero(T845)))
TIMES1_IN_AAG(one(T846), T847, zero(T845)) → P20_IN_AAAG(T846, T847, X1078, zero(T845))
TIMES1_IN_AAG(one(one(b)), T863, T855) → U79_AAG(T863, T855, add23_in_aag(T863, T863, T855))
TIMES1_IN_AAG(one(one(b)), T863, T855) → ADD23_IN_AAG(T863, T863, T855)
TIMES1_IN_AAG(one(zero(T875)), T876, T855) → U80_AAG(T875, T876, T855, p320_in_aaag(T875, T876, X1121, T855))
TIMES1_IN_AAG(one(zero(T875)), T876, T855) → P320_IN_AAAG(T875, T876, X1121, T855)
P320_IN_AAAG(T875, T876, X1121, T855) → U67_AAAG(T875, T876, X1121, T855, times22_in_aaa(T875, T876, X1121))
P320_IN_AAAG(T875, T876, X1121, T855) → TIMES22_IN_AAA(T875, T876, X1121)
P320_IN_AAAG(T875, T880, T879, T855) → U68_AAAG(T875, T880, T879, T855, timesc22_in_aaa(T875, T880, T879))
U68_AAAG(T875, T880, T879, T855, timesc22_out_aaa(T875, T880, T879)) → U69_AAAG(T875, T880, T879, T855, add23_in_aag(T880, zero(T879), T855))
U68_AAAG(T875, T880, T879, T855, timesc22_out_aaa(T875, T880, T879)) → ADD23_IN_AAG(T880, zero(T879), T855)
TIMES1_IN_AAG(one(one(T896)), T897, T855) → U81_AAG(T896, T897, T855, p324_in_aaaag(T896, T897, X1143, X1144, T855))
TIMES1_IN_AAG(one(one(T896)), T897, T855) → P324_IN_AAAAG(T896, T897, X1143, X1144, T855)
P324_IN_AAAAG(T896, T897, X1143, X1144, T855) → U70_AAAAG(T896, T897, X1143, X1144, T855, times22_in_aaa(T896, T897, X1143))
P324_IN_AAAAG(T896, T897, X1143, X1144, T855) → TIMES22_IN_AAA(T896, T897, X1143)
P324_IN_AAAAG(T896, T901, T900, X1144, T855) → U71_AAAAG(T896, T901, T900, X1144, T855, timesc22_in_aaa(T896, T901, T900))
U71_AAAAG(T896, T901, T900, X1144, T855, timesc22_out_aaa(T896, T901, T900)) → U72_AAAAG(T896, T901, T900, X1144, T855, add37_in_aaa(T901, T900, X1144))
U71_AAAAG(T896, T901, T900, X1144, T855, timesc22_out_aaa(T896, T901, T900)) → ADD37_IN_AAA(T901, T900, X1144)
P324_IN_AAAAG(T896, T912, T900, T911, T855) → U73_AAAAG(T896, T912, T900, T911, T855, timesc22_in_aaa(T896, T912, T900))
U73_AAAAG(T896, T912, T900, T911, T855, timesc22_out_aaa(T896, T912, T900)) → U74_AAAAG(T896, T912, T900, T911, T855, addc37_in_aaa(T912, T900, T911))
U74_AAAAG(T896, T912, T900, T911, T855, addc37_out_aaa(T912, T900, T911)) → U75_AAAAG(T896, T912, T900, T911, T855, add23_in_ggg(T912, T911, T855))
U74_AAAAG(T896, T912, T900, T911, T855, addc37_out_aaa(T912, T900, T911)) → ADD23_IN_GGG(T912, T911, T855)
ADD23_IN_GGG(b, T441, zero(T441)) → U61_GGG(T441, binaryZ43_in_g(T441))
ADD23_IN_GGG(b, T441, zero(T441)) → BINARYZ43_IN_G(T441)
ADD23_IN_GGG(zero(T477), T478, zero(T476)) → U62_GGG(T477, T478, T476, addz196_in_ggg(T477, T478, T476))
ADD23_IN_GGG(zero(T477), T478, zero(T476)) → ADDZ196_IN_GGG(T477, T478, T476)
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → U34_GGG(T497, T498, T496, addz196_in_ggg(T497, T498, T496))
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_GGG(T497, T498, T496)
ADDZ196_IN_GGG(zero(one(T524)), one(b), one(one(T524))) → U35_GGG(T524, binary54_in_g(T524))
ADDZ196_IN_GGG(zero(one(T524)), one(b), one(one(T524))) → BINARY54_IN_G(T524)
ADDZ196_IN_GGG(zero(zero(T529)), one(b), one(zero(T529))) → U36_GGG(T529, binaryZ48_in_g(T529))
ADDZ196_IN_GGG(zero(zero(T529)), one(b), one(zero(T529))) → BINARYZ48_IN_G(T529)
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → U37_GGG(T545, T546, T544, addz196_in_ggg(T545, T546, T544))
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_GGG(T545, T546, T544)
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → U38_GGG(T565, T566, T564, addy219_in_ggg(T565, T566, T564))
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → ADDY219_IN_GGG(T565, T566, T564)
ADDY219_IN_GGG(b, one(T572), one(T572)) → U55_GGG(T572, binary54_in_g(T572))
ADDY219_IN_GGG(b, one(T572), one(T572)) → BINARY54_IN_G(T572)
ADDY219_IN_GGG(b, zero(T577), zero(T577)) → U56_GGG(T577, binaryZ48_in_g(T577))
ADDY219_IN_GGG(b, zero(T577), zero(T577)) → BINARYZ48_IN_G(T577)
ADDY219_IN_GGG(T593, T594, T592) → U57_GGG(T593, T594, T592, addz196_in_ggg(T593, T594, T592))
ADDY219_IN_GGG(T593, T594, T592) → ADDZ196_IN_GGG(T593, T594, T592)
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → U39_GGG(T607, T608, T606, addc231_in_ggg(T607, T608, T606))
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → ADDC231_IN_GGG(T607, T608, T606)
ADDC231_IN_GGG(T619, b, T618) → U52_GGG(T619, T618, succZ241_in_gg(T619, T618))
ADDC231_IN_GGG(T619, b, T618) → SUCCZ241_IN_GG(T619, T618)
SUCCZ241_IN_GG(zero(T625), one(T625)) → U42_GG(T625, binaryZ48_in_g(T625))
SUCCZ241_IN_GG(zero(T625), one(T625)) → BINARYZ48_IN_G(T625)
SUCCZ241_IN_GG(one(T633), zero(T632)) → U43_GG(T633, T632, succ248_in_gg(T633, T632))
SUCCZ241_IN_GG(one(T633), zero(T632)) → SUCC248_IN_GG(T633, T632)
SUCC248_IN_GG(zero(T638), one(T638)) → U40_GG(T638, binaryZ48_in_g(T638))
SUCC248_IN_GG(zero(T638), one(T638)) → BINARYZ48_IN_G(T638)
SUCC248_IN_GG(one(T646), zero(T645)) → U41_GG(T646, T645, succ248_in_gg(T646, T645))
SUCC248_IN_GG(one(T646), zero(T645)) → SUCC248_IN_GG(T646, T645)
ADDC231_IN_GGG(b, T657, T656) → U53_GGG(T657, T656, succZ241_in_gg(T657, T656))
ADDC231_IN_GGG(b, T657, T656) → SUCCZ241_IN_GG(T657, T656)
ADDC231_IN_GGG(T673, T674, T672) → U54_GGG(T673, T674, T672, addC266_in_ggg(T673, T674, T672))
ADDC231_IN_GGG(T673, T674, T672) → ADDC266_IN_GGG(T673, T674, T672)
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → U44_GGG(T693, T694, T692, addz196_in_ggg(T693, T694, T692))
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_GGG(T693, T694, T692)
ADDC266_IN_GGG(zero(zero(T720)), one(b), zero(one(T720))) → U45_GGG(T720, binaryZ48_in_g(T720))
ADDC266_IN_GGG(zero(zero(T720)), one(b), zero(one(T720))) → BINARYZ48_IN_G(T720)
ADDC266_IN_GGG(zero(one(T732)), one(b), zero(zero(T731))) → U46_GGG(T732, T731, succ248_in_gg(T732, T731))
ADDC266_IN_GGG(zero(one(T732)), one(b), zero(zero(T731))) → SUCC248_IN_GG(T732, T731)
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → U47_GGG(T747, T748, T746, addC266_in_ggg(T747, T748, T746))
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_GGG(T747, T748, T746)
ADDC266_IN_GGG(one(b), zero(zero(T774)), zero(one(T774))) → U48_GGG(T774, binaryZ48_in_g(T774))
ADDC266_IN_GGG(one(b), zero(zero(T774)), zero(one(T774))) → BINARYZ48_IN_G(T774)
ADDC266_IN_GGG(one(b), zero(one(T786)), zero(zero(T785))) → U49_GGG(T786, T785, succ248_in_gg(T786, T785))
ADDC266_IN_GGG(one(b), zero(one(T786)), zero(zero(T785))) → SUCC248_IN_GG(T786, T785)
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → U50_GGG(T801, T802, T800, addC266_in_ggg(T801, T802, T800))
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_GGG(T801, T802, T800)
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → U51_GGG(T815, T816, T814, addc231_in_ggg(T815, T816, T814))
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → ADDC231_IN_GGG(T815, T816, T814)
ADD23_IN_GGG(one(T833), T834, one(T832)) → U63_GGG(T833, T834, T832, addy219_in_ggg(T833, T834, T832))
ADD23_IN_GGG(one(T833), T834, one(T832)) → ADDY219_IN_GGG(T833, T834, T832)
TIMES1_IN_AAG(zero(zero(T950)), T951, zero(zero(T949))) → U82_AAG(T950, T951, T949, times1_in_aag(T950, T951, T949))
TIMES1_IN_AAG(zero(one(T969)), T970, zero(T968)) → U83_AAG(T969, T970, T968, p20_in_aaag(T969, T970, X1210, T968))
TIMES1_IN_AAG(one(T982), T983, zero(T981)) → U84_AAG(T982, T983, T981, p20_in_aaag(T982, T983, X1226, zero(T981)))
TIMES1_IN_AAG(one(one(b)), T999, T991) → U85_AAG(T999, T991, add23_in_aag(T999, T999, T991))
TIMES1_IN_AAG(one(zero(T1011)), T1012, T991) → U86_AAG(T1011, T1012, T991, p320_in_aaag(T1011, T1012, X1269, T991))
TIMES1_IN_AAG(one(one(T1021)), T1022, T991) → U87_AAG(T1021, T1022, T991, p324_in_aaaag(T1021, T1022, X1287, X1288, T991))
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
TIMES1_IN_AAG(zero(zero(T34)), T35, zero(zero(T33))) → U76_AAG(T34, T35, T33, times1_in_aag(T34, T35, T33))
TIMES1_IN_AAG(zero(zero(T34)), T35, zero(zero(T33))) → TIMES1_IN_AAG(T34, T35, T33)
TIMES1_IN_AAG(zero(one(T53)), T54, zero(T52)) → U77_AAG(T53, T54, T52, p20_in_aaag(T53, T54, X56, T52))
TIMES1_IN_AAG(zero(one(T53)), T54, zero(T52)) → P20_IN_AAAG(T53, T54, X56, T52)
P20_IN_AAAG(T53, T54, X56, T52) → U58_AAAG(T53, T54, X56, T52, times22_in_aaa(T53, T54, X56))
P20_IN_AAAG(T53, T54, X56, T52) → TIMES22_IN_AAA(T53, T54, X56)
TIMES22_IN_AAA(zero(T76), T77, zero(X89)) → U1_AAA(T76, T77, X89, times22_in_aaa(T76, T77, X89))
TIMES22_IN_AAA(zero(T76), T77, zero(X89)) → TIMES22_IN_AAA(T76, T77, X89)
TIMES22_IN_AAA(one(T86), T87, X108) → U2_AAA(T86, T87, X108, times22_in_aaa(T86, T87, X107))
TIMES22_IN_AAA(one(T86), T87, X108) → TIMES22_IN_AAA(T86, T87, X107)
TIMES22_IN_AAA(one(T86), T91, X108) → U3_AAA(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U3_AAA(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U4_AAA(T86, T91, X108, add37_in_aaa(T91, T90, X108))
U3_AAA(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → ADD37_IN_AAA(T91, T90, X108)
ADD37_IN_AAA(b, T102, zero(T102)) → U64_AAA(T102, binaryZ43_in_a(T102))
ADD37_IN_AAA(b, T102, zero(T102)) → BINARYZ43_IN_A(T102)
BINARYZ43_IN_A(T113) → U33_A(T113, binaryZ48_in_a(T113))
BINARYZ43_IN_A(T113) → BINARYZ48_IN_A(T113)
BINARYZ48_IN_A(zero(T120)) → U5_A(T120, binaryZ48_in_a(T120))
BINARYZ48_IN_A(zero(T120)) → BINARYZ48_IN_A(T120)
BINARYZ48_IN_A(one(T125)) → U6_A(T125, binary54_in_a(T125))
BINARYZ48_IN_A(one(T125)) → BINARY54_IN_A(T125)
BINARY54_IN_A(zero(T131)) → U7_A(T131, binaryZ48_in_a(T131))
BINARY54_IN_A(zero(T131)) → BINARYZ48_IN_A(T131)
BINARY54_IN_A(one(T136)) → U8_A(T136, binary54_in_a(T136))
BINARY54_IN_A(one(T136)) → BINARY54_IN_A(T136)
ADD37_IN_AAA(zero(T161), T162, zero(X196)) → U65_AAA(T161, T162, X196, addz73_in_aaa(T161, T162, X196))
ADD37_IN_AAA(zero(T161), T162, zero(X196)) → ADDZ73_IN_AAA(T161, T162, X196)
ADDZ73_IN_AAA(zero(T175), zero(T176), zero(X223)) → U9_AAA(T175, T176, X223, addz73_in_aaa(T175, T176, X223))
ADDZ73_IN_AAA(zero(T175), zero(T176), zero(X223)) → ADDZ73_IN_AAA(T175, T176, X223)
ADDZ73_IN_AAA(zero(one(T197)), one(b), one(one(T197))) → U10_AAA(T197, binary54_in_a(T197))
ADDZ73_IN_AAA(zero(one(T197)), one(b), one(one(T197))) → BINARY54_IN_A(T197)
ADDZ73_IN_AAA(zero(zero(T203)), one(b), one(zero(T203))) → U11_AAA(T203, binaryZ48_in_a(T203))
ADDZ73_IN_AAA(zero(zero(T203)), one(b), one(zero(T203))) → BINARYZ48_IN_A(T203)
ADDZ73_IN_AAA(zero(T215), one(T216), one(X283)) → U12_AAA(T215, T216, X283, addz73_in_aaa(T215, T216, X283))
ADDZ73_IN_AAA(zero(T215), one(T216), one(X283)) → ADDZ73_IN_AAA(T215, T216, X283)
ADDZ73_IN_AAA(one(T229), zero(T230), one(X307)) → U13_AAA(T229, T230, X307, addy96_in_aaa(T229, T230, X307))
ADDZ73_IN_AAA(one(T229), zero(T230), one(X307)) → ADDY96_IN_AAA(T229, T230, X307)
ADDY96_IN_AAA(b, one(T237), one(T237)) → U30_AAA(T237, binary54_in_a(T237))
ADDY96_IN_AAA(b, one(T237), one(T237)) → BINARY54_IN_A(T237)
ADDY96_IN_AAA(b, zero(T243), zero(T243)) → U31_AAA(T243, binaryZ48_in_a(T243))
ADDY96_IN_AAA(b, zero(T243), zero(T243)) → BINARYZ48_IN_A(T243)
ADDY96_IN_AAA(T255, T256, X340) → U32_AAA(T255, T256, X340, addz73_in_aaa(T255, T256, X340))
ADDY96_IN_AAA(T255, T256, X340) → ADDZ73_IN_AAA(T255, T256, X340)
ADDZ73_IN_AAA(one(T265), one(T266), zero(X356)) → U14_AAA(T265, T266, X356, addc108_in_aaa(T265, T266, X356))
ADDZ73_IN_AAA(one(T265), one(T266), zero(X356)) → ADDC108_IN_AAA(T265, T266, X356)
ADDC108_IN_AAA(T272, b, X374) → U27_AAA(T272, X374, succZ118_in_aa(T272, X374))
ADDC108_IN_AAA(T272, b, X374) → SUCCZ118_IN_AA(T272, X374)
SUCCZ118_IN_AA(zero(T279), one(T279)) → U17_AA(T279, binaryZ48_in_a(T279))
SUCCZ118_IN_AA(zero(T279), one(T279)) → BINARYZ48_IN_A(T279)
SUCCZ118_IN_AA(one(T284), zero(X393)) → U18_AA(T284, X393, succ125_in_aa(T284, X393))
SUCCZ118_IN_AA(one(T284), zero(X393)) → SUCC125_IN_AA(T284, X393)
SUCC125_IN_AA(zero(T290), one(T290)) → U15_AA(T290, binaryZ48_in_a(T290))
SUCC125_IN_AA(zero(T290), one(T290)) → BINARYZ48_IN_A(T290)
SUCC125_IN_AA(one(T295), zero(X411)) → U16_AA(T295, X411, succ125_in_aa(T295, X411))
SUCC125_IN_AA(one(T295), zero(X411)) → SUCC125_IN_AA(T295, X411)
ADDC108_IN_AAA(b, T301, X428) → U28_AAA(T301, X428, succZ118_in_aa(T301, X428))
ADDC108_IN_AAA(b, T301, X428) → SUCCZ118_IN_AA(T301, X428)
ADDC108_IN_AAA(T313, T314, X447) → U29_AAA(T313, T314, X447, addC143_in_aaa(T313, T314, X447))
ADDC108_IN_AAA(T313, T314, X447) → ADDC143_IN_AAA(T313, T314, X447)
ADDC143_IN_AAA(zero(T327), zero(T328), one(X471)) → U19_AAA(T327, T328, X471, addz73_in_aaa(T327, T328, X471))
ADDC143_IN_AAA(zero(T327), zero(T328), one(X471)) → ADDZ73_IN_AAA(T327, T328, X471)
ADDC143_IN_AAA(zero(zero(T349)), one(b), zero(one(T349))) → U20_AAA(T349, binaryZ48_in_a(T349))
ADDC143_IN_AAA(zero(zero(T349)), one(b), zero(one(T349))) → BINARYZ48_IN_A(T349)
ADDC143_IN_AAA(zero(one(T356)), one(b), zero(zero(X524))) → U21_AAA(T356, X524, succ125_in_aa(T356, X524))
ADDC143_IN_AAA(zero(one(T356)), one(b), zero(zero(X524))) → SUCC125_IN_AA(T356, X524)
ADDC143_IN_AAA(zero(T367), one(T368), zero(X542)) → U22_AAA(T367, T368, X542, addC143_in_aaa(T367, T368, X542))
ADDC143_IN_AAA(zero(T367), one(T368), zero(X542)) → ADDC143_IN_AAA(T367, T368, X542)
ADDC143_IN_AAA(one(b), zero(zero(T389)), zero(one(T389))) → U23_AAA(T389, binaryZ48_in_a(T389))
ADDC143_IN_AAA(one(b), zero(zero(T389)), zero(one(T389))) → BINARYZ48_IN_A(T389)
ADDC143_IN_AAA(one(b), zero(one(T396)), zero(zero(X592))) → U24_AAA(T396, X592, succ125_in_aa(T396, X592))
ADDC143_IN_AAA(one(b), zero(one(T396)), zero(zero(X592))) → SUCC125_IN_AA(T396, X592)
ADDC143_IN_AAA(one(T407), zero(T408), zero(X610)) → U25_AAA(T407, T408, X610, addC143_in_aaa(T407, T408, X610))
ADDC143_IN_AAA(one(T407), zero(T408), zero(X610)) → ADDC143_IN_AAA(T407, T408, X610)
ADDC143_IN_AAA(one(T417), one(T418), one(X626)) → U26_AAA(T417, T418, X626, addc108_in_aaa(T417, T418, X626))
ADDC143_IN_AAA(one(T417), one(T418), one(X626)) → ADDC108_IN_AAA(T417, T418, X626)
ADD37_IN_AAA(one(T430), T431, one(X652)) → U66_AAA(T430, T431, X652, addy96_in_aaa(T430, T431, X652))
ADD37_IN_AAA(one(T430), T431, one(X652)) → ADDY96_IN_AAA(T430, T431, X652)
P20_IN_AAAG(T53, T58, T57, T52) → U59_AAAG(T53, T58, T57, T52, timesc22_in_aaa(T53, T58, T57))
U59_AAAG(T53, T58, T57, T52, timesc22_out_aaa(T53, T58, T57)) → U60_AAAG(T53, T58, T57, T52, add23_in_aag(T58, T57, T52))
U59_AAAG(T53, T58, T57, T52, timesc22_out_aaa(T53, T58, T57)) → ADD23_IN_AAG(T58, T57, T52)
ADD23_IN_AAG(b, T441, zero(T441)) → U61_AAG(T441, binaryZ43_in_g(T441))
ADD23_IN_AAG(b, T441, zero(T441)) → BINARYZ43_IN_G(T441)
BINARYZ43_IN_G(T113) → U33_G(T113, binaryZ48_in_g(T113))
BINARYZ43_IN_G(T113) → BINARYZ48_IN_G(T113)
BINARYZ48_IN_G(zero(T120)) → U5_G(T120, binaryZ48_in_g(T120))
BINARYZ48_IN_G(zero(T120)) → BINARYZ48_IN_G(T120)
BINARYZ48_IN_G(one(T125)) → U6_G(T125, binary54_in_g(T125))
BINARYZ48_IN_G(one(T125)) → BINARY54_IN_G(T125)
BINARY54_IN_G(zero(T131)) → U7_G(T131, binaryZ48_in_g(T131))
BINARY54_IN_G(zero(T131)) → BINARYZ48_IN_G(T131)
BINARY54_IN_G(one(T136)) → U8_G(T136, binary54_in_g(T136))
BINARY54_IN_G(one(T136)) → BINARY54_IN_G(T136)
ADD23_IN_AAG(zero(T477), T478, zero(T476)) → U62_AAG(T477, T478, T476, addz196_in_aag(T477, T478, T476))
ADD23_IN_AAG(zero(T477), T478, zero(T476)) → ADDZ196_IN_AAG(T477, T478, T476)
ADDZ196_IN_AAG(zero(T497), zero(T498), zero(T496)) → U34_AAG(T497, T498, T496, addz196_in_aag(T497, T498, T496))
ADDZ196_IN_AAG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_AAG(T497, T498, T496)
ADDZ196_IN_AAG(zero(one(T524)), one(b), one(one(T524))) → U35_AAG(T524, binary54_in_g(T524))
ADDZ196_IN_AAG(zero(one(T524)), one(b), one(one(T524))) → BINARY54_IN_G(T524)
ADDZ196_IN_AAG(zero(zero(T529)), one(b), one(zero(T529))) → U36_AAG(T529, binaryZ48_in_g(T529))
ADDZ196_IN_AAG(zero(zero(T529)), one(b), one(zero(T529))) → BINARYZ48_IN_G(T529)
ADDZ196_IN_AAG(zero(T545), one(T546), one(T544)) → U37_AAG(T545, T546, T544, addz196_in_aag(T545, T546, T544))
ADDZ196_IN_AAG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_AAG(T545, T546, T544)
ADDZ196_IN_AAG(one(T565), zero(T566), one(T564)) → U38_AAG(T565, T566, T564, addy219_in_aag(T565, T566, T564))
ADDZ196_IN_AAG(one(T565), zero(T566), one(T564)) → ADDY219_IN_AAG(T565, T566, T564)
ADDY219_IN_AAG(b, one(T572), one(T572)) → U55_AAG(T572, binary54_in_g(T572))
ADDY219_IN_AAG(b, one(T572), one(T572)) → BINARY54_IN_G(T572)
ADDY219_IN_AAG(b, zero(T577), zero(T577)) → U56_AAG(T577, binaryZ48_in_g(T577))
ADDY219_IN_AAG(b, zero(T577), zero(T577)) → BINARYZ48_IN_G(T577)
ADDY219_IN_AAG(T593, T594, T592) → U57_AAG(T593, T594, T592, addz196_in_aag(T593, T594, T592))
ADDY219_IN_AAG(T593, T594, T592) → ADDZ196_IN_AAG(T593, T594, T592)
ADDZ196_IN_AAG(one(T607), one(T608), zero(T606)) → U39_AAG(T607, T608, T606, addc231_in_aag(T607, T608, T606))
ADDZ196_IN_AAG(one(T607), one(T608), zero(T606)) → ADDC231_IN_AAG(T607, T608, T606)
ADDC231_IN_AAG(T619, b, T618) → U52_AAG(T619, T618, succZ241_in_ag(T619, T618))
ADDC231_IN_AAG(T619, b, T618) → SUCCZ241_IN_AG(T619, T618)
SUCCZ241_IN_AG(zero(T625), one(T625)) → U42_AG(T625, binaryZ48_in_g(T625))
SUCCZ241_IN_AG(zero(T625), one(T625)) → BINARYZ48_IN_G(T625)
SUCCZ241_IN_AG(one(T633), zero(T632)) → U43_AG(T633, T632, succ248_in_ag(T633, T632))
SUCCZ241_IN_AG(one(T633), zero(T632)) → SUCC248_IN_AG(T633, T632)
SUCC248_IN_AG(zero(T638), one(T638)) → U40_AG(T638, binaryZ48_in_g(T638))
SUCC248_IN_AG(zero(T638), one(T638)) → BINARYZ48_IN_G(T638)
SUCC248_IN_AG(one(T646), zero(T645)) → U41_AG(T646, T645, succ248_in_ag(T646, T645))
SUCC248_IN_AG(one(T646), zero(T645)) → SUCC248_IN_AG(T646, T645)
ADDC231_IN_AAG(b, T657, T656) → U53_AAG(T657, T656, succZ241_in_ag(T657, T656))
ADDC231_IN_AAG(b, T657, T656) → SUCCZ241_IN_AG(T657, T656)
ADDC231_IN_AAG(T673, T674, T672) → U54_AAG(T673, T674, T672, addC266_in_aag(T673, T674, T672))
ADDC231_IN_AAG(T673, T674, T672) → ADDC266_IN_AAG(T673, T674, T672)
ADDC266_IN_AAG(zero(T693), zero(T694), one(T692)) → U44_AAG(T693, T694, T692, addz196_in_aag(T693, T694, T692))
ADDC266_IN_AAG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_AAG(T693, T694, T692)
ADDC266_IN_AAG(zero(zero(T720)), one(b), zero(one(T720))) → U45_AAG(T720, binaryZ48_in_g(T720))
ADDC266_IN_AAG(zero(zero(T720)), one(b), zero(one(T720))) → BINARYZ48_IN_G(T720)
ADDC266_IN_AAG(zero(one(T732)), one(b), zero(zero(T731))) → U46_AAG(T732, T731, succ248_in_ag(T732, T731))
ADDC266_IN_AAG(zero(one(T732)), one(b), zero(zero(T731))) → SUCC248_IN_AG(T732, T731)
ADDC266_IN_AAG(zero(T747), one(T748), zero(T746)) → U47_AAG(T747, T748, T746, addC266_in_aag(T747, T748, T746))
ADDC266_IN_AAG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_AAG(T747, T748, T746)
ADDC266_IN_AAG(one(b), zero(zero(T774)), zero(one(T774))) → U48_AAG(T774, binaryZ48_in_g(T774))
ADDC266_IN_AAG(one(b), zero(zero(T774)), zero(one(T774))) → BINARYZ48_IN_G(T774)
ADDC266_IN_AAG(one(b), zero(one(T786)), zero(zero(T785))) → U49_AAG(T786, T785, succ248_in_ag(T786, T785))
ADDC266_IN_AAG(one(b), zero(one(T786)), zero(zero(T785))) → SUCC248_IN_AG(T786, T785)
ADDC266_IN_AAG(one(T801), zero(T802), zero(T800)) → U50_AAG(T801, T802, T800, addC266_in_aag(T801, T802, T800))
ADDC266_IN_AAG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_AAG(T801, T802, T800)
ADDC266_IN_AAG(one(T815), one(T816), one(T814)) → U51_AAG(T815, T816, T814, addc231_in_aag(T815, T816, T814))
ADDC266_IN_AAG(one(T815), one(T816), one(T814)) → ADDC231_IN_AAG(T815, T816, T814)
ADD23_IN_AAG(one(T833), T834, one(T832)) → U63_AAG(T833, T834, T832, addy219_in_aag(T833, T834, T832))
ADD23_IN_AAG(one(T833), T834, one(T832)) → ADDY219_IN_AAG(T833, T834, T832)
TIMES1_IN_AAG(one(T846), T847, zero(T845)) → U78_AAG(T846, T847, T845, p20_in_aaag(T846, T847, X1078, zero(T845)))
TIMES1_IN_AAG(one(T846), T847, zero(T845)) → P20_IN_AAAG(T846, T847, X1078, zero(T845))
TIMES1_IN_AAG(one(one(b)), T863, T855) → U79_AAG(T863, T855, add23_in_aag(T863, T863, T855))
TIMES1_IN_AAG(one(one(b)), T863, T855) → ADD23_IN_AAG(T863, T863, T855)
TIMES1_IN_AAG(one(zero(T875)), T876, T855) → U80_AAG(T875, T876, T855, p320_in_aaag(T875, T876, X1121, T855))
TIMES1_IN_AAG(one(zero(T875)), T876, T855) → P320_IN_AAAG(T875, T876, X1121, T855)
P320_IN_AAAG(T875, T876, X1121, T855) → U67_AAAG(T875, T876, X1121, T855, times22_in_aaa(T875, T876, X1121))
P320_IN_AAAG(T875, T876, X1121, T855) → TIMES22_IN_AAA(T875, T876, X1121)
P320_IN_AAAG(T875, T880, T879, T855) → U68_AAAG(T875, T880, T879, T855, timesc22_in_aaa(T875, T880, T879))
U68_AAAG(T875, T880, T879, T855, timesc22_out_aaa(T875, T880, T879)) → U69_AAAG(T875, T880, T879, T855, add23_in_aag(T880, zero(T879), T855))
U68_AAAG(T875, T880, T879, T855, timesc22_out_aaa(T875, T880, T879)) → ADD23_IN_AAG(T880, zero(T879), T855)
TIMES1_IN_AAG(one(one(T896)), T897, T855) → U81_AAG(T896, T897, T855, p324_in_aaaag(T896, T897, X1143, X1144, T855))
TIMES1_IN_AAG(one(one(T896)), T897, T855) → P324_IN_AAAAG(T896, T897, X1143, X1144, T855)
P324_IN_AAAAG(T896, T897, X1143, X1144, T855) → U70_AAAAG(T896, T897, X1143, X1144, T855, times22_in_aaa(T896, T897, X1143))
P324_IN_AAAAG(T896, T897, X1143, X1144, T855) → TIMES22_IN_AAA(T896, T897, X1143)
P324_IN_AAAAG(T896, T901, T900, X1144, T855) → U71_AAAAG(T896, T901, T900, X1144, T855, timesc22_in_aaa(T896, T901, T900))
U71_AAAAG(T896, T901, T900, X1144, T855, timesc22_out_aaa(T896, T901, T900)) → U72_AAAAG(T896, T901, T900, X1144, T855, add37_in_aaa(T901, T900, X1144))
U71_AAAAG(T896, T901, T900, X1144, T855, timesc22_out_aaa(T896, T901, T900)) → ADD37_IN_AAA(T901, T900, X1144)
P324_IN_AAAAG(T896, T912, T900, T911, T855) → U73_AAAAG(T896, T912, T900, T911, T855, timesc22_in_aaa(T896, T912, T900))
U73_AAAAG(T896, T912, T900, T911, T855, timesc22_out_aaa(T896, T912, T900)) → U74_AAAAG(T896, T912, T900, T911, T855, addc37_in_aaa(T912, T900, T911))
U74_AAAAG(T896, T912, T900, T911, T855, addc37_out_aaa(T912, T900, T911)) → U75_AAAAG(T896, T912, T900, T911, T855, add23_in_ggg(T912, T911, T855))
U74_AAAAG(T896, T912, T900, T911, T855, addc37_out_aaa(T912, T900, T911)) → ADD23_IN_GGG(T912, T911, T855)
ADD23_IN_GGG(b, T441, zero(T441)) → U61_GGG(T441, binaryZ43_in_g(T441))
ADD23_IN_GGG(b, T441, zero(T441)) → BINARYZ43_IN_G(T441)
ADD23_IN_GGG(zero(T477), T478, zero(T476)) → U62_GGG(T477, T478, T476, addz196_in_ggg(T477, T478, T476))
ADD23_IN_GGG(zero(T477), T478, zero(T476)) → ADDZ196_IN_GGG(T477, T478, T476)
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → U34_GGG(T497, T498, T496, addz196_in_ggg(T497, T498, T496))
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_GGG(T497, T498, T496)
ADDZ196_IN_GGG(zero(one(T524)), one(b), one(one(T524))) → U35_GGG(T524, binary54_in_g(T524))
ADDZ196_IN_GGG(zero(one(T524)), one(b), one(one(T524))) → BINARY54_IN_G(T524)
ADDZ196_IN_GGG(zero(zero(T529)), one(b), one(zero(T529))) → U36_GGG(T529, binaryZ48_in_g(T529))
ADDZ196_IN_GGG(zero(zero(T529)), one(b), one(zero(T529))) → BINARYZ48_IN_G(T529)
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → U37_GGG(T545, T546, T544, addz196_in_ggg(T545, T546, T544))
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_GGG(T545, T546, T544)
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → U38_GGG(T565, T566, T564, addy219_in_ggg(T565, T566, T564))
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → ADDY219_IN_GGG(T565, T566, T564)
ADDY219_IN_GGG(b, one(T572), one(T572)) → U55_GGG(T572, binary54_in_g(T572))
ADDY219_IN_GGG(b, one(T572), one(T572)) → BINARY54_IN_G(T572)
ADDY219_IN_GGG(b, zero(T577), zero(T577)) → U56_GGG(T577, binaryZ48_in_g(T577))
ADDY219_IN_GGG(b, zero(T577), zero(T577)) → BINARYZ48_IN_G(T577)
ADDY219_IN_GGG(T593, T594, T592) → U57_GGG(T593, T594, T592, addz196_in_ggg(T593, T594, T592))
ADDY219_IN_GGG(T593, T594, T592) → ADDZ196_IN_GGG(T593, T594, T592)
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → U39_GGG(T607, T608, T606, addc231_in_ggg(T607, T608, T606))
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → ADDC231_IN_GGG(T607, T608, T606)
ADDC231_IN_GGG(T619, b, T618) → U52_GGG(T619, T618, succZ241_in_gg(T619, T618))
ADDC231_IN_GGG(T619, b, T618) → SUCCZ241_IN_GG(T619, T618)
SUCCZ241_IN_GG(zero(T625), one(T625)) → U42_GG(T625, binaryZ48_in_g(T625))
SUCCZ241_IN_GG(zero(T625), one(T625)) → BINARYZ48_IN_G(T625)
SUCCZ241_IN_GG(one(T633), zero(T632)) → U43_GG(T633, T632, succ248_in_gg(T633, T632))
SUCCZ241_IN_GG(one(T633), zero(T632)) → SUCC248_IN_GG(T633, T632)
SUCC248_IN_GG(zero(T638), one(T638)) → U40_GG(T638, binaryZ48_in_g(T638))
SUCC248_IN_GG(zero(T638), one(T638)) → BINARYZ48_IN_G(T638)
SUCC248_IN_GG(one(T646), zero(T645)) → U41_GG(T646, T645, succ248_in_gg(T646, T645))
SUCC248_IN_GG(one(T646), zero(T645)) → SUCC248_IN_GG(T646, T645)
ADDC231_IN_GGG(b, T657, T656) → U53_GGG(T657, T656, succZ241_in_gg(T657, T656))
ADDC231_IN_GGG(b, T657, T656) → SUCCZ241_IN_GG(T657, T656)
ADDC231_IN_GGG(T673, T674, T672) → U54_GGG(T673, T674, T672, addC266_in_ggg(T673, T674, T672))
ADDC231_IN_GGG(T673, T674, T672) → ADDC266_IN_GGG(T673, T674, T672)
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → U44_GGG(T693, T694, T692, addz196_in_ggg(T693, T694, T692))
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_GGG(T693, T694, T692)
ADDC266_IN_GGG(zero(zero(T720)), one(b), zero(one(T720))) → U45_GGG(T720, binaryZ48_in_g(T720))
ADDC266_IN_GGG(zero(zero(T720)), one(b), zero(one(T720))) → BINARYZ48_IN_G(T720)
ADDC266_IN_GGG(zero(one(T732)), one(b), zero(zero(T731))) → U46_GGG(T732, T731, succ248_in_gg(T732, T731))
ADDC266_IN_GGG(zero(one(T732)), one(b), zero(zero(T731))) → SUCC248_IN_GG(T732, T731)
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → U47_GGG(T747, T748, T746, addC266_in_ggg(T747, T748, T746))
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_GGG(T747, T748, T746)
ADDC266_IN_GGG(one(b), zero(zero(T774)), zero(one(T774))) → U48_GGG(T774, binaryZ48_in_g(T774))
ADDC266_IN_GGG(one(b), zero(zero(T774)), zero(one(T774))) → BINARYZ48_IN_G(T774)
ADDC266_IN_GGG(one(b), zero(one(T786)), zero(zero(T785))) → U49_GGG(T786, T785, succ248_in_gg(T786, T785))
ADDC266_IN_GGG(one(b), zero(one(T786)), zero(zero(T785))) → SUCC248_IN_GG(T786, T785)
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → U50_GGG(T801, T802, T800, addC266_in_ggg(T801, T802, T800))
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_GGG(T801, T802, T800)
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → U51_GGG(T815, T816, T814, addc231_in_ggg(T815, T816, T814))
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → ADDC231_IN_GGG(T815, T816, T814)
ADD23_IN_GGG(one(T833), T834, one(T832)) → U63_GGG(T833, T834, T832, addy219_in_ggg(T833, T834, T832))
ADD23_IN_GGG(one(T833), T834, one(T832)) → ADDY219_IN_GGG(T833, T834, T832)
TIMES1_IN_AAG(zero(zero(T950)), T951, zero(zero(T949))) → U82_AAG(T950, T951, T949, times1_in_aag(T950, T951, T949))
TIMES1_IN_AAG(zero(one(T969)), T970, zero(T968)) → U83_AAG(T969, T970, T968, p20_in_aaag(T969, T970, X1210, T968))
TIMES1_IN_AAG(one(T982), T983, zero(T981)) → U84_AAG(T982, T983, T981, p20_in_aaag(T982, T983, X1226, zero(T981)))
TIMES1_IN_AAG(one(one(b)), T999, T991) → U85_AAG(T999, T991, add23_in_aag(T999, T999, T991))
TIMES1_IN_AAG(one(zero(T1011)), T1012, T991) → U86_AAG(T1011, T1012, T991, p320_in_aaag(T1011, T1012, X1269, T991))
TIMES1_IN_AAG(one(one(T1021)), T1022, T991) → U87_AAG(T1021, T1022, T991, p324_in_aaaag(T1021, T1022, X1287, X1288, T991))
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
BINARYZ48_IN_G(one(T125)) → BINARY54_IN_G(T125)
BINARY54_IN_G(zero(T131)) → BINARYZ48_IN_G(T131)
BINARYZ48_IN_G(zero(T120)) → BINARYZ48_IN_G(T120)
BINARY54_IN_G(one(T136)) → BINARY54_IN_G(T136)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
BINARYZ48_IN_G(one(T125)) → BINARY54_IN_G(T125)
BINARY54_IN_G(zero(T131)) → BINARYZ48_IN_G(T131)
BINARYZ48_IN_G(zero(T120)) → BINARYZ48_IN_G(T120)
BINARY54_IN_G(one(T136)) → BINARY54_IN_G(T136)
BINARYZ48_IN_G(one(T125)) → BINARY54_IN_G(T125)
BINARY54_IN_G(zero(T131)) → BINARYZ48_IN_G(T131)
BINARYZ48_IN_G(zero(T120)) → BINARYZ48_IN_G(T120)
BINARY54_IN_G(one(T136)) → BINARY54_IN_G(T136)
From the DPs we obtained the following set of size-change graphs:
SUCC248_IN_GG(one(T646), zero(T645)) → SUCC248_IN_GG(T646, T645)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
SUCC248_IN_GG(one(T646), zero(T645)) → SUCC248_IN_GG(T646, T645)
SUCC248_IN_GG(one(T646), zero(T645)) → SUCC248_IN_GG(T646, T645)
From the DPs we obtained the following set of size-change graphs:
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_GGG(T545, T546, T544)
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_GGG(T497, T498, T496)
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → ADDY219_IN_GGG(T565, T566, T564)
ADDY219_IN_GGG(T593, T594, T592) → ADDZ196_IN_GGG(T593, T594, T592)
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → ADDC231_IN_GGG(T607, T608, T606)
ADDC231_IN_GGG(T673, T674, T672) → ADDC266_IN_GGG(T673, T674, T672)
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_GGG(T693, T694, T692)
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_GGG(T747, T748, T746)
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_GGG(T801, T802, T800)
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → ADDC231_IN_GGG(T815, T816, T814)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_GGG(T545, T546, T544)
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_GGG(T497, T498, T496)
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → ADDY219_IN_GGG(T565, T566, T564)
ADDY219_IN_GGG(T593, T594, T592) → ADDZ196_IN_GGG(T593, T594, T592)
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → ADDC231_IN_GGG(T607, T608, T606)
ADDC231_IN_GGG(T673, T674, T672) → ADDC266_IN_GGG(T673, T674, T672)
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_GGG(T693, T694, T692)
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_GGG(T747, T748, T746)
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_GGG(T801, T802, T800)
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → ADDC231_IN_GGG(T815, T816, T814)
ADDZ196_IN_GGG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_GGG(T545, T546, T544)
ADDZ196_IN_GGG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_GGG(T497, T498, T496)
ADDZ196_IN_GGG(one(T565), zero(T566), one(T564)) → ADDY219_IN_GGG(T565, T566, T564)
ADDY219_IN_GGG(T593, T594, T592) → ADDZ196_IN_GGG(T593, T594, T592)
ADDZ196_IN_GGG(one(T607), one(T608), zero(T606)) → ADDC231_IN_GGG(T607, T608, T606)
ADDC231_IN_GGG(T673, T674, T672) → ADDC266_IN_GGG(T673, T674, T672)
ADDC266_IN_GGG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_GGG(T693, T694, T692)
ADDC266_IN_GGG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_GGG(T747, T748, T746)
ADDC266_IN_GGG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_GGG(T801, T802, T800)
ADDC266_IN_GGG(one(T815), one(T816), one(T814)) → ADDC231_IN_GGG(T815, T816, T814)
From the DPs we obtained the following set of size-change graphs:
SUCC248_IN_AG(one(T646), zero(T645)) → SUCC248_IN_AG(T646, T645)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
SUCC248_IN_AG(one(T646), zero(T645)) → SUCC248_IN_AG(T646, T645)
SUCC248_IN_AG(zero(T645)) → SUCC248_IN_AG(T645)
From the DPs we obtained the following set of size-change graphs:
ADDZ196_IN_AAG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_AAG(T545, T546, T544)
ADDZ196_IN_AAG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_AAG(T497, T498, T496)
ADDZ196_IN_AAG(one(T565), zero(T566), one(T564)) → ADDY219_IN_AAG(T565, T566, T564)
ADDY219_IN_AAG(T593, T594, T592) → ADDZ196_IN_AAG(T593, T594, T592)
ADDZ196_IN_AAG(one(T607), one(T608), zero(T606)) → ADDC231_IN_AAG(T607, T608, T606)
ADDC231_IN_AAG(T673, T674, T672) → ADDC266_IN_AAG(T673, T674, T672)
ADDC266_IN_AAG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_AAG(T693, T694, T692)
ADDC266_IN_AAG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_AAG(T747, T748, T746)
ADDC266_IN_AAG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_AAG(T801, T802, T800)
ADDC266_IN_AAG(one(T815), one(T816), one(T814)) → ADDC231_IN_AAG(T815, T816, T814)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
ADDZ196_IN_AAG(zero(T545), one(T546), one(T544)) → ADDZ196_IN_AAG(T545, T546, T544)
ADDZ196_IN_AAG(zero(T497), zero(T498), zero(T496)) → ADDZ196_IN_AAG(T497, T498, T496)
ADDZ196_IN_AAG(one(T565), zero(T566), one(T564)) → ADDY219_IN_AAG(T565, T566, T564)
ADDY219_IN_AAG(T593, T594, T592) → ADDZ196_IN_AAG(T593, T594, T592)
ADDZ196_IN_AAG(one(T607), one(T608), zero(T606)) → ADDC231_IN_AAG(T607, T608, T606)
ADDC231_IN_AAG(T673, T674, T672) → ADDC266_IN_AAG(T673, T674, T672)
ADDC266_IN_AAG(zero(T693), zero(T694), one(T692)) → ADDZ196_IN_AAG(T693, T694, T692)
ADDC266_IN_AAG(zero(T747), one(T748), zero(T746)) → ADDC266_IN_AAG(T747, T748, T746)
ADDC266_IN_AAG(one(T801), zero(T802), zero(T800)) → ADDC266_IN_AAG(T801, T802, T800)
ADDC266_IN_AAG(one(T815), one(T816), one(T814)) → ADDC231_IN_AAG(T815, T816, T814)
ADDZ196_IN_AAG(one(T544)) → ADDZ196_IN_AAG(T544)
ADDZ196_IN_AAG(zero(T496)) → ADDZ196_IN_AAG(T496)
ADDZ196_IN_AAG(one(T564)) → ADDY219_IN_AAG(T564)
ADDY219_IN_AAG(T592) → ADDZ196_IN_AAG(T592)
ADDZ196_IN_AAG(zero(T606)) → ADDC231_IN_AAG(T606)
ADDC231_IN_AAG(T672) → ADDC266_IN_AAG(T672)
ADDC266_IN_AAG(one(T692)) → ADDZ196_IN_AAG(T692)
ADDC266_IN_AAG(zero(T746)) → ADDC266_IN_AAG(T746)
ADDC266_IN_AAG(one(T814)) → ADDC231_IN_AAG(T814)
From the DPs we obtained the following set of size-change graphs:
BINARYZ48_IN_A(one(T125)) → BINARY54_IN_A(T125)
BINARY54_IN_A(zero(T131)) → BINARYZ48_IN_A(T131)
BINARYZ48_IN_A(zero(T120)) → BINARYZ48_IN_A(T120)
BINARY54_IN_A(one(T136)) → BINARY54_IN_A(T136)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
BINARYZ48_IN_A(one(T125)) → BINARY54_IN_A(T125)
BINARY54_IN_A(zero(T131)) → BINARYZ48_IN_A(T131)
BINARYZ48_IN_A(zero(T120)) → BINARYZ48_IN_A(T120)
BINARY54_IN_A(one(T136)) → BINARY54_IN_A(T136)
BINARYZ48_IN_A → BINARY54_IN_A
BINARY54_IN_A → BINARYZ48_IN_A
BINARYZ48_IN_A → BINARYZ48_IN_A
BINARY54_IN_A → BINARY54_IN_A
SUCC125_IN_AA(one(T295), zero(X411)) → SUCC125_IN_AA(T295, X411)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
SUCC125_IN_AA(one(T295), zero(X411)) → SUCC125_IN_AA(T295, X411)
SUCC125_IN_AA → SUCC125_IN_AA
ADDZ73_IN_AAA(zero(T215), one(T216), one(X283)) → ADDZ73_IN_AAA(T215, T216, X283)
ADDZ73_IN_AAA(zero(T175), zero(T176), zero(X223)) → ADDZ73_IN_AAA(T175, T176, X223)
ADDZ73_IN_AAA(one(T229), zero(T230), one(X307)) → ADDY96_IN_AAA(T229, T230, X307)
ADDY96_IN_AAA(T255, T256, X340) → ADDZ73_IN_AAA(T255, T256, X340)
ADDZ73_IN_AAA(one(T265), one(T266), zero(X356)) → ADDC108_IN_AAA(T265, T266, X356)
ADDC108_IN_AAA(T313, T314, X447) → ADDC143_IN_AAA(T313, T314, X447)
ADDC143_IN_AAA(zero(T327), zero(T328), one(X471)) → ADDZ73_IN_AAA(T327, T328, X471)
ADDC143_IN_AAA(zero(T367), one(T368), zero(X542)) → ADDC143_IN_AAA(T367, T368, X542)
ADDC143_IN_AAA(one(T407), zero(T408), zero(X610)) → ADDC143_IN_AAA(T407, T408, X610)
ADDC143_IN_AAA(one(T417), one(T418), one(X626)) → ADDC108_IN_AAA(T417, T418, X626)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
ADDZ73_IN_AAA(zero(T215), one(T216), one(X283)) → ADDZ73_IN_AAA(T215, T216, X283)
ADDZ73_IN_AAA(zero(T175), zero(T176), zero(X223)) → ADDZ73_IN_AAA(T175, T176, X223)
ADDZ73_IN_AAA(one(T229), zero(T230), one(X307)) → ADDY96_IN_AAA(T229, T230, X307)
ADDY96_IN_AAA(T255, T256, X340) → ADDZ73_IN_AAA(T255, T256, X340)
ADDZ73_IN_AAA(one(T265), one(T266), zero(X356)) → ADDC108_IN_AAA(T265, T266, X356)
ADDC108_IN_AAA(T313, T314, X447) → ADDC143_IN_AAA(T313, T314, X447)
ADDC143_IN_AAA(zero(T327), zero(T328), one(X471)) → ADDZ73_IN_AAA(T327, T328, X471)
ADDC143_IN_AAA(zero(T367), one(T368), zero(X542)) → ADDC143_IN_AAA(T367, T368, X542)
ADDC143_IN_AAA(one(T407), zero(T408), zero(X610)) → ADDC143_IN_AAA(T407, T408, X610)
ADDC143_IN_AAA(one(T417), one(T418), one(X626)) → ADDC108_IN_AAA(T417, T418, X626)
ADDZ73_IN_AAA → ADDZ73_IN_AAA
ADDZ73_IN_AAA → ADDY96_IN_AAA
ADDY96_IN_AAA → ADDZ73_IN_AAA
ADDZ73_IN_AAA → ADDC108_IN_AAA
ADDC108_IN_AAA → ADDC143_IN_AAA
ADDC143_IN_AAA → ADDZ73_IN_AAA
ADDC143_IN_AAA → ADDC143_IN_AAA
ADDC143_IN_AAA → ADDC108_IN_AAA
TIMES22_IN_AAA(one(T86), T87, X108) → TIMES22_IN_AAA(T86, T87, X107)
TIMES22_IN_AAA(zero(T76), T77, zero(X89)) → TIMES22_IN_AAA(T76, T77, X89)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
TIMES22_IN_AAA(one(T86), T87, X108) → TIMES22_IN_AAA(T86, T87, X107)
TIMES22_IN_AAA(zero(T76), T77, zero(X89)) → TIMES22_IN_AAA(T76, T77, X89)
TIMES22_IN_AAA → TIMES22_IN_AAA
TIMES1_IN_AAG(zero(zero(T34)), T35, zero(zero(T33))) → TIMES1_IN_AAG(T34, T35, T33)
timesc22_in_aaa(one(b), T65, T65) → timesc22_out_aaa(one(b), T65, T65)
timesc22_in_aaa(zero(T76), T77, zero(X89)) → U101_aaa(T76, T77, X89, timesc22_in_aaa(T76, T77, X89))
timesc22_in_aaa(one(T86), T91, X108) → U102_aaa(T86, T91, X108, timesc22_in_aaa(T86, T91, T90))
U102_aaa(T86, T91, X108, timesc22_out_aaa(T86, T91, T90)) → U103_aaa(T86, T91, X108, addc37_in_aaa(T91, T90, X108))
addc37_in_aaa(b, T102, zero(T102)) → U162_aaa(T102, binaryZc43_in_a(T102))
binaryZc43_in_a(T113) → U132_a(T113, binaryZc48_in_a(T113))
binaryZc48_in_a(zero(T120)) → U104_a(T120, binaryZc48_in_a(T120))
binaryZc48_in_a(one(T125)) → U105_a(T125, binaryc54_in_a(T125))
binaryc54_in_a(b) → binaryc54_out_a(b)
binaryc54_in_a(zero(T131)) → U106_a(T131, binaryZc48_in_a(T131))
U106_a(T131, binaryZc48_out_a(T131)) → binaryc54_out_a(zero(T131))
binaryc54_in_a(one(T136)) → U107_a(T136, binaryc54_in_a(T136))
U107_a(T136, binaryc54_out_a(T136)) → binaryc54_out_a(one(T136))
U105_a(T125, binaryc54_out_a(T125)) → binaryZc48_out_a(one(T125))
U104_a(T120, binaryZc48_out_a(T120)) → binaryZc48_out_a(zero(T120))
U132_a(T113, binaryZc48_out_a(T113)) → binaryZc43_out_a(T113)
U162_aaa(T102, binaryZc43_out_a(T102)) → addc37_out_aaa(b, T102, zero(T102))
addc37_in_aaa(zero(T161), T162, zero(X196)) → U163_aaa(T161, T162, X196, addzc73_in_aaa(T161, T162, X196))
addzc73_in_aaa(zero(T175), zero(T176), zero(X223)) → U108_aaa(T175, T176, X223, addzc73_in_aaa(T175, T176, X223))
addzc73_in_aaa(zero(one(T197)), one(b), one(one(T197))) → U109_aaa(T197, binaryc54_in_a(T197))
U109_aaa(T197, binaryc54_out_a(T197)) → addzc73_out_aaa(zero(one(T197)), one(b), one(one(T197)))
addzc73_in_aaa(zero(zero(T203)), one(b), one(zero(T203))) → U110_aaa(T203, binaryZc48_in_a(T203))
U110_aaa(T203, binaryZc48_out_a(T203)) → addzc73_out_aaa(zero(zero(T203)), one(b), one(zero(T203)))
addzc73_in_aaa(zero(T215), one(T216), one(X283)) → U111_aaa(T215, T216, X283, addzc73_in_aaa(T215, T216, X283))
addzc73_in_aaa(one(T229), zero(T230), one(X307)) → U112_aaa(T229, T230, X307, addyc96_in_aaa(T229, T230, X307))
addyc96_in_aaa(b, one(T237), one(T237)) → U129_aaa(T237, binaryc54_in_a(T237))
U129_aaa(T237, binaryc54_out_a(T237)) → addyc96_out_aaa(b, one(T237), one(T237))
addyc96_in_aaa(b, zero(T243), zero(T243)) → U130_aaa(T243, binaryZc48_in_a(T243))
U130_aaa(T243, binaryZc48_out_a(T243)) → addyc96_out_aaa(b, zero(T243), zero(T243))
addyc96_in_aaa(T255, T256, X340) → U131_aaa(T255, T256, X340, addzc73_in_aaa(T255, T256, X340))
addzc73_in_aaa(one(T265), one(T266), zero(X356)) → U113_aaa(T265, T266, X356, addcc108_in_aaa(T265, T266, X356))
addcc108_in_aaa(b, b, one(b)) → addcc108_out_aaa(b, b, one(b))
addcc108_in_aaa(T272, b, X374) → U126_aaa(T272, X374, succZc118_in_aa(T272, X374))
succZc118_in_aa(zero(T279), one(T279)) → U116_aa(T279, binaryZc48_in_a(T279))
U116_aa(T279, binaryZc48_out_a(T279)) → succZc118_out_aa(zero(T279), one(T279))
succZc118_in_aa(one(T284), zero(X393)) → U117_aa(T284, X393, succc125_in_aa(T284, X393))
succc125_in_aa(b, one(b)) → succc125_out_aa(b, one(b))
succc125_in_aa(zero(T290), one(T290)) → U114_aa(T290, binaryZc48_in_a(T290))
U114_aa(T290, binaryZc48_out_a(T290)) → succc125_out_aa(zero(T290), one(T290))
succc125_in_aa(one(T295), zero(X411)) → U115_aa(T295, X411, succc125_in_aa(T295, X411))
U115_aa(T295, X411, succc125_out_aa(T295, X411)) → succc125_out_aa(one(T295), zero(X411))
U117_aa(T284, X393, succc125_out_aa(T284, X393)) → succZc118_out_aa(one(T284), zero(X393))
U126_aaa(T272, X374, succZc118_out_aa(T272, X374)) → addcc108_out_aaa(T272, b, X374)
addcc108_in_aaa(b, T301, X428) → U127_aaa(T301, X428, succZc118_in_aa(T301, X428))
U127_aaa(T301, X428, succZc118_out_aa(T301, X428)) → addcc108_out_aaa(b, T301, X428)
addcc108_in_aaa(T313, T314, X447) → U128_aaa(T313, T314, X447, addCc143_in_aaa(T313, T314, X447))
addCc143_in_aaa(zero(T327), zero(T328), one(X471)) → U118_aaa(T327, T328, X471, addzc73_in_aaa(T327, T328, X471))
U118_aaa(T327, T328, X471, addzc73_out_aaa(T327, T328, X471)) → addCc143_out_aaa(zero(T327), zero(T328), one(X471))
addCc143_in_aaa(zero(zero(T349)), one(b), zero(one(T349))) → U119_aaa(T349, binaryZc48_in_a(T349))
U119_aaa(T349, binaryZc48_out_a(T349)) → addCc143_out_aaa(zero(zero(T349)), one(b), zero(one(T349)))
addCc143_in_aaa(zero(one(T356)), one(b), zero(zero(X524))) → U120_aaa(T356, X524, succc125_in_aa(T356, X524))
U120_aaa(T356, X524, succc125_out_aa(T356, X524)) → addCc143_out_aaa(zero(one(T356)), one(b), zero(zero(X524)))
addCc143_in_aaa(zero(T367), one(T368), zero(X542)) → U121_aaa(T367, T368, X542, addCc143_in_aaa(T367, T368, X542))
addCc143_in_aaa(one(b), zero(zero(T389)), zero(one(T389))) → U122_aaa(T389, binaryZc48_in_a(T389))
U122_aaa(T389, binaryZc48_out_a(T389)) → addCc143_out_aaa(one(b), zero(zero(T389)), zero(one(T389)))
addCc143_in_aaa(one(b), zero(one(T396)), zero(zero(X592))) → U123_aaa(T396, X592, succc125_in_aa(T396, X592))
U123_aaa(T396, X592, succc125_out_aa(T396, X592)) → addCc143_out_aaa(one(b), zero(one(T396)), zero(zero(X592)))
addCc143_in_aaa(one(T407), zero(T408), zero(X610)) → U124_aaa(T407, T408, X610, addCc143_in_aaa(T407, T408, X610))
addCc143_in_aaa(one(T417), one(T418), one(X626)) → U125_aaa(T417, T418, X626, addcc108_in_aaa(T417, T418, X626))
U125_aaa(T417, T418, X626, addcc108_out_aaa(T417, T418, X626)) → addCc143_out_aaa(one(T417), one(T418), one(X626))
U124_aaa(T407, T408, X610, addCc143_out_aaa(T407, T408, X610)) → addCc143_out_aaa(one(T407), zero(T408), zero(X610))
U121_aaa(T367, T368, X542, addCc143_out_aaa(T367, T368, X542)) → addCc143_out_aaa(zero(T367), one(T368), zero(X542))
U128_aaa(T313, T314, X447, addCc143_out_aaa(T313, T314, X447)) → addcc108_out_aaa(T313, T314, X447)
U113_aaa(T265, T266, X356, addcc108_out_aaa(T265, T266, X356)) → addzc73_out_aaa(one(T265), one(T266), zero(X356))
U131_aaa(T255, T256, X340, addzc73_out_aaa(T255, T256, X340)) → addyc96_out_aaa(T255, T256, X340)
U112_aaa(T229, T230, X307, addyc96_out_aaa(T229, T230, X307)) → addzc73_out_aaa(one(T229), zero(T230), one(X307))
U111_aaa(T215, T216, X283, addzc73_out_aaa(T215, T216, X283)) → addzc73_out_aaa(zero(T215), one(T216), one(X283))
U108_aaa(T175, T176, X223, addzc73_out_aaa(T175, T176, X223)) → addzc73_out_aaa(zero(T175), zero(T176), zero(X223))
U163_aaa(T161, T162, X196, addzc73_out_aaa(T161, T162, X196)) → addc37_out_aaa(zero(T161), T162, zero(X196))
addc37_in_aaa(one(T430), T431, one(X652)) → U164_aaa(T430, T431, X652, addyc96_in_aaa(T430, T431, X652))
U164_aaa(T430, T431, X652, addyc96_out_aaa(T430, T431, X652)) → addc37_out_aaa(one(T430), T431, one(X652))
U103_aaa(T86, T91, X108, addc37_out_aaa(T91, T90, X108)) → timesc22_out_aaa(one(T86), T91, X108)
U101_aaa(T76, T77, X89, timesc22_out_aaa(T76, T77, X89)) → timesc22_out_aaa(zero(T76), T77, zero(X89))
TIMES1_IN_AAG(zero(zero(T34)), T35, zero(zero(T33))) → TIMES1_IN_AAG(T34, T35, T33)
TIMES1_IN_AAG(zero(zero(T33))) → TIMES1_IN_AAG(T33)
From the DPs we obtained the following set of size-change graphs: