0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇔)
↳13 QDP
↳14 QDPSizeChangeProof (⇔)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔)
↳18 PiDP
↳19 PiDPToQDPProof (⇐)
↳20 QDP
↳21 QDPSizeChangeProof (⇔)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔)
↳25 PiDP
↳26 PiDPToQDPProof (⇐)
↳27 QDP
↳28 MRRProof (⇔)
↳29 QDP
↳30 QReductionProof (⇔)
↳31 QDP
↳32 MRRProof (⇔)
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 TRUE
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
LOG21_IN_GA(s(s(T12)), T14) → U8_GA(T12, T14, half17_in_ga(T12, X28))
LOG21_IN_GA(s(s(T12)), T14) → HALF17_IN_GA(T12, X28)
HALF17_IN_GA(T20, s(X46)) → U2_GA(T20, X46, half22_in_ga(T20, X46))
HALF17_IN_GA(T20, s(X46)) → HALF22_IN_GA(T20, X46)
HALF22_IN_GA(s(s(T23)), s(X55)) → U1_GA(T23, X55, half22_in_ga(T23, X55))
HALF22_IN_GA(s(s(T23)), s(X55)) → HALF22_IN_GA(T23, X55)
LOG21_IN_GA(s(s(T12)), s(0)) → U9_GA(T12, half17_in_gg(T12, 0))
LOG21_IN_GA(s(s(T12)), s(0)) → HALF17_IN_GG(T12, 0)
HALF17_IN_GG(T20, s(X46)) → U2_GG(T20, X46, half22_in_gg(T20, X46))
HALF17_IN_GG(T20, s(X46)) → HALF22_IN_GG(T20, X46)
HALF22_IN_GG(s(s(T23)), s(X55)) → U1_GG(T23, X55, half22_in_gg(T23, X55))
HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)
LOG21_IN_GA(s(s(T12)), s(0)) → U10_GA(T12, half17_in_gg(T12, s(0)))
LOG21_IN_GA(s(s(T12)), s(0)) → HALF17_IN_GG(T12, s(0))
LOG21_IN_GA(s(s(T12)), T30) → U11_GA(T12, T30, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), T30) → HALF17_IN_GA(T12, s(s(T28)))
U11_GA(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_GA(T12, T30, half17_in_ga(T28, X82))
U11_GA(T12, T30, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, X82)
LOG21_IN_GA(s(s(T12)), s(s(0))) → U13_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(0))) → HALF17_IN_GA(T12, s(s(T28)))
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → U14_GA(T12, half17_in_gg(T28, 0))
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GG(T28, 0)
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → U15_GA(T12, half17_in_gg(T28, s(0)))
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GG(T28, s(0))
LOG21_IN_GA(s(s(T12)), T40) → U16_GA(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_GA(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_GA(T12, T40, half17_in_ga(T28, s(s(T38))))
U16_GA(T12, T40, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U17_GA(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_GA(T12, T40, half17_in_ga(T38, X116))
U17_GA(T12, T40, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, X116)
LOG21_IN_GA(s(s(T12)), s(s(s(0)))) → U19_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(0)))) → HALF17_IN_GA(T12, s(s(T28)))
U19_GA(T12, half17_out_ga(T12, s(s(T28)))) → U20_GA(T12, half17_in_ga(T28, s(s(T38))))
U19_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → U21_GA(T12, half17_in_gg(T38, 0))
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GG(T38, 0)
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → U22_GA(T12, half17_in_gg(T38, s(0)))
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GG(T38, s(0))
LOG21_IN_GA(s(s(T12)), T50) → U23_GA(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_GA(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_GA(T12, T50, half17_in_ga(T28, s(s(T38))))
U23_GA(T12, T50, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U24_GA(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_GA(T12, T50, half17_in_ga(T38, s(s(T48))))
U24_GA(T12, T50, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U25_GA(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_GA(T12, T50, half17_in_ga(T48, X150))
U25_GA(T12, T50, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, X150)
LOG21_IN_GA(s(s(T12)), s(s(s(s(0))))) → U27_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(0))))) → HALF17_IN_GA(T12, s(s(T28)))
U27_GA(T12, half17_out_ga(T12, s(s(T28)))) → U28_GA(T12, half17_in_ga(T28, s(s(T38))))
U27_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U28_GA(T12, half17_out_ga(T28, s(s(T38)))) → U29_GA(T12, half17_in_ga(T38, s(s(T48))))
U28_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → U30_GA(T12, half17_in_gg(T48, 0))
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GG(T48, 0)
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → U31_GA(T12, half17_in_gg(T48, s(0)))
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GG(T48, s(0))
LOG21_IN_GA(s(s(T12)), T60) → U32_GA(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_GA(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_GA(T12, T60, half17_in_ga(T28, s(s(T38))))
U32_GA(T12, T60, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U33_GA(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_GA(T12, T60, half17_in_ga(T38, s(s(T48))))
U33_GA(T12, T60, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U34_GA(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_GA(T12, T60, half17_in_ga(T48, s(s(T58))))
U34_GA(T12, T60, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U35_GA(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_GA(T12, T60, half17_in_ga(T58, X184))
U35_GA(T12, T60, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, X184)
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → U37_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → HALF17_IN_GA(T12, s(s(T28)))
U37_GA(T12, half17_out_ga(T12, s(s(T28)))) → U38_GA(T12, half17_in_ga(T28, s(s(T38))))
U37_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U38_GA(T12, half17_out_ga(T28, s(s(T38)))) → U39_GA(T12, half17_in_ga(T38, s(s(T48))))
U38_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U39_GA(T12, half17_out_ga(T38, s(s(T48)))) → U40_GA(T12, half17_in_ga(T48, s(s(T58))))
U39_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → U41_GA(T12, half17_in_gg(T58, 0))
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GG(T58, 0)
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → U42_GA(T12, half17_in_gg(T58, s(0)))
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GG(T58, s(0))
LOG21_IN_GA(s(s(T12)), T70) → U43_GA(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_GA(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_GA(T12, T70, half17_in_ga(T28, s(s(T38))))
U43_GA(T12, T70, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U44_GA(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_GA(T12, T70, half17_in_ga(T38, s(s(T48))))
U44_GA(T12, T70, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U45_GA(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_GA(T12, T70, half17_in_ga(T48, s(s(T58))))
U45_GA(T12, T70, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U46_GA(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_GA(T12, T70, half17_in_ga(T58, s(s(T68))))
U46_GA(T12, T70, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U47_GA(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_GA(T12, T70, half17_in_ga(T68, X218))
U47_GA(T12, T70, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, X218)
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → HALF17_IN_GA(T12, s(s(T28)))
U49_GA(T12, half17_out_ga(T12, s(s(T28)))) → U50_GA(T12, half17_in_ga(T28, s(s(T38))))
U49_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U50_GA(T12, half17_out_ga(T28, s(s(T38)))) → U51_GA(T12, half17_in_ga(T38, s(s(T48))))
U50_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U51_GA(T12, half17_out_ga(T38, s(s(T48)))) → U52_GA(T12, half17_in_ga(T48, s(s(T58))))
U51_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U52_GA(T12, half17_out_ga(T48, s(s(T58)))) → U53_GA(T12, half17_in_ga(T58, s(s(T68))))
U52_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → U54_GA(T12, half17_in_gg(T68, 0))
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GG(T68, 0)
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → U55_GA(T12, half17_in_gg(T68, s(0)))
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GG(T68, s(0))
LOG21_IN_GA(s(s(T12)), T80) → U56_GA(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_GA(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_GA(T12, T80, half17_in_ga(T28, s(s(T38))))
U56_GA(T12, T80, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U57_GA(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_GA(T12, T80, half17_in_ga(T38, s(s(T48))))
U57_GA(T12, T80, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U58_GA(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_GA(T12, T80, half17_in_ga(T48, s(s(T58))))
U58_GA(T12, T80, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U59_GA(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_GA(T12, T80, half17_in_ga(T58, s(s(T68))))
U59_GA(T12, T80, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U60_GA(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_GA(T12, T80, half17_in_ga(T68, s(s(T78))))
U60_GA(T12, T80, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, s(s(T78)))
U61_GA(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_GA(T12, T80, half17_in_ga(T78, X252))
U61_GA(T12, T80, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GA(T78, X252)
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → HALF17_IN_GA(T12, s(s(T28)))
U63_GA(T12, half17_out_ga(T12, s(s(T28)))) → U64_GA(T12, half17_in_ga(T28, s(s(T38))))
U63_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U64_GA(T12, half17_out_ga(T28, s(s(T38)))) → U65_GA(T12, half17_in_ga(T38, s(s(T48))))
U64_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U65_GA(T12, half17_out_ga(T38, s(s(T48)))) → U66_GA(T12, half17_in_ga(T48, s(s(T58))))
U65_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U66_GA(T12, half17_out_ga(T48, s(s(T58)))) → U67_GA(T12, half17_in_ga(T58, s(s(T68))))
U66_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U67_GA(T12, half17_out_ga(T58, s(s(T68)))) → U68_GA(T12, half17_in_ga(T68, s(s(T78))))
U67_GA(T12, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, s(s(T78)))
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → U69_GA(T12, half17_in_gg(T78, 0))
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GG(T78, 0)
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → U70_GA(T12, half17_in_gg(T78, s(0)))
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GG(T78, s(0))
LOG21_IN_GA(s(s(T12)), T90) → U71_GA(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_GA(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_GA(T12, T90, half17_in_ga(T28, s(s(T38))))
U71_GA(T12, T90, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U72_GA(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_GA(T12, T90, half17_in_ga(T38, s(s(T48))))
U72_GA(T12, T90, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U73_GA(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_GA(T12, T90, half17_in_ga(T48, s(s(T58))))
U73_GA(T12, T90, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U74_GA(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_GA(T12, T90, half17_in_ga(T58, s(s(T68))))
U74_GA(T12, T90, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U75_GA(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_GA(T12, T90, half17_in_ga(T68, s(s(T78))))
U75_GA(T12, T90, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, s(s(T78)))
U76_GA(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_GA(T12, T90, half17_in_ga(T78, s(s(T88))))
U76_GA(T12, T90, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GA(T78, s(s(T88)))
U77_GA(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_GA(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
U77_GA(T12, T90, half17_out_ga(T78, s(s(T88)))) → P139_IN_GAGA(T88, X286, s(s(s(s(s(s(s(0))))))), T90)
P139_IN_GAGA(T88, X286, T92, T90) → U3_GAGA(T88, X286, T92, T90, half17_in_ga(T88, X286))
P139_IN_GAGA(T88, X286, T92, T90) → HALF17_IN_GA(T88, X286)
P139_IN_GAGA(T88, 0, T102, s(T102)) → U4_GAGA(T88, T102, half17_in_gg(T88, 0))
P139_IN_GAGA(T88, 0, T102, s(T102)) → HALF17_IN_GG(T88, 0)
P139_IN_GAGA(T88, s(0), T107, s(T107)) → U5_GAGA(T88, T107, half17_in_gg(T88, s(0)))
P139_IN_GAGA(T88, s(0), T107, s(T107)) → HALF17_IN_GG(T88, s(0))
P139_IN_GAGA(T88, s(s(T114)), T115, T117) → U6_GAGA(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
P139_IN_GAGA(T88, s(s(T114)), T115, T117) → HALF17_IN_GA(T88, s(s(T114)))
U6_GAGA(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_GAGA(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U6_GAGA(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → P139_IN_GAGA(T114, X323, s(T115), T117)
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
LOG21_IN_GA(s(s(T12)), T14) → U8_GA(T12, T14, half17_in_ga(T12, X28))
LOG21_IN_GA(s(s(T12)), T14) → HALF17_IN_GA(T12, X28)
HALF17_IN_GA(T20, s(X46)) → U2_GA(T20, X46, half22_in_ga(T20, X46))
HALF17_IN_GA(T20, s(X46)) → HALF22_IN_GA(T20, X46)
HALF22_IN_GA(s(s(T23)), s(X55)) → U1_GA(T23, X55, half22_in_ga(T23, X55))
HALF22_IN_GA(s(s(T23)), s(X55)) → HALF22_IN_GA(T23, X55)
LOG21_IN_GA(s(s(T12)), s(0)) → U9_GA(T12, half17_in_gg(T12, 0))
LOG21_IN_GA(s(s(T12)), s(0)) → HALF17_IN_GG(T12, 0)
HALF17_IN_GG(T20, s(X46)) → U2_GG(T20, X46, half22_in_gg(T20, X46))
HALF17_IN_GG(T20, s(X46)) → HALF22_IN_GG(T20, X46)
HALF22_IN_GG(s(s(T23)), s(X55)) → U1_GG(T23, X55, half22_in_gg(T23, X55))
HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)
LOG21_IN_GA(s(s(T12)), s(0)) → U10_GA(T12, half17_in_gg(T12, s(0)))
LOG21_IN_GA(s(s(T12)), s(0)) → HALF17_IN_GG(T12, s(0))
LOG21_IN_GA(s(s(T12)), T30) → U11_GA(T12, T30, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), T30) → HALF17_IN_GA(T12, s(s(T28)))
U11_GA(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_GA(T12, T30, half17_in_ga(T28, X82))
U11_GA(T12, T30, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, X82)
LOG21_IN_GA(s(s(T12)), s(s(0))) → U13_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(0))) → HALF17_IN_GA(T12, s(s(T28)))
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → U14_GA(T12, half17_in_gg(T28, 0))
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GG(T28, 0)
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → U15_GA(T12, half17_in_gg(T28, s(0)))
U13_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GG(T28, s(0))
LOG21_IN_GA(s(s(T12)), T40) → U16_GA(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_GA(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_GA(T12, T40, half17_in_ga(T28, s(s(T38))))
U16_GA(T12, T40, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U17_GA(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_GA(T12, T40, half17_in_ga(T38, X116))
U17_GA(T12, T40, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, X116)
LOG21_IN_GA(s(s(T12)), s(s(s(0)))) → U19_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(0)))) → HALF17_IN_GA(T12, s(s(T28)))
U19_GA(T12, half17_out_ga(T12, s(s(T28)))) → U20_GA(T12, half17_in_ga(T28, s(s(T38))))
U19_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → U21_GA(T12, half17_in_gg(T38, 0))
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GG(T38, 0)
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → U22_GA(T12, half17_in_gg(T38, s(0)))
U20_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GG(T38, s(0))
LOG21_IN_GA(s(s(T12)), T50) → U23_GA(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_GA(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_GA(T12, T50, half17_in_ga(T28, s(s(T38))))
U23_GA(T12, T50, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U24_GA(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_GA(T12, T50, half17_in_ga(T38, s(s(T48))))
U24_GA(T12, T50, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U25_GA(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_GA(T12, T50, half17_in_ga(T48, X150))
U25_GA(T12, T50, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, X150)
LOG21_IN_GA(s(s(T12)), s(s(s(s(0))))) → U27_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(0))))) → HALF17_IN_GA(T12, s(s(T28)))
U27_GA(T12, half17_out_ga(T12, s(s(T28)))) → U28_GA(T12, half17_in_ga(T28, s(s(T38))))
U27_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U28_GA(T12, half17_out_ga(T28, s(s(T38)))) → U29_GA(T12, half17_in_ga(T38, s(s(T48))))
U28_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → U30_GA(T12, half17_in_gg(T48, 0))
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GG(T48, 0)
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → U31_GA(T12, half17_in_gg(T48, s(0)))
U29_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GG(T48, s(0))
LOG21_IN_GA(s(s(T12)), T60) → U32_GA(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_GA(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_GA(T12, T60, half17_in_ga(T28, s(s(T38))))
U32_GA(T12, T60, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U33_GA(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_GA(T12, T60, half17_in_ga(T38, s(s(T48))))
U33_GA(T12, T60, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U34_GA(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_GA(T12, T60, half17_in_ga(T48, s(s(T58))))
U34_GA(T12, T60, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U35_GA(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_GA(T12, T60, half17_in_ga(T58, X184))
U35_GA(T12, T60, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, X184)
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → U37_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(0)))))) → HALF17_IN_GA(T12, s(s(T28)))
U37_GA(T12, half17_out_ga(T12, s(s(T28)))) → U38_GA(T12, half17_in_ga(T28, s(s(T38))))
U37_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U38_GA(T12, half17_out_ga(T28, s(s(T38)))) → U39_GA(T12, half17_in_ga(T38, s(s(T48))))
U38_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U39_GA(T12, half17_out_ga(T38, s(s(T48)))) → U40_GA(T12, half17_in_ga(T48, s(s(T58))))
U39_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → U41_GA(T12, half17_in_gg(T58, 0))
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GG(T58, 0)
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → U42_GA(T12, half17_in_gg(T58, s(0)))
U40_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GG(T58, s(0))
LOG21_IN_GA(s(s(T12)), T70) → U43_GA(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_GA(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_GA(T12, T70, half17_in_ga(T28, s(s(T38))))
U43_GA(T12, T70, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U44_GA(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_GA(T12, T70, half17_in_ga(T38, s(s(T48))))
U44_GA(T12, T70, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U45_GA(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_GA(T12, T70, half17_in_ga(T48, s(s(T58))))
U45_GA(T12, T70, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U46_GA(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_GA(T12, T70, half17_in_ga(T58, s(s(T68))))
U46_GA(T12, T70, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U47_GA(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_GA(T12, T70, half17_in_ga(T68, X218))
U47_GA(T12, T70, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, X218)
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(0))))))) → HALF17_IN_GA(T12, s(s(T28)))
U49_GA(T12, half17_out_ga(T12, s(s(T28)))) → U50_GA(T12, half17_in_ga(T28, s(s(T38))))
U49_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U50_GA(T12, half17_out_ga(T28, s(s(T38)))) → U51_GA(T12, half17_in_ga(T38, s(s(T48))))
U50_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U51_GA(T12, half17_out_ga(T38, s(s(T48)))) → U52_GA(T12, half17_in_ga(T48, s(s(T58))))
U51_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U52_GA(T12, half17_out_ga(T48, s(s(T58)))) → U53_GA(T12, half17_in_ga(T58, s(s(T68))))
U52_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → U54_GA(T12, half17_in_gg(T68, 0))
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GG(T68, 0)
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → U55_GA(T12, half17_in_gg(T68, s(0)))
U53_GA(T12, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GG(T68, s(0))
LOG21_IN_GA(s(s(T12)), T80) → U56_GA(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_GA(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_GA(T12, T80, half17_in_ga(T28, s(s(T38))))
U56_GA(T12, T80, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U57_GA(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_GA(T12, T80, half17_in_ga(T38, s(s(T48))))
U57_GA(T12, T80, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U58_GA(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_GA(T12, T80, half17_in_ga(T48, s(s(T58))))
U58_GA(T12, T80, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U59_GA(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_GA(T12, T80, half17_in_ga(T58, s(s(T68))))
U59_GA(T12, T80, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U60_GA(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_GA(T12, T80, half17_in_ga(T68, s(s(T78))))
U60_GA(T12, T80, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, s(s(T78)))
U61_GA(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_GA(T12, T80, half17_in_ga(T78, X252))
U61_GA(T12, T80, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GA(T78, X252)
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_GA(T12, half17_in_ga(T12, s(s(T28))))
LOG21_IN_GA(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → HALF17_IN_GA(T12, s(s(T28)))
U63_GA(T12, half17_out_ga(T12, s(s(T28)))) → U64_GA(T12, half17_in_ga(T28, s(s(T38))))
U63_GA(T12, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U64_GA(T12, half17_out_ga(T28, s(s(T38)))) → U65_GA(T12, half17_in_ga(T38, s(s(T48))))
U64_GA(T12, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U65_GA(T12, half17_out_ga(T38, s(s(T48)))) → U66_GA(T12, half17_in_ga(T48, s(s(T58))))
U65_GA(T12, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U66_GA(T12, half17_out_ga(T48, s(s(T58)))) → U67_GA(T12, half17_in_ga(T58, s(s(T68))))
U66_GA(T12, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U67_GA(T12, half17_out_ga(T58, s(s(T68)))) → U68_GA(T12, half17_in_ga(T68, s(s(T78))))
U67_GA(T12, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, s(s(T78)))
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → U69_GA(T12, half17_in_gg(T78, 0))
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GG(T78, 0)
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → U70_GA(T12, half17_in_gg(T78, s(0)))
U68_GA(T12, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GG(T78, s(0))
LOG21_IN_GA(s(s(T12)), T90) → U71_GA(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_GA(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_GA(T12, T90, half17_in_ga(T28, s(s(T38))))
U71_GA(T12, T90, half17_out_ga(T12, s(s(T28)))) → HALF17_IN_GA(T28, s(s(T38)))
U72_GA(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_GA(T12, T90, half17_in_ga(T38, s(s(T48))))
U72_GA(T12, T90, half17_out_ga(T28, s(s(T38)))) → HALF17_IN_GA(T38, s(s(T48)))
U73_GA(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_GA(T12, T90, half17_in_ga(T48, s(s(T58))))
U73_GA(T12, T90, half17_out_ga(T38, s(s(T48)))) → HALF17_IN_GA(T48, s(s(T58)))
U74_GA(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_GA(T12, T90, half17_in_ga(T58, s(s(T68))))
U74_GA(T12, T90, half17_out_ga(T48, s(s(T58)))) → HALF17_IN_GA(T58, s(s(T68)))
U75_GA(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_GA(T12, T90, half17_in_ga(T68, s(s(T78))))
U75_GA(T12, T90, half17_out_ga(T58, s(s(T68)))) → HALF17_IN_GA(T68, s(s(T78)))
U76_GA(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_GA(T12, T90, half17_in_ga(T78, s(s(T88))))
U76_GA(T12, T90, half17_out_ga(T68, s(s(T78)))) → HALF17_IN_GA(T78, s(s(T88)))
U77_GA(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_GA(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
U77_GA(T12, T90, half17_out_ga(T78, s(s(T88)))) → P139_IN_GAGA(T88, X286, s(s(s(s(s(s(s(0))))))), T90)
P139_IN_GAGA(T88, X286, T92, T90) → U3_GAGA(T88, X286, T92, T90, half17_in_ga(T88, X286))
P139_IN_GAGA(T88, X286, T92, T90) → HALF17_IN_GA(T88, X286)
P139_IN_GAGA(T88, 0, T102, s(T102)) → U4_GAGA(T88, T102, half17_in_gg(T88, 0))
P139_IN_GAGA(T88, 0, T102, s(T102)) → HALF17_IN_GG(T88, 0)
P139_IN_GAGA(T88, s(0), T107, s(T107)) → U5_GAGA(T88, T107, half17_in_gg(T88, s(0)))
P139_IN_GAGA(T88, s(0), T107, s(T107)) → HALF17_IN_GG(T88, s(0))
P139_IN_GAGA(T88, s(s(T114)), T115, T117) → U6_GAGA(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
P139_IN_GAGA(T88, s(s(T114)), T115, T117) → HALF17_IN_GA(T88, s(s(T114)))
U6_GAGA(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_GAGA(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U6_GAGA(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → P139_IN_GAGA(T114, X323, s(T115), T117)
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)
HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)
From the DPs we obtained the following set of size-change graphs:
HALF22_IN_GA(s(s(T23)), s(X55)) → HALF22_IN_GA(T23, X55)
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
HALF22_IN_GA(s(s(T23)), s(X55)) → HALF22_IN_GA(T23, X55)
HALF22_IN_GA(s(s(T23))) → HALF22_IN_GA(T23)
From the DPs we obtained the following set of size-change graphs:
P139_IN_GAGA(T88, s(s(T114)), T115, T117) → U6_GAGA(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_GAGA(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → P139_IN_GAGA(T114, X323, s(T115), T117)
log21_in_ga(0, 0) → log21_out_ga(0, 0)
log21_in_ga(s(0), 0) → log21_out_ga(s(0), 0)
log21_in_ga(s(s(T12)), T14) → U8_ga(T12, T14, half17_in_ga(T12, X28))
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
U8_ga(T12, T14, half17_out_ga(T12, X28)) → log21_out_ga(s(s(T12)), T14)
log21_in_ga(s(s(T12)), s(0)) → U9_ga(T12, half17_in_gg(T12, 0))
half17_in_gg(T20, s(X46)) → U2_gg(T20, X46, half22_in_gg(T20, X46))
half22_in_gg(0, 0) → half22_out_gg(0, 0)
half22_in_gg(s(0), 0) → half22_out_gg(s(0), 0)
half22_in_gg(s(s(T23)), s(X55)) → U1_gg(T23, X55, half22_in_gg(T23, X55))
U1_gg(T23, X55, half22_out_gg(T23, X55)) → half22_out_gg(s(s(T23)), s(X55))
U2_gg(T20, X46, half22_out_gg(T20, X46)) → half17_out_gg(T20, s(X46))
U9_ga(T12, half17_out_gg(T12, 0)) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), s(0)) → U10_ga(T12, half17_in_gg(T12, s(0)))
U10_ga(T12, half17_out_gg(T12, s(0))) → log21_out_ga(s(s(T12)), s(0))
log21_in_ga(s(s(T12)), T30) → U11_ga(T12, T30, half17_in_ga(T12, s(s(T28))))
U11_ga(T12, T30, half17_out_ga(T12, s(s(T28)))) → U12_ga(T12, T30, half17_in_ga(T28, X82))
U12_ga(T12, T30, half17_out_ga(T28, X82)) → log21_out_ga(s(s(T12)), T30)
log21_in_ga(s(s(T12)), s(s(0))) → U13_ga(T12, half17_in_ga(T12, s(s(T28))))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U14_ga(T12, half17_in_gg(T28, 0))
U14_ga(T12, half17_out_gg(T28, 0)) → log21_out_ga(s(s(T12)), s(s(0)))
U13_ga(T12, half17_out_ga(T12, s(s(T28)))) → U15_ga(T12, half17_in_gg(T28, s(0)))
U15_ga(T12, half17_out_gg(T28, s(0))) → log21_out_ga(s(s(T12)), s(s(0)))
log21_in_ga(s(s(T12)), T40) → U16_ga(T12, T40, half17_in_ga(T12, s(s(T28))))
U16_ga(T12, T40, half17_out_ga(T12, s(s(T28)))) → U17_ga(T12, T40, half17_in_ga(T28, s(s(T38))))
U17_ga(T12, T40, half17_out_ga(T28, s(s(T38)))) → U18_ga(T12, T40, half17_in_ga(T38, X116))
U18_ga(T12, T40, half17_out_ga(T38, X116)) → log21_out_ga(s(s(T12)), T40)
log21_in_ga(s(s(T12)), s(s(s(0)))) → U19_ga(T12, half17_in_ga(T12, s(s(T28))))
U19_ga(T12, half17_out_ga(T12, s(s(T28)))) → U20_ga(T12, half17_in_ga(T28, s(s(T38))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U21_ga(T12, half17_in_gg(T38, 0))
U21_ga(T12, half17_out_gg(T38, 0)) → log21_out_ga(s(s(T12)), s(s(s(0))))
U20_ga(T12, half17_out_ga(T28, s(s(T38)))) → U22_ga(T12, half17_in_gg(T38, s(0)))
U22_ga(T12, half17_out_gg(T38, s(0))) → log21_out_ga(s(s(T12)), s(s(s(0))))
log21_in_ga(s(s(T12)), T50) → U23_ga(T12, T50, half17_in_ga(T12, s(s(T28))))
U23_ga(T12, T50, half17_out_ga(T12, s(s(T28)))) → U24_ga(T12, T50, half17_in_ga(T28, s(s(T38))))
U24_ga(T12, T50, half17_out_ga(T28, s(s(T38)))) → U25_ga(T12, T50, half17_in_ga(T38, s(s(T48))))
U25_ga(T12, T50, half17_out_ga(T38, s(s(T48)))) → U26_ga(T12, T50, half17_in_ga(T48, X150))
U26_ga(T12, T50, half17_out_ga(T48, X150)) → log21_out_ga(s(s(T12)), T50)
log21_in_ga(s(s(T12)), s(s(s(s(0))))) → U27_ga(T12, half17_in_ga(T12, s(s(T28))))
U27_ga(T12, half17_out_ga(T12, s(s(T28)))) → U28_ga(T12, half17_in_ga(T28, s(s(T38))))
U28_ga(T12, half17_out_ga(T28, s(s(T38)))) → U29_ga(T12, half17_in_ga(T38, s(s(T48))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U30_ga(T12, half17_in_gg(T48, 0))
U30_ga(T12, half17_out_gg(T48, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
U29_ga(T12, half17_out_ga(T38, s(s(T48)))) → U31_ga(T12, half17_in_gg(T48, s(0)))
U31_ga(T12, half17_out_gg(T48, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(0)))))
log21_in_ga(s(s(T12)), T60) → U32_ga(T12, T60, half17_in_ga(T12, s(s(T28))))
U32_ga(T12, T60, half17_out_ga(T12, s(s(T28)))) → U33_ga(T12, T60, half17_in_ga(T28, s(s(T38))))
U33_ga(T12, T60, half17_out_ga(T28, s(s(T38)))) → U34_ga(T12, T60, half17_in_ga(T38, s(s(T48))))
U34_ga(T12, T60, half17_out_ga(T38, s(s(T48)))) → U35_ga(T12, T60, half17_in_ga(T48, s(s(T58))))
U35_ga(T12, T60, half17_out_ga(T48, s(s(T58)))) → U36_ga(T12, T60, half17_in_ga(T58, X184))
U36_ga(T12, T60, half17_out_ga(T58, X184)) → log21_out_ga(s(s(T12)), T60)
log21_in_ga(s(s(T12)), s(s(s(s(s(0)))))) → U37_ga(T12, half17_in_ga(T12, s(s(T28))))
U37_ga(T12, half17_out_ga(T12, s(s(T28)))) → U38_ga(T12, half17_in_ga(T28, s(s(T38))))
U38_ga(T12, half17_out_ga(T28, s(s(T38)))) → U39_ga(T12, half17_in_ga(T38, s(s(T48))))
U39_ga(T12, half17_out_ga(T38, s(s(T48)))) → U40_ga(T12, half17_in_ga(T48, s(s(T58))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U41_ga(T12, half17_in_gg(T58, 0))
U41_ga(T12, half17_out_gg(T58, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
U40_ga(T12, half17_out_ga(T48, s(s(T58)))) → U42_ga(T12, half17_in_gg(T58, s(0)))
U42_ga(T12, half17_out_gg(T58, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(0))))))
log21_in_ga(s(s(T12)), T70) → U43_ga(T12, T70, half17_in_ga(T12, s(s(T28))))
U43_ga(T12, T70, half17_out_ga(T12, s(s(T28)))) → U44_ga(T12, T70, half17_in_ga(T28, s(s(T38))))
U44_ga(T12, T70, half17_out_ga(T28, s(s(T38)))) → U45_ga(T12, T70, half17_in_ga(T38, s(s(T48))))
U45_ga(T12, T70, half17_out_ga(T38, s(s(T48)))) → U46_ga(T12, T70, half17_in_ga(T48, s(s(T58))))
U46_ga(T12, T70, half17_out_ga(T48, s(s(T58)))) → U47_ga(T12, T70, half17_in_ga(T58, s(s(T68))))
U47_ga(T12, T70, half17_out_ga(T58, s(s(T68)))) → U48_ga(T12, T70, half17_in_ga(T68, X218))
U48_ga(T12, T70, half17_out_ga(T68, X218)) → log21_out_ga(s(s(T12)), T70)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(0))))))) → U49_ga(T12, half17_in_ga(T12, s(s(T28))))
U49_ga(T12, half17_out_ga(T12, s(s(T28)))) → U50_ga(T12, half17_in_ga(T28, s(s(T38))))
U50_ga(T12, half17_out_ga(T28, s(s(T38)))) → U51_ga(T12, half17_in_ga(T38, s(s(T48))))
U51_ga(T12, half17_out_ga(T38, s(s(T48)))) → U52_ga(T12, half17_in_ga(T48, s(s(T58))))
U52_ga(T12, half17_out_ga(T48, s(s(T58)))) → U53_ga(T12, half17_in_ga(T58, s(s(T68))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U54_ga(T12, half17_in_gg(T68, 0))
U54_ga(T12, half17_out_gg(T68, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
U53_ga(T12, half17_out_ga(T58, s(s(T68)))) → U55_ga(T12, half17_in_gg(T68, s(0)))
U55_ga(T12, half17_out_gg(T68, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(0)))))))
log21_in_ga(s(s(T12)), T80) → U56_ga(T12, T80, half17_in_ga(T12, s(s(T28))))
U56_ga(T12, T80, half17_out_ga(T12, s(s(T28)))) → U57_ga(T12, T80, half17_in_ga(T28, s(s(T38))))
U57_ga(T12, T80, half17_out_ga(T28, s(s(T38)))) → U58_ga(T12, T80, half17_in_ga(T38, s(s(T48))))
U58_ga(T12, T80, half17_out_ga(T38, s(s(T48)))) → U59_ga(T12, T80, half17_in_ga(T48, s(s(T58))))
U59_ga(T12, T80, half17_out_ga(T48, s(s(T58)))) → U60_ga(T12, T80, half17_in_ga(T58, s(s(T68))))
U60_ga(T12, T80, half17_out_ga(T58, s(s(T68)))) → U61_ga(T12, T80, half17_in_ga(T68, s(s(T78))))
U61_ga(T12, T80, half17_out_ga(T68, s(s(T78)))) → U62_ga(T12, T80, half17_in_ga(T78, X252))
U62_ga(T12, T80, half17_out_ga(T78, X252)) → log21_out_ga(s(s(T12)), T80)
log21_in_ga(s(s(T12)), s(s(s(s(s(s(s(0)))))))) → U63_ga(T12, half17_in_ga(T12, s(s(T28))))
U63_ga(T12, half17_out_ga(T12, s(s(T28)))) → U64_ga(T12, half17_in_ga(T28, s(s(T38))))
U64_ga(T12, half17_out_ga(T28, s(s(T38)))) → U65_ga(T12, half17_in_ga(T38, s(s(T48))))
U65_ga(T12, half17_out_ga(T38, s(s(T48)))) → U66_ga(T12, half17_in_ga(T48, s(s(T58))))
U66_ga(T12, half17_out_ga(T48, s(s(T58)))) → U67_ga(T12, half17_in_ga(T58, s(s(T68))))
U67_ga(T12, half17_out_ga(T58, s(s(T68)))) → U68_ga(T12, half17_in_ga(T68, s(s(T78))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U69_ga(T12, half17_in_gg(T78, 0))
U69_ga(T12, half17_out_gg(T78, 0)) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
U68_ga(T12, half17_out_ga(T68, s(s(T78)))) → U70_ga(T12, half17_in_gg(T78, s(0)))
U70_ga(T12, half17_out_gg(T78, s(0))) → log21_out_ga(s(s(T12)), s(s(s(s(s(s(s(0))))))))
log21_in_ga(s(s(T12)), T90) → U71_ga(T12, T90, half17_in_ga(T12, s(s(T28))))
U71_ga(T12, T90, half17_out_ga(T12, s(s(T28)))) → U72_ga(T12, T90, half17_in_ga(T28, s(s(T38))))
U72_ga(T12, T90, half17_out_ga(T28, s(s(T38)))) → U73_ga(T12, T90, half17_in_ga(T38, s(s(T48))))
U73_ga(T12, T90, half17_out_ga(T38, s(s(T48)))) → U74_ga(T12, T90, half17_in_ga(T48, s(s(T58))))
U74_ga(T12, T90, half17_out_ga(T48, s(s(T58)))) → U75_ga(T12, T90, half17_in_ga(T58, s(s(T68))))
U75_ga(T12, T90, half17_out_ga(T58, s(s(T68)))) → U76_ga(T12, T90, half17_in_ga(T68, s(s(T78))))
U76_ga(T12, T90, half17_out_ga(T68, s(s(T78)))) → U77_ga(T12, T90, half17_in_ga(T78, s(s(T88))))
U77_ga(T12, T90, half17_out_ga(T78, s(s(T88)))) → U78_ga(T12, T90, p139_in_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90))
p139_in_gaga(T88, X286, T92, T90) → U3_gaga(T88, X286, T92, T90, half17_in_ga(T88, X286))
U3_gaga(T88, X286, T92, T90, half17_out_ga(T88, X286)) → p139_out_gaga(T88, X286, T92, T90)
p139_in_gaga(T88, 0, T102, s(T102)) → U4_gaga(T88, T102, half17_in_gg(T88, 0))
U4_gaga(T88, T102, half17_out_gg(T88, 0)) → p139_out_gaga(T88, 0, T102, s(T102))
p139_in_gaga(T88, s(0), T107, s(T107)) → U5_gaga(T88, T107, half17_in_gg(T88, s(0)))
U5_gaga(T88, T107, half17_out_gg(T88, s(0))) → p139_out_gaga(T88, s(0), T107, s(T107))
p139_in_gaga(T88, s(s(T114)), T115, T117) → U6_gaga(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_gaga(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → U7_gaga(T88, T114, T115, T117, p139_in_gaga(T114, X323, s(T115), T117))
U7_gaga(T88, T114, T115, T117, p139_out_gaga(T114, X323, s(T115), T117)) → p139_out_gaga(T88, s(s(T114)), T115, T117)
U78_ga(T12, T90, p139_out_gaga(T88, X286, s(s(s(s(s(s(s(0))))))), T90)) → log21_out_ga(s(s(T12)), T90)
P139_IN_GAGA(T88, s(s(T114)), T115, T117) → U6_GAGA(T88, T114, T115, T117, half17_in_ga(T88, s(s(T114))))
U6_GAGA(T88, T114, T115, T117, half17_out_ga(T88, s(s(T114)))) → P139_IN_GAGA(T114, X323, s(T115), T117)
half17_in_ga(T20, s(X46)) → U2_ga(T20, X46, half22_in_ga(T20, X46))
U2_ga(T20, X46, half22_out_ga(T20, X46)) → half17_out_ga(T20, s(X46))
half22_in_ga(0, 0) → half22_out_ga(0, 0)
half22_in_ga(s(0), 0) → half22_out_ga(s(0), 0)
half22_in_ga(s(s(T23)), s(X55)) → U1_ga(T23, X55, half22_in_ga(T23, X55))
U1_ga(T23, X55, half22_out_ga(T23, X55)) → half22_out_ga(s(s(T23)), s(X55))
P139_IN_GAGA(T88, T115) → U6_GAGA(T115, half17_in_ga(T88))
U6_GAGA(T115, half17_out_ga(s(s(T114)))) → P139_IN_GAGA(T114, s(T115))
half17_in_ga(T20) → U2_ga(half22_in_ga(T20))
U2_ga(half22_out_ga(X46)) → half17_out_ga(s(X46))
half22_in_ga(0) → half22_out_ga(0)
half22_in_ga(s(0)) → half22_out_ga(0)
half22_in_ga(s(s(T23))) → U1_ga(half22_in_ga(T23))
U1_ga(half22_out_ga(X55)) → half22_out_ga(s(X55))
half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)
U1_ga(x0)
half22_in_ga(s(0)) → half22_out_ga(0)
half22_in_ga(s(s(T23))) → U1_ga(half22_in_ga(T23))
U1_ga(half22_out_ga(X55)) → half22_out_ga(s(X55))
POL(0) = 0
POL(P139_IN_GAGA(x1, x2)) = 2 + x1 + x2
POL(U1_ga(x1)) = 3 + x1
POL(U2_ga(x1)) = 2 + x1
POL(U6_GAGA(x1, x2)) = x1 + x2
POL(half17_in_ga(x1)) = 2 + x1
POL(half17_out_ga(x1)) = x1
POL(half22_in_ga(x1)) = x1
POL(half22_out_ga(x1)) = x1
POL(s(x1)) = 2 + x1
P139_IN_GAGA(T88, T115) → U6_GAGA(T115, half17_in_ga(T88))
U6_GAGA(T115, half17_out_ga(s(s(T114)))) → P139_IN_GAGA(T114, s(T115))
half17_in_ga(T20) → U2_ga(half22_in_ga(T20))
U2_ga(half22_out_ga(X46)) → half17_out_ga(s(X46))
half22_in_ga(0) → half22_out_ga(0)
half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)
U1_ga(x0)
U1_ga(x0)
P139_IN_GAGA(T88, T115) → U6_GAGA(T115, half17_in_ga(T88))
U6_GAGA(T115, half17_out_ga(s(s(T114)))) → P139_IN_GAGA(T114, s(T115))
half17_in_ga(T20) → U2_ga(half22_in_ga(T20))
U2_ga(half22_out_ga(X46)) → half17_out_ga(s(X46))
half22_in_ga(0) → half22_out_ga(0)
half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)
U6_GAGA(T115, half17_out_ga(s(s(T114)))) → P139_IN_GAGA(T114, s(T115))
POL(0) = 0
POL(P139_IN_GAGA(x1, x2)) = 2 + 2·x1 + x2
POL(U2_ga(x1)) = 1 + x1
POL(U6_GAGA(x1, x2)) = x1 + 2·x2
POL(half17_in_ga(x1)) = 1 + x1
POL(half17_out_ga(x1)) = x1
POL(half22_in_ga(x1)) = x1
POL(half22_out_ga(x1)) = 2·x1
POL(s(x1)) = 1 + x1
P139_IN_GAGA(T88, T115) → U6_GAGA(T115, half17_in_ga(T88))
half17_in_ga(T20) → U2_ga(half22_in_ga(T20))
U2_ga(half22_out_ga(X46)) → half17_out_ga(s(X46))
half22_in_ga(0) → half22_out_ga(0)
half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)