0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
a(c(d(x))) → c(x) u(b(d(d(x)))) → b(x) v(a(a(x))) → u(v(x)) v(a(c(x))) → u(b(d(x))) v(c(x)) → b(x) w(a(a(x))) → u(w(x)) w(a(c(x))) → u(b(d(x))) w(c(x)) → b(x)
w1 > d1 > v1 > b1 > a1 > c1 > u1
a_1=3 c_1=1 d_1=2 u_1=1 b_1=8 v_1=7 w_1=7