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)) 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(top#) = 0 precedence: plus > s > and > top# ~ top ~ ok ~ proper ~ 0 ~ mark ~ active ~ tt problem: DPs: 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)) Arctic Interpretation Processor: dimension: 1 interpretation: [top#](x0) = x0, [top](x0) = 2, [ok](x0) = 4x0 + 1, [proper](x0) = 4x0, [s](x0) = 3x0 + 0, [plus](x0, x1) = 3x0 + 0, [0] = 2, [mark](x0) = 0, [active](x0) = x0, [and](x0, x1) = 1x0 + 1x1, [tt] = 0 orientation: top#(ok(X)) = 4X + 1 >= X = top#(active(X)) active(and(tt(),X)) = 1X + 1 >= 0 = mark(X) active(plus(N,0())) = 3N + 0 >= 0 = mark(N) active(plus(N,s(M))) = 3N + 0 >= 0 = mark(s(plus(N,M))) active(and(X1,X2)) = 1X1 + 1X2 >= 1X1 + 1X2 = and(active(X1),X2) active(plus(X1,X2)) = 3X1 + 0 >= 3X1 + 0 = plus(active(X1),X2) active(plus(X1,X2)) = 3X1 + 0 >= 3X1 + 0 = plus(X1,active(X2)) active(s(X)) = 3X + 0 >= 3X + 0 = s(active(X)) and(mark(X1),X2) = 1X2 + 1 >= 0 = mark(and(X1,X2)) plus(mark(X1),X2) = 3 >= 0 = mark(plus(X1,X2)) plus(X1,mark(X2)) = 3X1 + 0 >= 0 = mark(plus(X1,X2)) s(mark(X)) = 3 >= 0 = mark(s(X)) proper(and(X1,X2)) = 5X1 + 5X2 >= 5X1 + 5X2 = and(proper(X1),proper(X2)) proper(tt()) = 4 >= 4 = ok(tt()) proper(plus(X1,X2)) = 7X1 + 4 >= 7X1 + 0 = plus(proper(X1),proper(X2)) proper(0()) = 6 >= 6 = ok(0()) proper(s(X)) = 7X + 4 >= 7X + 0 = s(proper(X)) and(ok(X1),ok(X2)) = 5X1 + 5X2 + 2 >= 5X1 + 5X2 + 1 = ok(and(X1,X2)) plus(ok(X1),ok(X2)) = 7X1 + 4 >= 7X1 + 4 = ok(plus(X1,X2)) s(ok(X)) = 7X + 4 >= 7X + 4 = ok(s(X)) top(mark(X)) = 2 >= 2 = top(proper(X)) top(ok(X)) = 2 >= 2 = 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)) Subterm Criterion Processor: simple projection: pi(active#) = 0 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)) Subterm Criterion Processor: simple projection: pi(proper#) = 0 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)) Subterm Criterion Processor: simple projection: pi(s#) = 0 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)) Subterm Criterion Processor: simple projection: pi(plus#) = 1 problem: DPs: plus#(mark(X1),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)) Subterm Criterion Processor: simple projection: pi(plus#) = 0 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)) Subterm Criterion Processor: simple projection: pi(and#) = 1 problem: DPs: and#(mark(X1),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)) Subterm Criterion Processor: simple projection: pi(and#) = 0 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