0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
half(0) → 0 half(s(s(x))) → s(half(x)) log(s(0)) → 0 log(s(s(x))) → s(log(s(half(x))))
half1 > log1 > s1 > 0
0=1 half_1=0 s_1=1 log_1=2