MAYBE Problem: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Proof: DP Processor: DPs: active#(dbl(s(X))) -> dbl#(X) active#(dbl(s(X))) -> s#(dbl(X)) active#(dbl(s(X))) -> s#(s(dbl(X))) active#(dbls(cons(X,Y))) -> dbls#(Y) active#(dbls(cons(X,Y))) -> dbl#(X) active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y)) active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) active#(indx(cons(X,Y),Z)) -> indx#(Y,Z) active#(indx(cons(X,Y),Z)) -> sel#(X,Z) active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z)) active#(from(X)) -> s#(X) active#(from(X)) -> from#(s(X)) active#(from(X)) -> cons#(X,from(s(X))) active#(dbl1(s(X))) -> dbl1#(X) active#(dbl1(s(X))) -> s1#(dbl1(X)) active#(dbl1(s(X))) -> s1#(s1(dbl1(X))) active#(sel1(s(X),cons(Y,Z))) -> sel1#(X,Z) active#(quote(s(X))) -> quote#(X) active#(quote(s(X))) -> s1#(quote(X)) active#(quote(dbl(X))) -> dbl1#(X) active#(quote(sel(X,Y))) -> sel1#(X,Y) active#(dbl(X)) -> active#(X) active#(dbl(X)) -> dbl#(active(X)) active#(dbls(X)) -> active#(X) active#(dbls(X)) -> dbls#(active(X)) active#(sel(X1,X2)) -> active#(X1) active#(sel(X1,X2)) -> sel#(active(X1),X2) active#(sel(X1,X2)) -> active#(X2) active#(sel(X1,X2)) -> sel#(X1,active(X2)) active#(indx(X1,X2)) -> active#(X1) active#(indx(X1,X2)) -> indx#(active(X1),X2) active#(dbl1(X)) -> active#(X) active#(dbl1(X)) -> dbl1#(active(X)) active#(s1(X)) -> active#(X) active#(s1(X)) -> s1#(active(X)) active#(sel1(X1,X2)) -> active#(X1) active#(sel1(X1,X2)) -> sel1#(active(X1),X2) active#(sel1(X1,X2)) -> active#(X2) active#(sel1(X1,X2)) -> sel1#(X1,active(X2)) active#(quote(X)) -> active#(X) active#(quote(X)) -> quote#(active(X)) dbl#(mark(X)) -> dbl#(X) dbls#(mark(X)) -> dbls#(X) sel#(mark(X1),X2) -> sel#(X1,X2) sel#(X1,mark(X2)) -> sel#(X1,X2) indx#(mark(X1),X2) -> indx#(X1,X2) dbl1#(mark(X)) -> dbl1#(X) s1#(mark(X)) -> s1#(X) sel1#(mark(X1),X2) -> sel1#(X1,X2) sel1#(X1,mark(X2)) -> sel1#(X1,X2) quote#(mark(X)) -> quote#(X) proper#(dbl(X)) -> proper#(X) proper#(dbl(X)) -> dbl#(proper(X)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(dbls(X)) -> proper#(X) proper#(dbls(X)) -> dbls#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(sel(X1,X2)) -> proper#(X2) proper#(sel(X1,X2)) -> proper#(X1) proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2)) proper#(indx(X1,X2)) -> proper#(X2) proper#(indx(X1,X2)) -> proper#(X1) proper#(indx(X1,X2)) -> indx#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) proper#(dbl1(X)) -> proper#(X) proper#(dbl1(X)) -> dbl1#(proper(X)) proper#(s1(X)) -> proper#(X) proper#(s1(X)) -> s1#(proper(X)) proper#(sel1(X1,X2)) -> proper#(X2) proper#(sel1(X1,X2)) -> proper#(X1) proper#(sel1(X1,X2)) -> sel1#(proper(X1),proper(X2)) proper#(quote(X)) -> proper#(X) proper#(quote(X)) -> quote#(proper(X)) dbl#(ok(X)) -> dbl#(X) s#(ok(X)) -> s#(X) dbls#(ok(X)) -> dbls#(X) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) sel#(ok(X1),ok(X2)) -> sel#(X1,X2) indx#(ok(X1),ok(X2)) -> indx#(X1,X2) from#(ok(X)) -> from#(X) dbl1#(ok(X)) -> dbl1#(X) s1#(ok(X)) -> s1#(X) sel1#(ok(X1),ok(X2)) -> sel1#(X1,X2) quote#(ok(X)) -> quote#(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(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) TDG Processor: DPs: active#(dbl(s(X))) -> dbl#(X) active#(dbl(s(X))) -> s#(dbl(X)) active#(dbl(s(X))) -> s#(s(dbl(X))) active#(dbls(cons(X,Y))) -> dbls#(Y) active#(dbls(cons(X,Y))) -> dbl#(X) active#(dbls(cons(X,Y))) -> cons#(dbl(X),dbls(Y)) active#(sel(s(X),cons(Y,Z))) -> sel#(X,Z) active#(indx(cons(X,Y),Z)) -> indx#(Y,Z) active#(indx(cons(X,Y),Z)) -> sel#(X,Z) active#(indx(cons(X,Y),Z)) -> cons#(sel(X,Z),indx(Y,Z)) active#(from(X)) -> s#(X) active#(from(X)) -> from#(s(X)) active#(from(X)) -> cons#(X,from(s(X))) active#(dbl1(s(X))) -> dbl1#(X) active#(dbl1(s(X))) -> s1#(dbl1(X)) active#(dbl1(s(X))) -> s1#(s1(dbl1(X))) active#(sel1(s(X),cons(Y,Z))) -> sel1#(X,Z) active#(quote(s(X))) -> quote#(X) active#(quote(s(X))) -> s1#(quote(X)) active#(quote(dbl(X))) -> dbl1#(X) active#(quote(sel(X,Y))) -> sel1#(X,Y) active#(dbl(X)) -> active#(X) active#(dbl(X)) -> dbl#(active(X)) active#(dbls(X)) -> active#(X) active#(dbls(X)) -> dbls#(active(X)) active#(sel(X1,X2)) -> active#(X1) active#(sel(X1,X2)) -> sel#(active(X1),X2) active#(sel(X1,X2)) -> active#(X2) active#(sel(X1,X2)) -> sel#(X1,active(X2)) active#(indx(X1,X2)) -> active#(X1) active#(indx(X1,X2)) -> indx#(active(X1),X2) active#(dbl1(X)) -> active#(X) active#(dbl1(X)) -> dbl1#(active(X)) active#(s1(X)) -> active#(X) active#(s1(X)) -> s1#(active(X)) active#(sel1(X1,X2)) -> active#(X1) active#(sel1(X1,X2)) -> sel1#(active(X1),X2) active#(sel1(X1,X2)) -> active#(X2) active#(sel1(X1,X2)) -> sel1#(X1,active(X2)) active#(quote(X)) -> active#(X) active#(quote(X)) -> quote#(active(X)) dbl#(mark(X)) -> dbl#(X) dbls#(mark(X)) -> dbls#(X) sel#(mark(X1),X2) -> sel#(X1,X2) sel#(X1,mark(X2)) -> sel#(X1,X2) indx#(mark(X1),X2) -> indx#(X1,X2) dbl1#(mark(X)) -> dbl1#(X) s1#(mark(X)) -> s1#(X) sel1#(mark(X1),X2) -> sel1#(X1,X2) sel1#(X1,mark(X2)) -> sel1#(X1,X2) quote#(mark(X)) -> quote#(X) proper#(dbl(X)) -> proper#(X) proper#(dbl(X)) -> dbl#(proper(X)) proper#(s(X)) -> proper#(X) proper#(s(X)) -> s#(proper(X)) proper#(dbls(X)) -> proper#(X) proper#(dbls(X)) -> dbls#(proper(X)) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) proper#(sel(X1,X2)) -> proper#(X2) proper#(sel(X1,X2)) -> proper#(X1) proper#(sel(X1,X2)) -> sel#(proper(X1),proper(X2)) proper#(indx(X1,X2)) -> proper#(X2) proper#(indx(X1,X2)) -> proper#(X1) proper#(indx(X1,X2)) -> indx#(proper(X1),proper(X2)) proper#(from(X)) -> proper#(X) proper#(from(X)) -> from#(proper(X)) proper#(dbl1(X)) -> proper#(X) proper#(dbl1(X)) -> dbl1#(proper(X)) proper#(s1(X)) -> proper#(X) proper#(s1(X)) -> s1#(proper(X)) proper#(sel1(X1,X2)) -> proper#(X2) proper#(sel1(X1,X2)) -> proper#(X1) proper#(sel1(X1,X2)) -> sel1#(proper(X1),proper(X2)) proper#(quote(X)) -> proper#(X) proper#(quote(X)) -> quote#(proper(X)) dbl#(ok(X)) -> dbl#(X) s#(ok(X)) -> s#(X) dbls#(ok(X)) -> dbls#(X) cons#(ok(X1),ok(X2)) -> cons#(X1,X2) sel#(ok(X1),ok(X2)) -> sel#(X1,X2) indx#(ok(X1),ok(X2)) -> indx#(X1,X2) from#(ok(X)) -> from#(X) dbl1#(ok(X)) -> dbl1#(X) s1#(ok(X)) -> s1#(X) sel1#(ok(X1),ok(X2)) -> sel1#(X1,X2) quote#(ok(X)) -> quote#(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(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) graph: ... SCC Processor: #sccs: 14 #rules: 48 #arcs: 1004/8464 DPs: top#(ok(X)) -> top#(active(X)) top#(mark(X)) -> top#(proper(X)) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Open DPs: active#(dbl(X)) -> active#(X) active#(dbls(X)) -> active#(X) active#(sel(X1,X2)) -> active#(X1) active#(sel(X1,X2)) -> active#(X2) active#(indx(X1,X2)) -> active#(X1) active#(dbl1(X)) -> active#(X) active#(s1(X)) -> active#(X) active#(sel1(X1,X2)) -> active#(X1) active#(sel1(X1,X2)) -> active#(X2) active#(quote(X)) -> active#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(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(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: proper#(dbl(X)) -> proper#(X) proper#(s(X)) -> proper#(X) proper#(dbls(X)) -> proper#(X) proper#(cons(X1,X2)) -> proper#(X2) proper#(cons(X1,X2)) -> proper#(X1) proper#(sel(X1,X2)) -> proper#(X2) proper#(sel(X1,X2)) -> proper#(X1) proper#(indx(X1,X2)) -> proper#(X2) proper#(indx(X1,X2)) -> proper#(X1) proper#(from(X)) -> proper#(X) proper#(dbl1(X)) -> proper#(X) proper#(s1(X)) -> proper#(X) proper#(sel1(X1,X2)) -> proper#(X2) proper#(sel1(X1,X2)) -> proper#(X1) proper#(quote(X)) -> proper#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(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(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: quote#(mark(X)) -> quote#(X) quote#(ok(X)) -> quote#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(quote#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: sel1#(mark(X1),X2) -> sel1#(X1,X2) sel1#(X1,mark(X2)) -> sel1#(X1,X2) sel1#(ok(X1),ok(X2)) -> sel1#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(sel1#) = 1 problem: DPs: sel1#(mark(X1),X2) -> sel1#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(sel1#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s1#(mark(X)) -> s1#(X) s1#(ok(X)) -> s1#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(s1#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: dbl1#(mark(X)) -> dbl1#(X) dbl1#(ok(X)) -> dbl1#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(dbl1#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: from#(ok(X)) -> from#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(from#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: indx#(mark(X1),X2) -> indx#(X1,X2) indx#(ok(X1),ok(X2)) -> indx#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(indx#) = 1 problem: DPs: indx#(mark(X1),X2) -> indx#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(indx#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: sel#(mark(X1),X2) -> sel#(X1,X2) sel#(X1,mark(X2)) -> sel#(X1,X2) sel#(ok(X1),ok(X2)) -> sel#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(sel#) = 1 problem: DPs: sel#(mark(X1),X2) -> sel#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(sel#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: cons#(ok(X1),ok(X2)) -> cons#(X1,X2) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(cons#) = 1 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: dbls#(mark(X)) -> dbls#(X) dbls#(ok(X)) -> dbls#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(dbls#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: s#(ok(X)) -> s#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(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(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed DPs: dbl#(mark(X)) -> dbl#(X) dbl#(ok(X)) -> dbl#(X) TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Subterm Criterion Processor: simple projection: pi(dbl#) = 0 problem: DPs: TRS: active(dbl(0())) -> mark(0()) active(dbl(s(X))) -> mark(s(s(dbl(X)))) active(dbls(nil())) -> mark(nil()) active(dbls(cons(X,Y))) -> mark(cons(dbl(X),dbls(Y))) active(sel(0(),cons(X,Y))) -> mark(X) active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) active(indx(nil(),X)) -> mark(nil()) active(indx(cons(X,Y),Z)) -> mark(cons(sel(X,Z),indx(Y,Z))) active(from(X)) -> mark(cons(X,from(s(X)))) active(dbl1(0())) -> mark(01()) active(dbl1(s(X))) -> mark(s1(s1(dbl1(X)))) active(sel1(0(),cons(X,Y))) -> mark(X) active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) active(quote(0())) -> mark(01()) active(quote(s(X))) -> mark(s1(quote(X))) active(quote(dbl(X))) -> mark(dbl1(X)) active(quote(sel(X,Y))) -> mark(sel1(X,Y)) active(dbl(X)) -> dbl(active(X)) active(dbls(X)) -> dbls(active(X)) active(sel(X1,X2)) -> sel(active(X1),X2) active(sel(X1,X2)) -> sel(X1,active(X2)) active(indx(X1,X2)) -> indx(active(X1),X2) active(dbl1(X)) -> dbl1(active(X)) active(s1(X)) -> s1(active(X)) active(sel1(X1,X2)) -> sel1(active(X1),X2) active(sel1(X1,X2)) -> sel1(X1,active(X2)) active(quote(X)) -> quote(active(X)) dbl(mark(X)) -> mark(dbl(X)) dbls(mark(X)) -> mark(dbls(X)) sel(mark(X1),X2) -> mark(sel(X1,X2)) sel(X1,mark(X2)) -> mark(sel(X1,X2)) indx(mark(X1),X2) -> mark(indx(X1,X2)) dbl1(mark(X)) -> mark(dbl1(X)) s1(mark(X)) -> mark(s1(X)) sel1(mark(X1),X2) -> mark(sel1(X1,X2)) sel1(X1,mark(X2)) -> mark(sel1(X1,X2)) quote(mark(X)) -> mark(quote(X)) proper(dbl(X)) -> dbl(proper(X)) proper(0()) -> ok(0()) proper(s(X)) -> s(proper(X)) proper(dbls(X)) -> dbls(proper(X)) proper(nil()) -> ok(nil()) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(sel(X1,X2)) -> sel(proper(X1),proper(X2)) proper(indx(X1,X2)) -> indx(proper(X1),proper(X2)) proper(from(X)) -> from(proper(X)) proper(dbl1(X)) -> dbl1(proper(X)) proper(01()) -> ok(01()) proper(s1(X)) -> s1(proper(X)) proper(sel1(X1,X2)) -> sel1(proper(X1),proper(X2)) proper(quote(X)) -> quote(proper(X)) dbl(ok(X)) -> ok(dbl(X)) s(ok(X)) -> ok(s(X)) dbls(ok(X)) -> ok(dbls(X)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) sel(ok(X1),ok(X2)) -> ok(sel(X1,X2)) indx(ok(X1),ok(X2)) -> ok(indx(X1,X2)) from(ok(X)) -> ok(from(X)) dbl1(ok(X)) -> ok(dbl1(X)) s1(ok(X)) -> ok(s1(X)) sel1(ok(X1),ok(X2)) -> ok(sel1(X1,X2)) quote(ok(X)) -> ok(quote(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) Qed