(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, Y).
log2(0, I, I).
log2(s(0), I, I).
log2(s(s(X)), I, Y) :- ','(half(s(s(X)), X1), log2(X1, s(I), Y)).
half(0, 0).
half(s(0), 0).
half(s(s(X)), s(Y)) :- half(X, Y).

Queries:

log2(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

half22(0, 0).
half22(s(0), 0).
half22(s(s(T23)), s(X55)) :- half22(T23, X55).
half17(T20, s(X46)) :- half22(T20, X46).
p139(T88, X286, T92, T90) :- half17(T88, X286).
p139(T88, 0, T102, s(T102)) :- half17(T88, 0).
p139(T88, s(0), T107, s(T107)) :- half17(T88, s(0)).
p139(T88, s(s(T114)), T115, T117) :- ','(half17(T88, s(s(T114))), p139(T114, X323, s(T115), T117)).
log21(0, 0).
log21(s(0), 0).
log21(s(s(T12)), T14) :- half17(T12, X28).
log21(s(s(T12)), s(0)) :- half17(T12, 0).
log21(s(s(T12)), s(0)) :- half17(T12, s(0)).
log21(s(s(T12)), T30) :- ','(half17(T12, s(s(T28))), half17(T28, X82)).
log21(s(s(T12)), s(s(0))) :- ','(half17(T12, s(s(T28))), half17(T28, 0)).
log21(s(s(T12)), s(s(0))) :- ','(half17(T12, s(s(T28))), half17(T28, s(0))).
log21(s(s(T12)), T40) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), half17(T38, X116))).
log21(s(s(T12)), s(s(s(0)))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), half17(T38, 0))).
log21(s(s(T12)), s(s(s(0)))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), half17(T38, s(0)))).
log21(s(s(T12)), T50) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), half17(T48, X150)))).
log21(s(s(T12)), s(s(s(s(0))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), half17(T48, 0)))).
log21(s(s(T12)), s(s(s(s(0))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), half17(T48, s(0))))).
log21(s(s(T12)), T60) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), half17(T58, X184))))).
log21(s(s(T12)), s(s(s(s(s(0)))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), half17(T58, 0))))).
log21(s(s(T12)), s(s(s(s(s(0)))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), half17(T58, s(0)))))).
log21(s(s(T12)), T70) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), half17(T68, X218)))))).
log21(s(s(T12)), s(s(s(s(s(s(0))))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), half17(T68, 0)))))).
log21(s(s(T12)), s(s(s(s(s(s(0))))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), half17(T68, s(0))))))).
log21(s(s(T12)), T80) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), ','(half17(T68, s(s(T78))), half17(T78, X252))))))).
log21(s(s(T12)), s(s(s(s(s(s(s(0)))))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), ','(half17(T68, s(s(T78))), half17(T78, 0))))))).
log21(s(s(T12)), s(s(s(s(s(s(s(0)))))))) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), ','(half17(T68, s(s(T78))), half17(T78, s(0)))))))).
log21(s(s(T12)), T90) :- ','(half17(T12, s(s(T28))), ','(half17(T28, s(s(T38))), ','(half17(T38, s(s(T48))), ','(half17(T48, s(s(T58))), ','(half17(T58, s(s(T68))), ','(half17(T68, s(s(T78))), ','(half17(T78, s(s(T88))), p139(T88, X286, s(s(s(s(s(s(s(0))))))), T90)))))))).

Queries:

log21(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
log21_in: (b,f)
half17_in: (b,f) (b,b)
half22_in: (b,f) (b,b)
p139_in: (b,f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

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)

The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
LOG21_IN_GA(x1, x2)  =  LOG21_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
HALF17_IN_GA(x1, x2)  =  HALF17_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U9_GA(x1, x2)  =  U9_GA(x2)
HALF17_IN_GG(x1, x2)  =  HALF17_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)
HALF22_IN_GG(x1, x2)  =  HALF22_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U10_GA(x1, x2)  =  U10_GA(x2)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2)  =  U13_GA(x2)
U14_GA(x1, x2)  =  U14_GA(x2)
U15_GA(x1, x2)  =  U15_GA(x2)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U17_GA(x1, x2, x3)  =  U17_GA(x3)
U18_GA(x1, x2, x3)  =  U18_GA(x3)
U19_GA(x1, x2)  =  U19_GA(x2)
U20_GA(x1, x2)  =  U20_GA(x2)
U21_GA(x1, x2)  =  U21_GA(x2)
U22_GA(x1, x2)  =  U22_GA(x2)
U23_GA(x1, x2, x3)  =  U23_GA(x3)
U24_GA(x1, x2, x3)  =  U24_GA(x3)
U25_GA(x1, x2, x3)  =  U25_GA(x3)
U26_GA(x1, x2, x3)  =  U26_GA(x3)
U27_GA(x1, x2)  =  U27_GA(x2)
U28_GA(x1, x2)  =  U28_GA(x2)
U29_GA(x1, x2)  =  U29_GA(x2)
U30_GA(x1, x2)  =  U30_GA(x2)
U31_GA(x1, x2)  =  U31_GA(x2)
U32_GA(x1, x2, x3)  =  U32_GA(x3)
U33_GA(x1, x2, x3)  =  U33_GA(x3)
U34_GA(x1, x2, x3)  =  U34_GA(x3)
U35_GA(x1, x2, x3)  =  U35_GA(x3)
U36_GA(x1, x2, x3)  =  U36_GA(x3)
U37_GA(x1, x2)  =  U37_GA(x2)
U38_GA(x1, x2)  =  U38_GA(x2)
U39_GA(x1, x2)  =  U39_GA(x2)
U40_GA(x1, x2)  =  U40_GA(x2)
U41_GA(x1, x2)  =  U41_GA(x2)
U42_GA(x1, x2)  =  U42_GA(x2)
U43_GA(x1, x2, x3)  =  U43_GA(x3)
U44_GA(x1, x2, x3)  =  U44_GA(x3)
U45_GA(x1, x2, x3)  =  U45_GA(x3)
U46_GA(x1, x2, x3)  =  U46_GA(x3)
U47_GA(x1, x2, x3)  =  U47_GA(x3)
U48_GA(x1, x2, x3)  =  U48_GA(x3)
U49_GA(x1, x2)  =  U49_GA(x2)
U50_GA(x1, x2)  =  U50_GA(x2)
U51_GA(x1, x2)  =  U51_GA(x2)
U52_GA(x1, x2)  =  U52_GA(x2)
U53_GA(x1, x2)  =  U53_GA(x2)
U54_GA(x1, x2)  =  U54_GA(x2)
U55_GA(x1, x2)  =  U55_GA(x2)
U56_GA(x1, x2, x3)  =  U56_GA(x3)
U57_GA(x1, x2, x3)  =  U57_GA(x3)
U58_GA(x1, x2, x3)  =  U58_GA(x3)
U59_GA(x1, x2, x3)  =  U59_GA(x3)
U60_GA(x1, x2, x3)  =  U60_GA(x3)
U61_GA(x1, x2, x3)  =  U61_GA(x3)
U62_GA(x1, x2, x3)  =  U62_GA(x3)
U63_GA(x1, x2)  =  U63_GA(x2)
U64_GA(x1, x2)  =  U64_GA(x2)
U65_GA(x1, x2)  =  U65_GA(x2)
U66_GA(x1, x2)  =  U66_GA(x2)
U67_GA(x1, x2)  =  U67_GA(x2)
U68_GA(x1, x2)  =  U68_GA(x2)
U69_GA(x1, x2)  =  U69_GA(x2)
U70_GA(x1, x2)  =  U70_GA(x2)
U71_GA(x1, x2, x3)  =  U71_GA(x3)
U72_GA(x1, x2, x3)  =  U72_GA(x3)
U73_GA(x1, x2, x3)  =  U73_GA(x3)
U74_GA(x1, x2, x3)  =  U74_GA(x3)
U75_GA(x1, x2, x3)  =  U75_GA(x3)
U76_GA(x1, x2, x3)  =  U76_GA(x3)
U77_GA(x1, x2, x3)  =  U77_GA(x3)
U78_GA(x1, x2, x3)  =  U78_GA(x3)
P139_IN_GAGA(x1, x2, x3, x4)  =  P139_IN_GAGA(x1, x3)
U3_GAGA(x1, x2, x3, x4, x5)  =  U3_GAGA(x5)
U4_GAGA(x1, x2, x3)  =  U4_GAGA(x3)
U5_GAGA(x1, x2, x3)  =  U5_GAGA(x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)
U7_GAGA(x1, x2, x3, x4, x5)  =  U7_GAGA(x2, x5)

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

(6) Obligation:

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

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)

The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
LOG21_IN_GA(x1, x2)  =  LOG21_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
HALF17_IN_GA(x1, x2)  =  HALF17_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U9_GA(x1, x2)  =  U9_GA(x2)
HALF17_IN_GG(x1, x2)  =  HALF17_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)
HALF22_IN_GG(x1, x2)  =  HALF22_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x3)
U10_GA(x1, x2)  =  U10_GA(x2)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2)  =  U13_GA(x2)
U14_GA(x1, x2)  =  U14_GA(x2)
U15_GA(x1, x2)  =  U15_GA(x2)
U16_GA(x1, x2, x3)  =  U16_GA(x3)
U17_GA(x1, x2, x3)  =  U17_GA(x3)
U18_GA(x1, x2, x3)  =  U18_GA(x3)
U19_GA(x1, x2)  =  U19_GA(x2)
U20_GA(x1, x2)  =  U20_GA(x2)
U21_GA(x1, x2)  =  U21_GA(x2)
U22_GA(x1, x2)  =  U22_GA(x2)
U23_GA(x1, x2, x3)  =  U23_GA(x3)
U24_GA(x1, x2, x3)  =  U24_GA(x3)
U25_GA(x1, x2, x3)  =  U25_GA(x3)
U26_GA(x1, x2, x3)  =  U26_GA(x3)
U27_GA(x1, x2)  =  U27_GA(x2)
U28_GA(x1, x2)  =  U28_GA(x2)
U29_GA(x1, x2)  =  U29_GA(x2)
U30_GA(x1, x2)  =  U30_GA(x2)
U31_GA(x1, x2)  =  U31_GA(x2)
U32_GA(x1, x2, x3)  =  U32_GA(x3)
U33_GA(x1, x2, x3)  =  U33_GA(x3)
U34_GA(x1, x2, x3)  =  U34_GA(x3)
U35_GA(x1, x2, x3)  =  U35_GA(x3)
U36_GA(x1, x2, x3)  =  U36_GA(x3)
U37_GA(x1, x2)  =  U37_GA(x2)
U38_GA(x1, x2)  =  U38_GA(x2)
U39_GA(x1, x2)  =  U39_GA(x2)
U40_GA(x1, x2)  =  U40_GA(x2)
U41_GA(x1, x2)  =  U41_GA(x2)
U42_GA(x1, x2)  =  U42_GA(x2)
U43_GA(x1, x2, x3)  =  U43_GA(x3)
U44_GA(x1, x2, x3)  =  U44_GA(x3)
U45_GA(x1, x2, x3)  =  U45_GA(x3)
U46_GA(x1, x2, x3)  =  U46_GA(x3)
U47_GA(x1, x2, x3)  =  U47_GA(x3)
U48_GA(x1, x2, x3)  =  U48_GA(x3)
U49_GA(x1, x2)  =  U49_GA(x2)
U50_GA(x1, x2)  =  U50_GA(x2)
U51_GA(x1, x2)  =  U51_GA(x2)
U52_GA(x1, x2)  =  U52_GA(x2)
U53_GA(x1, x2)  =  U53_GA(x2)
U54_GA(x1, x2)  =  U54_GA(x2)
U55_GA(x1, x2)  =  U55_GA(x2)
U56_GA(x1, x2, x3)  =  U56_GA(x3)
U57_GA(x1, x2, x3)  =  U57_GA(x3)
U58_GA(x1, x2, x3)  =  U58_GA(x3)
U59_GA(x1, x2, x3)  =  U59_GA(x3)
U60_GA(x1, x2, x3)  =  U60_GA(x3)
U61_GA(x1, x2, x3)  =  U61_GA(x3)
U62_GA(x1, x2, x3)  =  U62_GA(x3)
U63_GA(x1, x2)  =  U63_GA(x2)
U64_GA(x1, x2)  =  U64_GA(x2)
U65_GA(x1, x2)  =  U65_GA(x2)
U66_GA(x1, x2)  =  U66_GA(x2)
U67_GA(x1, x2)  =  U67_GA(x2)
U68_GA(x1, x2)  =  U68_GA(x2)
U69_GA(x1, x2)  =  U69_GA(x2)
U70_GA(x1, x2)  =  U70_GA(x2)
U71_GA(x1, x2, x3)  =  U71_GA(x3)
U72_GA(x1, x2, x3)  =  U72_GA(x3)
U73_GA(x1, x2, x3)  =  U73_GA(x3)
U74_GA(x1, x2, x3)  =  U74_GA(x3)
U75_GA(x1, x2, x3)  =  U75_GA(x3)
U76_GA(x1, x2, x3)  =  U76_GA(x3)
U77_GA(x1, x2, x3)  =  U77_GA(x3)
U78_GA(x1, x2, x3)  =  U78_GA(x3)
P139_IN_GAGA(x1, x2, x3, x4)  =  P139_IN_GAGA(x1, x3)
U3_GAGA(x1, x2, x3, x4, x5)  =  U3_GAGA(x5)
U4_GAGA(x1, x2, x3)  =  U4_GAGA(x3)
U5_GAGA(x1, x2, x3)  =  U5_GAGA(x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)
U7_GAGA(x1, x2, x3, x4, x5)  =  U7_GAGA(x2, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)

The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
HALF22_IN_GG(x1, x2)  =  HALF22_IN_GG(x1, x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)

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

(12) PiDPToQDPProof (EQUIVALENT transformation)

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

(13) Obligation:

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

HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • HALF22_IN_GG(s(s(T23)), s(X55)) → HALF22_IN_GG(T23, X55)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

HALF22_IN_GA(s(s(T23)), s(X55)) → HALF22_IN_GA(T23, X55)

The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

HALF22_IN_GA(s(s(T23)), s(X55)) → HALF22_IN_GA(T23, X55)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
HALF22_IN_GA(x1, x2)  =  HALF22_IN_GA(x1)

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

HALF22_IN_GA(s(s(T23))) → HALF22_IN_GA(T23)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • HALF22_IN_GA(s(s(T23))) → HALF22_IN_GA(T23)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

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)

The TRS R consists of the following rules:

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)

The argument filtering Pi contains the following mapping:
log21_in_ga(x1, x2)  =  log21_in_ga(x1)
0  =  0
log21_out_ga(x1, x2)  =  log21_out_ga
s(x1)  =  s(x1)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
U9_ga(x1, x2)  =  U9_ga(x2)
half17_in_gg(x1, x2)  =  half17_in_gg(x1, x2)
U2_gg(x1, x2, x3)  =  U2_gg(x3)
half22_in_gg(x1, x2)  =  half22_in_gg(x1, x2)
half22_out_gg(x1, x2)  =  half22_out_gg
U1_gg(x1, x2, x3)  =  U1_gg(x3)
half17_out_gg(x1, x2)  =  half17_out_gg
U10_ga(x1, x2)  =  U10_ga(x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2)  =  U13_ga(x2)
U14_ga(x1, x2)  =  U14_ga(x2)
U15_ga(x1, x2)  =  U15_ga(x2)
U16_ga(x1, x2, x3)  =  U16_ga(x3)
U17_ga(x1, x2, x3)  =  U17_ga(x3)
U18_ga(x1, x2, x3)  =  U18_ga(x3)
U19_ga(x1, x2)  =  U19_ga(x2)
U20_ga(x1, x2)  =  U20_ga(x2)
U21_ga(x1, x2)  =  U21_ga(x2)
U22_ga(x1, x2)  =  U22_ga(x2)
U23_ga(x1, x2, x3)  =  U23_ga(x3)
U24_ga(x1, x2, x3)  =  U24_ga(x3)
U25_ga(x1, x2, x3)  =  U25_ga(x3)
U26_ga(x1, x2, x3)  =  U26_ga(x3)
U27_ga(x1, x2)  =  U27_ga(x2)
U28_ga(x1, x2)  =  U28_ga(x2)
U29_ga(x1, x2)  =  U29_ga(x2)
U30_ga(x1, x2)  =  U30_ga(x2)
U31_ga(x1, x2)  =  U31_ga(x2)
U32_ga(x1, x2, x3)  =  U32_ga(x3)
U33_ga(x1, x2, x3)  =  U33_ga(x3)
U34_ga(x1, x2, x3)  =  U34_ga(x3)
U35_ga(x1, x2, x3)  =  U35_ga(x3)
U36_ga(x1, x2, x3)  =  U36_ga(x3)
U37_ga(x1, x2)  =  U37_ga(x2)
U38_ga(x1, x2)  =  U38_ga(x2)
U39_ga(x1, x2)  =  U39_ga(x2)
U40_ga(x1, x2)  =  U40_ga(x2)
U41_ga(x1, x2)  =  U41_ga(x2)
U42_ga(x1, x2)  =  U42_ga(x2)
U43_ga(x1, x2, x3)  =  U43_ga(x3)
U44_ga(x1, x2, x3)  =  U44_ga(x3)
U45_ga(x1, x2, x3)  =  U45_ga(x3)
U46_ga(x1, x2, x3)  =  U46_ga(x3)
U47_ga(x1, x2, x3)  =  U47_ga(x3)
U48_ga(x1, x2, x3)  =  U48_ga(x3)
U49_ga(x1, x2)  =  U49_ga(x2)
U50_ga(x1, x2)  =  U50_ga(x2)
U51_ga(x1, x2)  =  U51_ga(x2)
U52_ga(x1, x2)  =  U52_ga(x2)
U53_ga(x1, x2)  =  U53_ga(x2)
U54_ga(x1, x2)  =  U54_ga(x2)
U55_ga(x1, x2)  =  U55_ga(x2)
U56_ga(x1, x2, x3)  =  U56_ga(x3)
U57_ga(x1, x2, x3)  =  U57_ga(x3)
U58_ga(x1, x2, x3)  =  U58_ga(x3)
U59_ga(x1, x2, x3)  =  U59_ga(x3)
U60_ga(x1, x2, x3)  =  U60_ga(x3)
U61_ga(x1, x2, x3)  =  U61_ga(x3)
U62_ga(x1, x2, x3)  =  U62_ga(x3)
U63_ga(x1, x2)  =  U63_ga(x2)
U64_ga(x1, x2)  =  U64_ga(x2)
U65_ga(x1, x2)  =  U65_ga(x2)
U66_ga(x1, x2)  =  U66_ga(x2)
U67_ga(x1, x2)  =  U67_ga(x2)
U68_ga(x1, x2)  =  U68_ga(x2)
U69_ga(x1, x2)  =  U69_ga(x2)
U70_ga(x1, x2)  =  U70_ga(x2)
U71_ga(x1, x2, x3)  =  U71_ga(x3)
U72_ga(x1, x2, x3)  =  U72_ga(x3)
U73_ga(x1, x2, x3)  =  U73_ga(x3)
U74_ga(x1, x2, x3)  =  U74_ga(x3)
U75_ga(x1, x2, x3)  =  U75_ga(x3)
U76_ga(x1, x2, x3)  =  U76_ga(x3)
U77_ga(x1, x2, x3)  =  U77_ga(x3)
U78_ga(x1, x2, x3)  =  U78_ga(x3)
p139_in_gaga(x1, x2, x3, x4)  =  p139_in_gaga(x1, x3)
U3_gaga(x1, x2, x3, x4, x5)  =  U3_gaga(x5)
p139_out_gaga(x1, x2, x3, x4)  =  p139_out_gaga(x2)
U4_gaga(x1, x2, x3)  =  U4_gaga(x3)
U5_gaga(x1, x2, x3)  =  U5_gaga(x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x3, x5)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x2, x5)
P139_IN_GAGA(x1, x2, x3, x4)  =  P139_IN_GAGA(x1, x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

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)

The TRS R consists of the following rules:

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))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
half17_in_ga(x1, x2)  =  half17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
half22_in_ga(x1, x2)  =  half22_in_ga(x1)
half22_out_ga(x1, x2)  =  half22_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
half17_out_ga(x1, x2)  =  half17_out_ga(x2)
P139_IN_GAGA(x1, x2, x3, x4)  =  P139_IN_GAGA(x1, x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x3, x5)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

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))

The TRS R consists of the following rules:

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))

The set Q consists of the following terms:

half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)
U1_ga(x0)

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

(28) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

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))

Used ordering: Polynomial interpretation [POLO]:

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   

(29) Obligation:

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

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))

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)
U1_ga(x0)

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

(30) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

U1_ga(x0)

(31) Obligation:

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

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))

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)

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

(32) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

U6_GAGA(T115, half17_out_ga(s(s(T114)))) → P139_IN_GAGA(T114, s(T115))


Used ordering: Polynomial interpretation [POLO]:

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   

(33) Obligation:

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

P139_IN_GAGA(T88, T115) → U6_GAGA(T115, half17_in_ga(T88))

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

half17_in_ga(x0)
U2_ga(x0)
half22_in_ga(x0)

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

(34) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(35) TRUE