YES(O(1), O(n^1)) 136.07/45.78 YES(O(1), O(n^1)) 136.47/45.81 136.47/45.81 136.47/45.81
136.47/45.81 136.47/45.810 CpxTRS136.47/45.81
↳1 CpxTrsMatchBoundsTAProof (⇔)136.47/45.81
↳2 BOUNDS(O(1), O(n^1))136.47/45.81
active(U11(tt, M, N)) → mark(U12(tt, M, N)) 136.47/45.81
active(U12(tt, M, N)) → mark(s(plus(N, M))) 136.47/45.81
active(plus(N, 0)) → mark(N) 136.47/45.81
active(plus(N, s(M))) → mark(U11(tt, M, N)) 136.47/45.81
active(U11(X1, X2, X3)) → U11(active(X1), X2, X3) 136.47/45.81
active(U12(X1, X2, X3)) → U12(active(X1), X2, X3) 136.47/45.81
active(s(X)) → s(active(X)) 136.47/45.81
active(plus(X1, X2)) → plus(active(X1), X2) 136.47/45.81
active(plus(X1, X2)) → plus(X1, active(X2)) 136.47/45.81
U11(mark(X1), X2, X3) → mark(U11(X1, X2, X3)) 136.47/45.81
U12(mark(X1), X2, X3) → mark(U12(X1, X2, X3)) 136.47/45.81
s(mark(X)) → mark(s(X)) 136.47/45.81
plus(mark(X1), X2) → mark(plus(X1, X2)) 136.47/45.81
plus(X1, mark(X2)) → mark(plus(X1, X2)) 136.47/45.81
proper(U11(X1, X2, X3)) → U11(proper(X1), proper(X2), proper(X3)) 136.47/45.81
proper(tt) → ok(tt) 136.47/45.81
proper(U12(X1, X2, X3)) → U12(proper(X1), proper(X2), proper(X3)) 136.47/45.81
proper(s(X)) → s(proper(X)) 136.47/45.81
proper(plus(X1, X2)) → plus(proper(X1), proper(X2)) 136.47/45.81
proper(0) → ok(0) 136.47/45.81
U11(ok(X1), ok(X2), ok(X3)) → ok(U11(X1, X2, X3)) 136.47/45.81
U12(ok(X1), ok(X2), ok(X3)) → ok(U12(X1, X2, X3)) 136.47/45.81
s(ok(X)) → ok(s(X)) 136.47/45.81
plus(ok(X1), ok(X2)) → ok(plus(X1, X2)) 136.47/45.81
top(mark(X)) → top(proper(X)) 136.47/45.81
top(ok(X)) → top(active(X))