YES Problem: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(plus(N,s(M))) -> plus#(N,M) active#(plus(N,s(M))) -> s#(plus(N,M)) active#(and(X1,X2)) -> active#(X1) active#(and(X1,X2)) -> and#(active(X1),X2) active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) and#(mark(X1),X2) -> and#(X1,X2) plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) s#(mark(X)) -> s#(X) proper#(and(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> proper#(X1) proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) and#(ok(X1),ok(X2)) -> and#(X1,X2) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) s#(ok(X)) -> s#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(plus(N,s(M))) -> plus#(N,M) active#(plus(N,s(M))) -> s#(plus(N,M)) active#(and(X1,X2)) -> active#(X1) active#(and(X1,X2)) -> and#(active(X1),X2) active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(s(X)) -> active#(X) active#(s(X)) -> s#(active(X)) and#(mark(X1),X2) -> and#(X1,X2) plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) s#(mark(X)) -> s#(X) proper#(and(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> proper#(X1) proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) and#(ok(X1),ok(X2)) -> and#(X1,X2) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) s#(ok(X)) -> s#(X) top#(mark(X)) -> proper#(X) top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X)) top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> top#(proper(X)) top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X) top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X) top#(ok(X)) -> active#(X) -> active#(plus(X1,X2)) -> plus#(X1,active(X2)) top#(ok(X)) -> active#(X) -> active#(plus(X1,X2)) -> active#(X2) top#(ok(X)) -> active#(X) -> active#(plus(X1,X2)) -> plus#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(plus(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(and(X1,X2)) -> and#(active(X1),X2) top#(ok(X)) -> active#(X) -> active#(and(X1,X2)) -> active#(X1) top#(ok(X)) -> active#(X) -> active#(plus(N,s(M))) -> s#(plus(N,M)) top#(ok(X)) -> active#(X) -> active#(plus(N,s(M))) -> plus#(N,M) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> top#(proper(X)) top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) top#(mark(X)) -> proper#(X) -> proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(plus(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(plus(X1,X2)) -> proper#(X2) top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X1) top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X)) proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X) proper#(s(X)) -> proper#(X) -> proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(plus(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(plus(X1,X2)) -> proper#(X2) proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X2) proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X) proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(and(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> proper#(X2) -> proper#(and(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(plus(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(and(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> proper#(X1) -> proper#(and(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) -> plus#(X1,mark(X2)) -> plus#(X1,X2) proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) -> plus#(mark(X1),X2) -> plus#(X1,X2) proper#(and(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> s#(proper(X)) proper#(and(X1,X2)) -> proper#(X2) -> proper#(s(X)) -> proper#(X) proper#(and(X1,X2)) -> proper#(X2) -> proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(and(X1,X2)) -> proper#(X2) -> proper#(plus(X1,X2)) -> proper#(X1) proper#(and(X1,X2)) -> proper#(X2) -> proper#(plus(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> proper#(X2) -> proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(and(X1,X2)) -> proper#(X2) -> proper#(and(X1,X2)) -> proper#(X1) proper#(and(X1,X2)) -> proper#(X2) -> proper#(and(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> s#(proper(X)) proper#(and(X1,X2)) -> proper#(X1) -> proper#(s(X)) -> proper#(X) proper#(and(X1,X2)) -> proper#(X1) -> proper#(plus(X1,X2)) -> plus#(proper(X1),proper(X2)) proper#(and(X1,X2)) -> proper#(X1) -> proper#(plus(X1,X2)) -> proper#(X1) proper#(and(X1,X2)) -> proper#(X1) -> proper#(plus(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> proper#(X1) -> proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) proper#(and(X1,X2)) -> proper#(X1) -> proper#(and(X1,X2)) -> proper#(X1) proper#(and(X1,X2)) -> proper#(X1) -> proper#(and(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) -> and#(ok(X1),ok(X2)) -> and#(X1,X2) proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) -> and#(mark(X1),X2) -> and#(X1,X2) and#(ok(X1),ok(X2)) -> and#(X1,X2) -> and#(ok(X1),ok(X2)) -> and#(X1,X2) and#(ok(X1),ok(X2)) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(X1,X2) and#(mark(X1),X2) -> and#(X1,X2) -> and#(ok(X1),ok(X2)) -> and#(X1,X2) and#(mark(X1),X2) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(X1,X2) s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X) s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) -> plus#(X1,mark(X2)) -> plus#(X1,X2) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) -> plus#(mark(X1),X2) -> plus#(X1,X2) plus#(mark(X1),X2) -> plus#(X1,X2) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) plus#(mark(X1),X2) -> plus#(X1,X2) -> plus#(X1,mark(X2)) -> plus#(X1,X2) plus#(mark(X1),X2) -> plus#(X1,X2) -> plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) -> plus#(X1,mark(X2)) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) -> plus#(mark(X1),X2) -> plus#(X1,X2) active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X) active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X) active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X)) active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X) active#(s(X)) -> active#(X) -> active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(s(X)) -> active#(X) -> active#(plus(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) -> active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(plus(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(and(X1,X2)) -> and#(active(X1),X2) active#(s(X)) -> active#(X) -> active#(and(X1,X2)) -> active#(X1) active#(s(X)) -> active#(X) -> active#(plus(N,s(M))) -> s#(plus(N,M)) active#(s(X)) -> active#(X) -> active#(plus(N,s(M))) -> plus#(N,M) active#(plus(X1,X2)) -> plus#(active(X1),X2) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) active#(plus(X1,X2)) -> plus#(active(X1),X2) -> plus#(X1,mark(X2)) -> plus#(X1,X2) active#(plus(X1,X2)) -> plus#(active(X1),X2) -> plus#(mark(X1),X2) -> plus#(X1,X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) -> plus#(X1,mark(X2)) -> plus#(X1,X2) active#(plus(X1,X2)) -> plus#(X1,active(X2)) -> plus#(mark(X1),X2) -> plus#(X1,X2) active#(plus(X1,X2)) -> active#(X2) -> active#(s(X)) -> s#(active(X)) active#(plus(X1,X2)) -> active#(X2) -> active#(s(X)) -> active#(X) active#(plus(X1,X2)) -> active#(X2) -> active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(plus(X1,X2)) -> active#(X2) -> active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> active#(X2) -> active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(plus(X1,X2)) -> active#(X2) -> active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X2) -> active#(and(X1,X2)) -> and#(active(X1),X2) active#(plus(X1,X2)) -> active#(X2) -> active#(and(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X2) -> active#(plus(N,s(M))) -> s#(plus(N,M)) active#(plus(X1,X2)) -> active#(X2) -> active#(plus(N,s(M))) -> plus#(N,M) active#(plus(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(plus(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(plus(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(plus(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> active#(X2) active#(plus(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(plus(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X1) -> active#(and(X1,X2)) -> and#(active(X1),X2) active#(plus(X1,X2)) -> active#(X1) -> active#(and(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X1) -> active#(plus(N,s(M))) -> s#(plus(N,M)) active#(plus(X1,X2)) -> active#(X1) -> active#(plus(N,s(M))) -> plus#(N,M) active#(plus(N,s(M))) -> s#(plus(N,M)) -> s#(ok(X)) -> s#(X) active#(plus(N,s(M))) -> s#(plus(N,M)) -> s#(mark(X)) -> s#(X) active#(plus(N,s(M))) -> plus#(N,M) -> plus#(ok(X1),ok(X2)) -> plus#(X1,X2) active#(plus(N,s(M))) -> plus#(N,M) -> plus#(X1,mark(X2)) -> plus#(X1,X2) active#(plus(N,s(M))) -> plus#(N,M) -> plus#(mark(X1),X2) -> plus#(X1,X2) active#(and(X1,X2)) -> and#(active(X1),X2) -> and#(ok(X1),ok(X2)) -> and#(X1,X2) active#(and(X1,X2)) -> and#(active(X1),X2) -> and#(mark(X1),X2) -> and#(X1,X2) active#(and(X1,X2)) -> active#(X1) -> active#(s(X)) -> s#(active(X)) active#(and(X1,X2)) -> active#(X1) -> active#(s(X)) -> active#(X) active#(and(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> plus#(X1,active(X2)) active#(and(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> active#(X2) active#(and(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> plus#(active(X1),X2) active#(and(X1,X2)) -> active#(X1) -> active#(plus(X1,X2)) -> active#(X1) active#(and(X1,X2)) -> active#(X1) -> active#(and(X1,X2)) -> and#(active(X1),X2) active#(and(X1,X2)) -> active#(X1) -> active#(and(X1,X2)) -> active#(X1) active#(and(X1,X2)) -> active#(X1) -> active#(plus(N,s(M))) -> s#(plus(N,M)) active#(and(X1,X2)) -> active#(X1) -> active#(plus(N,s(M))) -> plus#(N,M) SCC Processor: #sccs: 6 #rules: 18 #arcs: 145/841 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=2 interpretation: [top#](x0) = [1 2]x0, [1 0] [1] [top](x0) = [2 0]x0 + [0], [1 0] [0] [ok](x0) = [0 2]x0 + [1], [1 0] [0] [proper](x0) = [0 0]x0 + [1], [3] [s](x0) = x0 + [0], [1 0] [2 0] [plus](x0, x1) = [0 0]x0 + [0 1]x1, [2] [0] = [0], [1 0] [3] [mark](x0) = [0 0]x0 + [0], [active](x0) = x0, [2 0] [2 0] [1] [and](x0, x1) = [0 1]x0 + [0 0]x1 + [0], [3] [tt] = [0] orientation: top#(ok(X)) = [1 4]X + [2] >= [1 2]X = top#(active(X)) top#(mark(X)) = [1 0]X + [3] >= [1 0]X + [2] = top#(proper(X)) [2 0] [7] [1 0] [3] active(and(tt(),X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(X) [1 0] [4] [1 0] [3] active(plus(N,0())) = [0 0]N + [0] >= [0 0]N + [0] = mark(N) [2 0] [1 0] [6] [2 0] [1 0] [6] active(plus(N,s(M))) = [0 1]M + [0 0]N + [0] >= [0 0]M + [0 0]N + [0] = mark(s(plus(N,M))) [2 0] [2 0] [1] [2 0] [2 0] [1] active(and(X1,X2)) = [0 1]X1 + [0 0]X2 + [0] >= [0 1]X1 + [0 0]X2 + [0] = and(active(X1),X2) [1 0] [2 0] [1 0] [2 0] active(plus(X1,X2)) = [0 0]X1 + [0 1]X2 >= [0 0]X1 + [0 1]X2 = plus(active(X1),X2) [1 0] [2 0] [1 0] [2 0] active(plus(X1,X2)) = [0 0]X1 + [0 1]X2 >= [0 0]X1 + [0 1]X2 = plus(X1,active(X2)) [3] [3] active(s(X)) = X + [0] >= X + [0] = s(active(X)) [2 0] [2 0] [7] [2 0] [2 0] [4] and(mark(X1),X2) = [0 0]X1 + [0 0]X2 + [0] >= [0 0]X1 + [0 0]X2 + [0] = mark(and(X1,X2)) [1 0] [2 0] [3] [1 0] [2 0] [3] plus(mark(X1),X2) = [0 0]X1 + [0 1]X2 + [0] >= [0 0]X1 + [0 0]X2 + [0] = mark(plus(X1,X2)) [1 0] [2 0] [6] [1 0] [2 0] [3] plus(X1,mark(X2)) = [0 0]X1 + [0 0]X2 + [0] >= [0 0]X1 + [0 0]X2 + [0] = mark(plus(X1,X2)) [1 0] [6] [1 0] [6] s(mark(X)) = [0 0]X + [0] >= [0 0]X + [0] = mark(s(X)) [2 0] [2 0] [1] [2 0] [2 0] [1] proper(and(X1,X2)) = [0 0]X1 + [0 0]X2 + [1] >= [0 0]X1 + [0 0]X2 + [1] = and(proper(X1),proper(X2)) [3] [3] proper(tt()) = [1] >= [1] = ok(tt()) [1 0] [2 0] [0] [1 0] [2 0] [0] proper(plus(X1,X2)) = [0 0]X1 + [0 0]X2 + [1] >= [0 0]X1 + [0 0]X2 + [1] = plus(proper(X1),proper(X2)) [2] [2] proper(0()) = [1] >= [1] = ok(0()) [1 0] [3] [1 0] [3] proper(s(X)) = [0 0]X + [1] >= [0 0]X + [1] = s(proper(X)) [2 0] [2 0] [1] [2 0] [2 0] [1] and(ok(X1),ok(X2)) = [0 2]X1 + [0 0]X2 + [1] >= [0 2]X1 + [0 0]X2 + [1] = ok(and(X1,X2)) [1 0] [2 0] [0] [1 0] [2 0] [0] plus(ok(X1),ok(X2)) = [0 0]X1 + [0 2]X2 + [1] >= [0 0]X1 + [0 2]X2 + [1] = ok(plus(X1,X2)) [1 0] [3] [1 0] [3] s(ok(X)) = [0 2]X + [1] >= [0 2]X + [1] = ok(s(X)) [1 0] [4] [1 0] [1] top(mark(X)) = [2 0]X + [6] >= [2 0]X + [0] = top(proper(X)) [1 0] [1] [1 0] [1] top(ok(X)) = [2 0]X + [0] >= [2 0]X + [0] = top(active(X)) problem: DPs: TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: active#(and(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X1) active#(plus(X1,X2)) -> active#(X2) active#(s(X)) -> active#(X) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [active#](x0) = 2x0 + 2, [top](x0) = 4, [ok](x0) = x0 + 2, [proper](x0) = 4x0, [s](x0) = x0 + 1, [plus](x0, x1) = x0 + 4x1 + 1, [0] = 1, [mark](x0) = 0, [active](x0) = x0, [and](x0, x1) = 3x0 + 4, [tt] = 4 orientation: active#(and(X1,X2)) = 6X1 + 10 >= 2X1 + 2 = active#(X1) active#(plus(X1,X2)) = 2X1 + 8X2 + 4 >= 2X1 + 2 = active#(X1) active#(plus(X1,X2)) = 2X1 + 8X2 + 4 >= 2X2 + 2 = active#(X2) active#(s(X)) = 2X + 4 >= 2X + 2 = active#(X) active(and(tt(),X)) = 16 >= 0 = mark(X) active(plus(N,0())) = N + 5 >= 0 = mark(N) active(plus(N,s(M))) = 4M + N + 5 >= 0 = mark(s(plus(N,M))) active(and(X1,X2)) = 3X1 + 4 >= 3X1 + 4 = and(active(X1),X2) active(plus(X1,X2)) = X1 + 4X2 + 1 >= X1 + 4X2 + 1 = plus(active(X1),X2) active(plus(X1,X2)) = X1 + 4X2 + 1 >= X1 + 4X2 + 1 = plus(X1,active(X2)) active(s(X)) = X + 1 >= X + 1 = s(active(X)) and(mark(X1),X2) = 4 >= 0 = mark(and(X1,X2)) plus(mark(X1),X2) = 4X2 + 1 >= 0 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X1 + 1 >= 0 = mark(plus(X1,X2)) s(mark(X)) = 1 >= 0 = mark(s(X)) proper(and(X1,X2)) = 12X1 + 16 >= 12X1 + 4 = and(proper(X1),proper(X2)) proper(tt()) = 16 >= 6 = ok(tt()) proper(plus(X1,X2)) = 4X1 + 16X2 + 4 >= 4X1 + 16X2 + 1 = plus(proper(X1),proper(X2)) proper(0()) = 4 >= 3 = ok(0()) proper(s(X)) = 4X + 4 >= 4X + 1 = s(proper(X)) and(ok(X1),ok(X2)) = 3X1 + 10 >= 3X1 + 6 = ok(and(X1,X2)) plus(ok(X1),ok(X2)) = X1 + 4X2 + 11 >= X1 + 4X2 + 3 = ok(plus(X1,X2)) s(ok(X)) = X + 3 >= X + 3 = ok(s(X)) top(mark(X)) = 4 >= 4 = top(proper(X)) top(ok(X)) = 4 >= 4 = top(active(X)) problem: DPs: TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(and(X1,X2)) -> proper#(X2) proper#(and(X1,X2)) -> proper#(X1) proper#(plus(X1,X2)) -> proper#(X2) proper#(plus(X1,X2)) -> proper#(X1) proper#(s(X)) -> proper#(X) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) LPO Processor: argument filtering: pi(tt) = [] pi(and) = [0,1] pi(active) = 0 pi(mark) = 0 pi(0) = [] pi(plus) = [0,1] pi(s) = [0] pi(proper) = 0 pi(ok) = 0 pi(top) = 0 pi(proper#) = 0 precedence: plus > proper# ~ top ~ ok ~ proper ~ s ~ 0 ~ mark ~ active ~ and ~ tt problem: DPs: TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s#(mark(X)) -> s#(X) s#(ok(X)) -> s#(X) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [s#](x0) = 3x0, [top](x0) = 0, [ok](x0) = 2x0 + 1/2, [proper](x0) = 3x0, [s](x0) = x0, [plus](x0, x1) = x0 + x1, [0] = 2, [mark](x0) = x0 + 1, [active](x0) = 2x0 + 3/2, [and](x0, x1) = x0 + 2x1 + 1/2, [tt] = 3/2 orientation: s#(mark(X)) = 3X + 3 >= 3X = s#(X) s#(ok(X)) = 6X + 3/2 >= 3X = s#(X) active(and(tt(),X)) = 4X + 11/2 >= X + 1 = mark(X) active(plus(N,0())) = 2N + 11/2 >= N + 1 = mark(N) active(plus(N,s(M))) = 2M + 2N + 3/2 >= M + N + 1 = mark(s(plus(N,M))) active(and(X1,X2)) = 2X1 + 4X2 + 5/2 >= 2X1 + 2X2 + 2 = and(active(X1),X2) active(plus(X1,X2)) = 2X1 + 2X2 + 3/2 >= 2X1 + X2 + 3/2 = plus(active(X1),X2) active(plus(X1,X2)) = 2X1 + 2X2 + 3/2 >= X1 + 2X2 + 3/2 = plus(X1,active(X2)) active(s(X)) = 2X + 3/2 >= 2X + 3/2 = s(active(X)) and(mark(X1),X2) = X1 + 2X2 + 3/2 >= X1 + 2X2 + 3/2 = mark(and(X1,X2)) plus(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = mark(plus(X1,X2)) s(mark(X)) = X + 1 >= X + 1 = mark(s(X)) proper(and(X1,X2)) = 3X1 + 6X2 + 3/2 >= 3X1 + 6X2 + 1/2 = and(proper(X1),proper(X2)) proper(tt()) = 9/2 >= 7/2 = ok(tt()) proper(plus(X1,X2)) = 3X1 + 3X2 >= 3X1 + 3X2 = plus(proper(X1),proper(X2)) proper(0()) = 6 >= 9/2 = ok(0()) proper(s(X)) = 3X >= 3X = s(proper(X)) and(ok(X1),ok(X2)) = 2X1 + 4X2 + 2 >= 2X1 + 4X2 + 3/2 = ok(and(X1,X2)) plus(ok(X1),ok(X2)) = 2X1 + 2X2 + 1 >= 2X1 + 2X2 + 1/2 = ok(plus(X1,X2)) s(ok(X)) = 2X + 1/2 >= 2X + 1/2 = ok(s(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: plus#(mark(X1),X2) -> plus#(X1,X2) plus#(X1,mark(X2)) -> plus#(X1,X2) plus#(ok(X1),ok(X2)) -> plus#(X1,X2) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [plus#](x0, x1) = 4x0 + x1, [top](x0) = 4, [ok](x0) = x0 + 2, [proper](x0) = 5x0, [s](x0) = x0 + 1, [plus](x0, x1) = x0 + x1, [0] = 4, [mark](x0) = x0 + 1, [active](x0) = 2x0, [and](x0, x1) = 6x0 + 6x1 + 4, [tt] = 1 orientation: plus#(mark(X1),X2) = 4X1 + X2 + 4 >= 4X1 + X2 = plus#(X1,X2) plus#(X1,mark(X2)) = 4X1 + X2 + 1 >= 4X1 + X2 = plus#(X1,X2) plus#(ok(X1),ok(X2)) = 4X1 + X2 + 10 >= 4X1 + X2 = plus#(X1,X2) active(and(tt(),X)) = 12X + 20 >= X + 1 = mark(X) active(plus(N,0())) = 2N + 8 >= N + 1 = mark(N) active(plus(N,s(M))) = 2M + 2N + 2 >= M + N + 2 = mark(s(plus(N,M))) active(and(X1,X2)) = 12X1 + 12X2 + 8 >= 12X1 + 6X2 + 4 = and(active(X1),X2) active(plus(X1,X2)) = 2X1 + 2X2 >= 2X1 + X2 = plus(active(X1),X2) active(plus(X1,X2)) = 2X1 + 2X2 >= X1 + 2X2 = plus(X1,active(X2)) active(s(X)) = 2X + 2 >= 2X + 1 = s(active(X)) and(mark(X1),X2) = 6X1 + 6X2 + 10 >= 6X1 + 6X2 + 5 = mark(and(X1,X2)) plus(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = mark(plus(X1,X2)) s(mark(X)) = X + 2 >= X + 2 = mark(s(X)) proper(and(X1,X2)) = 30X1 + 30X2 + 20 >= 30X1 + 30X2 + 4 = and(proper(X1),proper(X2)) proper(tt()) = 5 >= 3 = ok(tt()) proper(plus(X1,X2)) = 5X1 + 5X2 >= 5X1 + 5X2 = plus(proper(X1),proper(X2)) proper(0()) = 20 >= 6 = ok(0()) proper(s(X)) = 5X + 5 >= 5X + 1 = s(proper(X)) and(ok(X1),ok(X2)) = 6X1 + 6X2 + 28 >= 6X1 + 6X2 + 6 = ok(and(X1,X2)) plus(ok(X1),ok(X2)) = X1 + X2 + 4 >= X1 + X2 + 2 = ok(plus(X1,X2)) s(ok(X)) = X + 3 >= X + 3 = ok(s(X)) top(mark(X)) = 4 >= 4 = top(proper(X)) top(ok(X)) = 4 >= 4 = top(active(X)) problem: DPs: TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: and#(mark(X1),X2) -> and#(X1,X2) and#(ok(X1),ok(X2)) -> and#(X1,X2) TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Matrix Interpretation Processor: dim=1 interpretation: [and#](x0, x1) = x0, [top](x0) = 0, [ok](x0) = x0 + 1, [proper](x0) = 4x0, [s](x0) = x0 + 2, [plus](x0, x1) = x0 + 2x1, [0] = 4, [mark](x0) = x0 + 2, [active](x0) = x0, [and](x0, x1) = 7x0 + 2x1 + 2, [tt] = 1 orientation: and#(mark(X1),X2) = X1 + 2 >= X1 = and#(X1,X2) and#(ok(X1),ok(X2)) = X1 + 1 >= X1 = and#(X1,X2) active(and(tt(),X)) = 2X + 9 >= X + 2 = mark(X) active(plus(N,0())) = N + 8 >= N + 2 = mark(N) active(plus(N,s(M))) = 2M + N + 4 >= 2M + N + 4 = mark(s(plus(N,M))) active(and(X1,X2)) = 7X1 + 2X2 + 2 >= 7X1 + 2X2 + 2 = and(active(X1),X2) active(plus(X1,X2)) = X1 + 2X2 >= X1 + 2X2 = plus(active(X1),X2) active(plus(X1,X2)) = X1 + 2X2 >= X1 + 2X2 = plus(X1,active(X2)) active(s(X)) = X + 2 >= X + 2 = s(active(X)) and(mark(X1),X2) = 7X1 + 2X2 + 16 >= 7X1 + 2X2 + 4 = mark(and(X1,X2)) plus(mark(X1),X2) = X1 + 2X2 + 2 >= X1 + 2X2 + 2 = mark(plus(X1,X2)) plus(X1,mark(X2)) = X1 + 2X2 + 4 >= X1 + 2X2 + 2 = mark(plus(X1,X2)) s(mark(X)) = X + 4 >= X + 4 = mark(s(X)) proper(and(X1,X2)) = 28X1 + 8X2 + 8 >= 28X1 + 8X2 + 2 = and(proper(X1),proper(X2)) proper(tt()) = 4 >= 2 = ok(tt()) proper(plus(X1,X2)) = 4X1 + 8X2 >= 4X1 + 8X2 = plus(proper(X1),proper(X2)) proper(0()) = 16 >= 5 = ok(0()) proper(s(X)) = 4X + 8 >= 4X + 2 = s(proper(X)) and(ok(X1),ok(X2)) = 7X1 + 2X2 + 11 >= 7X1 + 2X2 + 3 = ok(and(X1,X2)) plus(ok(X1),ok(X2)) = X1 + 2X2 + 3 >= X1 + 2X2 + 1 = ok(plus(X1,X2)) s(ok(X)) = X + 3 >= X + 3 = ok(s(X)) top(mark(X)) = 0 >= 0 = top(proper(X)) top(ok(X)) = 0 >= 0 = top(active(X)) problem: DPs: TRS: active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(and(X1,X2)) -> and(active(X1),X2) active(plus(X1,X2)) -> plus(active(X1),X2) active(plus(X1,X2)) -> plus(X1,active(X2)) active(s(X)) -> s(active(X)) and(mark(X1),X2) -> mark(and(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) s(mark(X)) -> mark(s(X)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(tt()) -> ok(tt()) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed