YES(O(1), O(n^1)) 136.53/45.66 YES(O(1), O(n^1)) 136.53/45.67 136.53/45.67 136.53/45.67
136.53/45.67 136.53/45.670 CpxTRS136.53/45.67
↳1 CpxTrsMatchBoundsTAProof (⇔)136.53/45.67
↳2 BOUNDS(O(1), O(n^1))136.53/45.67
active(and(tt, X)) → mark(X) 136.53/45.67
active(plus(N, 0)) → mark(N) 136.53/45.67
active(plus(N, s(M))) → mark(s(plus(N, M))) 136.53/45.67
active(and(X1, X2)) → and(active(X1), X2) 136.53/45.67
active(plus(X1, X2)) → plus(active(X1), X2) 136.53/45.67
active(plus(X1, X2)) → plus(X1, active(X2)) 136.53/45.67
active(s(X)) → s(active(X)) 136.53/45.67
and(mark(X1), X2) → mark(and(X1, X2)) 136.53/45.67
plus(mark(X1), X2) → mark(plus(X1, X2)) 136.53/45.67
plus(X1, mark(X2)) → mark(plus(X1, X2)) 136.53/45.67
s(mark(X)) → mark(s(X)) 136.53/45.67
proper(and(X1, X2)) → and(proper(X1), proper(X2)) 136.53/45.67
proper(tt) → ok(tt) 136.53/45.67
proper(plus(X1, X2)) → plus(proper(X1), proper(X2)) 136.53/45.67
proper(0) → ok(0) 136.53/45.67
proper(s(X)) → s(proper(X)) 136.53/45.67
and(ok(X1), ok(X2)) → ok(and(X1, X2)) 136.53/45.67
plus(ok(X1), ok(X2)) → ok(plus(X1, X2)) 136.53/45.67
s(ok(X)) → ok(s(X)) 136.53/45.67
top(mark(X)) → top(proper(X)) 136.53/45.67
top(ok(X)) → top(active(X))