0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
a(a(x)) → b(b(x)) b(b(a(x))) → a(b(b(x)))
b1 > a1
a_1=2 b_1=1